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:
fn secondary_thread_main(inter_thread_nfn: sel4::cap::Notification) {
sel4::debug_println!("In secondary thread");
inter_thread_nfn.signal();
}
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 }
to
#![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:
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());
}
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.