From 01e254c938480dc85a7b42a314fc355cc645f439 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 5 Jul 2026 17:31:55 +1000 Subject: [PATCH 1/3] faults: seL4 manual links and md lints - Link all mentions of the seL4 manual, not just one. - add blank lines where markdown lints demand Signed-off-by: Gerwin Klein --- tutorials/fault-handlers/fault-handlers.md | 41 ++++++++++++++-------- 1 file changed, 27 insertions(+), 14 deletions(-) diff --git a/tutorials/fault-handlers/fault-handlers.md b/tutorials/fault-handlers/fault-handlers.md index 9eb07ac..2f82320 100644 --- a/tutorials/fault-handlers/fault-handlers.md +++ b/tutorials/fault-handlers/fault-handlers.md @@ -24,7 +24,9 @@ You will learn: 1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) 2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities.html) -3. [IPC tutorial](https://docs.sel4.systems/Tutorials/ipc.html) +3. [IPC tutorial] + +[IPC tutorial]: https://docs.sel4.systems/Tutorials/ipc.html ## Initialising @@ -76,6 +78,7 @@ until the anomaly is cleared away. ## Thread faults vs other sources of faults There are several sources of faults in a running system; they include: + * Fault events generated by the CPU itself when it encounters anomalies in the instruction stream (aka, "processor exceptions"). * Fault events generated by hardware in the event of some hardware anomaly (such as a machine check or non-maskable interrupt). * Fault events generated by the seL4 kernel when it encounters anomalies in the current thread. @@ -100,17 +103,20 @@ to try executing the faulting thread once again. To tell the kernel to resume execution of the faulting thread, the fault handler can either: + * Invoke a reply operation (with `seL4_Reply()`) on the fault handler endpoint and make sure that the `label` in the `seL4_MessageInfo_t` tag is set to `0`; * Explicitly tell the kernel to resume executing the faulting thread using `seL4_TCB_Resume()`. Please note that if the `handler` sets message registers in the reply message, the kernel may interpret these as meaning something: some fault replies accept -parameters. See the seL4 manual for the reply message format for all faults. +parameters. See the [seL4 manual] for the reply message format for all faults. If the fault handler did not properly rectify the anomaly in the faulting thread, resuming the faulting thread will simply cause the kernel to re-generate the fault. +[seL4 manual]: https://sel4.systems/Info/Docs/seL4-manual-latest.pdf + ## Reasons for thread faults Thread faults can be generated for different reasons. When a fault occurs the @@ -137,7 +143,7 @@ about the fault which might help the fault handler to rectify the anomaly. Each anomaly has its own message format because the information needed to describe each anomaly will be different. For more information about the contents of the IPC message sent by the seL4 kernel for each fault anomaly, please see -the [seL4 Manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf). +the [seL4 manual]. The rest of this tutorial will attempt to teach the reader how to receive and handle seL4 thread faults. @@ -162,11 +168,10 @@ is delivered to the receiver just the same way it is delivered for any other IPC where there is a badge on the sender's cap. A keen reader would probably have realised that this means that a badge on the -kernel's cap to a fault endpoint can be used to distinguish fault messages -from different faulting threads, such that a single handler can handle -faults from multiple threads. Please see the -[IPC Tutorial](https://docs.sel4.systems/Tutorials/ipc.html) for a refresher on how -badged fault endpoints work. +kernel's cap to a fault endpoint can be used to distinguish fault messages from +different faulting threads, such that a single handler can handle faults from +multiple threads. Please see the [IPC tutorial] for a refresher on how badged +fault endpoints work. ### Differences between MCS and Master kernel @@ -185,10 +190,12 @@ threads which share the same CSpace. One of the threads is a fault handler while the other triggers a virtual memory fault. You will be guided through the following broad steps: + 1. Badging and configuring a fault handler for the faulting thread. 2. Having the faulting thread trigger a thread fault. 3. Handling the fault in the fault handler. 4. Resuming the execution of the faulting thread. +5. Determining the fault type. ### Description of the tutorial program @@ -217,10 +224,11 @@ the `handler` will `seL4_Reply()` to the `faulter` to let it know that it the After that we trigger a fault in the `faulter`, handle the fault in the `handler`, and then resume the `faulter` and that's the end of the exercise. -### Setting up the endpoint to be used for thread fault IPC messages. +### Setting up the endpoint to be used for thread fault IPC messages The first exercise is to configure the TCB of the faulter with a fault endpoint. This exercise is meant to achieve two learning outcomes: + 1. Explain that the end of the endpoint that is given to the kernel can be badged, and the kernel will return that badge value when it sends a fault IPC message. 2. Explain the differences between the Master and MCS kernels when it comes to telling the kernel about the fault endpoint. @@ -299,7 +307,9 @@ the CSpace of the `faulter` thread: /* Now wait for the fault IPC message from the kernel. */ seL4_Recv(faulter_fault_ep_cap, &tmp_badge); ``` + /*-- filter ExcludeDocs() -*/ + ```c /*-- filter TaskContent("fault-ep-setup", TaskContentType.COMPLETED, subtask="setup", completion="About to touch fault vaddr.") -*/ error = seL4_TCB_SetSpace( @@ -311,6 +321,7 @@ the CSpace of the `faulter` thread: 0); /*-- endfilter -*/ ``` + /*-- endfilter -*/ ### Receiving the IPC message from the kernel @@ -336,11 +347,13 @@ you'd wait for any other IPC message: ``` /*-- filter ExcludeDocs() -*/ + ```c /*-- filter TaskContent("fault-ipc-recv", TaskContentType.COMPLETED, subtask="getmr", completion="Fault occured at cap addr 3 within faulter's cspace.") -*/ foreign_faulter_capfault_cap = seL4_GetMR(seL4_CapFault_Addr); /*-- endfilter -*/ ``` + /*-- endfilter -*/ @@ -387,6 +400,7 @@ So here we'll copy an endpoint cap into the faulting slot: ``` /*-- filter ExcludeDocs() -*/ + ```c /*-- filter TaskContent("fault-handle", TaskContentType.COMPLETED, subtask="copy", completion="Successfully copied a cap into foreign faulting slot.") -*/ error = seL4_CNode_Copy( @@ -399,6 +413,7 @@ So here we'll copy an endpoint cap into the faulting slot: seL4_AllRights); /*-- endfilter -*/ ``` + /*-- endfilter -*/ ### Resuming a faulting thread @@ -527,6 +542,7 @@ int main(void) PROGNAME "(Only necessary on Master kernel.)\n"); /*-- endfilter --*/ ``` + ```c /*-- filter TaskContent("fault-ep-setup", TaskContentType.ALL, subtask="setup1") -*/ /* Here we need to keep in mind which CPtr we give the kernel. On the MCS @@ -612,8 +628,8 @@ int main(void) printf(PROGNAME "Successfully copied a cap into foreign faulting slot.\n" PROGNAME "About to resume the faulter thread.\n"); /*-- endfilter --*/ - ``` + ```c /*-- filter TaskContent("fault-resume", TaskContentType.BEFORE, subtask="reply", completion="About to resume the faulter thread.") -*/ /* EXERCISE: How do we resume a thread that has faulted? seL4_Reply()! */; @@ -626,7 +642,6 @@ int main(void) /*-- endfilter --*/ ``` - ```c /*-- filter ELF("handler") --*/ /*- set _ = state.stash.start_elf("handler") -*/ @@ -671,14 +686,12 @@ int main(void) printf(PROGNAME "Handler thread running!\n" PROGNAME "About to wait for empty slot from faulter.\n"); - seq_msginfo = seL4_Recv(sequencing_ep_cap, &tmp_badge); foreign_badged_faulter_empty_slot_cap = seL4_GetMR(0); printf(PROGNAME "Received init sequence msg: slot in faulter's cspace is " "%lu.\n", foreign_badged_faulter_empty_slot_cap); - /*? include_task_type_append([("fault-badge", 'badge1')]) ?*/ /*? include_task_type_append([("fault-badge", 'badge')]) ?*/ /*? include_task_type_append([("fault-badge", 'badge2')]) ?*/ @@ -687,7 +700,6 @@ int main(void) /*? include_task_type_append([("fault-badge", 'copy')]) ?*/ /*? include_task_type_append([("fault-badge", 'copy2')]) ?*/ - /*? include_task_type_append([("fault-ep-setup", 'setup1')]) ?*/ /*? include_task_type_append([("fault-ep-setup", 'setup')]) ?*/ /*? include_task_type_append([("fault-ep-setup", 'setup2')]) ?*/ @@ -708,5 +720,6 @@ int main(void) } /*-- endfilter --*/ ``` + /*? ExternalFile("CMakeLists.txt") ?*/ /*- endfilter -*/ From aaa8ece186abe52bc32158ba077918bc70a0f839 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 5 Jul 2026 17:33:13 +1000 Subject: [PATCH 2/3] fault-handlers: keep waiting for faults Avoid the VM/cap fault at the end of the handler that tends to confuse people by instead waiting for faults forever. Signed-off-by: Gerwin Klein --- tutorials/fault-handlers/fault-handlers.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tutorials/fault-handlers/fault-handlers.md b/tutorials/fault-handlers/fault-handlers.md index 2f82320..af660d7 100644 --- a/tutorials/fault-handlers/fault-handlers.md +++ b/tutorials/fault-handlers/fault-handlers.md @@ -716,7 +716,11 @@ int main(void) /*? include_task_type_append([("fault-resume", 'reply2')]) ?*/ - return 0; + /* Ignore all further faults: */ + while (1) { + /* It is Ok to pass NULL if we are not interested in the badge */ + seL4_Recv(faulter_fault_ep_cap, NULL); + } } /*-- endfilter --*/ ``` From fa4aefcd5f715baa4af2747fa5006e3f738890c3 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 5 Jul 2026 17:34:19 +1000 Subject: [PATCH 3/3] fault-handlers: avoid printing race at the end Similar to the notification tutorial, the fault handler tutorial has a printing race at the very end when both the fault handler and the faulter thread are finishing. This can leave to interleaved output, which leaves no recognisable success string for CI. Instead, use this to talk about the final VM fault of the faulter thread and show how to get the fault type from the message label, which so far has not been part of the tutorial. Catch the final VM fault and do nothing. This serialises the output. Signed-off-by: Gerwin Klein --- tutorials/fault-handlers/fault-handlers.md | 57 ++++++++++++++++------ 1 file changed, 41 insertions(+), 16 deletions(-) diff --git a/tutorials/fault-handlers/fault-handlers.md b/tutorials/fault-handlers/fault-handlers.md index af660d7..4b1bbcf 100644 --- a/tutorials/fault-handlers/fault-handlers.md +++ b/tutorials/fault-handlers/fault-handlers.md @@ -5,14 +5,16 @@ --> # Fault handling + /*? declare_task_ordering( - ['fault-badge', 'fault-ep-setup', 'fault-ipc-recv', 'fault-handle', 'fault-resume']) + ['fault-badge', 'fault-ep-setup', 'fault-ipc-recv', 'fault-handle', 'fault-resume', 'fault-end']) ?*/ This tutorial covers fault handling in seL4. You will learn: + 1. About thread faults. 2. That a thread fault is different from a processor hardware fault. 3. About fault handlers. @@ -422,19 +424,48 @@ Finally, to have the `faulter` thread wake up and try to execute again, we `seL4_Reply()` to it: ```c +/*-- filter TaskContent("fault-resume", TaskContentType.COMPLETED, subtask="reply", completion="Faulter: Finished execution.") -*/ seL4_Reply(seL4_MessageInfo_new(0, 0, 0, 0)); - - printf(PROGNAME "Successfully resumed faulter thread.\n" - PROGNAME "Finished execution.\n"); + /* faulter thread is now resumed */ +/*-- endfilter -*/ ``` -/*-- filter ExcludeDocs() -*/ +### Fault labels + +As mentioned above, the IPC message from the kernel contains information about +the fault. As we have seen in the [IPC tutorial], `seL4_Recv` returns a message +info struct, which among other fields contains the message label. For fault +messages, this label contains the type of fault, e.g. `seL4_Fault_CapFault` +which we handled above, or `seL4_Fault_VMFault` which is generated for instance +when the faulting thread accesses an address that is not mapped. The chapter on +faults in the [seL4 manual] contains the full list of fault types. + +When our `faulter` thread finishes and returns from `main()`, there is nothing +to return to, since `main()` was not called by another C function. This will +generate a VM fault, which the handler will receive. + +A typical fault handler would wait for such faults in a loop and then act based +on the fault type in the message label and further information received in the +fault message. There is nothing to repair and resume any more in our case, since +the `faulter` thread has finished execution. + ```c -/*-- filter TaskContent("fault-resume", TaskContentType.COMPLETED, subtask="reply", completion="Faulter: Finished execution.") -*/ - seL4_Reply(seL4_MessageInfo_new(0, 0, 0, 0)); -/*-- endfilter -*/ +/*-- filter TaskContent("fault-end", TaskContentType.ALL, subtask="end", completion="Done.") -*/ + /* When the faulter thread returns from "main", this return will generate a VM fault. */ + seL4_MessageInfo_t msg_info = seL4_Recv(faulter_fault_ep_cap, &tmp_badge); + + /* The IPC message label says which kind of fault we have received */ + switch (seL4_MessageInfo_get_label(msg_info)) { + case seL4_Fault_VMFault: + printf(PROGNAME "Faulter has returned from \"main\". Done.\n"); + /* nothing to resume, the faulter has finished */ + break; + default: + printf(PROGNAME "Received unexpected fault.\n"); + break; + } +/*-- endfilter --*/ ``` -/*-- endfilter -*/ ## Further exercises @@ -634,12 +665,6 @@ int main(void) /*-- filter TaskContent("fault-resume", TaskContentType.BEFORE, subtask="reply", completion="About to resume the faulter thread.") -*/ /* EXERCISE: How do we resume a thread that has faulted? seL4_Reply()! */; /*-- endfilter --*/ - - -/*-- filter TaskContent("fault-resume", TaskContentType.ALL, subtask="reply2") -*/ - printf(PROGNAME "Successfully resumed faulter thread.\n" - PROGNAME "Finished execution.\n"); -/*-- endfilter --*/ ``` ```c @@ -713,8 +738,8 @@ int main(void) /*? include_task_type_append([("fault-handle", 'copy2')]) ?*/ /*? include_task_type_append([("fault-resume", 'reply')]) ?*/ -/*? include_task_type_append([("fault-resume", 'reply2')]) ?*/ +/*? include_task_type_append([("fault-end", 'end')]) ?*/ /* Ignore all further faults: */ while (1) {