Skip to content

minor threads tutorial updates #121

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
lsf37 merged 4 commits into from
Jun 1, 2026
Merged

minor threads tutorial updates #121

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
607ff2a
threads: update domain schedule description
lsf37 Jun 1, 2026
d4e3a80
threads: remove duplicate capDL section
lsf37 Jun 1, 2026
f46b959
threads: update expected output
lsf37 Jun 1, 2026
2583de6
threads: fix minor markdown lints
lsf37 Jun 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
68 changes: 29 additions & 39 deletions tutorials/threads/threads.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,11 @@
/*- set progname = "threads" -*/

# Threads

This is a tutorial for using threads on seL4.

In this tutorial, you will:

1. Learn the jargon TCB.
2. Learn how to start a thread in the same address space.
3. Learn how to read and update TCB register state.
Expand All @@ -26,24 +28,6 @@ In this tutorial, you will:
2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities.html)
3. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping.html)

## capDL Loader

Previous tutorials have taken place in the root task where the starting CSpace layout is set by the
seL4 boot protocol. This tutorial uses the *capDL loader*, a root task which allocates statically
configured objects and capabilities.

The capDL loader parses
a static description of the system and the relevant ELF binaries.
It is primarily used in [CAmkES](https://docs.sel4.systems/projects/camkes/) projects
but we also use it in the tutorials to reduce redundant code.
The program that you construct will end up with its own CSpace and VSpace, which are separate
from the root task, meaning CSlots like `seL4_CapInitThreadVSpace` have no meaning
in applications loaded by the capDL loader.

More information about capDL projects can be found [here](https://docs.sel4.systems/projects/capdl/).

For this tutorial clone the [capDL repo](https://github.com/sel4/capdl). This can be added in a directory that is adjacent to the main `tutorials` directory.

## Initialising

/*? macros.tutorial_init("threads") ?*/
Expand All @@ -66,6 +50,7 @@ seL4 provides threads to represent an execution context and manage processor tim
seL4 are realised by *thread control block* objects (TCBs), one for each kernel thread.

TCBs contain the following information:

* a priority and maximum control priority,
* register state and floating-point context,
* CSpace capability,
Expand Down Expand Up @@ -102,25 +87,29 @@ Threads can surrender their current timeslice using the `seL4_Yield` system call

#### Domain scheduling

In order to provide confidentiality seL4 provides a top-level hierarchical scheduler which
provides static, cyclical scheduling of scheduling partitions known as domains. Domains are
statically configured at compile time with a cyclic schedule, and are non-preemptible resulting in
completely deterministic scheduling of domains.
For systems with strict confidentiality requirements, seL4 provides an optional
top-level hierarchical scheduler with provides static, cyclical scheduling of
scheduling partitions known as domains. Domains and domain schedules can be
configured using the `seL4_DomainSet` capability, and are non-preemptible
resulting in completely deterministic scheduling of domains. By default, only
domain 0 runs and threads start in the domain they were retyped in.

Threads can be assigned to domains, and threads are only scheduled
Threads can also be manually assigned to domains. Threads are only scheduled
when their domain is active. Cross-domain IPC is delayed until a domain switch, and
seL4_Yield between domains is not possible. When there are no threads to run while a
`seL4_Yield` between domains has no effect. When there are no threads to run while a
domain is scheduled, a domain-specific idle thread will run until a switch occurs.

Assigning a thread to a domain requires access to the `seL4_DomainSet` capability. This allows a
thread to be added to any domain.
Assigning a thread to a domain requires access to the `seL4_DomainSet`
capability. This allows a thread to be added to any domain.

```c
/* Set thread's domain */
seL4_Error seL4_DomainSet_Set(seL4_DomainSet _service, seL4_Uint8 domain, seL4_TCB thread);

```

See the [seL4 manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf) for information
on how to set up domain schedules.

### Thread Attributes

seL4 threads are configured by [invocations on the TCB object](https://docs.sel4.systems/projects/sel4/api-doc.html#sel4_tcb).
Expand Down Expand Up @@ -161,7 +150,7 @@ The program that you construct will end up with its own CSpace and VSpace, which
from the root task, meaning CSlots like `seL4_CapInitThreadVSpace` have no meaning
in applications loaded by the capDL loader.

Information about capDL projects can be found [here](https://docs.sel4.systems/projects/capdl/).
More information about capDL can be found on the [seL4 docsite](https://docs.sel4.systems/projects/capdl/).

### Configure a TCB

Expand All @@ -171,8 +160,8 @@ Hello, World!
Dumping all tcbs!
Name State IP Prio Core
--------------------------------------------------------------------------------------
tcb_threads running 0x4012ef 254 0
idle_thread idle (nil) 0 0
tcb_threads running 0x4012ef 254 0
idle_thread idle 0 0 0
rootserver inactive 0x4024c2 255 0
<<seL4(CPU 0) [decodeInvocation/530 T0xffffff8008140c00 "tcb_threads" @4012ef]: Attempted to invoke a >
main@threads.c:42 [Cond failed: result]
Expand Down Expand Up @@ -283,6 +272,7 @@ as the current thread. Use the IPC buffer we have provided, but don't set a faul


You should now be getting the following error:

```
<<seL4(CPU 0) [decodeSetPriority/1035 T0xffffff8008140c00 "tcb_threads" @4012ef]: Set priority: author>
main@threads.c:51 [Cond failed: result]
Expand Down Expand Up @@ -329,10 +319,10 @@ set to the same as the main thread in the next `seL4_DebugDumpScheduler()` call.
```
Name State IP Prio Core
--------------------------------------------------------------------------------------
child of: 'tcb_threads' inactive (nil) 254 0
child of: 'tcb_threads' inactive 0 254 0
tcb_threads running 0x4012ef 254 0
idle_thread idle (nil) 0 0
rootserver inactive 0x4024c2 255 0
idle_thread idle 0 0 0
rootserver inactive 0x4024c2 255 0
<<seL4(CPU 0) [decodeInvocation/530 T0xffffff8008140c00 "tcb_threads" @4012ef]: Attempted to invoke a >
main@threads.c:57 [Err seL4_InvalidCapability]:
/*-- filter TaskCompletion("threads-priority", TaskContentType.COMPLETED) -*/
Expand Down Expand Up @@ -509,7 +499,7 @@ The last part of this tutorial is what to do when your thread faults. We provide
kernel printing a fault message, as the thread you have created does not have a fault handler.

In the output below you can see a cap fault has occurred. The first part of the error is that
the kernel was unable to send a fault to a fault handler as it is set to `(nil)`. The kernel
the kernel was unable to send a fault to a fault handler as it is set to `0`. The kernel
then prints out the fault it was trying to send. In this case, the fault is a virtual memory fault.
The new thread has tried to access data at address `0x2` which is an invalid and unmapped address.
The output shows that the program counter of the thread when it faulted was `0x401e66`.
Expand All @@ -521,7 +511,7 @@ The size of the stack dump is configurable, using the
`KernelUserStackTraceLength` cmake variable.

```
Caught cap fault in send phase at address (nil)
Caught cap fault in send phase at address 0
while trying to handle:
vm fault on data at address 0x2 with status 0x4
in thread 0xffffff8008140400 "child of: 'tcb_threads'" at address 0x401e66
Expand Down Expand Up @@ -613,10 +603,10 @@ Now you should have a new thread, which immediately calls the function passed in
That's all for the detailed content of this tutorial. Below we list other ideas for exercises you can try,
to become more familiar with TCBs and threading in seL4.

- Using different TCB invocations to change the new thread's attributes or objects
- Investigate how setting different priorities affects when the threads are scheduled to run
- Implementing synchronisation primitives using global memory.
- Trying to repeat this tutorial in the root task where there are more resources available to
* Using different TCB invocations to change the new thread's attributes or objects
* Investigate how setting different priorities affects when the threads are scheduled to run
* Implementing synchronisation primitives using global memory.
* Trying to repeat this tutorial in the root task where there are more resources available to
create more thread objects.


Expand Down