Dear seL4 community,

The long-rumoured enhanced real-time support for seL4 is available for evaluation, released as a branch of the mainline kernel. While still considered “experimental”, the model and implementation are actually quite mature, and we don’t expect massive changes. It is already being deployed in a number of experimental systems, especially under the DARPA HACMS program.

We will soon start migrating the new features into the mainstream kernel, and it will eventually be verified like the rest of the kernel.

A high-level summary of the new features are: - a periodic thread model that provides temporal isolation via time budgets - capability-contolled allocation of CPU resources - mechanisms to enable proper accounting of time consumed by a server on behalf of clients - support for mixed-criticality real-time systems, where criticality is orthogonal to priority

More details are in this announcement on the seL4 developers list and in resources linked from that: https://sel4.systems/pipermail/devel/2016-June/000831.html

Gernot on behalf of the Trustworthy Systems team at Data61 (formerly NICTA).

________________________________

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.