README.md
1<!--
2 Copyright 2019, Data61
3 Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 ABN 41 687 119 230.
5
6 This software may be distributed and modified according to the terms of
7 the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 See "LICENSE_BSD2.txt" for details.
9
10 @TAG(DATA61_BSD)
11-->
12# The seL4 Run-time
13
14This provides a minimal runtime for running a C or C-compatible process,
15i.e. one with a C-like `main`, in a minimal seL4 environment.
16
17This runtime provides mechanisms for accessing everything a standard
18process would expect to need at start and provides additional utilities
19for delegating the creation of processes and threads.
20
21## Standard Processes
22
23All processes (except for the root task) will use the entry-points
24provided here as normal and require the `_start` entry-point provided in
25the architecture-dependant `crt0.S`. This will then bootstrap into the
26runtime entry-point `__sel4_start_c` which simply processes the stack to
27find the argument, environment, and auxiliary vectors.
28
29The found vectors, along with`main`, are passed into
30`__sel4_start_main` which configures the runtime before starting
31`main`.
32
33## Root Task
34
35The root task requires an alternate entry-point `_sel4_start` which
36assumes that the `seL4_BootInfo` argument has been passed to it and that
37it has not been given a stack.
38
39This entry-point moves onto a static 16 kilobyte stack before invoking
40`__sel4_start_root`, which constructs the argument, environment, and
41auxiliary vectors. It then passes the constructed vectors, along with
42`main`, into `__sel4_start_main` which configures the runtime before
43starting `main`.
44
45## Thread-local storage layout
46
47There are two standard layouts for thread local storage commonly used.
48One where the TLS base address refers to the first address in memory of
49the region and one where it refers to the address that immediately
50follows the region. Intel's x86_64 and ia32 architectures use the latter
51method as it aligns with the segmentation view of memory presented by
52the processor. Most other platforms use former method, where the TLS can
53be said to be 'above' the thread pointer.
54
55In order to store metadata for the current thread in the same memory
56allocation as the TLS, the run-time utilises memory on the other side of
57the thread pointer for it's thread structure.
58