seL4 Level-1 Tutorials - Exercise #6: Interprocess Communication (IPC)

Objectives

Spawn a child thread with an IPCBuffer.
Spawn a child process using an ELF image.
Let the child process and child thread communicate independently of main process.

Background

IPC in seL4 is a synchronous model. That is, for every receive there should be a send and vice versa. Otherwise, the caller will block while waiting its turn in the queue to come up. This stems from the way IPCBuffer is structured. The structure of an IPCBuffer is described in Table 4.1, Section 4.2 in the seL4 Reference Manual. 

TCBs only have one IPCBuffer each (they can be shared). Therefore, they have to use the same buffer for all communications. 

The tag field is key to all IPC in seL4. It is the backbone of communication since it describes how to deal with the IPCBuffer. The tag field is what all IPC APIs use (e.g. seL4_Recv, seL4_Send, …, etc.). Once a tag is received, the receiver can decode its content and find out what exactly to read from its IPCBuffer. 

Tag fields are: 

Label (see seL4 Reference Manual, not used in this exercise).
Unwrapped capabilities (see seL4 Reference Manual, not used in this exercise).
Extra capabilities: describes number of capabilities sent/received.
Length: described the number of used message registers.

In order to establish an IPC, threads should allocate or share IPCBuffers. In this exercise we allocate a new IPCBuffer for our child thread. To allocate IPCBuffer, we need to page map it using a virtual address. Usually we pick a random virtual address and attempt to map into it. However, that may or may not succeed. On failure, we create a page table, and use it to map IPCBuffer to a random virtual address. Once the IPCBuffer is mapped, we need to tell the new thread about it. Therefore, we create a Thread Local Storage (TLS), and set the IPCBuffer virtual address as its IPCBuffer variable. Finally, we pass the created TLS to the new thread’s TCB. 

After initializing and passing IPCBuffer to the new thread, one major step remains: tell the IPCBuffer where to place received capabilities. If the IPCBuffer is not told where to place received capabilities, it will simply reject receiving any of them. This happens when the received tag holds 0 extra capabilities while the sent tag has a different figure. 

Once the IPCBuffer knows where to receive capabilities, we should be able to send it some capabilities by specifying the extra-capabilities field in the tag. 

This exercise aims to spawn a child process and a child thread and have them communicate in the background. To do so, we need two endpoints (one for each).

Note: for simplicity, the exercise already maps IPCBuffer and puts it into child thread’s TLS (see init_handler_thread function in src/main.c). This was excluded from the tasks. 

Steps

    1.  Initialize build environment:

         The output should be:

    2.  Set capability receiving path for child thread (TODO #1). In this step, we let the child thread know where to save capabilities upon reception. This step is crucial because we want to let the child thread communicate with the child process, but neither one knows about the other as of yet.

seL4_SetCapRecivePath(seL4_CPtr root_cnode, seL4_CPtr index, seL4_Word depth)

- root_cnode:      root node representing start of cspace to receive at it must be within reach of the running thread? (hint cspace_cap)
- index:                 where to place capabilities with respect to root_cnode if you have specialized cspace for the thread, you can leave this at 0 be careful in assigning this value
- depth:                depth of each capability (hint seL4_WordBits)
                               NOTE: this varies from one architecture to another; using seL4_WordBits ensures we use correct data.

          Recompile and simulate. The output should be: 

    3.  Send the child process communication endpoint capability to the child thread (TODO #2 in main function in main.c). Now that the child thread knows where to receive capabilities, we need to let the main process send the capability to the child thread. Since the IPCBuffer is already initialized and configured, we can do that using the seL4_MessageInfo_t tag structure.

1.  tag is seL4_MessageInfo_t type so it can specify whether to use message registers or other stuff from IPCBuffer
2.  seL4_MessageInfo_new can prepare a tag with the following IN ORDER:
    a)  label
    b)  caps_unwrapped (see seL4 Reference Manual for more info - not covered here)
    c)  extra_caps - this is what concerns us, 1 means read one capability from IPCBuffer
    d)  messageregisters - length of message - useful to confirm the received message is of the same size expected. This is NOT NECESSARY when transferring caps!!!
3.  seL4_SetCap(int, cap) allows you to set capability in certain places in IPCBuffer
4.  seL4_Send(endpoint, tag) - USE THREAD ENDPOINT because we're sending the cap to the thread!

         Recompile and simulate. The output should be: 

    4.  Receive the capability in the child thread (TODO #3, function ipc_handler_thread() in main.c). The last step is to let the child thread receive the capability. Then it can use it directly to communicate with the spawned child process.

         Recompile and simulate. The output should be: 

Learned APIs

seL4_SetCapReceivePath
seL4_MessageInfo_new
seL4_SetCap
seL4_GetCap

Additional APIs to parse tags properly

seL4_MessageInfo_get_label(tag)
seL4_MessageInfo_get_capsUnwrapped(tag)
seL4_MessageInfo_get_extraCaps(tag)
seL4_MessageInfo_get_length(tag)

⟵ Exercise-5

table of contents

Exercise-7 ⟶