seL4 MCS pre-release (5.2.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:

  • They provide a container for the once-off reply capability generated by a seL4_Call to be stored. This means that the reply cap is always saved and cannot be overriden as it is no longer stored in the internal CNode of a TCB, and seL4_CNode_SaveCaller no longer needs to be used.
  • They track scheduling context donation over IPC to passive servers.

MCS ABI and libsel4

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

Changes

  • seL4_TCB_Configure arguments changed (scheduling context cap added).
  • seL4_Recv, seL4_ReplyRecv, seL4_NBRecv now take a reply object such that the caller can receive a call. The reply capability is generated in the reply object, rather than being saved into the TCB CNode internally. seL4_Call must be paired with seL4_Recv - and seL4_CNode_SaveCaller is no longer required.
  • seL4_Wait, seL4_NBWait and variants do not require a reply object and can be paired with seL4_Send on endpoints and notifications. Instead of being an API wrapper, this is now a real system call.
  • the x86 kernel ABI now only has 1 message register, due to the need to store the reply object.
  • seL4_MsgLengthBits increased - this increases amount of caps can be sent per message.
  • seL4_MsgMaxLength is now 115, as a result.
  • seL4_NotificationBits - increased.

API Additions

Constants

  • seL4_SchedContextObject - new object for that allows threads access to CPU time
  • seL4_MinSchedContextBits - minimum size n (2\^n) of a scheduling context object
  • seL4_CoreSchedContextBytes - the amount of bytes required for the fields in a scheduling context that are not sporadic refills.
  • seL4_RefillSizeBytes - the size of a single refill. Together with the above, these can be used to determine the number of refills that will fit in a scheduling context object of a certain size.
  • seL4_ReplyObject - new object to track scheduling context donation over IPC and store reply capabilities.
  • seL4_ReplyObjectBits - size of a reply object (2\^n).
  • seL4_CapInitThreadSC - capability to the initial threads scheduling context

System calls

  • seL4_NBSendRecv - new system call which allows a single kernel invocation to perform a non-blocking send on one capability, and recieve on another.
  • seL4_NBSendRecvWithMRs - uses above new system call without touching the IPC buffer, passing only data in registers
  • seL4_NBSendWait - new system call which allows a single kernel invocation to perform a non-blocking send on one capability, and wait on another (no reply object).
  • seL4_NBSendWaitWithMRs - uses above new system call without touching the IPC buffer, passing only data in registers
  • seL4_SchedControl_Configure - invokes the scheduling control cap to populate a scheduling context with parameters
  • seL4_SchedContext_Bind - bind a TCB to a scheduling context, if the TCB is runnable and scheduling context has budget, this will start the TCB running
  • seL4_SchedContext_Unbind - remove binding of a scheduling context from a TCB, TCB will no longer run but state will be preserved
  • seL4_SchedContext_Unbind Object - remove binding of a scheduling context from a TCB, TCB will no longer run but state will be preserved
  • seL4_Wait - block on an endpoint or notification without providing a reply object. Can be paired with seL4_Send but not seL4_Call.
  • seL4_NBWait - a non-blocking variant of the above.
  • seL4_WaitWithMRs - a variant of seL4_Wait that does not touch the IPC buffer.

libsel4

  • seL4_SetReserved, seL4_GetReserved: set a reserved word in the IPC buffer that may be used by the kernel ABI for arguments that do not fit into registers.
  • seL4_MaxExtraRefills is provided to allow users to calculate the maximum number of extra refills for a specific scheduling context size.
  • seL4_Time: type for specifying time arguments.

Structures

  • A sched control capability is provided to the root task per node via the seL4_BootInfo structure.

Deletions

  • seL4_CNode_SaveCaller (deprecated by reply objects)
  • seL4_Reply (replaced by invoking a reply object)
  • seL4_ReplyWithMRs (as above)

Library & test compatability

  • CAmkES and CapDL both support seL4 5.2.0-mcs on their master branches.
  • seL4_libs and sel4test both have 5.2.0-mcs-compatible branches that work with the forked API
  • You can obtain and run sel4test for seL4 5.2.0-mcs by doing the following:
$ 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.

  • seL4 RT tutorial a new tutorial which covers all of the API changes and features is available here.
  • Tutorials Otherwise it’s worth going through all of the tutorials, as all have been ported to the MCS kernel on the ‘mcs’ branch.