README.md

<!--
     Copyright 2019, Data61
     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
     ABN 41 687 119 230.

     This software may be distributed and modified according to the terms of
     the BSD 2-Clause license. Note that NO WARRANTY is provided.
     See "LICENSE_BSD2.txt" for details.

     @TAG(DATA61_BSD)
-->
# 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 with`main`, 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.