From e8737bd21bb6029d7b283a76b33ccc542e0618f3 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 14 Jul 2025 18:36:18 +1000 Subject: [PATCH] Markdown lints and spelling - CapDL -> capDL - add language for code blocks for syntax highlighting - fix lints: - empty line before/after headings - empty line before/after fenced code blocks - replace
by empty line - remove duplicated CAmkES tutorial endings Signed-off-by: Gerwin Klein --- .../camkes-vm-crossvm/camkes-vm-crossvm.md | 2 +- tutorials/camkes-vm-linux/camkes-vm-linux.md | 14 +- tutorials/capabilities/capabilities.md | 2 +- tutorials/fault-handlers/fault-handlers.md | 16 +- tutorials/hello-camkes-1/hello-camkes-1.md | 128 ++++++++------- tutorials/hello-camkes-2/hello-camkes-2.md | 147 +++++++++++------- .../hello-camkes-timer/hello-camkes-timer.md | 108 ++++++++----- tutorials/hello-world/hello-world.md | 2 +- tutorials/interrupts/interrupts.md | 37 +++-- tutorials/ipc/ipc.md | 10 +- tutorials/libraries-1/libraries-1.md | 70 +++++++-- tutorials/libraries-2/libraries-2.md | 84 ++++++---- tutorials/libraries-3/libraries-3.md | 43 +++-- tutorials/libraries-4/libraries-4.md | 2 +- tutorials/mapping/mapping.md | 2 +- tutorials/mcs/mcs.md | 2 +- tutorials/notifications/notifications.md | 10 +- tutorials/threads/threads.md | 12 +- tutorials/untyped/untyped.md | 2 +- 19 files changed, 424 insertions(+), 269 deletions(-) diff --git a/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md b/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md index 62cbcf3..94d71b5 100644 --- a/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md +++ b/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md @@ -29,7 +29,7 @@ In this tutorial you will learn how to:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("camkes-vm-crossvm") ?*/ diff --git a/tutorials/camkes-vm-linux/camkes-vm-linux.md b/tutorials/camkes-vm-linux/camkes-vm-linux.md index 6b45651..f4362d8 100644 --- a/tutorials/camkes-vm-linux/camkes-vm-linux.md +++ b/tutorials/camkes-vm-linux/camkes-vm-linux.md @@ -21,13 +21,13 @@ You will become familiar with: 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 +## capDL Loader This tutorial uses the *capDL loader*, a root task which allocates statically configured objects and capabilities.
-Get CapDL +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/projects/camkes/) projects @@ -35,10 +35,10 @@ 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. + +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 @@ -47,7 +47,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("camkes-vm-linux") ?*/ diff --git a/tutorials/capabilities/capabilities.md b/tutorials/capabilities/capabilities.md index 3549af7..370d765 100644 --- a/tutorials/capabilities/capabilities.md +++ b/tutorials/capabilities/capabilities.md @@ -24,7 +24,7 @@ You will learn:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("capabilities") ?*/ diff --git a/tutorials/fault-handlers/fault-handlers.md b/tutorials/fault-handlers/fault-handlers.md index 6b6396c..9eb07ac 100644 --- a/tutorials/fault-handlers/fault-handlers.md +++ b/tutorials/fault-handlers/fault-handlers.md @@ -32,20 +32,20 @@ You will learn:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("fault-handlers") ?*/
-## CapDL Loader +## capDL Loader This tutorial uses the *capDL loader*, a root task which allocates statically configured objects and capabilities.
-Get CapDL +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/projects/camkes/) projects @@ -53,10 +53,10 @@ 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. + +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.
## Background: What is a fault, and what is a fault handler? @@ -180,7 +180,7 @@ See the [MCS tutorial](https://docs.sel4.systems/Tutorials/mcs.html) for more in ## Exercises -This tutorial has one address space set up by the CapDL loader, containing two +This tutorial has one address space set up by the capDL loader, containing two threads which share the same CSpace. One of the threads is a fault handler while the other triggers a virtual memory fault. diff --git a/tutorials/hello-camkes-1/hello-camkes-1.md b/tutorials/hello-camkes-1/hello-camkes-1.md index c41ac1e..b130e60 100644 --- a/tutorials/hello-camkes-1/hello-camkes-1.md +++ b/tutorials/hello-camkes-1/hello-camkes-1.md @@ -5,21 +5,23 @@ --> # Introduction to CAmkES + /*? declare_task_ordering(['hello']) ?*/ -This tutorial is an introduction to -CAmkES: bootstrapping a basic static CAmkES application, describing its -components, and linking them together. +This tutorial is an introduction to CAmkES: bootstrapping a basic static CAmkES +application, describing its components, and linking them together. Outcomes: + 1. Understand the structure of a CAmkES application, as a described, -well-defined, static system. + 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.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.html) 2. [CAmkES hello world tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-0.html) @@ -29,7 +31,7 @@ Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("hello-camkes-1") ?*/ @@ -42,49 +44,47 @@ The fundamentals of CAmkES are the component, the interface and the connection. ### Components -*Components* are logical -groupings of code and resources. They communicate with other component -instances via well-defined interfaces which must be statically defined, -over communication channels. This tutorial will lead you through the -construction of a CAmkES application with two components: an Echo -server, and its Client that makes calls to it. These components are -defined when you initialise your build repository, found in -the following camkes file: +*Components* are logical groupings of code and resources. They communicate with +other component instances via well-defined interfaces which must be statically +defined, over communication channels. This tutorial will lead you through the +construction of a CAmkES application with two components: an Echo server, and +its Client that makes calls to it. These components are defined when you +initialise your build repository, found in the following camkes file: - `hello-camkes-1/hello-1.camkes` -Find the Component manual section here: - +See also the [Component +definition](https://docs.sel4.systems/projects/camkes/manual.html#component) in +the CAmkES manual. ### Connections - The second fundamental component of CAmkES applications -is the *Connection*: a connection is the representation of a method of -communication between two software components in CAmkES. The underlying -implementation may be shared memory, synchronous IPC, notifications or -some other implementation-provided means. In this particular tutorial, -we are using synchronous IPC. In implementation terms, this boils down -to the `seL4_Call` syscall on seL4. +The second fundamental component of CAmkES applications is the *Connection*: a +connection is the representation of a method of communication between two +software components in CAmkES. The underlying implementation may be shared +memory, synchronous IPC, notifications or some other implementation-provided +means. In this particular tutorial, 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: - +See also the [Connection +keyword](https://docs.sel4.systems/projects/camkes/manual.html#connection) in +the CAmkES manual. ### Interfaces - All communications over a CAmkES connection must be well -defined: static systems' communications should be able to be reasoned -about at build time. All the function calls which will be delivered over -a communication channel then, also are well defined, and logically -grouped so as to provide clear directional understanding of all -transmissions over a connection. Components are connected together in -CAmkES, yes -- but the interfaces that are exposed over each connection -for calling by other components, are also described. - -There are different -kinds of interfaces: --Dataports, --Procedural interfaces, --and Notifications. +All communications over a CAmkES connection must be well defined: static +systems' communications should be able to be reasoned about at build time. All +the function calls which will be delivered over a communication channel then, +also are well defined, and logically grouped so as to provide clear directional +understanding of all transmissions over a connection. Components are connected +together in CAmkES, yes --- but the interfaces that are exposed over each +connection for calling by other components, are also described. + +There are different kinds of interfaces: + +- Dataports, +- Procedural interfaces, +- and Notifications. This tutorial will lead you through the construction of a Procedural interface, which is an interface over which function calls are made @@ -93,16 +93,16 @@ kind of interface in CAmkES is `procedure`. The definition of this Procedure interface may be found here: `hello-camkes-1/interfaces/HelloSimple.idl4` -Find the "Procedure" keyword definition here: - +See also the [Procedure +keyword](https://docs.sel4.systems/projects/camkes/manual.html#procedure) in the +CAmkES manual. ### Component source - Based on the ADL, CAmkES generates boilerplate which -conforms to your system's architecture, and enables you to fill in the -spaces with your program's logic. The two generated files in this -tutorial application are, in accordance with the Components we have -defined: +Based on the ADL, CAmkES generates boilerplate which conforms to your system's +architecture, and enables you to fill in the spaces with your program's logic. +The two generated files in this tutorial application are, in accordance with the +Components we have defined: - `hello-camkes-1/components/Echo/src/echo.c` - `hello-camkes-1/components/Client/src/client.c` @@ -127,8 +127,8 @@ instances of functions in an Interface with the Interface-instance's name. In the dual-function NIC device's case, it might have a `provides serial` and a `provides nic`. When a caller wants to call for the NIC-send, it would call, -nic_send(), and when a caller wants to invoke the Serial-send, it would -call, "serial_send()". +`nic_send()`, and when a caller wants to invoke the Serial-send, it would +call, `serial_send()`. So if the `Hello` interface is provided once by `Echo` as `a`, you would call for the `a` instance of Echo's `Hello` by calling for `a_hello()`. @@ -143,7 +143,7 @@ the second one was named `a2`? Then in order to call on that second **Exercise** First modify `hello-1.camkes`. Define instances of `Echo` and `Client` in the `composition` section of the ADL. -``` +```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="define",completion="Booting all finished, dropped to user space") -*/ assembly { composition { @@ -155,7 +155,7 @@ assembly {
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="define") -*/ assembly { composition { @@ -164,6 +164,7 @@ assembly { component Echo echo; /*-- endfilter -*/ ``` +
### Add a connection @@ -187,6 +188,7 @@ assembly { connection seL4RPCCall hello_con(from client.hello, to echo.hello); /*-- endfilter -*/ ``` +
### Define an interface @@ -207,14 +209,16 @@ procedure HelloSimple {
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="interface") -*/ void say_hello(in string str); /*-- endfilter -*/ ``` +
-### Implement a RPC function +### Implement an RPC function + **Exercise** Implement the RPC hello function. ```c @@ -236,7 +240,7 @@ procedure HelloSimple {
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="rpc") -*/ /* Implement the RPC function. */ void hello_say_hello(const char *str) { @@ -244,9 +248,10 @@ void hello_say_hello(const char *str) { } /*-- endfilter -*/ ``` +
-### Invoke a RPC function +### Invoke an RPC function **Exercise** Invoke the RPC function in `components/Client/src/client.c`. @@ -266,22 +271,22 @@ void hello_say_hello(const char *str) {
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="hello") -*/ /* Invoke the RPC function */ char *shello = "hello world"; hello_say_hello(shello); /*-- endfilter -*/ ``` +
## Done -Now build and run the project, if it compiles: Congratulations! Be sure to read up on the keywords and -structure of ADL: it's key to understanding CAmkES. And well done on -writing your first CAmkES application. +Now build and run the project. If it compiles: Congratulations! /*-- filter ExcludeDocs() -*/ + ```c /*- filter File("components/Client/src/client.c") --*/ /* @@ -322,7 +327,7 @@ int run(void) { ``` -``` +```c /*- filter File("hello-1.camkes") --*/ /* * CAmkES tutorial part 1: components with RPC. @@ -355,7 +360,8 @@ component Echo { } /*-- endfilter -*/ ``` -``` + +```c /*- filter File("interfaces/HelloSimple.idl4") --*/ /* Simple RPC interface */ procedure HelloSimple { @@ -364,7 +370,8 @@ procedure HelloSimple { /*-- endfilter -*/ ``` -``` + +```c /*- filter TaskCompletion("hello", TaskContentType.ALL) --*/ Component echo saying: hello world /*-- endfilter -*/ @@ -395,4 +402,5 @@ GenerateCAmkESRootserver() /*? macros.cmake_check_script(state) ?*/ /*-- endfilter -*/ ``` + /*-- endfilter -*/ diff --git a/tutorials/hello-camkes-2/hello-camkes-2.md b/tutorials/hello-camkes-2/hello-camkes-2.md index 9bf0ce1..154bddc 100644 --- a/tutorials/hello-camkes-2/hello-camkes-2.md +++ b/tutorials/hello-camkes-2/hello-camkes-2.md @@ -22,13 +22,13 @@ Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master 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 +## capDL Loader This tutorial uses the *capDL loader*, a root task which allocates statically configured objects and capabilities.
-Get CapDL +Get capDL The capDL loader parses a static description of the system and the relevant ELF binaries. It is primarily used in @@ -38,9 +38,9 @@ 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/). +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. +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 @@ -73,7 +73,7 @@ You are strongly advised to read the manual section on Events here: #### Specify an events interface -``` +```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="event-task1") -*/ /* TASK 1: the event interfaces */ /* hint 1: specify 2 interfaces: one "emits" and one "consumes" @@ -86,7 +86,7 @@ You are strongly advised to read the manual section on Events here:
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="event-task1") -*/ /* TASK 1: the event interfaces */ emits TheEvent echo; @@ -96,7 +96,7 @@ You are strongly advised to read the manual section on Events here:
-``` +```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="event-task3") -*/ /* TASK 3: the event interfaces */ /* hint 1: specify 2 interfaces: one "emits" and one "consumes" @@ -109,7 +109,7 @@ You are strongly advised to read the manual section on Events here:
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="event-task3") -*/ /* TASK 3: the event interfaces */ consumes TheEvent echo; @@ -120,7 +120,7 @@ You are strongly advised to read the manual section on Events here: #### Add connections -``` +```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="event-task5") -*/ /* TASK 5: Event connections */ /* hint 1: connect each "emits" interface in a component to the "consumes" interface in the other @@ -129,29 +129,31 @@ You are strongly advised to read the manual section on Events here: */ /*-- endfilter -*/ ``` +
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="event-task5") -*/ /* TASK 5: Event connections */ connection seL4Notification echo_event(from client.echo, to echo.echo); connection seL4Notification client_event(from echo.client, to client.client); /*-- endfilter -*/ ``` +
### Data -Recall that CAmkES prefixes the name -of the interface instance to the function being called across that -interface? This is the same phenomenon, but for events; in the case of a -connection over which events are sent, there is no API, but rather -CAmkES will generate \_emit() and \_wait() functions to enable the + +Recall that CAmkES prefixes the name of the interface instance to the function +being called across that interface? This is the same phenomenon, but for events; +in the case of a connection over which events are sent, there is no API, but +rather CAmkES will generate \_emit() and \_wait() functions to enable the application to transparently interact with these events. #### Signal that the data is available -``` +```c /*-- 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 @@ -169,10 +171,12 @@ application to transparently interact with these events. echo_emit(); /*-- endfilter -*/ ``` +
#### Wait for data to become available -``` + +```c /*-- 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 @@ -180,6 +184,7 @@ application to transparently interact with these events. */ /*-- endfilter -*/ ``` +
Quick solution @@ -189,6 +194,7 @@ application to transparently interact with these events. client_wait(); /*-- endfilter -*/ ``` +
#### Signal that data is available @@ -209,6 +215,7 @@ application to transparently interact with these events. echo_emit(); /*-- endfilter -*/ ``` +
#### Wait for data to be read @@ -229,9 +236,11 @@ application to transparently interact with these events. client_wait(); /*-- endfilter -*/ ``` +
#### Signal that data is available + ```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="notify-task22") -*/ /* TASK 22: notify the client that there is new data available for it */ @@ -250,6 +259,7 @@ application to transparently interact with these events. client_emit(); /*-- endfilter -*/ ``` +
#### Signal that data has been read @@ -272,13 +282,15 @@ application to transparently interact with these events. client_emit(); /*-- endfilter -*/ ``` + ### Handle notifications -One way to handle notifications in CAmkES is to -use callbacks when they are raised. CAmkES generates functions that -handle the registration of callbacks for each notification interface -instance. These steps help you to become familiar with this approach. + +One way to handle notifications in CAmkES is to use callbacks when they are +raised. CAmkES generates functions that handle the registration of callbacks for +each notification interface instance. These steps help you to become familiar +with this approach. #### Register a callback handler @@ -303,6 +315,7 @@ instance. These steps help you to become familiar with this approach. ZF_LOGF_IF(error != 0, "Failed to register callback"); /*-- endfilter -*/ ``` + #### Register another callback handler @@ -317,6 +330,7 @@ instance. These steps help you to become familiar with this approach. */ /*-- endfilter -*/ ``` +
Quick solution @@ -327,6 +341,7 @@ instance. These steps help you to become familiar with this approach. ZF_LOGF_IF(error != 0, "Failed to register callback"); /*-- endfilter -*/ ``` +
#### Register a callback handler @@ -352,28 +367,30 @@ instance. These steps help you to become familiar with this approach. ZF_LOGF_IF(error != 0, "Failed to register callback"); /*-- endfilter -*/ ``` + ------------------------------------------------------------------------ ### Dataports -Dataports are typed shared memory mappings. In your -CAmkES ADL specification, you state what C data type you'll be using to -access the data in the shared memory -- so you can specify a C struct -type, etc. + +Dataports are typed shared memory mappings. In your CAmkES ADL specification, +you state what C data type you'll be using to access the data in the shared +memory -- so you can specify a C struct type, etc. The really neat part is more that CAmkES provides access control for -accessing these shared memory mappings: if a shared mem mapping is such +accessing these shared memory mappings: if a shared memory mapping is such that one party writes and the other reads and never writes, we can tell CAmkES about this access constraint in ADL. So in TASKs 2 and 4, you're first being led to create the "Dataport" interface instances on each of the components that will be participating -in the shared mem communication. We will then link them together using a +in the shared memory communication. We will then link them together using a "seL4SharedData" connector later on. #### Specify dataport interfaces -``` + +```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="dataport-task2") -*/ /* 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" @@ -386,7 +403,7 @@ in the shared mem communication. We will then link them together using a
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="dataport-task2") -*/ /* TASK 2: the dataport interfaces */ dataport Buf d; @@ -398,7 +415,8 @@ in the shared mem communication. We will then link them together using a
#### Specify dataport interfaces -``` + +```c /*-- 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" @@ -410,7 +428,7 @@ in the shared mem communication. We will then link them together using a
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="dataport-task4") -*/ /* TASK 4: the dataport interfaces */ dataport Buf d; @@ -418,17 +436,18 @@ in the shared mem communication. We will then link them together using a dataport ptr_buf_t d_ptrs; /*-- endfilter -*/ ``` +
### Dataport connections -And here we are: we're about to specify connections -between the shared memory pages in each client, and tell CAmkES to link -these using shared underlying Frame objects. Fill out this step, and -proceed. + +And here we are: we're about to specify connections between the shared memory +pages in each client, and tell CAmkES to link these using shared underlying +Frame objects. Fill out this step, and proceed. #### Specify dataport connections -``` +```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="dataport-task6") -*/ /* TASK 6: Dataport connections */ /* hint 1: connect the corresponding dataport interfaces of the components to each other @@ -441,7 +460,7 @@ proceed.
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="dataport-task6") -*/ /* TASK 6: Dataport connections */ connection seL4SharedData data_conn(from client.d, to echo.d); @@ -449,14 +468,17 @@ proceed. connection seL4SharedData ptr_data_conn(from client.d_ptrs, to echo.d_ptrs); /*-- endfilter -*/ ``` +
### Access and manipulate share memory mapping (Dataport) of the client -These steps are asking you to write some C code -to access and manipulate the data in the shared memory mapping -(Dataport) of the client. Follow through to the next step. + +These steps are asking you to write some C code to access and manipulate the +data in the shared memory mapping (Dataport) of the client. Follow through to +the next step. #### Copy strings to an untyped dataport + ```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="copy-task9") -*/ /* TASK 9: copy strings to an untyped dataport */ @@ -485,10 +507,12 @@ to access and manipulate the data in the shared memory mapping } /*-- endfilter -*/ ``` + #### Read the reply data from a typed dataport -``` + +```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="read-task12") -*/ /* TASK 12: read the reply data from a typed dataport */ /* hint 1: use the "str_buf_t" dataport as defined in the Client.camkes file @@ -505,7 +529,7 @@ to access and manipulate the data in the shared memory mapping
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="read-task12") -*/ /* TASK 12: read the reply data from a typed dataport */ for (int i = 0; i < d_typed->n; i++) { @@ -513,11 +537,12 @@ to access and manipulate the data in the shared memory mapping } /*-- endfilter -*/ ``` +
#### Send data using dataports -``` +```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="send-task13") -*/ /* TASK 13: send the data over again, this time using two dataports, one * untyped dataport containing the data, and one typed dataport containing @@ -554,14 +579,17 @@ to access and manipulate the data in the shared memory mapping } /*-- endfilter -*/ ``` + ### Access and manipulate share memory mapping (Dataport) of the server + And these steps are asking you to write some C code to access and manipulate the data in the shared memory mapping (Dataport) of the server. #### Read data from an untyped dataport + ```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="read-task19") -*/ /* TASK 19: read some data from the untyped dataport */ @@ -589,6 +617,7 @@ code to access and manipulate the data in the shared memory mapping } /*-- endfilter -*/ ``` + #### Put data into a typed dataport @@ -626,6 +655,7 @@ code to access and manipulate the data in the shared memory mapping d_typed->n = *n; /*-- endfilter -*/ ``` + #### Read data from a typed dataport @@ -647,6 +677,7 @@ code to access and manipulate the data in the shared memory mapping */ /*-- endfilter -*/ ``` +
Quick solution @@ -663,15 +694,17 @@ code to access and manipulate the data in the shared memory mapping } /*-- endfilter -*/ ``` +
### CAmkES attributes + This is an introduction to CAmkES attributes: you're being asked to set the priority of the components. #### Set component priorities -``` +```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="set-task7") -*/ /* TASK 7: set component priorities */ /* hint 1: component priority is specified as an attribute with the name .priority @@ -683,16 +716,18 @@ being asked to set the priority of the components.
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="set-task7") -*/ /* TASK 7: set component priorities */ client.priority = 255; echo.priority = 254; /*-- endfilter -*/ ``` +
### Specify the data access constraints for Dataports + This is where we specify the data access constraints for the Dataports in a shared memory connection. We then go about attempting to violate those constraints to see how CAmkES has truly met @@ -700,7 +735,7 @@ our constraints when mapping those Dataports. #### Restrict access to dataports -``` +```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="restrict-task8") -*/ /* TASK 8: restrict access to dataports */ /* hint 1: use attribute ._access for each component and interface @@ -714,7 +749,7 @@ our constraints when mapping those Dataports.
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="restrict-task8") -*/ /* TASK 8: restrict access to dataports */ echo.d_access = "R"; @@ -723,10 +758,12 @@ our constraints when mapping those Dataports. client.d_typed_access = "R"; /*-- endfilter -*/ ``` +
#### Test the read and write permissions on the dataport -``` + +```c /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="test-task16") -*/ /* TASK 16: test the read and write permissions on the dataport. * When we try to write to a read-only dataport, we will get a VM fault. @@ -738,7 +775,7 @@ our constraints when mapping those Dataports.
Quick solution -``` +```c /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="test-task16") -*/ /* TASK 16: test the read and write permissions on the dataport. * When we try to write to a read-only dataport, we will get a VM fault. @@ -746,17 +783,16 @@ our constraints when mapping those Dataports. d_typed->n = 0; /*-- endfilter -*/ ``` +
## Done! - Congratulations: be sure to read up on the keywords and -structure of ADL: it's key to understanding CAmkES. And well done on -writing your first CAmkES application. - +Congratulations! You have completed the third CAmkES tutorial. /*-- filter ExcludeDocs() -*/ + ```c /*- filter File("components/Client/Client.camkes") --*/ @@ -791,6 +827,7 @@ component Echo { /*-- endfilter -*/ ``` + ```c /*- filter File("hello-2.camkes") --*/ /* @@ -858,6 +895,7 @@ typedef struct { /*-- endfilter -*/ ``` + ```c /*- filter File("components/Client/src/client.c") --*/ /* @@ -982,7 +1020,7 @@ void echo__init(void) { ``` -``` +```c /*- filter TaskCompletion("hello", TaskContentType.BEFORE) --*/ client: the next instruction will cause a vm fault due to permissions /*-- endfilter -*/ @@ -1015,4 +1053,5 @@ GenerateCAmkESRootserver() /*? macros.cmake_check_script(state) ?*/ /*-- endfilter -*/ ``` + /*-- endfilter -*/ \ No newline at end of file diff --git a/tutorials/hello-camkes-timer/hello-camkes-timer.md b/tutorials/hello-camkes-timer/hello-camkes-timer.md index f9619e4..5fc3974 100644 --- a/tutorials/hello-camkes-timer/hello-camkes-timer.md +++ b/tutorials/hello-camkes-timer/hello-camkes-timer.md @@ -22,33 +22,31 @@ The solutions to this tutorial primarily uses the method of manually defining hardware details. The solutions to the second part are also included, albeit commented out. -## Initialising - -/*? macros.tutorial_init("hello-camkes-timer") ?*/ - ## Prerequisites 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 +## capDL Loader This tutorial uses the *capDL loader*, a root task which allocates statically configured objects and capabilities.
-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/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. +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/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 @@ -57,7 +55,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-timer") ?*/ @@ -67,10 +65,11 @@ All tutorials come with complete solutions. To get solutions run: ## Exercises - Part 1 ### Instantiate a Timer and Timerbase + Start in `hello-camkes-timer.camkes`. Instantiate some components. You're already given one component instance -- `client`. You need to instantiate additional components, a timer driver and +--- `client`. You need to instantiate additional components, a timer driver and a component instance representing the timer hardware itself. Look in `components/Timer/Timer.camkes` for the definitions of the components. @@ -89,7 +88,7 @@ timer.hello);` and `timer.sem_value = 0;` in the `hello-camkes-timer.camkes` file. They assume that the name of the timer ''driver'' will be `timer`. If you wish to call your driver something else, you'll have to change these lines. -``` +```c /*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task1") -*/ /* Part 1, TASK 1: component instances */ /* hint 1: one hardware component and one driver component @@ -102,7 +101,7 @@ wish to call your driver something else, you'll have to change these lines.
Quick solution -``` +```c /*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task1") -*/ /* Part 1, TASK 1: component instances */ component Timerbase timerbase; @@ -113,12 +112,13 @@ wish to call your driver something else, you'll have to change these lines. ### Connect a timer driver component + Connect the timer driver component (`Timer`) to the timer hardware component (`Timerbase`). The timer hardware component exposes two interfaces which must be connected to the timer driver. One of these represents memory-mapped registers. The other represents an interrupt. -``` +```c /*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task2") -*/ /* Part 1, TASK 2: connections */ /* hint 1: use seL4HardwareMMIO to connect device memory @@ -132,22 +132,24 @@ registers. The other represents an interrupt.
Quick solution -``` +```c /*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task2") -*/ /* Part 1, TASK 2: connections */ connection seL4HardwareMMIO timer_mem(from timer.reg, to timerbase.reg); connection seL4HardwareInterrupt timer_irq(from timerbase.irq, to timer.irq); /*-- endfilter -*/ ``` +
### Configure a timer hardware component instance + Configure the timer hardware component instance with device-specific info. The physical address of the timer's memory-mapped registers, and its IRQ number must both be configured. -``` +```c /*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task3") -*/ /* Part 1, TASK 3: hardware resources */ /* Timer and Timerbase: @@ -161,7 +163,7 @@ must both be configured.
Quick solution -``` +```c /*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task3") -*/ /* Part 1, TASK 3: hardware resources */ timerbase.reg_paddr = 0xF8001000; // paddr of mmio registers @@ -169,9 +171,11 @@ must both be configured. timerbase.irq_irq_number = 42; // timer irq number /*-- endfilter -*/ ``` +
### Call into a supplied driver to handle the interrupt + Now open `components/Timer/src/timer.c`. We'll start by completing the `irq_handle` function, which is called in @@ -206,9 +210,11 @@ inform the driver that an interrupt has occurred. timer_handle_irq(&timer_drv); /*-- endfilter -*/ ``` +
### Stop a timer + Stop the timer from running. The `timer_stop` function will be helpful here. ```c @@ -228,9 +234,11 @@ Stop the timer from running. The `timer_stop` function will be helpful here. timer_stop(&timer_drv); /*-- endfilter -*/ ``` +
### Acknowledge an interrupt + The interrupt now needs to be acknowledged. CAmkES generates the seL4-specific code for ack-ing an interrupt and provides a @@ -255,9 +263,11 @@ connected with `seL4HardwareInterrupt`). ZF_LOGF_IF(error != 0, "failed to acknowledge interrupt"); /*-- endfilter -*/ ``` + ### Get a timer handler + Now we'll complete `hello__init` - a function which is called once before the component's interfaces start running. @@ -284,9 +294,11 @@ handle to the driver in the global variable `timer_drv`. assert(error == 0); /*-- endfilter -*/ ``` + ### Start a timer + After initialising the timer, we now need to start the timer. Do so by calling `timer_start` and passing the handle to the driver. @@ -308,9 +320,11 @@ After initialising the timer, we now need to start the timer. Do so by calling assert(error == 0); /*-- endfilter -*/ ``` + -### Implement a RPC interface +### Implement an RPC interface + Note that this task is to understand the existing code. You won't have to modify anything for this task. @@ -335,6 +349,7 @@ need to implement is called `hello_sleep`. */ /*-- endfilter -*/ ``` +
Quick solution @@ -345,9 +360,11 @@ void hello_sleep(int sec) { int error = 0; /*-- endfilter -*/ ``` +
### Set a timer interrupt + Tell the timer to interrupt after the given number of seconds. The `timer_set_timeout` function from the included driver will help. Note that it expects its time argument to be given in nanoseconds. @@ -371,6 +388,7 @@ expects its time argument to be given in nanoseconds. assert(error == 0); /*-- endfilter -*/ ``` + Note the existing code in `hello_sleep`. It waits on a binary semaphore. @@ -380,7 +398,8 @@ the function to return after the delay. Expect the following output with a 2 second delay between the last 2 lines: -``` + +```log Starting the client ------Sleep for 2 seconds------ After the client: wakeup @@ -393,14 +412,15 @@ hardware component to initialise hardware resources, this part of the tutorial will teach you how to use the `seL4DTBHardware` connector to do that automatically. -The connector requires a devicetree blob which describes an ARM platform. +The connector requires a device tree blob which describes an ARM platform. Additionally, the blob's interrupt fields also need to follow the same format -of the ARM GIC v1 and v2. There are devicetree source files bundled with the +of the ARM GIC v1 and v2. There are device tree source files bundled with the kernel, look in the `tools/dts/` folder of the kernel sources. If a suitable -devicetree blob is not available for your platform, then do not proceed with +device tree blob is not available for your platform, then do not proceed with the tutorial. ### Instantiate a TimerDTB component + Navigate to the `hello-camkes-timer.camkes` file. Remove the `Timerbase` and `Timer` component instantiations and instantiate a @@ -408,7 +428,7 @@ Remove the `Timerbase` and `Timer` component instantiations and instantiate a hello_timer(from client.hello, to timer.hello);` and `timer.sem_value = 0;` lines if necessary. -``` +```c /*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part2-task1") -*/ /* Part 2, TASK 1: component instances */ /* hint 1: a single TimerDTB component @@ -421,21 +441,23 @@ lines if necessary.
Quick solution -``` +```c /*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part2-task1") -*/ /* Part 2, TASK 1: component instances */ //uncomment the line below // component TimerDTB timer; /*-- endfilter -*/ ``` +
### Connect interfaces using the seL4DTBHardware connector + Remove the `seL4HardwareMMIO` and `seL4HardwareInterrupt` connections. Connect the two interfaces inside the `TimerDTB` component with the `seL4DTBHardware` connector. -``` +```c /*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part2-task2") -*/ /* Part 2, TASK 2: connections */ /* hint 1: connect the dummy_source and timer interfaces @@ -449,27 +471,29 @@ connector.
Quick solution -``` +```c /*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part2-task2") -*/ /* Part 2, TASK 2: connections */ // uncomment the line below // connection seL4DTBHardware timer_dtb(from timer.dummy_source, to timer.tmr); /*-- endfilter -*/ ``` +
### Configure the TimerDTB component + Before opening `components/Timer/Timer.camkes`, remove the `Timerbase` settings inside the configurations block. Configure the `TimerDTB` component to pass in the correct DTB path to a timer to the connector and also initialise the interrupt resources for the timer. -This will allow the connector to read a device node from the devicetree blob +This will allow the connector to read a device node from the device tree blob and grab the necessary data to initialise hardware resources. More specifically, it reads the registers field and optionally the interrupts field to allocate memory and interrupts. -``` +```c /*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part2-task3") -*/ /* Part 2, TASK 3: hardware resources */ /* TimerDTB: @@ -484,7 +508,7 @@ to allocate memory and interrupts.
Quick solution -``` +```c /*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part2-task3") -*/ /* Part 2, TASK 3: hardware resources */ // uncomment the lines below @@ -492,9 +516,11 @@ to allocate memory and interrupts. // tmr.generate_interrupts = 1; // tell seL4DTBHardware to init interrupts /*-- endfilter -*/ ``` +
### Handle the interrupt + Move to `components/TimerDTB/src/timerdtb.c`. Similar to part one, we'll start with the `tmr_irq_handle` function. This @@ -532,9 +558,11 @@ included driver in `timer_driver` and the task here is to call timer_handle_irq(&timer_drv); /*-- endfilter -*/ ``` + ### Stop a timer + Stop the timer from running. The `timer_stop` function will be helpful here. ```c @@ -554,9 +582,11 @@ Stop the timer from running. The `timer_stop` function will be helpful here. timer_stop(&timer_drv); /*-- endfilter -*/ ``` + ### Acknowledge the interrupt + Again, the interrupt now has to be acknowledged. For the `seL4DTBHardware` connector, CAmkES also generates and provides a @@ -585,6 +615,7 @@ you wish to acknowledge. ZF_LOGF_IF(error != 0, "failed to acknowledge interrupt"); /*-- endfilter -*/ ``` + ### TASK 7 - 10 @@ -595,6 +626,7 @@ You should also expect the same output as the first part. /*-- filter ExcludeDocs() -*/ + ```c /*-- filter File("components/Client/Client.camkes") --*/ /* @@ -750,7 +782,7 @@ void hello__init() { * where "interface name" is the name of the * interface where you set the path of the DTB (foo.dtb = dtb({...})) * and "register number" is the index of the register block in the device - * node in the devicetree blob + * node in the device tree blob */ /*- if solution -*/ int error = timer_init(&timer_drv, DEFAULT_TIMER_ID, tmr_0); diff --git a/tutorials/hello-world/hello-world.md b/tutorials/hello-world/hello-world.md index 8250690..4b1d1c6 100644 --- a/tutorials/hello-world/hello-world.md +++ b/tutorials/hello-world/hello-world.md @@ -56,7 +56,7 @@ This step creates two new directories in `tutorials/`, namely `hello-world` and
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("hello-world") ?*/ diff --git a/tutorials/interrupts/interrupts.md b/tutorials/interrupts/interrupts.md index 6f34f8d..1e35c01 100644 --- a/tutorials/interrupts/interrupts.md +++ b/tutorials/interrupts/interrupts.md @@ -7,9 +7,11 @@ /*? declare_task_ordering(['timer-start', 'timer-get', 'timer-set', 'timer-ack']) ?*/ # Interrupts + This tutorial covers seL4 interrupts. You will learn: + 1. The purpose of the IRQControl capability. 2. How to obtain capabilities for specific interrupts. 3. How to handle interrupts and their relation with notification objects. @@ -25,7 +27,7 @@ You will learn:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("interrupts") ?*/ @@ -33,13 +35,13 @@ All tutorials come with complete solutions. To get solutions run: Answers are also available in drop down menus under each section.
-## CapDL Loader +## capDL Loader This tutorial uses the *capDL loader*, a root task which allocates statically configured objects and capabilities.
-Get CapDL +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/projects/camkes/) projects @@ -47,10 +49,10 @@ 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. + +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.
## Background @@ -69,7 +71,7 @@ IRQHandler capabilities give access to a single irq and are standard seL4 capabi invoking the IRQControl capability, with architecture specific parameters. Below is an example of obtaining an IRQHandler. -```bash +```c // Get a capability for irq number 7 and place it in cslot 10 in a single-level cspace. error = seL4_IRQControl_Get(seL4_IRQControl, 7, cspace_root, 10, seL4_WordBits); ``` @@ -85,7 +87,8 @@ dependent, including: Interrupts are received by registering a capability to a notification object with the IRQHandler capability for that irq, as follows: -```bash + +```c seL4_IRQHandler_SetNotification(irq_handler, notification); ``` @@ -124,7 +127,7 @@ makes a single request. On successful initialisation of the tutorial, you will see the following: -``` +```log timer client: hey hey hey timer: got a message from 61 to sleep 2 seconds <> @@ -141,7 +144,7 @@ The timer driver we are using emits an interrupt in the `TTC0_TIMER1_IRQ` number **Exercise** Invoke `irq_control`, which contains the `seL4_IRQControl` capability, the place the `IRQHandler` capability for `TTC0_TIMER1_IRQ` into the `irq_handler` CSlot. -``` +```c /*-- filter TaskContent("timer-start", TaskContentType.ALL, subtask='get') -*/ /* TODO invoke irq_control to put the interrupt for TTC0_TIMER1_IRQ in cslot irq_handler (depth is seL4_WordBits) */ @@ -166,7 +169,7 @@ the place the `IRQHandler` capability for `TTC0_TIMER1_IRQ` into the `irq_handle On success, you should see the following output, without the error message that occurred earlier, as the irq_handle capability is now valid: -``` +```log /*-- filter TaskCompletion("timer-get", TaskContentType.COMPLETED) -*/ Undelivered IRQ: 42 /*-- endfilter -*/ @@ -176,9 +179,10 @@ This is a warning message from the kernel that an IRQ was recieved for irq numbe notification capability is set to sent a signal to. ### Set NTFN + **Exercise** Now set the notification capability (`ntfn`) by invoking the irq handler. -``` +```c /*-- filter TaskContent("timer-start", TaskContentType.ALL, subtask='set') -*/ /* TODO set ntfn as the notification for irq_handler */ /*-- endfilter -*/ @@ -201,7 +205,7 @@ notification capability is set to sent a signal to. Now the output will be: -``` +```log /*-- filter TaskCompletion("timer-set", TaskContentType.COMPLETED) -*/ Tick /*-- endfilter -*/ @@ -215,7 +219,7 @@ before replying to the client. **Exercise** Acknowledge the interrupt after handling it in the timer driver. -``` +```c /*-- filter TaskContent("timer-start", TaskContentType.ALL, subtask='ack') -*/ /* TODO ack the interrupt */ /*-- endfilter -*/ @@ -237,7 +241,7 @@ before replying to the client. Now the timer interrupts continue to come in, and the reply is delivered to the client. -``` +```log /*-- filter TaskCompletion("timer-ack", TaskContentType.COMPLETED) -*/ timer client wakes up /*-- endfilter -*/ @@ -246,6 +250,7 @@ timer client wakes up That's it for this tutorial. /*-- filter ExcludeDocs() -*/ + ```c /*-- filter ELF("client") -*/ /*- set _ = state.stash.start_elf("client") -*/ diff --git a/tutorials/ipc/ipc.md b/tutorials/ipc/ipc.md index a2c4ae9..1702229 100644 --- a/tutorials/ipc/ipc.md +++ b/tutorials/ipc/ipc.md @@ -26,7 +26,7 @@ You will learn:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("ipc") ?*/ @@ -34,13 +34,13 @@ All tutorials come with complete solutions. To get solutions run: Answers are also available in drop down menus under each section.
-## CapDL Loader +## capDL Loader This tutorial uses the *capDL loader*, a root task which allocates statically configured objects and capabilities.
-Get CapDL +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/projects/camkes/) projects @@ -49,9 +49,9 @@ 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. -More information about CapDL projects can be found [here](https://docs.sel4.systems/projects/capdl/). +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. +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.
## Background diff --git a/tutorials/libraries-1/libraries-1.md b/tutorials/libraries-1/libraries-1.md index e19b619..f87c2cf 100644 --- a/tutorials/libraries-1/libraries-1.md +++ b/tutorials/libraries-1/libraries-1.md @@ -39,8 +39,9 @@ Don't gloss over the globals declared before `main()` -- they're declared for your benefit so you can grasp some of the basic data structures. Outcomes: + - Understand the kernel's startup procedure. -- Understand that the kernel centers around certain objects and +- Understand that the kernel centres around certain objects and capabilities to those objects. - Understand that libraries exist to automate the very fine-grained nature of the seL4 API, and get a rough idea of @@ -64,7 +65,7 @@ Outcomes:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("libraries-1") ?*/ @@ -76,7 +77,7 @@ Answers are also available in drop down menus under each section. When you first run the tutorial, you should see the following output: -``` +```log Booting all finished, dropped to user space main@main.c:89 [Cond failed: info == NULL] /*-- filter TaskCompletion("task-1", TaskContentType.BEFORE) -*/ @@ -112,7 +113,6 @@ It also sets up the IPC buffer so that it can perform some syscalls such as `seL /*? task_1_desc ?*/ /*-- filter TaskContent("task-1", TaskContentType.BEFORE) -*/ /*-- endfilter -*/ -} ```
@@ -123,23 +123,27 @@ It also sets up the IPC buffer so that it can perform some syscalls such as `seL info = platsupport_get_bootinfo(); /*-- endfilter -*/ ``` +
On success, you should see the following: -``` + +```log libraries-1: main@main.c:124 [Cond failed: allocman == NULL] /*-- filter TaskCompletion("task-1", TaskContentType.COMPLETED) -*/ - Failed to initialize alloc manager. - Memory pool sufficiently sized? - Memory pool pointer valid? + Failed to initialize alloc manager. + Memory pool sufficiently sized? + Memory pool pointer valid? /*-- endfilter -*/ ``` ### Initialise simple `libsel4simple` provides an abstraction for the boot environment of a thread. -You need to initialize it with some default state before using it. +You need to initialise it with some default state before using it. + - + ```c /*-- set task_2_desc -*/ /* TASK 2: initialise simple object */ @@ -151,6 +155,7 @@ You need to initialize it with some default state before using it. /*-- endset -*/ /*? task_2_desc ?*/ ``` +
Quick solution @@ -159,6 +164,7 @@ You need to initialize it with some default state before using it. simple_default_init_bootinfo(&simple, info); /*-- endfilter -*/ ``` +
On successful completion of this task, the output should not change. @@ -186,13 +192,14 @@ Use a `simple` function to print out the contents of the `seL4_BootInfo` functio simple_print(&simple); /*-- endfilter -*/ ``` +
- The error message should remain, but your output should now also contain something like: -``` +```log Node 0 of 1 IOPT levels: 4294967295 IPC buffer: 0x52c000 @@ -219,6 +226,7 @@ don't go through that procedure, but you'll encounter it later. For now, use the allocman and VKA allocation system. The allocman library requires some initial memory to bootstrap its metadata. Complete this step. + - ```c @@ -243,15 +251,16 @@ step. allocman = bootstrap_use_current_simple(&simple, ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool); /*-- endfilter -*/ ``` +
The output should now be as follows: -``` +```log <> libraries-1: main@main.c:199 [Err seL4_InvalidCapability]: /*-- filter TaskCompletion("task-4", TaskContentType.COMPLETED) -*/ - Failed to set the priority for the new TCB object. + Failed to set the priority for the new TCB object. /*-- endfilter -*/ ``` @@ -264,6 +273,7 @@ seL4 considers all memory that hasn't been explicitly earmarked for a purpose to be "untyped", and in order to repurpose any memory into a useful object, you must give it an seL4-specific type. This is retyping, and the VKA library simplifies this for you, among other things. + - ```c @@ -286,6 +296,7 @@ and the VKA library simplifies this for you, among other things. allocman_make_vka(&vka, allocman); /*-- endfilter -*/ ``` + On successful completion this task, the output should not change. @@ -313,6 +324,7 @@ On successful completion this task, the output should not change. cspace_cap = simple_get_cnode(&simple); /*-- endfilter -*/ ``` + This is where the differences between seL4 and contemporary kernels @@ -360,6 +372,7 @@ On successful completion this task, the output should not change. pd_cap = simple_get_pd(&simple); /*-- endfilter -*/ ``` + Just as in the previous step, you were made to grab a reference to the @@ -372,7 +385,6 @@ On successful completion this task, the output should not change. ### Allocate a TCB Object ```c - /*-- set task_8_desc -*/ /* TASK 8: create a new TCB */ /* hint: vka_alloc_tcb() @@ -394,6 +406,7 @@ On successful completion this task, the output should not change. error = vka_alloc_tcb(&vka, &tcb_object); /*-- endfilter -*/ ``` + In order to manage the threads that are created in seL4, the seL4 kernel @@ -408,13 +421,15 @@ still manually fill it out. After completing this task, the errors should disappear, and you should see the following output: -``` + +```log /*-- filter TaskCompletion("task-8", TaskContentType.COMPLETED) -*/ main: hello world /*-- endfilter -*/ ``` ### Configure the new TCB + ```c /*-- set task_9_desc -*/ /* TASK 9: initialise the new TCB */ @@ -447,6 +462,7 @@ main: hello world error = seL4_TCB_Configure(tcb_object.cptr, seL4_CapNull, cspace_cap, seL4_NilData, pd_cap, seL4_NilData, 0, 0); /*-- endfilter -*/ ``` + You must create a new VSpace for your new thread if you need it to @@ -465,11 +481,13 @@ In addition, a thread needs to have a priority set on it in order for it to run. will give your new thread the same priority as the current thread, allowing it to be run the next time the seL4 scheduler is invoked. The seL4 scheduler is invoked everytime there is a kernel timer tick. + - On successful completion this task, the output should not change. ### Name the new TCB + ```c /*-- set task_10_desc -*/ /* TASK 10: give the new thread a name */ @@ -486,6 +504,7 @@ On successful completion this task, the output should not change. NAME_THREAD(tcb_object.cptr, "libraries-1: thread_2"); /*-- endfilter -*/ ``` + This is a convenience function -- sets a name string for the TCB object. @@ -493,6 +512,7 @@ This is a convenience function -- sets a name string for the TCB object. On successful completion this task, the output should not change. ### Set the instruction pointer + ```c /*-- set task_11_desc -*/ /* @@ -520,6 +540,7 @@ On successful completion this task, the output should not change. sel4utils_set_instruction_pointer(®s, (seL4_Word)thread_2); /*-- endfilter -*/ ``` + Pay attention to the line that precedes this particular task -- the line @@ -529,10 +550,13 @@ manually. That includes the new thread's initial register contents. You can set the value of the stack pointer, the instruction pointer, and if you want to get a little creative, you can pass some initial data to your new thread through its registers. + - On successful completion this task, the output should not change. + ### Set the stack pointer + ```c /*-- set task_12_desc -*/ /* TASK 12: set stack pointer for the new thread */ @@ -555,17 +579,20 @@ On successful completion this task, the output should not change. sel4utils_set_stack_pointer(®s, thread_2_stack_top); /*-- endfilter -*/ ``` + This TASK is just some pointer arithmetic. The cautionary note that the stack grows down is meant to make you think about the arithmetic. Processor stacks push new values toward decreasing addresses, so give it some thought. + - On successful completion this task, the output should not change. ### Write the registers + ```c /*-- set task_13_desc -*/ /* TASK 13: actually write the TCB registers. We write 2 registers: @@ -591,16 +618,19 @@ On successful completion this task, the output should not change. error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, ®s); /*-- endfilter -*/ ``` + As explained above, we've been filling out our new thread's TCB for the last few operations, so now we're writing the values we've chosen, to the TCB object in the kernel. + - On successful completion this task, the output should not change. ### Start the new thread + ```c /*-- set task_14_desc -*/ /* TASK 14: start the new thread running */ @@ -621,6 +651,7 @@ On successful completion this task, the output should not change. error = seL4_TCB_Resume(tcb_object.cptr); /*-- endfilter -*/ ``` + Finally, we tell the kernel that our new thread is runnable. From here, @@ -631,14 +662,15 @@ policy. - On successful completion this task, the output should not change. + ### Print something + ```c /*--set task_15_desc -*/ /* TASK 15: print something */ /* hint: printf() */ /*-- endset -*/ /*? task_15_desc ?*/ -} ```
@@ -649,6 +681,7 @@ On successful completion this task, the output should not change. printf("thread_2: hallo wereld\n"); /*-- endfilter -*/ ``` +
For the sake of confirmation that our new thread was executed by the @@ -675,7 +708,8 @@ That's it for this tutorial. /*-- filter ExcludeDocs() -*/ /*? ExternalFile("CMakeLists.txt") ?*/ -``` + +```c /*-- filter File("main.c") -*/ /* * Copyright 2018, Data61, CSIRO (ABN 41 687 119 230). @@ -826,9 +860,11 @@ int main(void) { } /*-- endfilter -*/ ``` -/```cmake + +```cmake /*- filter File("settings.cmake") -*/ set(KernelRootCNodeSizeBits 12 CACHE STRING "" FORCE) /*- endfilter -*/ ``` + /*-- endfilter -*/ diff --git a/tutorials/libraries-2/libraries-2.md b/tutorials/libraries-2/libraries-2.md index 2ec43a1..0857943 100644 --- a/tutorials/libraries-2/libraries-2.md +++ b/tutorials/libraries-2/libraries-2.md @@ -72,7 +72,7 @@ Learning outcomes:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("libraries-2") ?*/ @@ -83,7 +83,8 @@ Answers are also available in drop down menus under each section. ## Exercises When you first run this tutorial, you will see a fault as follows: -``` + +```log /*-- filter TaskCompletion("task-1", TaskContentType.ALL) -*/ Booting all finished, dropped to user space Caught cap fault in send phase at address (nil) @@ -112,7 +113,7 @@ of a MMU-utilizing kernel apply. - -``` +```c /*-- set task_1_desc -*/ /* TASK 1: get a frame cap for the ipc buffer */ /* hint: vka_alloc_frame() @@ -138,6 +139,7 @@ of a MMU-utilizing kernel apply. "\tNB: This frame is not an immediately usable, virtually mapped page.\n") /*-- endfilter -*/ ``` +
/*-- filter ExcludeDocs() -*/ @@ -170,7 +172,7 @@ into a VSpace, and the mapping of a new page-table into a VSpace. - - -``` +```c /*-- set task_2_desc -*/ /* TASK 2: try to map the frame the first time */ /* hint 1: seL4_ARCH_Page_Map() @@ -208,13 +210,15 @@ into a VSpace, and the mapping of a new page-table into a VSpace. seL4_AllRights, seL4_ARCH_Default_VMAttributes); /*-- endfilter -*/ ``` + On completion, the output will be as follows: -``` + +```log libraries-2: main@main.c:260 [Err seL4_FailedLookup]: /*--filter TaskCompletion("task-2", TaskContentType.COMPLETED) -*/ - Failed to allocate new page table. + Failed to allocate new page table. /*-- endfilter -*/ ``` @@ -226,7 +230,7 @@ page-table object to use as a leaf page-table in your VSpace. - -``` +```c /*-- set task_3_desc -*/ /* TASK 3: create a page table */ /* hint: vka_alloc_page_table() @@ -248,6 +252,7 @@ page-table object to use as a leaf page-table in your VSpace. error = vka_alloc_page_table(&vka, &pt_object); /*-- endfilter -*/ ``` + On completion, you will see another fault. @@ -267,7 +272,7 @@ try again to finally map the IPC-buffer's frame object into the VSpace. - - -``` +```c /*-- set task_4_desc -*/ /* TASK 4: map the page table */ /* hint 1: seL4_ARCH_PageTable_Map() @@ -315,7 +320,8 @@ Booting all finished, dropped to user space Use `seL4_ARCH_Page_Map` to map the frame in. If everything was done correctly, there is no reason why this step should fail. Complete it and proceed. -``` + +```c /*-- set task_5_desc -*/ /* TASK 5: then map the frame in */ /* hint 1: use seL4_ARCH_Page_Map() as above @@ -336,16 +342,18 @@ should fail. Complete it and proceed. ipc_buffer_vaddr, seL4_AllRights, seL4_ARCH_Default_VMAttributes); /*-- endfilter -*/ ``` + On completion, you will see the following: -``` + +```log /*--filter TaskCompletion("task-5", TaskContentType.COMPLETED) -*/ main: hello world /*-- endfilter -*/ libraries-2: main@main.c:464 [Cond failed: seL4_MessageInfo_get_length(tag) != 1] - Response data from thread_2 was not the length expected. - How many registers did you set with seL4_SetMR within thread_2? + Response data from thread_2 was not the length expected. + How many registers did you set with seL4_SetMR within thread_2? ``` ### Allocate an endpoint @@ -364,7 +372,7 @@ and proceed. - -``` +```c /*-- set task_6_desc -*/ /* TASK 6: create an endpoint */ /* hint: vka_alloc_endpoint() @@ -385,6 +393,7 @@ and proceed. error = vka_alloc_endpoint(&vka, &ep_object); /*-- endfilter -*/ ``` + On completion, the output will not change. @@ -415,7 +424,7 @@ data, and know which sender you are. Complete the step and proceed. - - -``` +```c /*-- set task_7_desc -*/ /* TASK 7: make a badged copy of it in our cspace. This copy will be used to send * an IPC message to the original cap */ @@ -444,6 +453,7 @@ data, and know which sender you are. Complete the step and proceed. EP_BADGE); /*-- endfilter -*/ ``` + On completion, the output will not change. @@ -471,7 +481,7 @@ transmitted in the message. - - -``` +```c /*-- set task_8_desc -*/ /* TASK 8: set the data to send. We send it in the first message register */ /* hint 1: seL4_MessageInfo_new() @@ -508,13 +518,15 @@ transmitted in the message. seL4_SetMR(0, MSG_DATA); /*-- endfilter -*/ ``` + On completion, the output should change as follows: -``` + +```log libraries-2: main@main.c:472 [Cond failed: msg != ~MSG_DATA] /*-- filter TaskCompletion("task-8", TaskContentType.COMPLETED) -*/ - Response data from thread_2's content was not what was expected. + Response data from thread_2's content was not what was expected. /*-- endfilter -*/ ``` @@ -554,7 +566,7 @@ response message, if the sender doesn't want it to. - - -``` +```c /*-- set task_9_desc -*/ /* TASK 9: send and wait for a reply. */ /* hint: seL4_Call() @@ -580,10 +592,12 @@ response message, if the sender doesn't want it to. tag = seL4_Call(ep_cap_path.capPtr, tag); /*-- endfilter -*/ ``` + On completion, you should see thread_2 fault as follows: -``` + +```log /*--filter TaskCompletion("task-9", TaskContentType.COMPLETED) -*/ thread_2: hallo wereld thread_2: got a message 0 from 0 @@ -608,7 +622,7 @@ designated, single IPC buffer. - -``` +```c /*-- set task_10_desc -*/ /* TASK 10: get the reply message */ /* hint: seL4_GetMR() @@ -628,6 +642,7 @@ designated, single IPC buffer. msg = seL4_GetMR(0); /*-- endfilter -*/ ``` + On completion, the output should not change. @@ -646,7 +661,7 @@ explicitly interested in distinguishing the sender. - - -``` +```c /*-- set task_11_desc -*/ /* TASK 11: wait for a message to come in over the endpoint */ /* hint 1: seL4_Recv() @@ -662,6 +677,7 @@ explicitly interested in distinguishing the sender. /*-- endset -*/ /*? task_11_desc ?*/ ``` +
Quick solution @@ -670,10 +686,12 @@ explicitly interested in distinguishing the sender. tag = seL4_Recv(ep_object.cptr, &sender_badge); /*-- endfilter -*/ ``` +
On completion, the output should change slightly: -``` + +```log /*-- filter TaskCompletion("task-11", TaskContentType.COMPLETED) -*/ thread_2: got a message 0 from 0x61 /*-- endfilter -*/ @@ -687,7 +705,7 @@ Complete them and proceed to the next step. - -``` +```c /*-- set task_12_desc -*/ /* TASK 12: make sure it is what we expected */ /* hint 1: check the badge. is it EP_BADGE? @@ -716,6 +734,7 @@ Complete them and proceed to the next step. "\tHow many registers did you set with seL4_SetMR, within the root thread?\n"); /*-- endfilter -*/ ``` + On completion, the output should not change. @@ -726,7 +745,7 @@ Again, just reading the data from the Message Registers. - -``` +```c /*-- set task_13_desc -*/ /* TASK 13: get the message stored in the first message register */ /* hint: seL4_GetMR() @@ -746,10 +765,12 @@ Again, just reading the data from the Message Registers. msg = seL4_GetMR(0); /*-- endfilter -*/ ``` + On completion, the output should change slightly: -``` + +```log /*--filter TaskCompletion("task-13", TaskContentType.COMPLETED) -*/ thread_2: got a message 0x6161 from 0x61 /*-- endfilter -*/ @@ -761,7 +782,7 @@ And writing Message Registers again. - -``` +```c /*-- set task_14_desc -*/ /* TASK 14: copy the modified message back into the message register */ /* hint: seL4_SetMR() @@ -781,6 +802,7 @@ And writing Message Registers again. seL4_SetMR(0, msg); /*-- endfilter -*/ ``` + On completion, the output should not change. @@ -805,7 +827,7 @@ Complete the step and pat yourself on the back. - - -``` +```c /*-- set task_15_desc -*/ /* TASK 15: send the message back */ /* hint 1: seL4_ReplyRecv() @@ -832,10 +854,12 @@ Complete the step and pat yourself on the back. seL4_ReplyRecv(ep_object.cptr, tag, &sender_badge); /*-- endfilter -*/ ``` + On completion, the output should change, with the fault message replaced with the following: -``` + +```log /*--filter TaskCompletion("task-15", TaskContentType.COMPLETED) -*/ main: got a reply: [0xffff9e9e|0xffffffffffff9e9e] /*-- endfilter -*/ @@ -847,7 +871,8 @@ That's it for this tutorial. /*- filter ExcludeDocs() -*/ /*? ExternalFile("CMakeLists.txt") ?*/ -``` + +```c /*-- filter File("main.c") -*/ /* * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230) @@ -1115,4 +1140,5 @@ int main(void) { } /*- endfilter -*/ ``` + /*- endfilter -*/ diff --git a/tutorials/libraries-3/libraries-3.md b/tutorials/libraries-3/libraries-3.md index 4c4e58b..2f27916 100644 --- a/tutorials/libraries-3/libraries-3.md +++ b/tutorials/libraries-3/libraries-3.md @@ -56,7 +56,7 @@ Learning outcomes:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("libraries-3") ?*/ @@ -71,7 +71,7 @@ Tasks in this tutorial are in `main.c` and `app.c`. When you first run this tutorial, you should see the following output: -``` +```log Booting all finished, dropped to user space Node 0 of 1 IOPT levels: 4294967295 @@ -86,7 +86,7 @@ Initial thread cnode size: 12 libraries-3: vspace_reserve_range_aligned@vspace.h:621 Not implemented libraries-3: main@main.c:117 [Cond failed: virtual_reservation.res == NULL] /*-- filter TaskCompletion("task-1", TaskContentType.BEFORE) -*/ - Failed to reserve a chunk of memory. + Failed to reserve a chunk of memory. /*-- endfilter -*/ ``` @@ -136,11 +136,12 @@ function may seem tedious, it's doing some important things. &data, simple_get_pd(&simple), &vka, info); /*-- endfilter -*/ ``` +
On success, you should see a different error: -``` +```log <> /*-- filter TaskCompletion("task-1", TaskContentType.COMPLETED) -*/ halting... @@ -187,15 +188,16 @@ thread. error = sel4utils_configure_process_custom(&new_process, &vka, &vspace, config); /*-- endfilter -*/ ``` + On success, you should see a different error: -``` +```log libraries-3: main@main.c:196 [Cond failed: new_ep_cap == 0] /*-- filter TaskCompletion("task-2", TaskContentType.COMPLETED) -*/ - Failed to mint a badged copy of the IPC endpoint into the new thread's CSpace. - sel4utils_mint_cap_to_process takes a cspacepath_t: double check what you passed. + Failed to mint a badged copy of the IPC endpoint into the new thread's CSpace. + sel4utils_mint_cap_to_process takes a cspacepath_t: double check what you passed. /*-- endfilter -*/ ``` @@ -255,6 +257,7 @@ wouldn't know who was whom. vka_cspace_make_path(&vka, ep_object.cptr, &ep_cap_path); /*-- endfilter -*/ ``` + On success, the output should not change. @@ -295,16 +298,17 @@ free slot that the VKA library found for us. seL4_AllRights, EP_BADGE); /*-- endfilter -*/ ``` + On success, the output should look something like: -``` +```log NEW CAP SLOT: 6ac. main: hello world libraries-3: main@main.c:247 [Cond failed: sender_badge != EP_BADGE] /*-- filter TaskCompletion("task-4", TaskContentType.COMPLETED) -*/ - The badge we received from the new thread didn't match our expectation + The badge we received from the new thread didn't match our expectation /*-- endfilter -*/ ``` @@ -359,22 +363,23 @@ communicate with us, we can let it run. Complete this step and proceed. error = sel4utils_spawn_process_v(&new_process, &vka, &vspace, argc, (char**) &argv, 1); /*-- endfilter -*/ ``` + On success, you should be able to see the second process running. The output should be as follows: -``` +```log NEW CAP SLOT: 6ac. process_2: hey hey hey main@app.c:67 [Cond failed: msg != ~MSG_DATA] /*-- filter TaskCompletion("task-5", TaskContentType.COMPLETED) -*/ - Unexpected response from root thread. + Unexpected response from root thread. /*-- endfilter -*/ main: hello world libraries-3: main@main.c:255 [Cond failed: sender_badge != EP_BADGE] - The badge we received from the new thread didn't match our expectation. + The badge we received from the new thread didn't match our expectation. ``` ### Receive a message @@ -401,12 +406,11 @@ Then we verify the fidelity of the data that was transmitted. /*? task_6_desc ?*/ /*-- filter ExcludeDocs() -*/ /*-- filter TaskCompletion("task-6", TaskContentType.COMPLETED) -*/ - Unexpected response from root thread. + Unexpected response from root thread. /*-- endfilter -*/ /*-- endfilter -*/ ``` -
Quick solution @@ -415,6 +419,7 @@ Then we verify the fidelity of the data that was transmitted. tag = seL4_Recv(ep_cap_path.capPtr, &sender_badge); /*-- endfilter -*/ ``` +
On success, the badge error should no longer be visible. @@ -444,7 +449,7 @@ message sent by the new thread. /*? task_7_desc ?*/ /*-- filter ExcludeDocs() -*/ /*-- filter TaskCompletion("task-7", TaskContentType.COMPLETED) -*/ - Unexpected response from root thread. + Unexpected response from root thread. /*-- endfilter -*/ /*-- endfilter -*/ ``` @@ -457,6 +462,7 @@ message sent by the new thread. seL4_ReplyRecv(ep_cap_path.capPtr, tag, &sender_badge); /*-- endfilter -*/ ``` + On success, the output should not change. @@ -496,10 +502,11 @@ that was sent, and that's the end. tag = seL4_Call(ep, tag); /*-- endfilter -*/ ``` + On success, you should see the following: -``` +```log /*-- filter TaskCompletion("task-8", TaskContentType.COMPLETED) -*/ process_2: hey hey hey main: got a message 0x6161 from 0x61 @@ -512,7 +519,8 @@ That's it for this tutorial. /*-- filter ExcludeDocs() -*/ /*? ExternalFile("CMakeLists.txt") ?*/ -``` + +```c /*-- filter File("main.c") -*/ /* * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230) @@ -749,4 +757,5 @@ int main(int argc, char **argv) { } /*-- endfilter -*/ ``` + /*-- endfilter -*/ diff --git a/tutorials/libraries-4/libraries-4.md b/tutorials/libraries-4/libraries-4.md index 2d34043..ef3581c 100644 --- a/tutorials/libraries-4/libraries-4.md +++ b/tutorials/libraries-4/libraries-4.md @@ -39,7 +39,7 @@ Learning outcomes:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("libraries-4") ?*/ diff --git a/tutorials/mapping/mapping.md b/tutorials/mapping/mapping.md index 47c1daa..1b21bb3 100644 --- a/tutorials/mapping/mapping.md +++ b/tutorials/mapping/mapping.md @@ -21,7 +21,7 @@ This tutorial provides an introduction to virtual memory management on seL4.
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("mapping") ?*/ diff --git a/tutorials/mcs/mcs.md b/tutorials/mcs/mcs.md index 5818ebc..a22ba50 100644 --- a/tutorials/mcs/mcs.md +++ b/tutorials/mcs/mcs.md @@ -41,7 +41,7 @@ Then initialise the tutorial:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("mcs") ?*/ diff --git a/tutorials/notifications/notifications.md b/tutorials/notifications/notifications.md index b48c378..7dbcc17 100644 --- a/tutorials/notifications/notifications.md +++ b/tutorials/notifications/notifications.md @@ -28,7 +28,7 @@ You will learn how to:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("notifications") ?*/ @@ -36,13 +36,13 @@ All tutorials come with complete solutions. To get solutions run: Answers are also available in drop down menus under each section.
-## CapDL Loader +## capDL Loader This tutorial uses the *capDL loader*, a root task which allocates statically configured objects and capabilities.
-Get CapDL +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/projects/camkes/) projects @@ -51,9 +51,9 @@ 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. -More information about CapDL projects can be found [here](https://docs.sel4.systems/projects/capdl/). +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. +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.
## Background diff --git a/tutorials/threads/threads.md b/tutorials/threads/threads.md index 4c846db..c3ae24f 100644 --- a/tutorials/threads/threads.md +++ b/tutorials/threads/threads.md @@ -26,7 +26,7 @@ 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 +## 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 @@ -40,9 +40,9 @@ 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. -More information about CapDL projects can be found [here](https://docs.sel4.systems/projects/capdl/). +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. +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 @@ -50,7 +50,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("threads") ?*/ @@ -147,7 +147,7 @@ int new_thread(void *arg1, void *arg2, void *arg3) { /*- endfilter -*/ ``` -### CapDL Loader +### 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 a the *capDL loader*, a root task which allocates statically @@ -161,7 +161,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/). +Information about capDL projects can be found [here](https://docs.sel4.systems/projects/capdl/). ### Configure a TCB diff --git a/tutorials/untyped/untyped.md b/tutorials/untyped/untyped.md index e8f00ab..ba0f75d 100644 --- a/tutorials/untyped/untyped.md +++ b/tutorials/untyped/untyped.md @@ -27,7 +27,7 @@ It covers:
Hint: tutorial solutions -
+ All tutorials come with complete solutions. To get solutions run: /*? macros.tutorial_init_with_solution("untyped") ?*/