From 14a74a607174007cd2c47dc037c1c505ad7bd4ce Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 11 Jul 2025 10:20:02 +1000 Subject: [PATCH 1/4] tutorials: CAmkES spelling Signed-off-by: Gerwin Klein --- tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md | 2 +- tutorials/camkes-vm-linux/camkes-vm-linux.md | 2 +- tutorials/fault-handlers/fault-handlers.md | 2 +- tutorials/hello-camkes-2/hello-camkes-2.md | 2 +- tutorials/hello-camkes-timer/hello-camkes-timer.md | 4 ++-- tutorials/interrupts/interrupts.md | 2 +- tutorials/notifications/notifications.md | 2 +- tutorials/threads/threads.md | 4 ++-- 8 files changed, 10 insertions(+), 10 deletions(-) diff --git a/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md b/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md index 8cca7aff..02c4d496 100644 --- a/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md +++ b/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md @@ -11,7 +11,7 @@ # CAmkES Cross VM Connectors This tutorial provides an introduction to using the cross virtual machine (VM) connector mechanisms -provided by seL4 and Camkes in order to connect processes in a guest Linux instance to Camkes components. +provided by seL4 and CAmkES in order to connect processes in a guest Linux instance to CAmkES components. In this tutorial you will learn how to: diff --git a/tutorials/camkes-vm-linux/camkes-vm-linux.md b/tutorials/camkes-vm-linux/camkes-vm-linux.md index f616cbcf..d776f6bd 100644 --- a/tutorials/camkes-vm-linux/camkes-vm-linux.md +++ b/tutorials/camkes-vm-linux/camkes-vm-linux.md @@ -30,7 +30,7 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +It is primarily used in [CAmkES](https://docs.sel4.systems/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 diff --git a/tutorials/fault-handlers/fault-handlers.md b/tutorials/fault-handlers/fault-handlers.md index 932c1ff3..b3fb0811 100644 --- a/tutorials/fault-handlers/fault-handlers.md +++ b/tutorials/fault-handlers/fault-handlers.md @@ -48,7 +48,7 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +It is primarily used in [CAmkES](https://docs.sel4.systems/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 diff --git a/tutorials/hello-camkes-2/hello-camkes-2.md b/tutorials/hello-camkes-2/hello-camkes-2.md index 6dd02584..4aa12607 100644 --- a/tutorials/hello-camkes-2/hello-camkes-2.md +++ b/tutorials/hello-camkes-2/hello-camkes-2.md @@ -29,7 +29,7 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +It is primarily used in [CAmkES](https://docs.sel4.systems/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 diff --git a/tutorials/hello-camkes-timer/hello-camkes-timer.md b/tutorials/hello-camkes-timer/hello-camkes-timer.md index d55daaa5..8167a11b 100644 --- a/tutorials/hello-camkes-timer/hello-camkes-timer.md +++ b/tutorials/hello-camkes-timer/hello-camkes-timer.md @@ -29,7 +29,7 @@ commented out. ## Prerequisites 1. [Set up your machine](https://docs.sel4.systems/HostDependencies). -2. [Camkes 2](https://docs.sel4.systems/Tutorials/hello-camkes-2) +2. [CAmkES 2](https://docs.sel4.systems/Tutorials/hello-camkes-2) ## CapDL Loader @@ -40,7 +40,7 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +It is primarily used in [CAmkES](https://docs.sel4.systems/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 diff --git a/tutorials/interrupts/interrupts.md b/tutorials/interrupts/interrupts.md index 5bcce8eb..22335874 100644 --- a/tutorials/interrupts/interrupts.md +++ b/tutorials/interrupts/interrupts.md @@ -42,7 +42,7 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +It is primarily used in [CAmkES](https://docs.sel4.systems/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 diff --git a/tutorials/notifications/notifications.md b/tutorials/notifications/notifications.md index 5daf8c02..1a00d6d6 100644 --- a/tutorials/notifications/notifications.md +++ b/tutorials/notifications/notifications.md @@ -45,7 +45,7 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +It is primarily used in [CAmkES](https://docs.sel4.systems/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 diff --git a/tutorials/threads/threads.md b/tutorials/threads/threads.md index fa8b8f08..211463c8 100644 --- a/tutorials/threads/threads.md +++ b/tutorials/threads/threads.md @@ -34,7 +34,7 @@ seL4 boot protocol. This tutorial uses the *capDL loader*, a root task which all 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/CAmkES/) projects +It is primarily used in [CAmkES](https://docs.sel4.systems/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 @@ -155,7 +155,7 @@ seL4 boot protocol. This tutorial uses a the *capDL loader*, a root task which a 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/CAmkES/) projects +It is primarily used in [CAmkES](https://docs.sel4.systems/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 From 479ebea0b27717171a5a2e81aa72944dedee27ad Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 11 Jul 2025 10:25:25 +1000 Subject: [PATCH 2/4] Update README with new links Signed-off-by: Gerwin Klein --- README.md | 30 ++++++++++++++---------------- 1 file changed, 14 insertions(+), 16 deletions(-) diff --git a/README.md b/README.md index 64be8566..bfd6064b 100644 --- a/README.md +++ b/README.md @@ -10,14 +10,15 @@ Various tutorials for using seL4, its libraries, and CAmkES. ## Prerequisites -Follow the instructions for setting up your host environment on the [seL4 docsite](https://docs.sel4.systems/HostDependencies). +Follow the instructions for setting up your host environment on the [seL4 +docsite](https://docs.sel4.systems/Tutorials/setting-up.html). ## Starting a tutorial This tutorial repository is part of a larger collection of repositories, which are required to run the tutorial and are coordinated in a manifest file. See -[this guide](https://docs.sel4.systems/Tutorials/#the-tutorials) on how to check -out a consistent set. +[this guide](https://docs.sel4.systems/Tutorials/get-the-tutorials.html) on how +to check out a consistent set. Once you have that, a tutorial is started through the use of the `init` script that is provided in the root directory. Using this script you can specify a @@ -80,24 +81,21 @@ not appropriate for learning how to create and structure new applications/system tutorials for this will be forthcoming. For now it is suggested to look at other existing applications for ideas. -# Documentation +## Documentation -## Developer wiki +### seL4 docsite -A walkthrough of each tutorial is available on the [`docs site`](https://docs.sel4.systems/Tutorials) +A walkthrough of each tutorial is available on the [seL4 docsite](https://docs.sel4.systems/Tutorials/) -## Tutorial Slides +### Tutorial Slides -The slides used for the tutorial are available in [`docs`](docs). +The slides used for the tutorial are available in [`docs`](docs/). -## seL4 Manual +### seL4 Manual -The seL4 manual lives in the kernel source in the [`manual`](https://github.com/seL4/seL4/tree/master/manual) directory. -To generate a PDF go into that directory and type `make`. -You will need to have LaTeX installed to build it. +A pre-generated PDF version of the seL4 manual can be found +[`here`](http://sel4.systems/Info/Docs/seL4-manual-latest.pdf). -A pre-generated PDF version can be found [`here`](http://sel4.systems/Info/Docs/seL4-manual-latest.pdf). +### CAmkES Documentation -## CAmkES Documentation - -CAmkES documentation lives in the camkes-tool repository in [docs/index.md](https://github.com/seL4/camkes-tool/blob/master/docs/index.md). +CAmkES documentation can be found on the [CAmkES page](https://docs.sel4.systems/projects/camkes/) of the docsite. From bc566fea93dba7390a2bb81835d22a07c73097e1 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 11 Jul 2025 13:21:16 +1000 Subject: [PATCH 3/4] Update links - don't assume implicit html extension, provide it explicitly instead - updates for docsite redirects - fix typos - fix anchors for API docs and others Signed-off-by: Gerwin Klein --- .../camkes-vm-crossvm/camkes-vm-crossvm.md | 4 +- tutorials/camkes-vm-linux/camkes-vm-linux.md | 12 +-- tutorials/capabilities/capabilities.md | 4 +- tutorials/fault-handlers/fault-handlers.md | 18 ++--- tutorials/hello-camkes-0/hello-camkes-0.md | 11 +-- tutorials/hello-camkes-1/hello-camkes-1.md | 20 ++--- tutorials/hello-camkes-2/hello-camkes-2.md | 73 ++++++++++--------- .../hello-camkes-timer/hello-camkes-timer.md | 22 +++--- tutorials/hello-world/hello-world.md | 4 +- tutorials/interrupts/interrupts.md | 22 +++--- tutorials/ipc/ipc.md | 16 ++-- tutorials/libraries-1/libraries-1.md | 4 +- tutorials/libraries-2/libraries-2.md | 4 +- tutorials/libraries-3/libraries-3.md | 6 +- tutorials/libraries-4/libraries-4.md | 4 +- tutorials/mapping/mapping.md | 10 +-- tutorials/mcs/mcs.md | 20 ++--- tutorials/notifications/notifications.md | 12 +-- tutorials/threads/threads.md | 18 ++--- tutorials/untyped/untyped.md | 6 +- 20 files changed, 147 insertions(+), 143 deletions(-) diff --git a/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md b/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md index 02c4d496..62cbcf3d 100644 --- a/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md +++ b/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md @@ -18,8 +18,8 @@ In this tutorial you will learn how to: * Configure processes in a Linux guest VM to communicate with CAmkES components ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [CAmkES VM Linux tutorial](https://docs.sel4.systems/Tutorials/camkes-vm-linux) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [CAmkES VM Linux tutorial](https://docs.sel4.systems/Tutorials/camkes-vm-linux.html) *Note that the instructions for this tutorial are only for Linux.* diff --git a/tutorials/camkes-vm-linux/camkes-vm-linux.md b/tutorials/camkes-vm-linux/camkes-vm-linux.md index d776f6bd..6b456514 100644 --- a/tutorials/camkes-vm-linux/camkes-vm-linux.md +++ b/tutorials/camkes-vm-linux/camkes-vm-linux.md @@ -18,8 +18,8 @@ You will become familiar with: *Note that the instructions for this tutorial are only for Linux.* ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [CAmkES timer tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-timer) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [CAmkES timer tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-timer.html) ## CapDL Loader @@ -30,13 +30,13 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +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/CapDL.html). +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. @@ -151,7 +151,7 @@ The values of `vm0.kernel_cmdline`, `vm0.kernel_image` and `vm0.initrd_image` ar strings specifying: - boot arguments to the guest Linux, - the name of the guest Linux kernel image file, - - and the name of the guest Linux initrd file (the root filesystem to use during system initialization). + - and the name of the guest Linux initrd file (the root filesystem to use during system initialisation). The kernel command-line is defined in the `VM_GUEST_CMDLINE` macro. The kernel image and rootfs names are defined in the applications `CMakeLists.txt` file. @@ -160,7 +160,7 @@ linked into the VMM. In the simple configuration for thie tutorial, the VMM uses the `bzimage` and `rootfs.cpio` names to find the appropriate files in this archive. -To see how the `Init` component and CPIO archive are definied within the build system, +To see how the `Init` component and CPIO archive are defined within the build system, look at the app's `CMakeList.txt`: ```cmake diff --git a/tutorials/capabilities/capabilities.md b/tutorials/capabilities/capabilities.md index 93afbf60..3549af70 100644 --- a/tutorials/capabilities/capabilities.md +++ b/tutorials/capabilities/capabilities.md @@ -15,8 +15,8 @@ You will learn: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Hello world](https://docs.sel4.systems/Tutorials/hello-world) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Hello world](https://docs.sel4.systems/Tutorials/hello-world.html) ## Initialising diff --git a/tutorials/fault-handlers/fault-handlers.md b/tutorials/fault-handlers/fault-handlers.md index b3fb0811..6b6396c1 100644 --- a/tutorials/fault-handlers/fault-handlers.md +++ b/tutorials/fault-handlers/fault-handlers.md @@ -22,9 +22,9 @@ You will learn: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities) -3. [IPC tutorial](https://docs.sel4.systems/Tutorials/ipc) +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) ## Initialising @@ -48,13 +48,13 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +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/CapDL.html). +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. @@ -65,7 +65,7 @@ A fault handler is a separate instruction stream which the CPU can jump to in order to rectify an anomalous condition in the current thread and then return to the previous instruction stream. -In seL4, faults are modeled as separately programmer-designated "fault handler" +In seL4, faults are modelled as separately programmer-designated "fault handler" threads. In monolithic kernels, faults are not usually delivered to a userspace handler, but they are handled by the monolithic kernel itself. @@ -131,7 +131,7 @@ In addition, the following fault types are added by the MCS kernel: When a fault is generated, the kernel will deliver an IPC message across the fault endpoint. This IPC message contains information that tells the fault -handler why the fault occured as well as surrounding contextual information +handler why the fault occurred as well as surrounding contextual information 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 @@ -161,11 +161,11 @@ When the kernel sends a fault IPC message using a badged endpoint cap, the badge 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 realized that this means that a badge on the +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) for a refresher on how +[IPC Tutorial](https://docs.sel4.systems/Tutorials/ipc.html) for a refresher on how badged fault endpoints work. ### Differences between MCS and Master kernel diff --git a/tutorials/hello-camkes-0/hello-camkes-0.md b/tutorials/hello-camkes-0/hello-camkes-0.md index a164b925..88693b82 100644 --- a/tutorials/hello-camkes-0/hello-camkes-0.md +++ b/tutorials/hello-camkes-0/hello-camkes-0.md @@ -12,16 +12,17 @@ This tutorial is an introduction to CAmkES. This will involve introducing the CA static CAmkES application and describing its components. Outcomes: + 1. Understand the structure of a CAmkES application, as a described, well-defined, static system. 2. Understand the file-layout of a CAmkES ADL project. 3. Become acquainted with the basics of creating a practical CAmkES application. -Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master/docs/CAmkESTutorial.pdf) to guide you through the tutorials [0](https://docs.sel4.systems/Tutorials/hello-camkes-0), [1](https://docs.sel4.systems/Tutorials/hello-camkes-1) and [2](https://docs.sel4.systems/Tutorials/hello-camkes-2). +Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master/docs/CAmkESTutorial.pdf) to guide you through the tutorials [0](https://docs.sel4.systems/Tutorials/hello-camkes-0.html), [1](https://docs.sel4.systems/Tutorials/hello-camkes-1.html) and [2](https://docs.sel4.systems/Tutorials/hello-camkes-2.html). ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up). -2. [Hello world tutorial](https://docs.sel4.systems/Tutorials/hello-world) -3. Familiarise yourself with the [CAmkES manual](https://github.com/seL4/camkes-tool/blob/master/docs/index.md). +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html). +2. [Hello world tutorial](https://docs.sel4.systems/Tutorials/hello-world.html) +3. Familiarise yourself with the [CAmkES manual](https://docs.sel4.systems/projects/camkes/manual.html). Note that it's possible to successfully complete the CAmkES tutorial without having read the manual, however highly recommended. @@ -34,7 +35,7 @@ interfaces which must be statically defined, over communication channels. ### Component As briefly described above, we identify a component as a functional grouping of code and resources. We -use the term component in CAmkES to refer to the *type* of our functional grouping (see the Component section in the [manual](https://github.com/seL4/camkes-tool/blob/master/docs/index.md#component)). +use the term component in CAmkES to refer to the *type* of our functional grouping (see the Component section in the [manual](https://docs.sel4.systems/projects/camkes/manual.html#component)). An example of this in concrete CAmkES syntax can be seen below: ```c diff --git a/tutorials/hello-camkes-1/hello-camkes-1.md b/tutorials/hello-camkes-1/hello-camkes-1.md index 4ba3ef8c..c41ac1e7 100644 --- a/tutorials/hello-camkes-1/hello-camkes-1.md +++ b/tutorials/hello-camkes-1/hello-camkes-1.md @@ -17,11 +17,11 @@ well-defined, static system. 2. Understand the file-layout of a CAmkES ADL project. 3. Become acquainted with the basics of creating a practical CAmkES application. -Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master/docs/CAmkESTutorial.pdf) to guide you through the tutorials [0](https://docs.sel4.systems/Tutorials/hello-camkes-0), [1](https://docs.sel4.systems/Tutorials/hello-camkes-1) and [2](https://docs.sel4.systems/Tutorials/hello-camkes-2). +Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master/docs/CAmkESTutorial.pdf) to guide you through the tutorials [0](https://docs.sel4.systems/Tutorials/hello-camkes-0.html), [1](https://docs.sel4.systems/Tutorials/hello-camkes-1.html) and [2](https://docs.sel4.systems/Tutorials/hello-camkes-2.html). ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [CAmkES hello world tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-0) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [CAmkES hello world tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-0.html) ## Initialising @@ -54,7 +54,7 @@ the following camkes file: - `hello-camkes-1/hello-1.camkes` Find the Component manual section here: - + ### Connections @@ -67,7 +67,7 @@ we are using synchronous IPC. In implementation terms, this boils down to the `seL4_Call` syscall on seL4. Find the "Connection" keyword manual section here: - + ### Interfaces @@ -94,7 +94,7 @@ Procedure interface may be found here: `hello-camkes-1/interfaces/HelloSimple.idl4` Find the "Procedure" keyword definition here: - + ### Component source @@ -174,7 +174,7 @@ assembly { /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="connect") -*/ /* hint 1: use seL4RPCCall as the connector (or you could use seL4RPC if you prefer) * hint 2: look at - * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application + * https://docs.sel4.systems/projects/camkes/manual.html#creating-an-application */ /*-- endfilter -*/ ``` @@ -199,7 +199,7 @@ procedure HelloSimple { /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="interface") -*/ /* TODO define RPC functions */ /* hint 1: define at least one function that takes a string as input parameter. call it say_hello. no return value - * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application + * hint 2: look at https://docs.sel4.systems/projects/camkes/manual.html#creating-an-application */ /*-- endfilter -*/ ``` @@ -227,7 +227,7 @@ procedure HelloSimple { * hint 4: so the function would be: hello_say_hello() * hint 5: the CAmkES 'string' type maps to 'const char *' in C * hint 6: make the function print out a mesage using printf - * hint 7: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application + * hint 7: look at https://docs.sel4.systems/projects/camkes/manual.html#creating-an-application */ /*-- endfilter -*/ ``` @@ -258,7 +258,7 @@ void hello_say_hello(const char *str) { * hint 2: the interfaces available are defined by the component, e.g. in hello-1.camkes * hint 3: the function name is defined by the interface definition, e.g. in interfaces/HelloSimple.idl4 * hint 4: so the function would be: hello_say_hello() - * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application + * hint 5: look at https://docs.sel4.systems/projects/camkes/manual.html#creating-an-application */ /*-- endfilter -*/ ``` diff --git a/tutorials/hello-camkes-2/hello-camkes-2.md b/tutorials/hello-camkes-2/hello-camkes-2.md index 4aa12607..9bf0ce1e 100644 --- a/tutorials/hello-camkes-2/hello-camkes-2.md +++ b/tutorials/hello-camkes-2/hello-camkes-2.md @@ -7,18 +7,20 @@ /*? declare_task_ordering(['hello']) ?*/ # Events in CAmkES + This tutorial shows how to build events in CAmkES. Learn how to: + - Represent and implement events in CAmkES. - Use Dataports. -Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master/docs/CAmkESTutorial.pdf) to guide you through the tutorials [0](https://docs.sel4.systems/Tutorials/hello-camkes-0), [1](https://docs.sel4.systems/Tutorials/hello-camkes-1) and [2](https://docs.sel4.systems/Tutorials/hello-camkes-2). +Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master/docs/CAmkESTutorial.pdf) to guide you through the tutorials [0](https://docs.sel4.systems/Tutorials/hello-camkes-0.html), [1](https://docs.sel4.systems/Tutorials/hello-camkes-1.html) and [2](https://docs.sel4.systems/Tutorials/hello-camkes-2.html). ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Introduction to CAmkES tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-1) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Introduction to CAmkES tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-1.html) ## CapDL Loader @@ -27,16 +29,17 @@ This tutorial uses the *capDL loader*, a root task which allocates statically
Get CapDL -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/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/CapDL.html). -
+ +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.
@@ -46,7 +49,7 @@ For this tutorial clone the [CapDL repo](https://github.com/sel4/capdl). This ca
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("hello-camkes-2") ?*/ @@ -54,14 +57,14 @@ All tutorials come with complete solutions. To get solutions run:
- ### Specify an events interface + Here you're declaring the events that will be bounced back and forth in this tutorial. An event is a signal is sent over a Notification connection. You are strongly advised to read the manual section on Events here: -. +. ''Ensure that when declaring the consumes and emits keywords between the Client.camkes and Echo.camkes files, you match them up so that @@ -75,7 +78,7 @@ You are strongly advised to read the manual section on Events here: /* TASK 1: the event interfaces */ /* hint 1: specify 2 interfaces: one "emits" and one "consumes" * hint 2: you can use an arbitrary string as the interface type (it doesn't get used) - * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events + * hint 3: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-events */ /*-- endfilter -*/ ``` @@ -98,7 +101,7 @@ You are strongly advised to read the manual section on Events here: /* TASK 3: the event interfaces */ /* hint 1: specify 2 interfaces: one "emits" and one "consumes" * hint 2: you can use an arbitrary string as the interface type (it doesn't get used) - * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events + * hint 3: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-events */ /*-- endfilter -*/ ``` @@ -122,7 +125,7 @@ You are strongly advised to read the manual section on Events here: /* TASK 5: Event connections */ /* hint 1: connect each "emits" interface in a component to the "consumes" interface in the other * hint 2: use seL4Notification as the connector - * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events + * hint 3: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-events */ /*-- endfilter -*/ ``` @@ -152,7 +155,7 @@ application to transparently interact with these events. /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="signal-task10") -*/ /* TASK 10: emit event to signal that the data is available */ /* hint 1: use the function _emit - * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events + * hint 2: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-events */ /*-- endfilter -*/ ``` @@ -173,7 +176,7 @@ application to transparently interact with these events. /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="wait-task11") -*/ /* TASK 11: wait to get an event back signalling that the reply data is available */ /* hint 1: use the function _wait - * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events + * hint 2: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-events */ /*-- endfilter -*/ ``` @@ -233,7 +236,7 @@ application to transparently interact with these events. /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="notify-task22") -*/ /* TASK 22: notify the client that there is new data available for it */ /* hint 1: use the function _emit - * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events + * hint 2: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-events */ /*-- endfilter -*/ ``` @@ -255,7 +258,7 @@ application to transparently interact with these events. /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="notify-task25") -*/ /* TASK 25: notify the client that we are done reading the data */ /* hint 1: use the function _emit - * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events + * hint 2: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-events */ /*-- endfilter -*/ ``` @@ -285,7 +288,7 @@ instance. These steps help you to become familiar with this approach. /* hint 1: use the function _reg_callback() * hint 2: register the function "callback_handler_1" * hint 3: pass NULL as the extra argument to the callback - * hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events + * hint 4: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-events */ /*-- endfilter -*/ ``` @@ -310,7 +313,7 @@ instance. These steps help you to become familiar with this approach. /* hint 1: use the function _reg_callback() * hint 2: register the function "callback_handler_2" * hint 3: pass NULL as the extra argument to the callback - * hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events + * hint 4: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-events */ /*-- endfilter -*/ ``` @@ -334,7 +337,7 @@ instance. These steps help you to become familiar with this approach. /* hint 1: use the function _reg_callback() * hint 2: register the function "callback_handler_1" * hint 3: pass NULL as the extra argument to the callback - * hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events + * hint 4: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-events */ /*-- endfilter -*/ ``` @@ -375,7 +378,7 @@ in the shared mem communication. We will then link them together using a /* TASK 2: the dataport interfaces */ /* hint 1: specify 3 interfaces: one of type "Buf", one of type "str_buf_t" and one of type "ptr_buf_t" * hint 2: for the definition of these types see "str_buf.h". - * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports + * hint 3: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-dataports */ /*-- endfilter -*/ ``` @@ -399,7 +402,7 @@ in the shared mem communication. We will then link them together using a /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="dataport-task4") -*/ /* TASK 4: the dataport interfaces */ /* hint 1: specify 3 interfaces: one of type "Buf", one of type "str_buf_t" and one of type "ptr_buf_t" - * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports + * hint 3: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-dataports */ /*-- endfilter -*/ ``` @@ -430,7 +433,7 @@ proceed. /* TASK 6: Dataport connections */ /* hint 1: connect the corresponding dataport interfaces of the components to each other * hint 2: use seL4SharedData as the connector - * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports + * hint 3: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-dataports */ /*-- endfilter -*/ ``` @@ -462,7 +465,7 @@ to access and manipulate the data in the shared memory mapping * For example if you defined it as "dataport Buf d" then you would use "d" to refer to the dataport in C. * hint 3: first write the number of strings (NUM_STRINGS) to the dataport * hint 4: then copy all the strings from "s_arr" to the dataport. - * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports + * hint 5: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-dataports */ /*-- endfilter -*/ ``` @@ -494,7 +497,7 @@ to access and manipulate the data in the shared memory mapping * hint 3: for the definition of "str_buf_t" see "str_buf.h". * hint 4: use the "n" field to determine the number of strings in the dataport * hint 5: print out the specified number of strings from the "str" field - * hint 6: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports + * hint 6: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-dataports */ /*-- endfilter -*/ ``` @@ -528,7 +531,7 @@ to access and manipulate the data in the shared memory mapping * hint 6: use the "ptr" field of the typed dataport to store the dataport pointers * hint 7: use the function "dataport_wrap_ptr()" to create a dataport pointer from a regular pointer * hint 8: the dataport pointers should point into the untyped dataport - * hint 9: for more information about dataport pointers see: https://github.com/seL4/camkes-tool/blob/master/docs/index.md + * hint 9: for more information about dataport pointers see: https://docs.sel4.systems/projects/camkes/manual.html */ /*-- endfilter -*/ ``` @@ -567,7 +570,7 @@ code to access and manipulate the data in the shared memory mapping * For example if you defined it as "dataport Buf d" then you would use "d" to refer to the dataport in C. * hint 3: first read the number of strings from the dataport * hint 4: then print each string from the dataport - * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports + * hint 5: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-dataports */ /*-- endfilter -*/ ``` @@ -601,7 +604,7 @@ code to access and manipulate the data in the shared memory mapping * hint 5: for the definition of "str_buf_t" see "str_buf.h" * hint 6: use the "n" field to specify the number of strings in the dataport * hint 7: copy the specified number of strings from the "Buf" dataport to the "str" field - * hint 8: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports + * hint 8: look at https://docs.sel4.systems/projects/camkes/manual.html#an-example-of-dataports * hint 9: you could combine this TASK with the previous one in a single loop if you want */ /*-- endfilter -*/ @@ -639,7 +642,7 @@ code to access and manipulate the data in the shared memory mapping * hint 4: the "n" field of the typed dataport specifies the number of dataport pointers * hint 5: the "ptr" field of the typed dataport contains the dataport pointers * hint 6: use the function "dataport_unwrap_ptr()" to create a regular pointer from a dataport pointer - * hint 7: for more information about dataport pointers see: https://github.com/seL4/camkes-tool/blob/master/docs/index.md + * hint 7: for more information about dataport pointers see: https://docs.sel4.systems/projects/camkes/manual.html * hint 8: print out the string pointed to by each dataport pointer */ /*-- endfilter -*/ diff --git a/tutorials/hello-camkes-timer/hello-camkes-timer.md b/tutorials/hello-camkes-timer/hello-camkes-timer.md index 8167a11b..f9619e4a 100644 --- a/tutorials/hello-camkes-timer/hello-camkes-timer.md +++ b/tutorials/hello-camkes-timer/hello-camkes-timer.md @@ -28,8 +28,8 @@ commented out. ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/HostDependencies). -2. [CAmkES 2](https://docs.sel4.systems/Tutorials/hello-camkes-2) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html). +2. [CAmkES 2](https://docs.sel4.systems/Tutorials/hello-camkes-2.html) ## CapDL Loader @@ -40,13 +40,13 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +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/CapDL.html). +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. @@ -94,7 +94,7 @@ wish to call your driver something else, you'll have to change these lines. /* Part 1, TASK 1: component instances */ /* hint 1: one hardware component and one driver component * hint 2: look at - * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application + * https://docs.sel4.systems/projects/camkes/manual.html#creating-an-application */ /*-- endfilter -*/ ``` @@ -124,7 +124,7 @@ registers. The other represents an interrupt. /* hint 1: use seL4HardwareMMIO to connect device memory * hint 2: use seL4HardwareInterrupt to connect interrupt * hint 3: look at - * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application + * https://docs.sel4.systems/projects/camkes/manual.html#creating-an-application */ /*-- endfilter -*/ ``` @@ -153,7 +153,7 @@ must both be configured. /* Timer and Timerbase: * hint 1: find out the device memory address and IRQ number from the hardware data sheet * hint 2: look at - * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#hardware-components + * https://docs.sel4.systems/projects/camkes/manual.html#hardware-components */ /*-- endfilter -*/ ``` @@ -331,7 +331,7 @@ need to implement is called `hello_sleep`. * hint 4: so the function would be: hello_sleep() * hint 5: the camkes 'int' type maps to 'int' in c * hint 6: invoke a function in supplied driver the to set up the timer - * hint 7: look at https://github.com/sel4/camkes-tool/blob/master/docs/index.md#creating-an-application + * hint 7: look at https://docs.sel4.systems/projects/camkes/manual.html#creating-an-application */ /*-- endfilter -*/ ``` @@ -413,7 +413,7 @@ lines if necessary. /* Part 2, TASK 1: component instances */ /* hint 1: a single TimerDTB component * hint 2: look at - * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application + * https://docs.sel4.systems/projects/camkes/manual.html#creating-an-application */ /*-- endfilter -*/ ``` @@ -441,7 +441,7 @@ connector. /* hint 1: connect the dummy_source and timer interfaces * hint 2: the dummy_source should be the 'from' end * hint 3: look at - * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application + * https://docs.sel4.systems/projects/camkes/manual.html#creating-an-application */ /*-- endfilter -*/ ``` @@ -773,7 +773,7 @@ void hello__init() { * hint 4: so the function would be: hello_sleep() * hint 5: the camkes 'int' type maps to 'int' in c * hint 6: invoke a function in the supplied driver to set a timeout - * hint 7: look at https://github.com/sel4/camkes-tool/blob/master/docs/index.md#creating-an-application + * hint 7: look at https://docs.sel4.systems/projects/camkes/manual.html#creating-an-application */ void hello_sleep(int sec) { int error = 0; diff --git a/tutorials/hello-world/hello-world.md b/tutorials/hello-world/hello-world.md index 15a9b49d..82506908 100644 --- a/tutorials/hello-world/hello-world.md +++ b/tutorials/hello-world/hello-world.md @@ -15,7 +15,7 @@ In this tutorial you will: 4. Have a basic understanding of the role of the `CMakeLists.txt` file in applications ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) ## Building your first program seL4 is a microkernel, not an operating system, and as a result only provides very minimal services. @@ -28,7 +28,7 @@ The tutorial is already set up to print "Hello, world!", so at this point all y ## Revisiting containers -We will use two terminals, as described in [Setting up your machine](https://docs.sel4.systems/Tutorials/setting-up#mapping-a-container). +We will use two terminals, as described in [Setting up your machine](https://docs.sel4.systems/Tutorials/setting-up.html#mapping-a-container). - Terminal A is just a normal terminal, and is used for git operations, editing (e.g., vim, emacs), and other normal operations. - Terminal B is running in a container, and is only used for compilation. diff --git a/tutorials/interrupts/interrupts.md b/tutorials/interrupts/interrupts.md index 22335874..6f34f8d0 100644 --- a/tutorials/interrupts/interrupts.md +++ b/tutorials/interrupts/interrupts.md @@ -16,8 +16,8 @@ You will learn: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Notifications tutorial](https://docs.sel4.systems/Tutorials/notifications) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Notifications tutorial](https://docs.sel4.systems/Tutorials/notifications.html) # Initialising @@ -42,13 +42,13 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +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/CapDL.html). +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. @@ -77,9 +77,9 @@ error = seL4_IRQControl_Get(seL4_IRQControl, 7, cspace_root, 10, seL4_WordBits); There are a variety of different invocations to obtain irq capabilities which are hardware dependent, including: -* [`seL4_IRQControl_GetIOAPIC`](https://docs.sel4.systems/ApiDoc.html#get-io-apic) (x86) -* [`seL4_IRQControl_GetMSI`](https://docs.sel4.systems/ApiDoc.html#get-msi) (x86) -* [`seL4_IRQControl_GetTrigger`](https://docs.sel4.systems/ApiDoc.html#gettrigger) (ARM) +* [`seL4_IRQControl_GetIOAPIC`](https://docs.sel4.systems/projects/sel4/api-doc.html#get-io-apic-handler) (x86) +* [`seL4_IRQControl_GetMSI`](https://docs.sel4.systems/projects/sel4/api-doc.html#get-msi-handler) (x86) +* [`seL4_IRQControl_GetTrigger`](https://docs.sel4.systems/projects/sel4/api-doc.html#get-irq-handler-with-trigger-type) (ARM) ### Receiving interrupts @@ -93,22 +93,22 @@ On success, this call will result in signals being delivered to the notification an interrupt occurs. To handle multiple interrupts on the same notification object, you can set different badges on the notification capabilities bound to each IRQHandler. When an interrupt arrives, -the badge of the notification object bound to that IRQHandler is bitwise orred with the data +the badge of the notification object bound to that IRQHandler is bitwise or-ed with the data word in the notification object. Recall the badging technique for differentiating signals from the - [notification tutorial](https://docs.sel4.systems/Tutorials/notifications). + [notification tutorial](https://docs.sel4.systems/Tutorials/notifications.html). Interrupts can be polled for using `seL4_Poll` or waited for using `seL4_Wait`. Either system call results in the data word of the notification object being delivered as the badge of the message, and the data word cleared. -[`seL4_IRQHandler_Clear`](https://docs.sel4.systems/ApiDoc.html#clear) can be used to unbind +[`seL4_IRQHandler_Clear`](https://docs.sel4.systems/projects/sel4/api-doc.html#clear) can be used to unbind the notification from an IRQHandler. ### Handling interrupts Once an interrupt is received and processed by the software, you can unmask the interrupt -using [`seL4_IRQHandler_Ack`](https://docs.sel4.systems/ApiDoc.html#ack) on the IRQHandler. +using [`seL4_IRQHandler_Ack`](https://docs.sel4.systems/projects/sel4/api-doc.html#acknowledge) on the IRQHandler. seL4 will not deliver any further interrupts after an IRQ is raised until that IRQHandler has been acked. diff --git a/tutorials/ipc/ipc.md b/tutorials/ipc/ipc.md index 1ce6b724..a2c4ae97 100644 --- a/tutorials/ipc/ipc.md +++ b/tutorials/ipc/ipc.md @@ -17,8 +17,8 @@ You will learn: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities.html) ## Initialising @@ -43,13 +43,13 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +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/CapDL.html). +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. @@ -85,7 +85,7 @@ does the same, except it sends the reply and blocks on the provided endpoint in Since TCBs have a single space to store a reply capability, if servers need to service multiple requests (e.g saving requests to reply at a later time, after hardware operations have been completed), -[`seL4_CNode_SaveCaller`](https://docs.sel4.systems/ApiDoc.html#save-caller) can be used to save +[`seL4_CNode_SaveCaller`](https://docs.sel4.systems/projects/sel4/api-doc.html#save-caller) can be used to save the reply capability to an empty slot in the receivers CSpace. ### IPC Buffer @@ -154,8 +154,8 @@ It contains the following fields: Along with the message the kernel additionally delivers the badge of the endpoint capability that the sender invoked to send the message. Endpoints can be badged using -[`seL4_CNode_Mint`](https://docs.sel4.systems/ApiDoc.html#mint) or - [`seL4_CNode_Mutate`](https://docs.sel4.systems/ApiDoc.html#mutate). Once an endpoint is badged, +[`seL4_CNode_Mint`](https://docs.sel4.systems/projects/sel4/api-doc.html#mint) or + [`seL4_CNode_Mutate`](https://docs.sel4.systems/projects/sel4/api-doc.html#mutate). Once an endpoint is badged, the badge of the endpoint is transferred to any receiver that receives messages on that endpoint. The code example below demonstrates this: @@ -356,7 +356,7 @@ lazy **Exercise** Currently each client is scheduled for its full timeslice until it is preempted. Alter your server to only print one message from each client, alternating. You will need to use -[`seL4_CNode_SaveCaller`](https://docs.sel4.systems/ApiDoc.html#save-caller) to save the reply +[`seL4_CNode_SaveCaller`](https://docs.sel4.systems/projects/sel4/api-doc.html#save-caller) to save the reply capability for each sender. You can use `free_slot` to store the reply capabilities. diff --git a/tutorials/libraries-1/libraries-1.md b/tutorials/libraries-1/libraries-1.md index bfda9368..e19b6193 100644 --- a/tutorials/libraries-1/libraries-1.md +++ b/tutorials/libraries-1/libraries-1.md @@ -54,8 +54,8 @@ Outcomes: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Hello world tutorial](https://docs.sel4.systems/Tutorials/hello-world) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Hello world tutorial](https://docs.sel4.systems/Tutorials/hello-world.html) ## Initialising diff --git a/tutorials/libraries-2/libraries-2.md b/tutorials/libraries-2/libraries-2.md index f2691de9..2ec43a1e 100644 --- a/tutorials/libraries-2/libraries-2.md +++ b/tutorials/libraries-2/libraries-2.md @@ -62,8 +62,8 @@ Learning outcomes: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Libraries: initialisation & threading](https://docs.sel4.systems/Tutorials/libraries-1) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Libraries: initialisation & threading](https://docs.sel4.systems/Tutorials/libraries-1.html) ## Initialising diff --git a/tutorials/libraries-3/libraries-3.md b/tutorials/libraries-3/libraries-3.md index b3102a76..4c4e58bb 100644 --- a/tutorials/libraries-3/libraries-3.md +++ b/tutorials/libraries-3/libraries-3.md @@ -38,7 +38,7 @@ Learning outcomes: different CSpaces. This is an automatic side effect of the way that sel4utils creates new "processes". - Learn how the init thread in an seL4 system performs some types - of initialization that aren't traditionally left to userspace. + of initialisation that aren't traditionally left to userspace. - Observe and understand the effects of creating thread that do not share the same CSpace. - Understand IPC across CSpace boundaries. @@ -47,8 +47,8 @@ Learning outcomes: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Libraries: IPC](https://docs.sel4.systems/Tutorials/libraries-2) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Libraries: IPC](https://docs.sel4.systems/Tutorials/libraries-2.html) ## Initialising diff --git a/tutorials/libraries-4/libraries-4.md b/tutorials/libraries-4/libraries-4.md index 3ac0ce21..2d340433 100644 --- a/tutorials/libraries-4/libraries-4.md +++ b/tutorials/libraries-4/libraries-4.md @@ -30,8 +30,8 @@ Learning outcomes: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Libraries: processes & elf loading](https://docs.sel4.systems/Tutorials/libraries-3) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Libraries: processes & elf loading](https://docs.sel4.systems/Tutorials/libraries-3.html) ## Initialising diff --git a/tutorials/mapping/mapping.md b/tutorials/mapping/mapping.md index 5ca70334..47c1daa7 100644 --- a/tutorials/mapping/mapping.md +++ b/tutorials/mapping/mapping.md @@ -12,8 +12,8 @@ This tutorial provides an introduction to virtual memory management on seL4. ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities.html) ## Initialising @@ -142,7 +142,7 @@ This is because while the provided code maps in a `seL4_PDPT` object, there are paging structures. The value corresponds to the `libsel4` constant `SEL4_MAPPING_LOOKUP_NO_PD` which is the number of bits in the virtual address that could not be resolved due to missing paging structures. -**Exercise** Map in the `pd` structure using (`seL4_PageDirectory_Map`)[https://docs.sel4.systems/ApiDoc.html#map-5]. +**Exercise** Map in the `pd` structure using (`seL4_PageDirectory_Map`)[https://docs.sel4.systems/projects/sel4/api-doc.html#map-5]. ```c /*-- filter TaskContent("mapping-start", TaskContentType.ALL, subtask='pd', completion='Failed to map page') -*/ @@ -173,7 +173,7 @@ main@main.c:34 [Cond failed: error != seL4_NoError] Note that in the above output, the number of failed bits has changed from `30` to `21`: this is because another 9 bits could be resolved from the newly mapped page directory. -**Exercise** Map in the `pt` structure using [`seL4_PageTable_Map`](https://docs.sel4.systems/ApiDoc.html#map-6). +**Exercise** Map in the `pt` structure using [`seL4_PageTable_Map`](https://docs.sel4.systems/projects/sel4/api-doc.html#map-6). ```c /*-- filter TaskContent("mapping-start", TaskContentType.ALL, subtask='pt') -*/ @@ -220,7 +220,7 @@ that the fault occured on (address). ### Remap a page **Exercise** Fix the fault by remapping the page with `seL4_ReadWrite` permissions, using the -[seL4_X86_Page_Map](https://docs.sel4.systems/ApiDoc.html#map-4) invocation. +[seL4_X86_Page_Map](https://docs.sel4.systems/projects/sel4/api-doc.html#map-4) invocation. ```c /*-- filter TaskContent("mapping-start", TaskContentType.ALL, subtask='remap') -*/ // TODO remap the page diff --git a/tutorials/mcs/mcs.md b/tutorials/mcs/mcs.md index 11308b12..5818ebce 100644 --- a/tutorials/mcs/mcs.md +++ b/tutorials/mcs/mcs.md @@ -21,16 +21,16 @@ Learn: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Hello world tutorial](https://docs.sel4.systems/Tutorials/hello-world) -3. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities) -4. [Untyped tutorial](https://docs.sel4.systems/Tutorials/untyped) -5. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping) -6. [Threads tutorial](https://docs.sel4.systems/Tutorials/threads) -7. [IPC tutorial](https://docs.sel4.systems/Tutorials/ipc) -8. [Notifications tutorial](https://docs.sel4.systems/Tutorials/notifications) -9. [Interrupts tutorial](https://docs.sel4.systems/Tutorials/interrupts) -10. [Fault handlers tutorial](https://docs.sel4.systems/Tutorials/fault-handlers) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Hello world tutorial](https://docs.sel4.systems/Tutorials/hello-world.html) +3. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities.html) +4. [Untyped tutorial](https://docs.sel4.systems/Tutorials/untyped.html) +5. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping.html) +6. [Threads tutorial](https://docs.sel4.systems/Tutorials/threads.html) +7. [IPC tutorial](https://docs.sel4.systems/Tutorials/ipc.html) +8. [Notifications tutorial](https://docs.sel4.systems/Tutorials/notifications.html) +9. [Interrupts tutorial](https://docs.sel4.systems/Tutorials/interrupts.html) +10. [Fault handlers tutorial](https://docs.sel4.systems/Tutorials/fault-handlers.html) ## Initialising diff --git a/tutorials/notifications/notifications.md b/tutorials/notifications/notifications.md index 1a00d6d6..b48c378d 100644 --- a/tutorials/notifications/notifications.md +++ b/tutorials/notifications/notifications.md @@ -16,10 +16,10 @@ You will learn how to: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities) -3. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping) -4. [Threads tutorial](https://docs.sel4.systems/Tutorials/threads) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities.html) +3. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping.html) +4. [Threads tutorial](https://docs.sel4.systems/Tutorials/threads.html) ## Initialising @@ -45,13 +45,13 @@ This tutorial uses the *capDL loader*, a root task which allocates statically Get CapDL 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/CAmkES/) projects +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/CapDL.html). +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. diff --git a/tutorials/threads/threads.md b/tutorials/threads/threads.md index 211463c8..4c846dbc 100644 --- a/tutorials/threads/threads.md +++ b/tutorials/threads/threads.md @@ -22,9 +22,9 @@ In this tutorial, you will: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities) -3. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities.html) +3. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping.html) ## CapDL Loader @@ -34,13 +34,13 @@ seL4 boot protocol. This tutorial uses the *capDL loader*, a root task which all 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/CAmkES/) projects +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/CapDL.html). +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. @@ -123,7 +123,7 @@ seL4_Error seL4_DomainSet_Set(seL4_DomainSet _service, seL4_Uint8 domain, seL4_T ### Thread Attributes -seL4 threads are configured by [invocations on the TCB object](https://docs.sel4.systems/ApiDoc.html#sel4_tcb). +seL4 threads are configured by [invocations on the TCB object](https://docs.sel4.systems/projects/sel4/api-doc.html#sel4_tcb). ## Exercises @@ -155,13 +155,13 @@ seL4 boot protocol. This tutorial uses a the *capDL loader*, a root task which a 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/CAmkES/) projects +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. -Information about CapDL projects can be found [here](https://docs.sel4.systems/CapDL.html). +Information about CapDL projects can be found [here](https://docs.sel4.systems/projects/capdl/). ### Configure a TCB @@ -183,7 +183,7 @@ Failed to retype thread: 2 `Dumping all tcbs!` and the following table is generated by a debug syscall called `seL4_DebugDumpScheduler()`. seL4 has a series of debug syscalls that are available in debug kernel builds. The available debug syscalls -can be found in [libsel4](https://docs.sel4.systems/ApiDoc.html#debugging-system-calls). `seL4_DebugDumpScheduler()` +can be found in [libsel4](https://docs.sel4.systems/projects/sel4/api-doc.html#debugging-system-calls). `seL4_DebugDumpScheduler()` is used to dump the current state of the scheduler and can be useful to debug situations where a system seems to have hung. diff --git a/tutorials/untyped/untyped.md b/tutorials/untyped/untyped.md index efdf34af..e8f00aba 100644 --- a/tutorials/untyped/untyped.md +++ b/tutorials/untyped/untyped.md @@ -17,8 +17,8 @@ It covers: ## Prerequisites -1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up) -2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities) +1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html) +2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities.html) ## Initialising @@ -81,7 +81,7 @@ shows how to print out the initial untyped capabilities provided from `seL4_Boot ### Retyping Untyped capabilities have a single invocation: -[seL4_Untyped_Retype](https://docs.sel4.systems/ApiDoc.html#retype) which is +[seL4_Untyped_Retype](https://docs.sel4.systems/projects/sel4/api-doc.html#retype) which is used to create a new capability (and potentially object) from an untyped capability. Specifically, the new capability created by a retype invocation provides access to a subset of the memory range of the original capability, From 45fbb4b0cfe302a56fd439bf000d0d62cd96141e Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 11 Jul 2025 19:57:28 +1000 Subject: [PATCH 4/4] template.py: remove URL replacement This is already done by Jekyll, no need to process twice. Signed-off-by: Gerwin Klein --- template.py | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/template.py b/template.py index ee8aa8ef..c4460973 100755 --- a/template.py +++ b/template.py @@ -81,18 +81,6 @@ def render_file(args, env, state, file): input = in_stream.read() template = env.from_string(input) - if (args.__getattribute__("docsite")): - s = StringIO(input) - lines = input.split('\n') - - i = 0 - for line in s: - lines[i] = line.replace("https://docs.sel4.systems/Tutorials/", "/Tutorials/") - i = i + 1 - - new_text = ''.join(lines) - template = env.from_string(str(new_text)) - out_stream.write(template.render(context.get_context(args, state)))