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.
All processes (except for the root task) will use the entry-points
provided here as normal and require the
_start entry-point provided in
crt0.S. This will then bootstrap into the
__sel4_start_c which simply processes the stack to
find the argument, environment, and auxiliary vectors.
The found vectors, along with
main, are passed into
__sel4_start_main which configures the runtime before starting
The root task requires an alternate entry-point
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
__sel4_start_main which configures the runtime before
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.
File included from github repo edit
The standard convention for a static C run-time provides the following 3 files:
crt0.o; This provides the
_startsymbol which is used as the entry point into a C program.
crti.o; This provides the prologue to the
_finisymbols. As it occurs in the linker arguments before other object files, other object files may add function calls to the body of these symbols.
crtn.o; This provides the epilogue to the
_finisymbols and occurs in the linker arguments after all other object files.
Constructors and Destructors.
The C runtime provides a mechanism for providing functions to be
executed before and after
main as constructors and destructors for
object files and global state.
There are two mechanisms that provide this as documented in the System V ABI.
The first is the aforementioned
_fini symbols. The second
is a set of regions called
.fini_array. Each of these is simply a vector of void function
pointers to be executed.
The runtime must, before
_init, all function pointers
.preinit_array, then all function pointers in
runtime must also, at
exit, execute all function pointers in
.fini_array in reverse, then execute
To assist in iterating through these arrays, GCC’s internal linker
script defines the symbols
the appropriate sections marking the first function in each and the end
of the array.
_start are on the stack for all platforms.
The top of the stack is structured as so:
- argument count
- array of argument pointers
- an empty string
- array of environment pointers
- a null terminator
- array of auxiliary vector entries
- an ‘zero’ auxiliary vector
- unspecified data
For simplicity, we simply pass a pointer to the stack to the C entry in the runtime and dissasemble the stack there. The entry we use is as follows:
void __sel4_start_c(void *stack);
__sel4_start_c is a void function as it should call the
_exit symbol after calling
File included from github repo edit