seL4 MCS pre-release (9.0.0-mcs)

This is a pre-release of the seL4 mixed-criticality systems (RT) extensions. This branch is not verified and is under active verification. This is a subset of the previously released RT extensions, which still exist and can be provided on request.

Highlights

The goals of the MCS kernel is to provide strong temporal isolation and a basis for reasoning about time.

IPC & Signal ordering

Signal and IPC delivery is now priority ordered and FIFO within a priority, rather than plain FIFO

Scheduling contexts

This branch adds scheduling contexts to seL4, which represent CPU time (as budget/period). Scheduling contexts are separate from threads (although threads require one to run) and can be passed around over IPC, if the target of an IPC does not have its own scheduling context.

Scheduling contexts allow developers to create periodic threads, temporally isolate threads and have variable timeslices for round robin threads. If budget == period, the scheduling context acts as timeslice and the thread it is bound to is treated as round-robin.

Periodic scheduling

Periodic threads can be created by binding them to scheduling contexts with a budget < period. seL4_Yield for these threads will sacrifice the remaining budget until the next period.

Isolation through sporadic servers

Temporal isolation is provided with scheduling context by an implementation of sporadic servers. Please see the manual or tutorial for further explanation.

However, in seL4, threads without budget left in their sporadic server are not runnable at all - this is used to provide an absolute cap on CPU time executed by a scheduling context. More complex scheduling algorithms can be implemented at user-level.

Scheduling contexts are of a variable size, allowing for a variable maximum number of sporadic replenishment (termed refills in the API for brevity) pre scheduling context object.

Passive Servers

Passive servers run on their clients scheduling context, as the do not have one of their own. This allows for basic temporal isolation of shared resources, however clients must provide enough budget for the server to finish the request. Futher extensions in future add timeout exceptions, which allows a passive server to detect and recover from an overrun, however they are not included in this release.

Threads can be converted to passive by removing their scheduling context while they are waiting on an endpoint. Then, any calling threads will automatically donate their scheduling context to this thread when they send it an IPC.

Reply objects

Reply objects are a new object in the API which serve two purposes:

MCS ABI and libsel4

This section documents kernel ABI and libsel4 changes as compared with seL4 9.0.0.

Changes

API Additions

Constants

System calls

Invocations

libsel4

Structures

Deletions

Library & test compatability

$ mkdir sel4test-mcs $ cd sel4test-mcs
$ repo init -u <https://github.com/seL4/sel4test-manifest.git> -m 5.2.x-mcs.xml
$ repo sync

Hardware support

The RT kernel currently supports:

Other hardware platforms will be added as required (the ports require updated kernel and user-level timer drivers)

More details

See the 5.2.0-mcs manual included in the release.

We have developed a branch of the seL4 and CAmkES tutorials for the MCS kernel.