User Tools

Site Tools



This shows you the differences between two versions of the page.

Link to this comparison view

wiki:initialuserspace [2018/05/08 19:30] (current)
Line 1: Line 1:
 +====== Deep Dive into the Initial seL4 User Space ======
 +This section contains a deep dive into what is available to the developer from the root thread. This loosely follows how the basic tutorials from Data61 set up their user spaces manually but serves to bring in snippets from the libraries so that the developer can see it all in one page instead of jumping between files and trying to keep too much in their head.
 +===== Root thread =====
 +The most important chunk of data to worry about once the root thread’s main function starts to execute is the ''​%%bootinfo%%''​ structure. This is what other objects are built from.
 +Some important information that the ''​%%bootinfo%%''​ struct contains is the root thread’s TCB object, the initial CSpace, VSpace, and IPC buffer.
 +The ''​%%bootinfo%%''​ struct can be found in ''​%%kernel/​libsel4/​include/​sel4/​bootinfo_types.h%%'':​
 +<code c>
 +typedef struct {
 +    seL4_Word ​        ​extraLen; ​       /* length of any additional bootinfo information */
 +    seL4_NodeId ​      ​nodeID; ​         /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */
 +    seL4_Word ​        ​numNodes; ​       /* number of seL4 nodes (1 if uniprocessor) */
 +    seL4_Word ​        ​numIOPTLevels; ​  /* number of IOMMU PT levels (0 if no IOMMU support) */
 +    seL4_IPCBuffer* ​  ​ipcBuffer; ​      /* pointer to initial thread'​s IPC buffer */
 +    seL4_SlotRegion ​  ​empty; ​          /* empty slots (null caps) */
 +    seL4_SlotRegion ​  ​sharedFrames; ​   /* shared-frame caps (shared between seL4 nodes) */
 +    seL4_SlotRegion ​  ​userImageFrames;​ /* userland-image frame caps */
 +    seL4_SlotRegion ​  ​userImagePaging;​ /* userland-image paging structure caps */
 +    seL4_SlotRegion ​  ​ioSpaceCaps; ​    /* IOSpace caps for ARM SMMU */
 +    seL4_SlotRegion ​  ​extraBIPages; ​   /* caps for any pages used to back the additional bootinfo information */
 +    seL4_Uint8 ​       initThreadCNodeSizeBits;​ /* initial thread'​s root CNode size (2^n slots) */
 +    seL4_Domain ​      ​initThreadDomain;​ /* Initial thread'​s domain ID */
 +    seL4_Word ​        ​archInfo; ​       /* tsc freq on x86, unused on arm */
 +    seL4_SlotRegion ​  ​untyped; ​        /* untyped-object caps (untyped caps) */
 +    seL4_UntypedDesc ​ untypedList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS];​ /* information about each untyped */
 +    /* the untypedList should be the last entry in this struct, in order
 +     * to make this struct easier to represent in other languages */
 +} SEL4_PACKED seL4_BootInfo;​
 +To acquire the original boot information,​ the ''​%%platsupport_get_bootinfo%%''​ function will initialize a user space boot info variable. From here, memory can be allocated, capabilities minted and passed, and a whole slew of other exciting seL4 activities.
 +===== Architecting your environment from seL4 building blocks =====
 +A developer may find it daunting to stitch together all that seL4 provides into something usable. The ''​%%seL4_libs/​libsel4simple%%''​ and ''​%%seL4_libs/​libsel4simple-default%%''​ libraries provide a way to associate the bootinfo with more context as well as helper functions to interact with it.
 +The main data type that is provided by these libraries is the ''​%%simple_t%%''​ structure found in ''​%%seL4_libs/​libsel4simple/​include/​simple/​simple.h%%'':​
 +<code c>
 +typedef struct simple_t {
 +    void *data;
 +    simple_get_frame_cap_fn frame_cap;
 +    simple_get_frame_mapping_fn frame_mapping;​
 +    simple_get_frame_info_fn frame_info;
 +    simple_ASIDPool_assign_fn ASID_assign;​
 +    simple_get_cap_count_fn cap_count;
 +    simple_get_nth_cap_fn nth_cap;
 +    simple_get_init_cap_fn init_cap;
 +    simple_get_cnode_size_fn cnode_size;
 +    simple_get_untyped_count_fn untyped_count;​
 +    simple_get_nth_untyped_fn nth_untyped;​
 +    simple_get_userimage_count_fn userimage_count;​
 +    simple_get_nth_userimage_fn nth_userimage;​
 +    simple_get_core_count_fn core_count;
 +    simple_print_fn print;
 +    simple_get_sched_ctrl_fn sched_ctrl;
 +    simple_get_arch_info_fn arch_info;
 +    simple_get_extended_bootinfo_len_fn extended_bootinfo_len;​
 +    simple_get_extended_bootinfo_fn extended_bootinfo;​
 +    arch_simple_t arch_simple;​
 +} simple_t;
 +It is initialized from the ''​%%simple_default_init_bootinfo%%''​ function, found in ''​%%seL4_libs/​libsel4simple-defaults/​src/​libsel4simple-default.c%%'':​
 +<code c>
 +void simple_default_init_bootinfo(simple_t *simple, seL4_BootInfo *bi) {
 +    assert(simple);​
 +    assert(bi);
 +    simple->​data = bi;
 +    simple->​frame_info = &​simple_default_get_frame_info;​
 +    simple->​frame_cap = &​simple_default_get_frame_cap;​
 +    simple->​frame_mapping = &​simple_default_get_frame_mapping;​
 +    simple->​ASID_assign = &​simple_default_set_ASID;​
 +    simple->​cap_count = &​simple_default_cap_count;​
 +    simple->​nth_cap = &​simple_default_nth_cap;​
 +    simple->​init_cap = &​simple_default_init_cap;​
 +    simple->​cnode_size = &​simple_default_cnode_size;​
 +    simple->​untyped_count = &​simple_default_untyped_count;​
 +    simple->​nth_untyped = &​simple_default_nth_untyped;​
 +    simple->​userimage_count = &​simple_default_userimage_count;​
 +    simple->​core_count = &​simple_default_core_count;​
 +    simple->​nth_userimage = &​simple_default_nth_userimage;​
 +    simple->​print = &​simple_default_print;​
 +    simple->​sched_ctrl = &​simple_default_sched_control;​
 +    simple->​arch_info = &​simple_default_arch_info;​
 +    simple->​extended_bootinfo_len = &​simple_default_get_extended_bootinfo_size;​
 +    simple->​extended_bootinfo = &​simple_default_get_extended_bootinfo;​
 +    simple_default_init_arch_simple(&​simple->​arch_simple,​ NULL);
 +It can be seen here that the simple structure is now associated with functions for acting on the ''​%%bootinfo%%''​ and the boot info is pointed at by the ''​''​ field.
 +It is common to have a global ''​%%simple_t%%''​ variable and a ''​%%seL4_BootInfo*%%''​ variable that the information is stored in with the use of the helper functions.
 +As a side note, the ''​%%sel4test%%''​ project builds off of the ''​%%simple_t%%''​ structure and uses an environment structure which further encapsulates and associates other data structures to aid in setting up and managing the seL4 user environment. The ''​%%sel4test%%''​ environment structure can be found, for reference, in ''​%%sel4test/​apps/​sel4test-driver/​src/​test.h%%'':​
 +<code c>
 +struct driver_env {
 +    /* An initialised vka that may be used by the test. */
 +    vka_t vka;
 +    /* virtual memory management interface */
 +    vspace_t vspace;
 +    /* abtracts over kernel version and boot environment */
 +    simple_t simple;
 +    /* IO ops for devices */
 +    ps_io_ops_t ops;
 +    /* initialised timer */
 +    seL4_timer_t timer;
 +    /* The main timer notification that sel4-driver receives ltimer IRQ on */
 +    vka_object_t timer_notification;​
 +    /* A notification used by sel4-driver to signal sel4test-tests that there
 +     * is a timer interrupt. The timer_notify_test is copied to new tests
 +     * before actually starting them.
 +     */
 +    vka_object_t timer_notify_test;​
 +    /* Only needed if we're on RT kernel */
 +    vka_object_t reply;
 +    serial_objects_t serial_objects;​
 +    /* init data frame vaddr */
 +    test_init_data_t *init;
 +    /* extra cap to the init data frame for mapping into the remote vspace */
 +    seL4_CPtr init_frame_cap_copy;​
 +    void* remote_vaddr;​
 +    sel4utils_process_t test_process;​
 +    seL4_CPtr endpoint;
 +    int num_untypeds;​
 +    vka_object_t* untypeds;
 +    /* time server for managing timeouts */
 +    time_manager_t tm;
 +typedef struct driver_env *driver_env_t;​
 +The sel4test code initializes the environment structure based on global variables with the ''​%%init_env%%''​ function. This is an interesting approach because now the developer has a more complete picture of the environment. This environment structure and initialization method of the sel4 test project isn’t the only way to set up an environment,​ many of the tutorials don’t do this but it is nice to see another way to think about some of these concepts and how another project groups them together.
 +==== Tools of the trade ====
 +With the initial data structures in place, the developer needs to sculpt the virtual address space and the capability space for the other threads to run and access resources. We need to make some tools for that. In this section, the snippets help to show how some of these structures are initialized. A good use case for understanding these structures is so that it is easier to trace through function pointers, such as the ''​%%vka_t%%''​ structure’s,​ ''​%%vka_cspace_alloc_fn%%''​. Later you will see that the ''​%%allocman_make_vka%%''​ function initializes it to point to the ''​%%am_vka_cspace_alloc%%''​ function.
 +First we need to create an Allocation Manager, commonly referred to as ''​%%allocman%%''​. It is common to have a ''​%%allocman_t*%%''​ global variable that points to the environment allocation manager. The global variables here are defined in the same file as the main function, limiting the scope of this variable to the root thread. The ''​%%allocman_t%%''​ structure is defined in ''​%%seL4_libs/​libsel4allocman/​include/​allocman/​allocman.h%%'':​
 +<code c>
 + * The allocman itself. This is generally the only type you will need to pass around
 + * to deal with allocation. It is declared in full here so that the compiler is able
 + * to calculate its size so it can be allocated on stacks/​globals etc as required
 + */
 +typedef struct allocman {
 +    /* link to our underlying allocators. some are lazily added. the mspace will always be here,
 +     * and have_mspace can be used to check if the allocman is initialized at all */
 +    int have_mspace;​
 +    struct mspace_interface mspace;
 +    int have_cspace;​
 +    struct cspace_interface cspace;
 +    int have_utspace;​
 +    struct utspace_interface utspace;
 +    /* Flag that tracks whether any alloc/​free/​other function has been entered yet */
 +    int in_operation;​
 +    /* Counts that track re-entry into each specific alloc/free function */
 +    size_t cspace_alloc_depth;​
 +    size_t cspace_free_depth;​
 +    size_t utspace_alloc_depth;​
 +    size_t utspace_free_depth;​
 +    size_t mspace_alloc_depth;​
 +    size_t mspace_free_depth;​
 +    /* Track whether the watermark is currently refilled so we don't recursively do it */
 +    int refilling_watermark;​
 +    /* Has a watermark resource been used. This is just an optimization */
 +    int used_watermark;​
 +    /* track resources that we have not yet been able to free due to circular dependencies */
 +    size_t desired_freed_slots;​
 +    size_t num_freed_slots;​
 +    cspacepath_t *freed_slots;​
 +    size_t desired_freed_mspace_chunks;​
 +    size_t num_freed_mspace_chunks;​
 +    struct allocman_freed_mspace_chunk *freed_mspace_chunks;​
 +    size_t desired_freed_utspace_chunks;​
 +    size_t num_freed_utspace_chunks;​
 +    struct allocman_freed_utspace_chunk *freed_utspace_chunks;​
 +    /* cspace watermark resources */
 +    size_t desired_cspace_slots;​
 +    size_t num_cspace_slots;​
 +    cspacepath_t *cspace_slots;​
 +    /* mspace watermark resources */
 +    size_t num_mspace_chunks;​
 +    struct allocman_mspace_chunk *mspace_chunk;​
 +    size_t *mspace_chunk_count;​
 +    void ***mspace_chunks;​
 +    /* utspace watermark resources */
 +    size_t num_utspace_chunks;​
 +    struct allocman_utspace_chunk *utspace_chunk;​
 +    size_t *utspace_chunk_count;​
 +    struct allocman_utspace_allocation **utspace_chunks;​
 +} allocman_t;
 +The environments’ allocation manager can be created with the help of a ''​%%libsel4allocman%%''​ helper function: ''​%%bootstrap_use_current_simple%%''​. This function takes in a pointer to the environment’s ''​%%simple%%''​ structure, the size of the allocator pool, and an array of the same size.
 +From the allocation manager, a Virtual Kernel Manager can be created, commonly denoted with the ''​%%vka%%''​ prefix. It is common to have a ''​%%vka_t%%''​ global variable to store the virtual kernel manager.
 +The virtual kernel allocator structure can be found in ''​%%seL4_libs/​libsel4vka/​include/​vka/​vka.h%%'':​
 +<code c>
 + * Generic Virtual Kernel Allocator (VKA) data structure.
 + *
 + * This is similar in concept to the Linux VFS structures, but for
 + * the seL4 kernel object allocator instead of the Linux file system.
 + *
 + * Alternatively,​ you can think of this as a abstract class in an
 + * OO hierarchy, of which has several implementations.
 + */
 +typedef struct vka {
 +    void *data;
 +    vka_cspace_alloc_fn cspace_alloc;​
 +    vka_cspace_make_path_fn cspace_make_path;​
 +    vka_utspace_alloc_fn utspace_alloc;​
 +    vka_utspace_alloc_maybe_device_fn utspace_alloc_maybe_device;​
 +    vka_utspace_alloc_at_fn utspace_alloc_at;​
 +    vka_cspace_free_fn cspace_free;​
 +    vka_utspace_free_fn utspace_free;​
 +    vka_utspace_paddr_fn utspace_paddr;​
 +} vka_t;
 +The ''​%%allocman_make_vka%%''​ (''​%%seL4_libs/​libsel4allocman/​src/​vka.c%%''​) function is used to populate the fields in the Virtual Kernel Allocator that is passed in.
 +<code c>
 +void allocman_make_vka(vka_t *vka, allocman_t *alloc)
 +    assert(vka);​
 +    assert(alloc);​
 +    vka->​data = alloc;
 +    vka->​cspace_alloc = &​am_vka_cspace_alloc;​
 +    vka->​cspace_make_path = &​am_vka_cspace_make_path;​
 +    vka->​utspace_alloc = &​am_vka_utspace_alloc;​
 +    vka->​utspace_alloc_maybe_device = &​am_vka_utspace_alloc_maybe_device;​
 +    vka->​utspace_alloc_at = &​am_vka_utspace_alloc_at;​
 +    vka->​cspace_free = &​am_vka_cspace_free;​
 +    vka->​utspace_free = &​am_vka_utspace_free;​
 +    vka->​utspace_paddr = &​am_vka_utspace_paddr;​
 +It can be seen that the virtual kernel allocator is initialized with the allocation manager and associated functions. This virtual kernel allocator is now the abstracted interface to use the allocation manager.
 +Now we can make a couple variables to keep track of the CSpace root CNode and the root page directory capability. The ''​%%simple%%''​ library has some helper functions here:
 +<code c>
 +seL4_CPtr cspace_cap = simple_get_cnode(&​simple);​
 +seL4_CPtr pagedir_cap = simple_get_pd(&​simple);​
 +At this point, the developer can create either thread control blocks (TCB) or processes and objects to grant resources to them. Processes are a little more complicated to set up but have the advantage of being able to accept arguments as a normal C program via the main function. Here, a simple thread control block is set up.
 +A thread control block is described with the ''​%%vka_object_t%%''​ (''​%%libsel4vka/​include/​vka/​object.h%%''​) because it is a seL4 managed object.
 +<code c>
 + * A wrapper to hold all the allocation information for an '​object'​
 + * An object here is just combination of cptr and untyped allocation
 + * The type and size of the allocation is also stored to make free
 + * more convenient.
 + */
 +typedef struct vka_object {
 +    seL4_CPtr cptr;
 +    seL4_Word ut;
 +    seL4_Word type;
 +    seL4_Word size_bits;
 +} vka_object_t;​
 +This structure is initialized with the ''​%%vka_alloc_tcb%%''​ function. This sets the fields of the VKA object thread control block. It is three abstractions away from the generic object allocator, ''​%%vka_alloc_object_at_maybe_dev%%''​. Here, the thread control block object is allocated a CSlot with the virtual kernel allocator and it is stored in the object’s ''​%%cptr%%''​ field. The ''​%%ut%%''​ field is initialized as a ''​%%cspacepath_t%%''​ to it’s capability. The ''​%%type%%''​ is initialized to ''​%%seL4_TCBObject%%''​ and the size is set to ''​%%seL4_TCBBits%%''​.
 +This can be further configured with the ''​%%seL4_TCB_Configure%%''​ function, which is referenced in the seL4 API Reference section of the manual. This function, however, is not in the source because is generated. It can be found under the ''​%%build%%''​ directory in ''​%%libsel4/​include/​interfaces/​sel4_client.h%%''​ if you’d like to see the guts of it. The function takes 9 arguments
 +  * ''​%%seL4_TCB _service%%''​ : The capability to the thread control block object that is being configured. Here, this would be the ''​%%cptr%%''​ field of the object.
 +  * ''​%%seL4_Word fault_ep%%''​ : The capability pointer to the fault endpoint for this thread. Here, since this is a bare-bones thread control block object, it can be ''​%%seL4_CapNull%%''​.
 +  * ''​%%seL4_PrioProps_t priority%%''​ : The priority for this thread.
 +  * ''​%%seL4_CNode cspace_root%%''​ : The CSpace root of the environment,​ which we grabbed earlier with the call to ''​%%simple_get_cnode%%''​.
 +  * ''​%%seL4_Word cspace_root_data%%''​ : The guard and guard size of the environments CNode. This is optional and will just be ''​%%seL4_NilData%%''​
 +  * ''​%%seL4_CNode vspace_root%%''​ : The VSpace root. We grabbed this earlier with the call to ''​%%simple_get_pd%%''​.
 +  * ''​%%seL4_Word vspace_root_data%%''​ : This optional argument is not used on ia32 or ARM platforms. We will set it to ''​%%seL4_NilData%%''​.
 +  * ''​%%seL4_Word buffer%%''​ : The location to the thread’s IPC buffer. This is a bare-bones thread and doesn’t have a buffer, so we will set it to ''​%%seL4_NilData%%''​.
 +  * ''​%%seL4_CPtr bufferFrame%%''​ : The capability to the page containing the thread’s IPC buffer. This is a bare-bones thread with no IPC buffer, so it doesn’t have a capability to it either. We will set it to ''​%%seL4_NilData%%''​.
 +The ''​%%seL4_TCB_Configure%%''​ function takes this data and makes some system calls, registering this thread control block, it’s CSpace and VSpace with the kernel.
 +It is now necessary to tell the thread control block what function to execute and set up the register context for it. First, we need to set up some variables to keep track of the registers. The registers are stored in a ''​%%seL4_UserContext%%''​ variable. This is a generated structure for the architecture. For example, on an ''​%%aarch64%%''​ platform the generated xml definition can be seen after a build has completed in ''​%%stage/​$ARCH/​$PLAT/​include/​interfaces/​sel4arch.xml%%'':​
 +<code xml>
 +    <struct name="​seL4_UserContext">​
 +        <member name="​pc"/>​
 +        <member name="​sp"/>​
 +        <member name="​spsr"/>​
 +        <member name="​x0"/>​
 +        <member name="​x1"/>​
 +        <member name="​x2"/>​
 +        <member name="​x3"/>​
 +        <member name="​x4"/>​
 +        <member name="​x5"/>​
 +        <member name="​x6"/>​
 +        <member name="​x7"/>​
 +        <member name="​x8"/>​
 +        <member name="​x16"/>​
 +        <member name="​x17"/>​
 +        <member name="​x18"/>​
 +        <member name="​x29"/>​
 +        <member name="​x30"/>​
 +        <member name="​x9"/>​
 +        <member name="​x10"/>​
 +        <member name="​x11"/>​
 +        <member name="​x12"/>​
 +        <member name="​x13"/>​
 +        <member name="​x14"/>​
 +        <member name="​x15"/>​
 +        <member name="​x19"/>​
 +        <member name="​x20"/>​
 +        <member name="​x21"/>​
 +        <member name="​x22"/>​
 +        <member name="​x23"/>​
 +        <member name="​x24"/>​
 +        <member name="​x25"/>​
 +        <member name="​x26"/>​
 +        <member name="​x27"/>​
 +        <member name="​x28"/>​
 +    </​struct>​
 +A variable of this type is commonly initialized to ''​%%{0}%%''​. This register context’s program counter (pc) now has to be associated with a function. For the purposes of this wiki we will pretend there is some function prototyped as ''​%%void the_thread_fn(void);​%%''​. The ''​%%sel4utils_set_instruction_pointer%%''​ function will set the program counter of the user register context to the function of interest if used as so:
 +<code c>
 +sel4utils_set_instruction_pointer(&​regs,​ (seL4Word)the_thread_fn);​
 +Then, the stack pointer of the user register context structure is set by creating a stack for the thread and passing it to ''​%%sel4utils_set_stack_pointer%%''​. The stack is an array of the type ''​%%uint64_t%%''​ and is generally a global variable.
 +<code c>
 +// -- Globals --
 +#define THREAD_STACK_SIZE 512
 +uint64_t thread_stack[THREAD_STACK_SIZE];​
 +<code c>
 +// -- in the main root thread --
 +uintptr_t thread_stack_top = (uintptr_t)thread_stack + sizeof(thread_stack);​
 +The top of the thread stack and the user register context variable are passed to the ''​%%sel4utils_set_stack_pointer%%''​ function:
 +<code c>
 +sel4utils_set_stack_pointer(&​regs,​ thread_stack_top);​
 +Now the registers are in an initial state and can be written to the thread control block object’s registers. This is done with the ''​%%seL4_TCB_WriteRegisters%%''​ function. This function is generated at build time but it is included in the Architecture-Independent Object Methods section of the manual. The ''​%%seL4_TCB_WriteRegisters%%''​ function takes the following arguments:
 +  * ''​%%seL4_TCB _service%%''​ : The capability of the thread control block. This should be the ''​%%cptr%%''​ field of the thread structure.
 +  * ''​%%seL4_Bool resume_target%%''​ : This flag lets the thread execute code. If using this function to finish setting up the thread control block, leave this as ''​%%0%%''​.
 +  * ''​%%seL4_Uint8 arch_flags%%''​ : This is an optional argument that does not have any meaning for ia32 or ARM architectures. This can be left as ''​%%0%%''​.
 +  * ''​%%seL4_Word count%%''​ : The number of registers to be set. If setting the program counter and stack pointer, this would just be ''​%%2%%''​.
 +  * ''​%%seL4_UserContext *regs%%''​ : This is a pointer to the user context register structure.
 +Now the developer can call ''​%%seL4_TCB_Resume%%''​ and pass it the capability of the newly set up thread (''​%%cptr%%''​ field of the structure) and it will execute code at the configured function.
 +To take this further, one could set up endpoints so that the thread can communicate with other threads with messages or notifications. There is also the ability to set up fault end points. These endpoints are important because it allows a faulting thread to communicate to the system when it fails, which allows the root thread to react to a failing thread and do something about it.
wiki/initialuserspace.txt · Last modified: 2018/05/08 19:30 (external edit)