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:
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:
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:
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:
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:
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:
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()}}:
&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.