The seL4 Run-time

This provides a minimal runtime for running a C or C-compatible process, i.e. one with a C-like main, in a minimal seL4 environment.

This runtime provides mechanisms for accessing everything a standard process would expect to need at start and provides additional utilities for delegating the creation of processes and threads.

Standard Processes

All processes (except for the root task) will use the entry-points provided here as normal and require the _start entry-point provided in the architecture-dependant crt0.S. This will then bootstrap into the runtime entry-point __sel4_start_c which simply processes the stack to find the argument, environment, and auxiliary vectors.

The found vectors, along withmain, are passed into __sel4_start_main which configures the runtime before starting main.

Root Task

The root task requires an alternate entry-point _sel4_start which assumes that the seL4_BootInfo argument has been passed to it and that it has not been given a stack.

This entry-point moves onto a static 16 kilobyte stack before invoking __sel4_start_root, which constructs the argument, environment, and auxiliary vectors. It then passes the constructed vectors, along with main, into __sel4_start_main which configures the runtime before starting main.

Thread-local storage layout

There are two standard layouts for thread local storage commonly used. One where the TLS base address refers to the first address in memory of the region and one where it refers to the address that immediately follows the region. Intel’s x86_64 and ia32 architectures use the latter method as it aligns with the segmentation view of memory presented by the processor. Most other platforms use former method, where the TLS can be said to be ‘above’ the thread pointer.

In order to store metadata for the current thread in the same memory allocation as the TLS, the run-time utilises memory on the other side of the thread pointer for it’s thread structure.