The development branch of the for the seL4 realtime extensions. This branch is not verified and is under active development.
- Previously seL4 would not allow threads to set any other thread’s priority to higher than its own. This has been extracted into a separate field for the RT kernel, a maximum priority, which limits what thread cans set their own or other threads priorities to.
- This branch adds scheduling contexts to seL4, which represent CPU time. Scheduling contexts are separate to threads (although threads required one to run) and can be passed around over IPC.
- Scheduling contexts allow developers to create periodic threads, temporally isolation threads and have variable timeslices for round robin threads.
For more details, please see the manual. Most of the updates are in the threads chapter.
seL4_TCB_Configurearguments changed (domain removed, scheduling context cap and max priority added).
seL4_CapSchedControl- initial cap for control of CPU time
seL4_SchedContextObject- new object for that allows threads access to CPU time
seL4_SchedContextBits- size in bits of a scheduling context object
seL4_NBSendRecv- new system call which allows once kernel invocation to perform a non-blocking send on one capability, and wait on another.
seL4_NBSendRecvWithMRs- uses above new system call without touching the IPC buffer, passing only data in registers
seL4_Time- type for specifying temporal units to the kernel
seL4_TCB_SetMaxPriority- set the max priority for a tcb, threads can only start / set priorities threads up to and including their max priority
seL4_Prio_t- type for priority and max priority, used in
seL4_CNode_SaveTCBCaller- save the reply cap of the target tcb. This allows another thread to reply on behalf of the owner of the reply cap.
seL4_SchedControl_Configure- invokes the scheduling control cap to populate a scheduling context with parameters
seL4_SchedContext_Yield- end the timeslice of the thread bound to the sched context invoked.
seL4_SchedContext_BindTCB- 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_UnbindTCB- remove binding of a scheduling context from a tcb, tcb will no longer run but state will be preserved
seL4_CapInitThreadSC- capability to the initial threads scheduling context
seL4_CapSchedControl- scheduling control capability, which is given to the root thread
seL4_SchedContext_BindNotification- Bind a notification to a scheduling context. Passive threads waiting on this notification will borrow the scheduling context.
seL4_SchedContext_UnbindNotification- unbind the notification.
- Domain scheduler removed.
Library & test compatability
The ‘rt’ branch of
seL4_libs has been adapted to the rt branch of seL4,
and the rt branch of sel4test has been ported to the
kernel, along with many more tests written suited to the rt kernel. To
run it, checkout the
default.xml manifest on the rt branch of
The rt branch is in no way compatible with the master branch of seL4.
More details See the
0.0.1-rt-dev manual included in the release.