seL4 Level-1 Tutorials - Exercise #4: Basic Threads

Objective

Initialize basic thread without interprocess-communication buffer (IPCBuffer). 

Background

Threads in seL4 have a very high level of isolation. Every thread has a CNode root which points to the first capability in the CSpace (capability space) of the thread. Threads also have their own virtual spaces, which enhances their high isolation. 

To initialize a thread, a thread control block (TCB) object must be initialized. It provides the necessary means for the parent TCB to control the behavior of the child thread. Initializing a thread can be done in two ways:

Without IPCBuffer: Basic threads. Capability transfer is done using simple APIs (exercise-2).
With IPCBuffer: Allows transfer of capabilities to and from the thread.

This exercise focuses on the first method. The steps to initialize a thread can be summarized in: allocating a TCB object for the thread, configuring the TCB (cspace, vspace, IPBuffer), setting the execution priority, setting the registers (instruction and stack pointers), and finally, starting the thread. 

Steps

    1.  Initialize build environment:

         The output should be:

    2.  Allocate a TCB object for the new thread (TODO #1). This uses the virtual kernel allocator (see Exercise-3) for the allocation. The step is straightforward.

         Recompile and simulate. The output should be: 

    3.  Configure the thread (TODO #2). Now that we have the object, we need to let the thread know what its capability and virtual spaces are (if any). This step can also be used to set the IPCBuffer, but the IPCBuffer requires its own initialization (see Exercise-6 for IPCBuffer initialization). The cspace_root_data and vspace_root_data can be configured to null because they are unnecessary. And the IPCBuffer and its frame can also be ignored. There are further hints in the source code to help set them correctly.

seL4_TCB_Configure(seL4_CPtr _service, seL4_Word fault_ep
                                        seL4_CPtr cspace_root, seL4_Word cspace_root_data,
                                        seL4_CPtr vspace_root, seL4_Word vspace_root_data,
                                        seL4_Word buffer, seL4_CPtr bufferFrame)

- service:                                 cptr of tcb object (hint - tcb_object.cptr)
- fault_ep:                               fault endpoint capability to notify parent thread on faults (can be set to 0)
- cspace_root:                       cspace root capability
- cspace_root_data:             optional (can be set to 0)
- vspace_root:                        vspace root we wish to assign for new tcb
- vspace_root_data:             irrelevent for x86_64 (can be set to 0)
- buffer:                                   IPCBuffer's location (can be set to 0)
-bufferFrame:                        IPCBuffer frame capability - must be mapped (can be set to 0)

         Recompile and simulate. The output should be: 

    4.  Set priority of execution for the new thread (TODO #3). In seL4, a priority can be set using one of 256 values. 255 represents highest priority while 0 is lowest. 

         Recompile and simulate. The output should be: 

    5.  Set the thread’s execution logic (TODO #4). Now that we have configured the thread and initialized everything, we can tell it what it needs to do. We first define a function (thread_proc) and we need to pass a pointer of that function to the thread so it can do the work.

         Recompile and simulate. The output should be: 

    6.  Resume the thread, then suspend it after it is done executing (TODO #5 and TODO #6). By default, when the TCB object is initialized, it is suspended to allow us to set its registers and all the necessary configurations. After having done all of that, we need to resume it to actually start it. It’s worth noting that resume also works after a manual suspension. After the thread is done executing its logic, we suspend it to prevent any unnecessary memory usage in the background. 

         Recompile and simulate. The output should be: 

Learned APIs

vka_alloc_tcb
seL4_TCB_Configure
seL4_TCB_SetPriority
seL4_TCB_WriteRegisters
seL4_TCB_Resume

⟵ Exercise-3

table of contents

Exercise-5 ⟶