seL4 Level-1 Tutorials - Exercise #3: Allocation

Objectives

The purpose of this exercise is to learn: 

Rootserver and boot information structure (bootinfo)
Simple object allocator (simple)
Allocation manager (allocman)
Virtual kernel allocator (vka)
Virtual spaces (vspace)

Background

Applications declare one rootserver which is the transition point from the kernel. From there on, everything executes within the userspace. 

The seL4 kernel passes boot information (bootinfo) to the rootserver. This structure contains a lot of useful information needed for allocation. By default, bootinfo is used to initialize a ‘simple’ object allocator. 

Simple contains information about untyped and device untyped memory regions, it also provides means to get capability pointers to either capability or virtual spaces. Therefore, it is crucial to have simple initialized before any allocation is attempted. 

Simple is not only built using bootinfo. It can be custom built and passed to other child processes allowing them to initialize their own allocators which work within their own isolated spaces. An example of this is the seL4-test driver.

After having the simple object allocator initialized, we can use it to create an allocation manager which works within its boundaries. The allocation manager allows the configuration of static and virtual pools which can be used to create cspaces and vspaces. Once the allocation manager is up, it’s used to create a virtual kernel allocator which provides wide range of objects to retype from the untyped memory region. The virtual kernel allocator can be used to create new thread TCB capabilities, endpoints, …, etc. 

Steps

Initialize build environment:

          The output should be: 

    2.  Initialize a simple object allocator (TODO #1 in main.c). The purpose of this task is to use the bootinfo (passed from the kernel to the rootserver) to initialize a simple object allocation. This behavior is provided by default to every root server and it is the easiest way to initialize a simple object allocator. 

          Recompile and simulate. The output should be: 

    3.  Create an allocation manager using the simple object retrieved from bootinfo (TODO #2). For this task, we bootstrap an allocation manager and have it point to a memory pool. 

         Recompile and simulate. The output should be: 

    4.  Create a virtual kernel allocator (TODO #3). A virtual kernel allocator represents an interface that allows interaction with the kernel and this allows us to allocate objects as necessary in the userspace. This process requires an allocation manager (from previous task).

         Recompile and simulate. The output should be: 

    5.  Create virtual space (TODO #4). This step uses a virtual kernel allocator to create a virtual space that can fit different objects for future use. 

sel4utils_bootstrap_vspace_with_bootinfo_leaky(vspace_t *vspace,
                                                                                              sel4utils_alloc_data_t *data,
                                                                                              seL4_CPtr vspace_root,
                                                                                              vka_t *vka,
                                                                                              seL4_BootInfo *info)

- vspace:                   uninitialized vspace to initialize
- data:                        uninitialized data structure for vspace to fill and use
- vpsace_root:         root object for vspace (hint, simple_get_pd(&simple))
- vka:                          initialized vka to allocate the vspace
- info:                         platsupport provided bootinfo
- RETURNS:              error code (0 on success)

         Recompile and simulate. The output should be: 

Learned APIs

simple_default_init_bootinfo
bootstrap_use_current_simple
allocman_make_vka
sel4utils_bootstrap_vspace_with_bootinfo_leaky

⟵ Exercise-2

table of contents

Exercise-4 ⟶