The Trustworthy Systems team is pleased to announce a new branch of seL4, which provides advanced support for real-time systems, including explicit support for
mixed-criticality systems (MCS) for the x86, x64 and ARM v7/v8 architectures. Key features include:
the ability to limit CPU bandwidth consumed by a thread, as a way to prevent high-priority threads from monopolising the processor
a new scheduling-context mechanisms, which extends capability-based access control to the time resource
a principled mechanism for passing CPU allocation between cooperating threads, which provides accurate accounting of CPU time yet retains seL4’s trademark ultra-fast IPC performance
low-overhead support for standard real-time locking protocols, especially the immediate priority ceiling protocol (IPCP)
support for low-overhead user-level scheduler implementation, enabling alternative scheduling policies.
This is the first (and largest) step towards a kernel API that provides full temporal integrity enforcement, and support for general MCS, without inhibiting existing use cases. The new version can faithfully emulate the scheduling behaviour of mainline seL4.
Further (less dramatic) features will be rolled in over the next year or so.
The MCS kernel’s API is formally specified and there is a verification roadmap, but we emphasise that, at present, this version is
not fully formally verified and may contain bugs. Verification will take a while, and completion is subject to availability of funding.
It is important to understand that the MCS kernel represents the future of seL4. We plan to switch over to this as our mainline API once formal verification is completed. Until that time, the present mainline kernel should be used were verification
is important.
Note that even without full verification, the MCS version of seL4 is already a highly-dependable OS, sharing the majority of its code base with the verified mainline kernel. Specifically we believe that it is the only OS with a high degree of robustness that
truly supports MCS without such limitations as strict static temporal partitioning (which results in inherently low resource utilisation).
For these reasons we strongly encourage any new developments to consider adopting the MCS kernel, especially where deployment is still years out (by which time hopefully verification has caught up).