I am new in seL4. It is really interesting OS.
I would like to ask some questions even though the FAQ explains many things.
1. How different is seL4+VMM with OKL4 or codezero?
If there is some performance gap between them, I am curious where the
overheads are for?
2. I am wondering how well seL4 can support virtualization services.
Can seL4 supports more than two linux simultaneously on the VMM layers?
Moreover, can it execute different kind of guest OSes at the same time?
What about RTOS? A RTOS can be executed with keeping their real time
property on the seL4+VMM??
Lastly, I would like to know when new version of the VMM for A15 support
will be released.
3. Did you use a code generator when you hit the steps for
“Specification”, “Haskell Prototype” and “C code” In the Proof Processing?
If you did it using any automatic tool, I am so curious how you verified
and validated the codes.
4., According to the FAQ, current multicore support is through a
Do you have any plan for one seL4 kernel to manage several processors?
Thank you much in advance.