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.