seL4 MCS pre-release (10.1.1-mcs)

This is a pre-release of the seL4 mixed-criticality systems (MCS) extensions. This branch is not verified and is under active verification.

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 10.1.1.

Changes

  • seL4_TCB_Configure arguments changed (fault ep removed)
  • seL4_TCB_SetSchedParams also sets scheduling context, and fault endpoint. The fault endpoint is a capability in the current thread’s cspace, unlike on the master kernel, where it is in the target thread’s cspace.
  • 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_MsgMaxLength is now 119, as a reserved word is needed in the IPC buffer on 32-bit x86.
  • 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.

Invocations

  • seL4_TCBSetTimeoutEndpoint - new TCB invocation which allows a timeout endpoint to be set for a TCB.
  • seL4_SchedControl_Configure - allows scheduling context parameters to be set.
  • seL4_SchedContext_Bind - Allows a notification or TCB object to be bound to a scheduling context object.
  • seL4_SchedContext_Unbind - Unbind any object bound to a scheduling context.
  • seL4_SchedContext_UnbindObject - Unbind a specific object from a scheduling context.
  • seL4_SchedContext_Consumed - Read and reset the amount of time consumed from scheduling context.
  • seL4_SchedContext_YieldTo - Place the active thread bound to this scheduling context at the head of the scheduling queue for its priority. Read and reset the amount of time consumed.

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.
  • seL4_isTimeoutFault_tag: detect a timeout fault message.
  • seL4_TimeoutReply_new: construct a reply to a timeout fault message.

Structures

  • A sched control capability per core 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

Please contact us if you need compatible libraries for the MCS kernel for a specific version.

Hardware support

The MCS 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 10.1.1-mcs manual included in the release.