User Tools

Site Tools


wiki:initialuserspace

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:

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:

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:

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 simple.data 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:

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:

/**
 * 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:

/*
 * 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.

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:

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.

/*
 * 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:

    <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:

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.

// -- Globals --
#define THREAD_STACK_SIZE 512
uint64_t thread_stack[THREAD_STACK_SIZE];
// -- 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:

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)