1. How different is seL4+VMM with OKL4 or codezero?
That’s a bit difficult to answer, given that of the three, only seL4 is open-source.
Codezero (when it was still open source) was a clone of the then OKL4 microkernel, without any of the optimisations that make L4 microkernels fast. Not sure how it evolved since.
The OKL4 Microvisor has a different API, especially designed to support efficient para-virtualization. It has fairly mature userland, especially a driver framework.
If there is some performance gap between them, I am curious where the overheads are for? seL4 is the fastest L4 microkernel (which means it’s the fastest general-purpose microkernel). The present release hasn’t got all the performance optimisations in, but they’ll eventually show up. We won’t be beaten on performance. 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? seL4 supports (hardware-supported) full virtualisation. The userland VMM required to support VMs has’t yet been released for ARM, but it works pretty well internally and will be released soon. We have no plans to support para-virtulized VMs.
Yes, multiple VMs are supported, including heterogenous ones.
What about RTOS? A RTOS can be executed with keeping their real time property on the seL4+VMM?? seL4 is the world’s only hypervisor with a sound worst-case execution-time (WCET) analysis, and as such the only one that can give you actual real-time guarantees, no matter what others may be claiming. (If someone else tells you they can make such guarantees, ask them to make them in public so I can call out their bullshit.)
That said, the analysis was performed on an earlier version of the kernel, not the presently released one. We are currently re-doing that analysis. This will require some updates to the kernel to reduce interrupt latencies where they have crept up due to recent changes.
More importantly, we’re working on improvements for enabling the kind of temporal isolation that’s required for supporting mixed-criticality scheduling. That will take 6-12 months to make it into the release, by which time it’ll have been comprehensively tested and evaluated, among others in the SMACCM project: http://ssrg.nicta.com.au/projects/TS/SMACCM/
Im actually not convinced that running an RTOS in a VM is necessarily the way to go, although that somewhat depends on your circumstances. In general you’re better off running RT apps in a native seL4 environment. Lastly, I would like to know when new version of the VMM for A15 support will be released.
I’m not prepared to commit to a release data ATM, but it’s working well in the lab and shouldn’t be far off.
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.
No, we didn't. The TOCS paper describes the approach in detail: http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstrac... 4., According to the FAQ, current multicore support is through a multikernel configuration. Do you have any plan for one seL4 kernel to manage several processors? A multicore kernel is presently undergoing extensive benchmarking and stability testing, it should be ready for release soon.
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.