seL4 Level-1 Tutorials - Exercise #5: Processes

Objective

Spawn a process from a pre-built Executable and Linkable Format (ELF) image. 

Background

Conceptually, processes are not different from threads in seL4. The major difference between threads and processes is the way they are initialized and spawned. 

Thread procedures are usually defined within the same image as the caller. Processes, on the other hand, have their procedures defined in different images which must be declared in the CMakeLists.txt file. For x86_64 architecture, these images follow the ELF format and there is an ELF-Loader as part of seL4 supporting projects which allows loading those processes. 

Capabilities can be passed to processes in different ways: 

Mint capability to process during configuration prior to spawning.
Use IPC to transfer capabilities during runtime.

This exercise covers how to initialize a process, pass it an endpoint capability, and communicate back and forth. 

Steps

    1.  Initialize build environment:

         The output should be:

    2.  Apply configuration to a new process (TODO #1 in main.c). Thanks to Exercise-3, we know how to do all the allocation stuff, and we use that for this exercise as well. The first step in creating a process is to set its configuration. The config details are already set in function configure_and_spawn_process in main.c:

sel4utils_configure_process_custom(sel4utils_process_t *process,
                                                                       vka_t *vka, vspace_t *vspace,
                                                                       sel4utils_process_config_t config)

- process:          pointer to process we wish to custom configure
- vka:                  pointer to initialized vka object
- vspace:           pointer to initialized vspace
- config:             initialized configure
- RETURNS:      error code (0 on success)

          Recompile and simulate. The output should be: 

    3.  Create an endpoint capability (TODO #2 in main.c). This step is crucial to allow communication with the child process. The capability pointer will be shared between the two processes.

          Recompile and simulate. The output should be: 

    4.  Create a capability path using the endpoint capability pointer (TODO #3 in main.c). This step prepares to mint the capability to the child process. Though we can’t directly mint a capability in seL4, we can mint a capability path instead.

         Recompile and simulate. The output should be: 

    5.  Mint the endpoint capability path to the child process and create a badge to that endpoint (TODO #4 in main.c). Minting the capability will allow the child process to obtain the capability it needs to send the main process messages. The purpose of the badge is to allow the main process to distinguish between the different processes it spawns. When it listens on a certain endpoint, it expects a certain badge number to be presented, if the received badge number is different from what the main process has minted, the program must know.

sel4utils_mint_cap_to_process(sel4utils_process_t *process,
                                                             cspacepath_t path,
                                                             seL4_CapRights_t rights,
                                                             seL4_Word data);

- process:             target process to mint the cap into
- path:                   cspacepath which is the result of the capability conversion
- rights:                 capability rights
- data:                   badge number - very useful to distinguish between multiple process endpoints
- RETURNS:         cptr to minted capability (0 on error)

         Recompile and simulate. The output should be: 

    6.  Spawn the process (TODO #5 in main.c): the final step is spawn the process and get it up and running. The process will have its own memory and isolation. But we still need to know where it is with respect to the main process (the one spawning the child process). 

sel4utils_spawn_process_v(sel4utils_process_t *process,
                                                      vka_t *vka,
                                                      vspace_t *vspace
                                                      int argc, char **argv,
                                                      int resume)

- process:            the initialized process - should be ready to go before this call
- vka:                    pointer to initialized vka
- vspace:             pointer to current initialized vspace
- argc:                  number of command line arguments to pass into the process's main(...)
- argv:                  values of command line arguments passed to the process
- resume :           start process resumed? (1 for true, 0 for false)
- RETURNS:        error code (0 on success)

         Recompile and simulate. The output should be: 

    7.  Observe the loop in function main in main.c to see how the main process receives messages from the two child processes.

Learned APIs

sel4utils_configure_process_custom
vka_alloc_endpoint
vka_cspace_make_path
sel4utils_mint_cap_to_process
sel4utils_spawn_process_v
seL4_Recv

⟵ Exercise-4

table of contents

Exercise-6 ⟶