Using Rust in seL4 Userspace

This training session is part of the seL4 Summit 2024 and has been funded by the seL4 Foundation.

It is lead by Nick Spinale ([email protected]).

Introduction

Support for Rust in seL4 userspace has been an official seL4 Foundation project since November 2023:

The exports of this project covered in this training are:

Rust bindings for the seL4 API
A runtime for root tasks
Rust bindings for the seL4 Microkit API
A runtime for seL4 Microkit protection domains
Custom rustc target specifications for seL4 userspace

This training is a self-paced, hands-on tutorial that will lead you through the usage of those exports. There is more tutorial here than could be worked through during this training session, so feel to skip around.

Important: The instructor is eager to work through exercises or discuss any related issues or topic on an individual basis with you. Take advantage of the fact that this is an in-person interactive session!

Part I covers the Rust bindings for the seL4 API and the runtime for root tasks. Familiarity with the seL4 API isn't necessarily assumed or required, but this text doesn't introduce its elements in as much detail as the seL4 Manual. Please let the instructor know if you'd like an introduction or review for any seL4 API concepts or details.

Part II is much shorter, and covers the Rust language runtime for seL4 Microkit protection domains and implementation of the Microkit API. This part does assume that the reader is familiar with the basics of the Microkit framework and API, or is using a companion resource to learn about the Microkit in parallel.

Setup

This training session is presented as a linear series of patches to https://github.com/coliasgroup/seL4-summit-2024-rust-training-code, starting at commit 46869faeee42, and ending with commit f0e140493945. Each patch, or step, as we shall call them, is an instructive modification to a code example. You are encouraged (but by no means required) to attempt those marked as exercises in this text on your own. Note that while most step patches include tests, the reader is not expected to write tests for exercises themselves.

Clone the repository and checkout the starting commit:

git clone https://github.com/coliasgroup/seL4-summit-2024-rust-training-code
cd seL4-summit-2024-rust-training-code
git checkout 46869faeee42

Observe the steps ahead:

git log 46869faeee42..f0e140493945

Each step header contains two icons. Clicking the clipboard copies the commit hash corresponding to the step to the clipboard. The GitHub icon is a link to the commit on GitHub.

Use any Git workflow that works for you. For example, you could cherry-pick the steps that are not marked as exercises after examining and understanding them, and then attempt the exercises on your own, using those step commits as hints when necessary.

Docker

We will work inside of a Docker container built with docker/Dockerfile. This Dockerfile installs some build-time dependencies, and then builds seL4, seL4 Microkit, and some additional programs and tools.

Build the image:

make -C docker build

Run a container in the background:

make -C docker run

Start a shell inside the container:

make -C docker exec

The rest of this text assumes that you are in a shell inside the container.

Two Workspaces

To simplify our Cargo invocations, this repository's Rust code has been divided between two distinct workspaces: workspaces/root-task and workspaces/microkit. Both are subject to the top-level .cargo/config.toml, whereas workspaces/root-task/.cargo/config.toml and workspaces/microkit/.cargo/config.toml each apply to only one. These workspace-specific config.toml files demonstrate all that is required to configure the crates in the rust-sel4 project:

An environment variable pointing at libsel4 (which includes the kernel configuration). See the relevant crate docs for information on this environment variable.
A reference to a custom rustc target specification (the location of the target specification is given at .cargo/config.toml:8, which refers to target-specs).

VSCode + Dev Containers

If you want help from rust-analyzer, the Rust Language Server, you can use VSCode with the Dev Containers extension. This will enable you to run VSCode inside of the container you just built, which contains the seL4 build artifacts that rust-analyzer will require to analyzer your code.

This repository provides a separate Dev Container configuration for each workspace:

To work in a particular workspace, open this repository in VSCode, run > Dev Containers: Reopen in Container, and select the corresponding configuration. You should now be able to use the rust-analyzer VSCode extension normally for the code in the selected workspace.

Rustdoc

Rustdoc for the rust-sel4 project is hosted here:

https://sel4.github.io/rust-sel4/

However, for the sake of consistency, rustdoc for the particular configurations studied in this text are hosted here too. There is one set of rustdoc for each of the two workspace configurations mentioned in Two Workspaces. Rustdoc does not generate an index page, but you can navigate across crates within a workspace configuration using the sidebar present on top-level rustdoc page for any module.

The Root Task

After initializing itself, the seL4 kernel passes control to a userspace program called the root task, whose image is provided to the kernel at boot-time. The root task's capability space contains capabilities for all memory and boot-time objects. That is to say, the root task spawns with the maximum privilege that a userspace program can have. The kernel provides the root task with a map of its initial capability space in the form of the BootInfo frame. You can read more about the root task's environment in seL4 Reference Manual § 9.1.

Part I of this training will focus on writing from-scratch root tasks in Rust. Some of the code in Part I will be quite low-level, interacting with the language runtime, the linker, and some of the finer details related to bootstrapping an seL4-based system. The only seL4-related crates we will be using are the language runtime and bindings for the seL4 API. Unlike situations where higher-level seL4-related libraries (such as seL4_libs) are used, we will be allocating objects and manage virtual address spaces from scratch.

At boot time, the seL4 kernel and root task are loaded into memory by a kind of bootloader stub referred to as a seL4 kernel loader. For Part I, we will use the kernel loader from the rust-sel4 project. We won't cover how it works or how to use it explicitly in this text. It is built at docker/Dockerfile:94:108, and used at mk/root-task.mk:31:36.

Hello, World!

Run the hello world example:

cd workspaces/root-task/hello-world
make simulate

Press ctrl-a x to exit QEMU.

Here is its source:

hello-world/src/main.rs:7:17

#![no_std]
#![no_main]

use sel4_root_task::root_task;

#[root_task]
fn main(_bootinfo: &sel4::BootInfoPtr) -> ! {
    sel4::debug_println!("Hello, World!");

    sel4::init_thread::suspend_self()
}

The Rust standard library is divided into three layers:

core: dependency-free foundation
alloc: implements heap-backed data structures, but requires a runtime that provides a heap allocator
std includes core and alloc, and adds APIs that depend on OS services such as networking and filesystems

The high-level std doesn't support the low-level seL4 root task target. #![no_std] declares that this crate does not depend on std, and prevents rustc from automatically importing it.

Our language runtime will handle the program's entrypoint differently than a typical Rust program. #![no_main] informs rustc of this fact.

The sel4 crate binds the seL4 API. It is generated from source (.xml, .bf, and .h) in libsel4. We will cover the contents of this crate in future chapters.

The sel4_root_task crate implements a Rust language runtime for the root task environment.

The #[root_task] attribute macro declares a function to be the root task's entrypoint. The entrypoint function must have a signature of the form:

fn(&sel4::BootInfoPtr) -> T
where
    T: sel4_root_task::Termination

(Rustdoc for BootInfoPtr and Termination)

The root task has no way to exit, so, to terminate cleanly, it must suspend its own thread. sel4::init_thread::suspend_self() does exactly this.

Step 2.A (exercise)

Exercise: Cause a panic.

Step 2.B (exercise)

Exercise: Catch the panic using sel4_root_task::panicking::catch_unwind().

Step 2.C (exercise)

You can set a custom panic hook with sel4_root_task::panicking::PanicHook. The default hook just prints the panic's ExternalPanicInfo.

Exercise: Set a custom panic hook.

Step 2.D (exercise)

Exercise: Cause a stack overflow.

Step 2.E (exercise)

The #[root_task] attribute macro accepts a named stack_size parameter, which can be any expression of type usize and whose value is interpreted as the root task's initial thread's stack size, in bytes. For example:

#[root_task(stack_size = 13 * 37)]

The default stack size is sel4_root_task::DEFAULT_STACK_SIZE.

Exercise: Adjust the root task's initial thread's stack size to prevent the stack overflow you just caused.

Step 2.F (exercise)

By default, the sel4_root_task runtime does not include a heap. Any attempt to use the alloc crate will result in a link-time failure.

The #[root_task] attribute macro accepts a heap_size parameter, which can be any expression of type usize and whose value is interpreted as the root task's heap size, in bytes. Note that heap_size must come after stack_size in the case where both are present. For example:

#[root_task(heap_size = 0xf00d)]

#[root_task(stack_size = 13 * 37, heap_size = 0xf00d)]

Exercise: Add a heap and use it.

Step 2.G

The sel4_logging crate builds on top of the log crate to add utilities for initializing simple loggers in minimal environments, such as a seL4 root task. This step demonstrates one way to initialize a logger using this crate:

hello-world/src/main.rs:17:20 after 2.G

static LOGGER: Logger = LoggerBuilder::const_default()
    .level_filter(LevelFilter::Info)
    .write(|s| sel4::debug_print!("{}", s))
    .build();

hello-world/src/main.rs:41 after 2.G

    LOGGER.set().unwrap();

Allocating Kernel Objects

Start by navigating to and running this chapter's example, which, so far, is empty.

cd workspaces/root-task/kernel-objects
make simulate

Userspace operates the seL4 kernel by creating, managing, and accessing kernel objects via references called capabilites. See seL4 Reference Manual § 2.3 (Kernel Objects) for an outline of the core types of kernel objects.

In the context of seL4, a capability is a granular, unforgeable token of authority that references a kernel object and carries access rights that limit what the user of a cabability can do with the referenced kernel object. In general, a system call in seL4 amounts to refering to a cabability and an action on the kernel object the cabability points to. This is called invoking a capability.

Just as each thread is associated with a virtual address space which the hardware uses to translate virtual memory addresses into locations in physical memory, each seL4 thread is also assocated with a capability space (CSpace) which the kernel uses to translate so-called capability pointers (CPointers or CPtrs) into locations (slots) in the kernel's capability tables called CNodes.

The sel4::CPtr type is a wrapper around a machine word. The sel4::Cap<T> type wraps a CPtr associated with the current thread's CSpace, and thus points to a particular capability slot within the kernel. It is paramterized by a capability type T: sel4::CapType, representing the type of capability in that slot. It is up to the crate user to ensure that Cap's are valid and well-typed in the current thread.

The sel4::cap module contains aliases of the form sel4::Cap<sel4::cap_type::*>.

Depending on the Cap's type T, a Cap has a number of methods available, which correspond to invocations for that capability type. For example, sel4::Cap::tcb_resume() is available when T is sel4::cap_type::Tcb.

Step 3.A

As elaborated in seL4 Reference Manual § 2.4 (Kernel Memory Allocation), userspace is responsible for managing the memory associated with kernel objects. Untyped memory is the name of the object type for free memory. At boot time, the root task is granted untyped memory capabilities for all of the system's memory, except for the memory used for the kernel and the root task's own resources.

Print the untyped memory described by the BootInfo frame:

workspaces/root-task/kernel-objects/src/main.rs:14:22 after 3.A

    sel4::debug_println!("untyped:");
    for ut_desc in bootinfo.untyped_list() {
        sel4::debug_println!(
            "    paddr: {:#016x?}, size bits: {:02?}, is device: {:?}",
            ut_desc.paddr(),
            ut_desc.size_bits(),
            ut_desc.is_device()
        );
    }

Sample output:

untyped:
    paddr: 0x00000000000000, size bits: 27, is device: true
    paddr: 0x00000008001000, size bits: 12, is device: true
    paddr: 0x00000008002000, size bits: 13, is device: true
    paddr: 0x00000008004000, size bits: 14, is device: true
    paddr: 0x00000008008000, size bits: 15, is device: true
    paddr: 0x00000008011000, size bits: 12, is device: true
    paddr: 0x00000008012000, size bits: 13, is device: true
    ...

sel4::UntypedDesc::size_bits() returns the log base 2 of the size of the region of memory described by the descriptor.

sel4::UntypedDesc::is_device() returns whether the region is device memory or kernel memory. Device memory can only be used for creating frames, whereas kernel memory has no such restrictions.

Step 3.B

Add a function that finds the largest untyped region passed to the root task:

workspaces/root-task/kernel-objects/src/main.rs:32:42 after 3.B

fn find_largest_kernel_untyped(bootinfo: &sel4::BootInfo) -> sel4::cap::Untyped {
    let (ut_ix, _desc) = bootinfo
        .untyped_list()
        .iter()
        .enumerate()
        .filter(|(_i, desc)| !desc.is_device())
        .max_by_key(|(_i, desc)| desc.size_bits())
        .unwrap();

    bootinfo.untyped().index(ut_ix).cap()
}

The expression bootinfo.untyped().index(ut_ix).cap() indexes into bootinfo.untyped(): SlotRegion<Untyped> to retrieve a Slot<Untyped>, which can be turned into a Cap<Untyped> (= cap::Untyped).

Step 3.C

In this step, we will allocate a Notification object.

We already know how to refer to a capability in the current thread's CSpace: a CPtr. However, some capability invocations allow us to refer to a capability slot in any CSpace whose root CNode is present in the current thread's CSpace. In these cases, we must provide:

A CPtr, interpreted in the context of the current thread's CSpace, which points to the target CSpace's root CNode
A CPtr, interpreted in the context of the target CSpace, which points to the target capability slot
A depth, which is the number of bits of the second CPtr to interpret. This allows for the second CPtr to point to a CNode. Why this is necessary is outside the scope of this training, but you can read about it in seL4 Reference Manual § 2.4 (CSpace Addressing).

Consider, for example, the seL4_CNode_Mint capability invocation. dest_* and src_* are both capability slots addressed in this way.

This more flexible method of capability slot addressing is encapsulated in the sel4::AbsoluteCPtr type.

The seL4_Untyped_Retype method is used for allocating new objects from an untyped object. The _service parameter is the address of the untyped object as a normal CPtr. root, node_index, and node_depth address, in the more flexible way outlined above, the destination CNode into which capabilities for the new objects will be inserted. node_offset and num_objects specify a range of slots within the selected CNode for the new capabilites (and, simultaneously, the number of new objects that will be created).

type and size_bits specify the shape of the new object(s) Note that size_bits is relevant for only certain object types (see seL4 Reference Manual § 2.4.2 (Summary of Object Sizes) for more information). This shape information is encapsulated in the sel4::ObjectBlueprint type.

Multiple kernel objects can be allocated from a single unytped object. For each untyped object, the kernel maintains a watermark which tracks how much of the untyped object has been used up for object allocation. seL4_Untyped_Retype aligns the watermark to the desired object type's size, and then advances it according to the object type size and number of objects. This process is detailed in the fourth paragraph of seL4 Reference Manual § 2.4.1 (Reusing Memory).

Let us now work towards calling sel4::cap::Untyped::untyped_retype() on our previously acquired largest_kernel_ut. We wish to allocate one notification object and insert a capability for it into a free slot in the current thread's own CSpace. More precisely, we need a sel4::AbsoluteCPtr for the current thread's own CSpace's root CNode, and an index into that CNode for a free slot.

The CPtr for the initial thread's own CSpace root is a constant:

workspaces/root-task/kernel-objects/src/main.rs:27:27 after 3.C

    let cnode = sel4::init_thread::slot::CNODE.cap();

bootinfo can tell us about a range of empty slots in this CSpace. We can leverage the fact that Rust's Range<T> type is an iterator for certain T to allocate slots in an ergonomic way:

workspaces/root-task/kernel-objects/src/main.rs:29:33 after 3.C

    let mut empty_slots = bootinfo
        .empty()
        .range()
        .map(sel4::init_thread::Slot::from_index);
    let notification_slot = empty_slots.next().unwrap();

The {{#rustdoc_link root-task sel4/cap/type.CNode.html#method.absolute_cptr_for_selfsel4::cap::CNode::absolute_cptr_for_self()}} method elaborates a sel4::cap::Cnode into a sel4::AbsoluteCPtr. Interestingly, there are two ways to do this, but the current implementation is just to use a depth of zero.

Now we can invoke our untyped capability to allocate a notification object:

workspaces/root-task/kernel-objects/src/main.rs:36:43 after 3.C

    largest_kernel_ut
        .untyped_retype(
            &sel4::ObjectBlueprint::Notification,
            &cnode.absolute_cptr_for_self(),
            notification_slot.index(),
            1,
        )
        .unwrap();

Now that we know that notification_slot contains a notification capability, we can cast it and get a sel4::cap::Notification:

workspaces/root-task/kernel-objects/src/main.rs:45:47 after 3.C

    let notification = notification_slot
        .downcast::<sel4::cap_type::Notification>()
        .cap();

Step 3.D (exercise)

Exercise:: Use sel4::cap::Notification::signal() and sel4::cap::Notification::wait() to signal and then wait on the notification.

Step 3.E (exercise)

As described in seL4 Reference Manual § 5 (Notifications), a notification capability can contain a word-sized mask called a badge. When that capability is used to signal the notification, the notification's word-sized state is bit-wise ored with the capability's badge. A wait call on the notification returns and clears the notification's state, provided that a signal call has occurred since the last wait call.

sel4::AbsoluteCPtr::mint() mints a new capability from an existing capability, updatings its access rights and badge.

Exercise:: Allocate a new empty slot in the current CNode.

A slot in the root task's CSpace (i.e. a value of type sel4::init_thread::Slot) can be turned into an sel4::AbsoluteCPtr using {{#rustdoc_link root-task sel4/cap/type.CNode.html#method.absolute_cptrsel4::CNode::absolute_cptr()}}:

workspaces/root-task/kernel-objects/src/main.rs:63:63 after 3.E

            &cnode.absolute_cptr(notification_slot.cptr()),

Exercise:: Mint a capability based on the capability in notification_slot into your newly allocated slot. Use sel4::CapRights::all() for the rights parameter, and specify a non-zero badge value.

Exercise:: Signal the notification using your newly minted badged capability. Using the return value of sel4::Notification::wait(), compare the badge value it returns with the badge you used to mint the capability.

Step 3.F (exercise)

Exercise:: sel4::CapRights::all() is overly-permissive. Use the overly-restrictive sel4::CapRights::none() instead and watch the program fail.

Step 3.G (exercise)

Exercise:: Now use the minimum rights necessary for the program to run.

Modifying the Address Space

This chapter will focus on using the seL4 virtual address space (VSpace) APIs to manipulate the root task's own address space. Start by navigating to and running this chapter's example, which, so far, is empty.

cd workspaces/root-task/address-space
make simulate

In seL4, each thread is associated with a virtual address space (VSpace). A VSpace is comprised of a tree of translation tables mapping virtual addresses into physical frames of memory. VSpaces are represented by their root translation structures. While the high-level virtual address space API concepts are architecture-independent, the specific kernel object types for a given architecture mirror that architecture's paging structures. That said, all architectures share two object types:

The top-level paging structure, called a VSpace, which is used to represent a virtual address space. In the sel4 crate, the corresponding sel4::CapType is sel4::cap_type::VSpace (note that, for some architectures, this is a type alias).
Frames of physical memory. The set of possible frames sizes is architecture-dependant. See seL4 Reference Manual § 7.1.3 (Page). In the sel4 crate, sel4::cap_type::Granule is an alias for the sel4::CapType corresponding to the smallest frame object type.

The root task is provided with capabilites for the objects comprising its own virtual address space. The locations of these capabilities in the root task's CSpace is provided in the BootInfo struct. Our goal for this chapter will be to create a frame object and experiment with mapping it into the root task's own address space.

Step 4.A (exercise)

Exercise: Using code snippets from Chapter 3 (Allocating Kernel Objects), create a frame object. We seek a value frame: sel4::cap::Granule (which can also be written as frame: sel4::Cap<sel4::cap_type::Granule>).

Note that, after importing the sel4::CapTypeForObjectOfFixedSize trait, you can express the appropriate sel4::ObjectBlueprint as sel4::cap_type::Granule::object_blueprint().

Step 4.B

In order to avoid interacting with intermediate translation structures, let's reserve an aligned granule-sized region in the root task's program image that we can use for our experiment:

workspaces/root-task/address-space/src/main.rs:15:20 after 4.B

const GRANULE_SIZE: usize = sel4::FrameObjectType::GRANULE.bytes(); // 4096

#[repr(C, align(4096))]
struct PagePlaceholder(#[allow(dead_code)] [u8; GRANULE_SIZE]);

static mut PAGE_A: PagePlaceholder = PagePlaceholder([0xee; GRANULE_SIZE]);

workspaces/root-task/address-space/src/main.rs:46:49 after 4.B

    let page_a_addr = ptr::addr_of!(PAGE_A).cast::<u8>();
    sel4::debug_println!("PAGE_A: {page_a_addr:#x?}");
    assert_eq!(page_a_addr as usize % GRANULE_SIZE, 0);
    assert_eq!(unsafe { page_a_addr.read() }, 0xee);

This reservation covers exactly one page in the root task's virtual address space.

Step 4.C

Let's unmap the page in the root task image that initially backs our reserved region. This will give us a hole in the root task VSpace, which we can use for our experiment.

This function determines the slot in the root task's CSpace of the page capability corresponding to the page in the root task's VSpace which contains the given address:

workspaces/root-task/address-space/src/main.rs:73:84 after 4.C

fn get_user_image_frame_slot(
    bootinfo: &sel4::BootInfo,
    addr: usize,
) -> sel4::init_thread::Slot<sel4::cap_type::Granule> {
    extern "C" {
        static __executable_start: usize;
    }
    let user_image_addr = ptr::addr_of!(__executable_start) as usize;
    bootinfo
        .user_image_frames()
        .index(addr / GRANULE_SIZE - user_image_addr / GRANULE_SIZE)
}

__executable_start is defined by the linker. We can use it, along with addr, to identify the offset into bootinfo.user_image_frames() of the capability we are after.

Use the get_user_image_frame_slot() function to find the capability corresponding to the frame backing our reserved region, and unmap that frame, leaving a hole in the root task's virtual address space. Try to access that region, and observe a page fault:

workspaces/root-task/address-space/src/main.rs:51:54 after 4.C

    let page_a_slot = get_user_image_frame_slot(bootinfo, page_a_addr as usize);
    page_a_slot.cap().frame_unmap().unwrap();

    unsafe { page_a_addr.read() };

Step 4.D (exercise)

Exercise: Map new_frame at page_a_addr using new_frame.frame_map(), which corresponds to seL4_ARM_Page_Map.

Here are some hints for the parameters of .frame_map():

vspace: A capability for the root task's VSpace can be expressed using sel4::init_thread::slot::VSPACE.cap().
rights: sel4::CapRights::read_write() are the most permissive rights, and will work for our purposes.
attrs: sel4::VmAttributes::default() will work here.

Using a Serial Device

In this chapter, we will build a root task that interacts with a serial device. Start by navigating to and running this chapter's example, which, so far, doesn't do anything interesting.

cd workspaces/root-task/serial-device
make simulate

The module at device.rs implements a higher-level interface over the serial device's MMIO registers, whose physical base address is:

workspaces/root-task/serial-device/src/main.rs:16:16

const SERIAL_DEVICE_MMIO_PADDR: usize = 0x0900_0000;

Our first goal will be to map the serial device's MMIO registers into the root task's address space.

After that, we will set up the root task's access to the serial device's interrupt, whose value is:

workspaces/root-task/serial-device/src/main.rs:18:18

const SERIAL_DEVICE_IRQ: usize = 33;

Finally, we will implement a simple loop that echoes serial input to serial output.

Step 5.A

First, add some familiar snippets that we will use for allocating CSlots and kernel objects:

workspaces/root-task/serial-device/src/main.rs:34:44 after 5.A

fn find_largest_kernel_untyped(bootinfo: &sel4::BootInfo) -> sel4::cap::Untyped {
    let (ut_ix, _desc) = bootinfo
        .untyped_list()
        .iter()
        .enumerate()
        .filter(|(_i, desc)| !desc.is_device())
        .max_by_key(|(_i, desc)| desc.size_bits())
        .unwrap();

    bootinfo.untyped().index(ut_ix).cap()
}

workspaces/root-task/serial-device/src/main.rs:22:27 after 5.A

    let mut empty_slots = bootinfo
        .empty()
        .range()
        .map(sel4::init_thread::Slot::<sel4::cap_type::Unspecified>::from_index);

    let largest_kernel_ut = find_largest_kernel_untyped(bootinfo);

Step 5.B (exercise)

largest_kernel_ut will be useful for allocating kernel objects whose backing physical addresses don't matter to us, but we must allocate the frame which contains the serial device's MMIO registers at a particular physicall address (SERIAL_DEVICE_MMIO_PADDR). Furthermore, the seL4 API distinguishes between general purpose untyped and device untyped. General purpose untyped is backed by normal memory, and can be used to create any type of object. Device untyped is not backed by normal memory, and can only be used to create frames. See the last two paragraphs of seL4 Reference Manual § 2.4 (Kernel Memory Allocation) for more information. So, we must allocate the serial device MMIO frame from the particular initial device untyped that contains SERIAL_DEVICE_MMIO_PADDR.

Exercice: Identify this initial untyped in the bootinfo. We will need a corresponding sel4::cap::Untyped along with the untyped's physical address (or sel4::UntypedDesc, which contains the physical address) for the next step.

Step 5.C

The untyped we've identified contains the frame we are targeting, but that frame may be somewhere in the middle of the region of device memory the untyped covers. To allocate the frame at SERIAL_DEVICE_MMIO_PADDR, we must allocate dummy objects from this untyped until its watermark is at SERIAL_DEVICE_MMIO_PADDR.

This trim_untyped function takes the untyped capability, its physical address, the desired physical address, and two empty slots for temporarily holding dummy objects. We need two slots because the kernel resets an untyped's watermark if it has no live children. So, we must always keep one child around so that our progress on advancing the watermark is never lost.

workspaces/root-task/serial-device/src/main.rs:43:49 after 5.C

    trim_untyped(
        device_ut_cap,
        device_ut_desc.paddr(),
        SERIAL_DEVICE_MMIO_PADDR,
        empty_slots.next().unwrap(),
        empty_slots.next().unwrap(),
    );

workspaces/root-task/serial-device/src/main.rs:68:95 after 5.C

fn trim_untyped(
    ut: sel4::cap::Untyped,
    ut_paddr: usize,
    target_paddr: usize,
    free_slot_a: sel4::init_thread::Slot,
    free_slot_b: sel4::init_thread::Slot,
) {
    let rel_a = sel4::init_thread::slot::CNODE
        .cap()
        .absolute_cptr(free_slot_a.cptr());
    let rel_b = sel4::init_thread::slot::CNODE
        .cap()
        .absolute_cptr(free_slot_b.cptr());
    let mut cur_paddr = ut_paddr;
    while cur_paddr != target_paddr {
        let size_bits = (target_paddr - cur_paddr).ilog2().try_into().unwrap();
        ut.untyped_retype(
            &sel4::ObjectBlueprint::Untyped { size_bits },
            &sel4::init_thread::slot::CNODE
                .cap()
                .absolute_cptr_for_self(),
            free_slot_b.index(),
            1,
        )
        .unwrap();
        rel_a.delete().unwrap();
        rel_a.move_(&rel_b).unwrap();
        cur_paddr += 1 << size_bits;

Step 5.D

device_ut_cap is now primed; the physical address of the next allocation will be SERIAL_DEVICE_MMIO_PADDR.

Exercise: Allocate a small frame object (sel4::cap_type::Granule) from device_ut_cap.

If your sel4::cap::Granule is called serial_device_frame_cap, then the following assertion should succeed:

workspaces/root-task/serial-device/src/main.rs:70:73 after 5.D

    assert_eq!(
        serial_device_frame_cap.frame_get_address().unwrap(),
        SERIAL_DEVICE_MMIO_PADDR
    );

Step 5.E (exercise)

Exercise: Using code from Step 4.B, Step 4.C, and Step 4.D, map serial_device_frame_cap into the root task's virtual address space.

You should now be able interact with the serial device's MMIO registers. Try printing "Hello, World!" to the serial console with something like:

workspaces/root-task/serial-device/src/main.rs:102:108 after 5.E

    let serial_device = unsafe { Device::new(serial_device_mmio_page_addr.cast()) };

    serial_device.init();

    for c in b"Hello, World!\n" {
        serial_device.put_char(*c);
    }

where serial_device_mmio_page_addr: *mut _ is a pointer to where the MMIO registers are mapped in the root task's virtual address space.

Step 5.F (exercise)

Interrupts are delivered to userspace via notifications. A IRQHandler capability represents the authority to manage a particular interrupt. Specifically, an IRQHandler capability (sel4::cap::IrqHandler) has the following methods:

seL4_IRQHandler_SetNotification(): Associate the interrupt with the given notification. Userspace can call seL4_Wait() or seL4_Poll() on this notification to receive the interrupt.
seL4_IRQHandler_Clear(): Disassociate the notification associated with this interrupts.
seL4_IRQHandler_Ack(): Tell the kernel to pass on acknowledgement of this interrupt to the interrupt controller.

The Rust bindings for these methods are:

The root task spawns with a special IRQControl capability (sel4::cap::IrqControl) which can be used to create IRQHandler capabilities with seL4_IRQControl_Get() (sel4::cap::IrqControl::irq_control_get()).

The intent behind this API is that a highly-privileged component will hold an IRQControl capability, which it will use to distribute more finely-grained IRQHandler capabilities to less privileged components for the interrupts they will manage.

The root task can access its IRQControl capability with sel4::init_thread::slot::IRQ_CONTROL.cap()

Exercise: Use sel4::init_thread::slot::IRQ_CONTROL.cap() to create a sel4::cap::IrqHandler for SERIAL_DEVICE_IRQ.

Step 5.G (exercise)

Exercise: Create a notification object from largest_kernel_ut and associate it with the IRQHandler you just created using sel4::cap::IrqHandler::irq_handler_set_notification().

Step 5.H (exercise)

Exercise: Use serial_device: Device, your IRQHandler, and the notification you associated with the interrupt to write a loop that echoes serial input to serial output.

Use serial_device.clear_all_interrupts() and irq_handler_cap.irq_handler_ack() in sequence to clear the interrupt at the device and interrupt controller levels respectively. Note that you should do this at the beginning of the loop in case your loop enters with an interrupt already pending.

Use irq_notification_cap.wait() to wait for hte interrupt.

Use serial_device.get_char() and serial_device.put_char() to read and write data.

Spawning a Thread

In this chapter, we will explore IPC through an example that spawns a secondary thread. This example starts with a more interesting program than the other examples we've worked with so far. It spawns a secondary thread, and then interacts with it using a notification.

Navigate to and run the example:

cd workspaces/root-task/spawn-thread
make simulate

Explore main.rs at will. If you're used to using seL4_libs, you may notice that our Rust code here is much more low-level and verbose. That is because we aren't using any higher-level seL4-related libraries such as <sel4utils/thread.h>. Our code is more like spawning a thread using <sel4/sel4.h> alone. Note, though, that our code does depend on a few Rust language runtime building block crates such as sel4-initialize-tls and sel4-stack .

The exercises in this chapter are only concerned with the following two functions, which run concurrently:

workspaces/root-task/spawn-thread/src/main.rs:75:79

fn secondary_thread_main(inter_thread_nfn: sel4::cap::Notification) {
    sel4::debug_println!("In secondary thread");

    inter_thread_nfn.signal();
}

workspaces/root-task/spawn-thread/src/main.rs:81:85

fn interact_with_secondary_thread(inter_thread_nfn: sel4::cap::Notification) {
    sel4::debug_println!("In primary thread");

    inter_thread_nfn.wait();
}

secondary_thread_main() runs in the secondary thread, and interact_with_secondary_thread() runs in the secondary thread.

Step 6.A

In this step, we introduce IPC between secondary_thread_main() and interact_with_secondary_thread by changing

#![allow(unused)]
fn main() {
inter_thread_nfn: sel4::cap::Notification
}

#![allow(unused)]
fn main() {
inter_thread_ep: sel4::cap::Endpoint
}

Before, the two sides of the notification communicated via inter_thread_nfn.signal() and inter_thread_nfn.wait().

Now, communication over this IPC endpoint will happen by inter_thread_ep.send() and inter_thread_ep.recv() .

As described in seL4 Reference Manual § 4 (Message Passing (IPC)) and seL4 Reference Manual § 4.2 (Endpoints), a capability for an Endpoint object can be invoked with send() and recv(). send() and recv() block until the two sides of the object rendezvous, at which point a message is passed from the sender to the receiver. This message may contain data and capabilities.

Each thread is associated with a special page of memory called an IPC buffer. The sender populates its own IPC buffer with data and/or CPtrs, and then calls send() with a metadata value called the MessageInfo. The kernel copies data from the sender's IPC buffer into that of the receiver, and/or capabilities from the sender's CSpace into that of the receiver. The kernel uses the MessageInfo to determine how much data to copy between the two IPC buffers (the length field) and how many CPtrs to read from the IPC buffers for copying betwen CSpaces (the caps_unwrapped and extra_caps fields). Finally, the kernel passes the MessageInfo, and control, to the receiver.

In Rust, the sender and receiver can interact with their own IPC buffer using sel4::with_ipc_buffer and sel4::with_ipc_buffer_mut. Message data is held in the message registers (an array of machine words), which is a field of the IPC buffer ( msg_regs and msg_regs_mut ). The length field of the MessageInfo specifies how many message registers will be copied into the receiver's IPC buffer.

One can also view the message registers as an array of bytes using msg_bytes and msg_bytes_mut. In this case, one rounds the length of their message up to the nearest multiple of the machine word size when computing the message length for the MessageInfo.

The MessageInfo also includes a few bits of data called a label (label_width bits wide) that is not interpreted by the kernel.

In Rust, the MessageInfoBuilder type is a clear and concise way to construct a MessageInfo.

In Rust, to smooth out differences between the mixed-criticality and legacy kernel schedulers, recv() always takes a reply_authority argument. Under legacy scheduler configurations, which is what this text uses, this argument can be of type ().

Taking all of this together, let's use our IPC endpoint to send an empty message:

workspaces/root-task/spawn-thread/src/main.rs:75:79 after 6.A

fn secondary_thread_main(inter_thread_ep: sel4::cap::Endpoint) {
    sel4::debug_println!("In secondary thread");

    inter_thread_ep.send(sel4::MessageInfoBuilder::default().label(123).build());
}

workspaces/root-task/spawn-thread/src/main.rs:81:87 after 6.A

fn interact_with_secondary_thread(inter_thread_ep: sel4::cap::Endpoint) {
    sel4::debug_println!("In primary thread");

    let (msg_info, _badge) = inter_thread_ep.recv(());

    assert_eq!(msg_info.label(), 123);
}

Step 6.B (exercise)

Exercise: use sel4::with_ipc_buffer and sel4::with_ipc_buffer_mut to send a message with some data.

Step 6.C (exercise)

See seL4 Reference Manual § 4.2.4 (Calling and Replying) for a description of the seL4_Call syscall (Endpoint::call() in Rust).

Exercise: Change the

#![allow(unused)]
fn main() {
inter_thread_ep.send()
}

in secondary_thread_main() to

#![allow(unused)]
fn main() {
inter_thread_ep.call()
}

and modify interact_with_secondary_thread() to sel4::reply with a message.

Spawning a Task (Challenge)

This final chapter of Part I contains a more open-ended and challenging exercise. We start with an example that spawns an entire new process, which, in the context of low-level seL4 userspace, is often called a task:

cd workspaces/root-task/spawn-task
make simulate

Similarly to what we saw in Chapter 6 (Spawning a Thread), the code in this example is more low-level and complex compared to what you have seen in code that leverages <sel4utils/process.h>. Again, our code here is more like spawning a task using <sel4/sel4.h> alone.

This example consists of two programs. The spawn-task crate is the root task, and the spawn-task-child crate is the child task.

The child task does not spawn in any standard sort of environment, so is includes its own ad-hoc Rust language runtime in child/src/runtime.rs, complete with thread-local storage, a global heap allocator, and exception handling. This runtime is built using a few Rust langauge runtime building block crates:

This minimal, ad-hoc language runtime is a neat, instructive piece of code. If you are interested in learning more about building a new Rust language runtime out of the building blocks provided by the rust-sel4 project, let the instructor know.

Explore the root task and child task at will. Let the instructor know if you would like to discuss any particular aspect of it.

Right now, all the child task does is send a test message over an endpoint back to the root task. The challenge in this chapter, step 7.E, is to extend the root task so that it sets up the child task to be able to interact with the serial device, and to extend the child task to implement the same echo loop as in [./serial-device.html#step-5h]. Steps 7.A, 7.B, 7.C, and 7.D, which are not exercises, make some incremental extensions towards those goals to help you get started.

Step 7.A

This step extends the ObjectAllocator type in workspaces/root-task/spawn-task/src/object_allocator.rs after 7.B with the recklessly_allocate_at() method. This method allocates an object according to the blueprint parameter at the given physical address paddr. Instead of just allocating the object from the largest kernel untyped like the allocate() method does, this method searches through the bootinfo to find the initial untyped capability whose corresponding untyped object contains paddr, allocates dummy objects from this untyped object until its watermark reaches paddr, and then allocates the desired object. recklessly_allocate_at()'s procedure is similar to that which we followed in step 5.C.

This implementation is "reckless" because it modifies the state of the untyped capability it allocates from (allocating from it and changing its watermark) without keeping track of having done so. So, subsequent calls for paddrs contained in the same initial untyped would fail or, worse, misbehave. However, we expect to only need to call it once, so we are okay with this caveat.

In step 7.E, you be able to use this method to allocate the serial device MMIO register frame.

Step 7.B

This step extends the create_child_vspace() function in workspaces/root-task/spawn-task/src/child_vspace.rs after 7.A to take an extra_frames parameter. create_child_vspace() now maps these extra frames into the child task's address space, after the end of the program image, and after the IPC buffer frame.

In step 7.E, you be able to use this parameter to pass in the serial device MMIO register frame to mapped into the child task's address space.

Step 7.C

This step simply copies the Device type from chapter 5 into the child task.

In step 7.E, you be able to use this type to interact with the serial device's MMIO registers, just like we as part of step 5.E.

Step 7.D

This step just adds the SERIAL_DEVICE_MMIO_PADDR and SERIAL_DEVICE_IRQ constants from chapter 5 to the root task.

Step 7.E (challenge)

Exercise: Extend the root task so that it sets up the child task to be able to interact with the serial device, and extend the child task to implement the same echo loop as in [./serial-device.html#step-5h-exercise].

Hint for the root task (click to expand)

Try following this sequence of sub-steps:

Allocate serial_device_frame_cap: sel4::cap::Granule using object_allocator.recklessly_allocate_at().
Map serial_device_frame_cap into the child task's address space using create_child_vspace()'s extra_frames parameter.
Similarly to how we did so in steps 5.F and 5.G, obtain irq_handler_cap: sel4::cap::IrqHandler for SERIAL_DEVICE_IRQ (object_allocator.allocate_slot() might come in handy), allocate irq_nfn_cap: sel4::cap::Notification, and associate irq_nfn_cap with SERIAL_DEVICE_IRQ using irq_handler_cap.
Copy irq_handler_cap and irq_nfn_cap into the child task's CSpace in a similar way to how child_tcb and inter_task_ep are copied.

Hint for the child task (click to expand)

Try following this sequence of sub-steps:

Declare constants IRQ_HANDLER: sel4::cap::IrqHandler and IRQ_NFN: sel4::cap::Notification after OWN_TCB and INTRA_TASK_EP.
Obtain the virtual address of the serial device MMIO frame with addr_of_page_beyond_image(1) (recall how create_child_vspace()'s extra_frames parameter works).
Initialize the serial device with Device::new() and Device::init() (as we did for part of step 5.E), and use the serial device just like we did in step 5.H.

seL4 Microkit

The seL4 Microkit is a framework for creating static systems based on seL4. This part of the text assumes that the reader is familiar with the basics of the Microkit framework and API, or is using a companion resource to learn about the Microkit in parallel. Here are three such resources:

The instructor
The Mirokit manual
The Mirokit tutorial

This part also assumes that the reader has worked through chapters 2 and 6 of Part I.

Hello, World!

Navigate to and run the hello world Microkit example:

cd workspaces/microkit/hello-world
make simulate

Here is its source:

hello-world/pds/hello/src/main.rs:7:22

#![no_std]
#![no_main]

use sel4_microkit::{debug_println, protection_domain, Handler, Infallible};

#[protection_domain]
fn init() -> impl Handler {
    debug_println!("Hello, World!");
    HandlerImpl
}

struct HandlerImpl;

impl Handler for HandlerImpl {
    type Error = Infallible;
}

The sel4_microkit crate implements a Rust language runtime for Microkit protection domains, and implements the Microkit API. It is written in pure Rust, and does not link against libmicrokit.

The Event Handler

The #[protection_domain] attribute macro declares a function to be the protection domain's initialization function. The entrypoint function must have a signature of the form:

fn() -> T
where
    T: sel4_microkit::Handler

An implementation of the Handler trait is used by the runtime as the event handler for the protection domain's main loop. The notified, protected, and fault methods correspond to their equivalents in <microkit.h>.

The default implementations of these methods just panic. Our event handler, which we've called HandlerImpl, is the simplest possible Handler implementation.

Language Runtime

As detailed in its rustdoc, the #[protection_domain] attribute macro takes the same parameters as #[root_task]. Furthermore, the sel4_microkit crate supports all of the same Rust language runtime elements that we explored in Chapter 2, including sel4_microkit::panicking::catch_unwind() and sel4_microkit::panicking::set_hook() .

IPC

This chapter covers making and handling protected procedure calls in protection domains written in Rust. Navigate to and run the example:

cd workspaces/microkit/ipc
make simulate

The example system description specifies two protection domains, with a channel between them:

ipc.system:7:20

<system>
    <protection_domain name="client" priority="100">
        <program_image path="microkit-ipc-client.elf" />
    </protection_domain>

    <protection_domain name="server" priority="200" pp="true">
        <program_image path="microkit-ipc-server.elf" />
    </protection_domain>

    <channel>
        <end pd="client" id="13" />
        <end pd="server" id="37" />
    </channel>
</system>

pds/client/src/main.rs:12:32

const SERVER: Channel = Channel::new(13);

#[protection_domain]
fn init() -> impl Handler {
    debug_println!("client: initializing");
    HandlerImpl
}

struct HandlerImpl;

impl Handler for HandlerImpl {
    type Error = Infallible;

    fn notified(&mut self, channel: Channel) -> Result<(), Self::Error> {
        debug_println!("client: notified by {:?}", channel);

        debug_println!("client: TEST_PASS");

        Ok(())
    }
}

pds/server/src/main.rs:12:39

const CLIENT: Channel = Channel::new(37);

#[protection_domain]
fn init() -> impl Handler {
    debug_println!("server: initializing");

    debug_println!("server: notifying client");

    CLIENT.notify();

    HandlerImpl
}

struct HandlerImpl;

impl Handler for HandlerImpl {
    type Error = Infallible;

    fn protected(
        &mut self,
        channel: Channel,
        msg_info: MessageInfo,
    ) -> Result<MessageInfo, Self::Error> {
        debug_println!("server: called by {:?}", channel);

        todo!()
    }
}

The Channel type is the Rust equivalent of the microkit_channel type alias in libmicrokit. Note how the functionality corresponding to libmicrokit's microkit_notify, microkit_irq_ack, and microkit_ppcall is implemented in methods for Channel.

The MessageInfo type is the Rust equivalent of the microkit_msginfo type alias in libmicrokit. Just as microkit_msginfo is an alias for seL4_MessageInfo_t, sel4_microkit::MessageInfo is just a thin wrapper around MessageInfo.

libmicrokit has microkit_mr_set() and microkit_mr_get() for interacting with the IPC buffer. In the sel4_microkit crate, we have get_mr() and set_mr() , but we also have with_msg_regs(), with_msg_regs_mut(), with_msg_bytes(), and with_msg_bytes_mut(), which use sel4::with_ipc_buffer() and sel4::with_ipc_buffer_mut() under the hood.

Step 10.A (exercise)

Exercise: In the client's notified() handler, make a protected procedure call to the server using SERVER.pp_call(). Handle the call in the server's protected() handler. Include data in the message using sel4_microkit::with_msg_regs{,_mut}.

Exercise (optional): Send something more interesting over IPC using msg_bytes and msg_bytes_mut . For example, the zerocopy crate can be used to view certain types as bytes and vice versa, and the lightweight postcard crate can be used to serialize and deserialize a wider range of types using serde.

!!! NOTE !!!

This chapter was rushed due to time constraints. Call over the instructor if you want to properly learn about this topic.

Shared Memory

This chapter covers interacting with shared memory from protection domains written in Rust. Navigate to and run the example:

cd workspaces/microkit/shared-memory
make simulate

The example system description specifies two protection domains which share two memory regions:

shared-memory.system:7:28

<system>
    <memory_region name="region_a" size="0x1_000" />

    <memory_region name="region_b" size="0x1_000" />

    <protection_domain name="client" priority="100">
        <program_image path="microkit-shared-memory-client.elf" />
        <map mr="region_a" vaddr="0x2_000_000" perms="rw" cached="true" setvar_vaddr="region_a_vaddr" />
        <map mr="region_b" vaddr="0x2_400_000" perms="rw" cached="true" setvar_vaddr="region_b_vaddr" />
    </protection_domain>

    <protection_domain name="server" priority="200" pp="true">
        <program_image path="microkit-shared-memory-server.elf" />
        <map mr="region_a" vaddr="0x2_000_000" perms="r" cached="true" setvar_vaddr="region_a_vaddr" />
        <map mr="region_b" vaddr="0x2_400_000" perms="r" cached="true" setvar_vaddr="region_b_vaddr" />
    </protection_domain>

    <channel>
        <end pd="client" id="13" />
        <end pd="server" id="37" />
    </channel>
</system>

The Microkit tool will inject memory region virtual addresses into protection domain images according to the setvar_vaddr attribute values. For example, the virtual address of the mapping of region_a into the client protection domain will be injected into the microkit-shared-memory-client.elf image at the location specified by then region_a_vaddr symbol.

In the case of Rust, declaring a symbol that the Microkit tool can patch requires a bit more intentionality than in the C case. The sel4_microkit::var! macro is provided to declare such symbols.

The var! macro's implementation is just a few lines of code. We want to express this symbol as a global variable that does not change at runtime, but which cannot be assumed to have the value we assign it at compile time, and which must not be optimized away. The near-trivial sel4_immutable_cell::ImmutableCell type encapsulates this pattern. The #[no_mangle] attribute instructs the compiler to use the name of the variable as the name of the symbol. This is the default in C, but not Rust. We direct the compiler to put this symbol in the .data section with #[link_section = ".data"] to ensure that space is allocated for it in the ELF file itself, not just the program image it describes.

So far, the example protection domains just store pointers to the shared memory regions in their handler state:

pds/client/src/main.rs:14:34

#[protection_domain]
fn init() -> impl Handler {
    debug_println!("client: initializing");

    let region_a = *var!(region_a_vaddr: usize = 0);
    let region_b = *var!(region_b_vaddr: usize = 0);

    debug_println!("client: region_a = {region_a:#x?}");
    debug_println!("client: region_b = {region_b:#x?}");

    HandlerImpl { region_a, region_b }
}

struct HandlerImpl {
    region_a: usize,
    region_b: usize,
}

impl Handler for HandlerImpl {
    type Error = Infallible;
}

pds/server/src/main.rs:14:34

#[protection_domain]
fn init() -> impl Handler {
    debug_println!("server: initializing");

    let region_a = *var!(region_a_vaddr: usize = 0);
    let region_b = *var!(region_b_vaddr: usize = 0);

    debug_println!("server: region_a = {region_a:#x?}");
    debug_println!("server: region_b = {region_b:#x?}");

    HandlerImpl { region_a, region_b }
}

struct HandlerImpl {
    region_a: usize,
    region_b: usize,
}

impl Handler for HandlerImpl {
    type Error = Infallible;
}

Step 11.A

Let's assign types to these shared memory regions. We can define our types in a crate that both the client and server can use:

pds/common/src/lib.rs:9:18

use zerocopy::{AsBytes, FromBytes, FromZeroes};

pub const REGION_A_SIZE: usize = 1337;

#[repr(C)]
#[derive(AsBytes, FromBytes, FromZeroes)]
pub struct RegionB {
    pub field_1: u64,
    pub foo: [u16; 16],
}

Suppose region_a: [u8; REGION_A_SIZE] and region_b: RegionB. You could just turn the virtual addresses we get in our var! symbols into pointers and start interacting with the shared memory regions with unsafe ptr::* operations, but we can leverage the Rust type system to come up with a solution that only requires unsafe at initialization time.

Step 11.B

The under-documented (for now) sel4-externally-shared provides a way for you to declare a memory region's type and bounds, along with the memory access operations that can safely be used on it, so that you can access it without unsafe code. That initial declaration is, however, unsafe.

For now, it is a fork of the volatile crate, generalized to enable the use of memory access operations beyond just the ptr::read_volatile, ptr::write_volatile, and friends supported by that crate. The sel4_externally_shared::ExternallySharedRef type alias is the now-abstract sel4_externally_shared::VolatileRef type instantiated with memory access operations suitable for memory that is shared with another protection domain.

The sel4_microkit::memory_region_symbol! macro is like the sel4_microkit::var! macro, except specialized for shared memory region virtual address symbols. For one, the underlying symbol is always of type usize and the macro returns a value of type NonNull<_>. memory_region_symbol! has a few additional features. For example, memory_region_symbol!(foo: *mut [u8] n = BAR) returns a NonNull<[u8]> with a runtime slice length of BAR.

See this step's diff for how to put this all together.

In Your Project (Challenge)

Exercise (challenge): If you have a Microkit project that you are hacking on, start a new branch and either begin replacing one of your protection domains with one written in Rust, or add a new one written in Rust.

The instructor can help you navigate the introduction of Rust into to your build system, and can help you apply what you've learned to your own project.