diff --git a/tutorials/threads/threads.md b/tutorials/threads/threads.md index fd1a408..0cb8c73 100644 --- a/tutorials/threads/threads.md +++ b/tutorials/threads/threads.md @@ -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. @@ -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") ?*/ @@ -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, @@ -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). @@ -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 @@ -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 < main@threads.c:42 [Cond failed: result] @@ -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: + ``` < main@threads.c:51 [Cond failed: result] @@ -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 < main@threads.c:57 [Err seL4_InvalidCapability]: /*-- filter TaskCompletion("threads-priority", TaskContentType.COMPLETED) -*/ @@ -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`. @@ -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 @@ -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.