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.
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
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
budget == period, the scheduling context acts as timeslice
and the thread it is bound to is treated as round-robin.
Periodic threads can be created by binding them to scheduling contexts
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 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 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_Callto 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_SaveCallerno 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_TCB_Configurearguments changed (scheduling context cap added).
seL4_NBRecvnow 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_Callmust be paired with
seL4_CNode_SaveCalleris no longer required.
seL4_NBWaitand variants do not require a reply object and can be paired with
seL4_Sendon 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_MsgLengthBitsincreased - this increases amount of caps can be sent per message.
seL4_MsgMaxLengthis now 115, as a result.
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
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_UnbindObject - 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_NBWait- a non-blocking variant of the above.
seL4_WaitWithMRs- a variant of
seL4_Waitthat does not touch the IPC buffer.
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_MaxExtraRefillsis 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.
- A sched control capability is provided to the root task per node
seL4_CNode_SaveCaller(deprecated by reply objects)
seL4_Reply(replaced by invoking a reply object)
Library & test compatability
- CAmkES and CapDL both support seL4
5.2.0-mcson their master branches.
- seL4_libs and sel4test both have
5.2.0-mcs-compatiblebranches that work with the forked API
- You can obtain and run sel4test for seL4
5.2.0-mcsby 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
- A new tutorial covers the difference in the APIs
The RT kernel currently supports:
Other hardware platforms will be added as required (the ports require updated kernel and user-level timer drivers)
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.