Skip to content

Commit 5f5b4ed

Browse files
committed
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 <br> by empty line - remove duplicated CAmkES tutorial endings Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
1 parent 3ec4ccf commit 5f5b4ed

File tree

19 files changed

+422
-267
lines changed

19 files changed

+422
-267
lines changed

tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ In this tutorial you will learn how to:
2929

3030
<details markdown='1'>
3131
<summary><em>Hint:</em> tutorial solutions</summary>
32-
<br>
32+
3333
All tutorials come with complete solutions. To get solutions run:
3434

3535
/*? macros.tutorial_init_with_solution("camkes-vm-crossvm") ?*/

tutorials/camkes-vm-linux/camkes-vm-linux.md

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -21,24 +21,24 @@ You will become familiar with:
2121
1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html)
2222
2. [CAmkES timer tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-timer.html)
2323

24-
## CapDL Loader
24+
## capDL Loader
2525

2626
This tutorial uses the *capDL loader*, a root task which allocates statically
2727
configured objects and capabilities.
2828

2929
<details markdown='1'>
30-
<summary>Get CapDL</summary>
30+
<summary>Get capDL</summary>
3131
The capDL loader parses
3232
a static description of the system and the relevant ELF binaries.
3333
It is primarily used in [CAmkES](https://docs.sel4.systems/projects/camkes/) projects
3434
but we also use it in the tutorials to reduce redundant code.
3535
The program that you construct will end up with its own CSpace and VSpace, which are separate
3636
from the root task, meaning CSlots like `seL4_CapInitThreadVSpace` have no meaning
3737
in applications loaded by the capDL loader.
38-
<br>
39-
More information about CapDL projects can be found [here](https://docs.sel4.systems/projects/capdl/).
40-
<br>
41-
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.
38+
39+
More information about capDL projects can be found [here](https://docs.sel4.systems/projects/capdl/).
40+
41+
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.
4242
</details>
4343

4444
## Initialising
@@ -47,7 +47,7 @@ For this tutorial clone the [CapDL repo](https://github.com/sel4/capdl). This ca
4747

4848
<details markdown='1'>
4949
<summary><em>Hint:</em> tutorial solutions</summary>
50-
<br>
50+
5151
All tutorials come with complete solutions. To get solutions run:
5252

5353
/*? macros.tutorial_init_with_solution("camkes-vm-linux") ?*/

tutorials/capabilities/capabilities.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ You will learn:
2424

2525
<details markdown='1'>
2626
<summary><em>Hint:</em> tutorial solutions</summary>
27-
<br>
27+
2828
All tutorials come with complete solutions. To get solutions run:
2929

3030
/*? macros.tutorial_init_with_solution("capabilities") ?*/

tutorials/fault-handlers/fault-handlers.md

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -32,31 +32,31 @@ You will learn:
3232

3333
<details markdown='1'>
3434
<summary><em>Hint:</em> tutorial solutions</summary>
35-
<br>
35+
3636
All tutorials come with complete solutions. To get solutions run:
3737

3838
/*? macros.tutorial_init_with_solution("fault-handlers") ?*/
3939

4040
</details>
4141

42-
## CapDL Loader
42+
## capDL Loader
4343

4444
This tutorial uses the *capDL loader*, a root task which allocates statically
4545
configured objects and capabilities.
4646

4747
<details markdown='1'>
48-
<summary>Get CapDL</summary>
48+
<summary>Get capDL</summary>
4949
The capDL loader parses
5050
a static description of the system and the relevant ELF binaries.
5151
It is primarily used in [CAmkES](https://docs.sel4.systems/projects/camkes/) projects
5252
but we also use it in the tutorials to reduce redundant code.
5353
The program that you construct will end up with its own CSpace and VSpace, which are separate
5454
from the root task, meaning CSlots like `seL4_CapInitThreadVSpace` have no meaning
5555
in applications loaded by the capDL loader.
56-
<br>
57-
More information about CapDL projects can be found [here](https://docs.sel4.systems/projects/capdl/).
58-
<br>
59-
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.
56+
57+
More information about capDL projects can be found [here](https://docs.sel4.systems/projects/capdl/).
58+
59+
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.
6060
</details>
6161

6262
## 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
180180

181181
## Exercises
182182

183-
This tutorial has one address space set up by the CapDL loader, containing two
183+
This tutorial has one address space set up by the capDL loader, containing two
184184
threads which share the same CSpace. One of the threads is a fault handler while
185185
the other triggers a virtual memory fault.
186186

tutorials/hello-camkes-1/hello-camkes-1.md

Lines changed: 66 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -5,21 +5,23 @@
55
-->
66

77
# Introduction to CAmkES
8+
89
/*? declare_task_ordering(['hello']) ?*/
910

10-
This tutorial is an introduction to
11-
CAmkES: bootstrapping a basic static CAmkES application, describing its
12-
components, and linking them together.
11+
This tutorial is an introduction to CAmkES: bootstrapping a basic static CAmkES
12+
application, describing its components, and linking them together.
1313

1414
Outcomes:
15+
1516
1. Understand the structure of a CAmkES application, as a described,
16-
well-defined, static system.
17+
well-defined, static system.
1718
2. Understand the file-layout of a CAmkES ADL project.
1819
3. Become acquainted with the basics of creating a practical CAmkES application.
1920

2021
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).
2122

2223
## Prerequisites
24+
2325
1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up.html)
2426
2. [CAmkES hello world tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-0.html)
2527

@@ -29,7 +31,7 @@ Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master
2931

3032
<details markdown='1'>
3133
<summary><em>Hint:</em> tutorial solutions</summary>
32-
<br>
34+
3335
All tutorials come with complete solutions. To get solutions run:
3436

3537
/*? macros.tutorial_init_with_solution("hello-camkes-1") ?*/
@@ -42,49 +44,47 @@ The fundamentals of CAmkES are the component, the interface and the connection.
4244

4345
### Components
4446

45-
*Components* are logical
46-
groupings of code and resources. They communicate with other component
47-
instances via well-defined interfaces which must be statically defined,
48-
over communication channels. This tutorial will lead you through the
49-
construction of a CAmkES application with two components: an Echo
50-
server, and its Client that makes calls to it. These components are
51-
defined when you initialise your build repository, found in
52-
the following camkes file:
47+
*Components* are logical groupings of code and resources. They communicate with
48+
other component instances via well-defined interfaces which must be statically
49+
defined, over communication channels. This tutorial will lead you through the
50+
construction of a CAmkES application with two components: an Echo server, and
51+
its Client that makes calls to it. These components are defined when you
52+
initialise your build repository, found in the following camkes file:
5353

5454
- `hello-camkes-1/hello-1.camkes`
5555

56-
Find the Component manual section here:
57-
<https://docs.sel4.systems/projects/camkes/manual.html#component>
56+
See also the [Component
57+
definition](https://docs.sel4.systems/projects/camkes/manual.html#component) in
58+
the CAmkES manual.
5859

5960
### Connections
6061

61-
The second fundamental component of CAmkES applications
62-
is the *Connection*: a connection is the representation of a method of
63-
communication between two software components in CAmkES. The underlying
64-
implementation may be shared memory, synchronous IPC, notifications or
65-
some other implementation-provided means. In this particular tutorial,
66-
we are using synchronous IPC. In implementation terms, this boils down
67-
to the `seL4_Call` syscall on seL4.
62+
The second fundamental component of CAmkES applications is the *Connection*: a
63+
connection is the representation of a method of communication between two
64+
software components in CAmkES. The underlying implementation may be shared
65+
memory, synchronous IPC, notifications or some other implementation-provided
66+
means. In this particular tutorial, we are using synchronous IPC. In
67+
implementation terms, this boils down to the `seL4_Call` syscall on seL4.
6868

69-
Find the "Connection" keyword manual section here:
70-
<https://docs.sel4.systems/projects/camkes/manual.html#connection>
69+
See also the [Connection
70+
keyword](https://docs.sel4.systems/projects/camkes/manual.html#connection) in
71+
the CAmkES manual.
7172

7273
### Interfaces
7374

74-
All communications over a CAmkES connection must be well
75-
defined: static systems' communications should be able to be reasoned
76-
about at build time. All the function calls which will be delivered over
77-
a communication channel then, also are well defined, and logically
78-
grouped so as to provide clear directional understanding of all
79-
transmissions over a connection. Components are connected together in
80-
CAmkES, yes -- but the interfaces that are exposed over each connection
81-
for calling by other components, are also described.
82-
83-
There are different
84-
kinds of interfaces:
85-
-Dataports,
86-
-Procedural interfaces,
87-
-and Notifications.
75+
All communications over a CAmkES connection must be well defined: static
76+
systems' communications should be able to be reasoned about at build time. All
77+
the function calls which will be delivered over a communication channel then,
78+
also are well defined, and logically grouped so as to provide clear directional
79+
understanding of all transmissions over a connection. Components are connected
80+
together in CAmkES, yes --- but the interfaces that are exposed over each
81+
connection for calling by other components, are also described.
82+
83+
There are different kinds of interfaces:
84+
85+
- Dataports,
86+
- Procedural interfaces,
87+
- and Notifications.
8888

8989
This tutorial will lead you through the construction of a Procedural
9090
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
9393
Procedure interface may be found here:
9494
`hello-camkes-1/interfaces/HelloSimple.idl4`
9595

96-
Find the "Procedure" keyword definition here:
97-
<https://docs.sel4.systems/projects/camkes/manual.html#procedure>
96+
See also the [Procedure
97+
keyword](https://docs.sel4.systems/projects/camkes/manual.html#procedure) in the
98+
CAmkES manual.
9899

99100
### Component source
100101

101-
Based on the ADL, CAmkES generates boilerplate which
102-
conforms to your system's architecture, and enables you to fill in the
103-
spaces with your program's logic. The two generated files in this
104-
tutorial application are, in accordance with the Components we have
105-
defined:
102+
Based on the ADL, CAmkES generates boilerplate which conforms to your system's
103+
architecture, and enables you to fill in the spaces with your program's logic.
104+
The two generated files in this tutorial application are, in accordance with the
105+
Components we have defined:
106106

107107
- `hello-camkes-1/components/Echo/src/echo.c`
108108
- `hello-camkes-1/components/Client/src/client.c`
@@ -127,8 +127,8 @@ instances of functions in an Interface with the Interface-instance's
127127
name. In the dual-function NIC device's case, it might have a
128128
`provides <INTERFACE_NAME> serial` and a `provides <INTERFACE_NAME> nic`.
129129
When a caller wants to call for the NIC-send, it would call,
130-
nic_send(), and when a caller wants to invoke the Serial-send, it would
131-
call, "serial_send()".
130+
`nic_send()`, and when a caller wants to invoke the Serial-send, it would
131+
call, `serial_send()`.
132132

133133
So if the `Hello` interface is provided once by `Echo` as `a`, you would
134134
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
143143
**Exercise** First modify `hello-1.camkes`. Define instances of `Echo` and `Client` in the
144144
`composition` section of the ADL.
145145

146-
```
146+
```c
147147
/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="define",completion="Booting all finished, dropped to user space") -*/
148148
assembly {
149149
composition {
@@ -155,7 +155,7 @@ assembly {
155155
<details markdown='1'>
156156
<summary><em>Quick solution</em></summary>
157157
158-
```
158+
```c
159159
/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="define") -*/
160160
assembly {
161161
composition {
@@ -164,6 +164,7 @@ assembly {
164164
component Echo echo;
165165
/*-- endfilter -*/
166166
```
167+
167168
</details>
168169

169170
### Add a connection
@@ -187,6 +188,7 @@ assembly {
187188
connection seL4RPCCall hello_con(from client.hello, to echo.hello);
188189
/*-- endfilter -*/
189190
```
191+
190192
</details>
191193
192194
### Define an interface
@@ -207,14 +209,16 @@ procedure HelloSimple {
207209
<details markdown='1'>
208210
<summary><em>Quick solution</em></summary>
209211

210-
```
212+
```c
211213
/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="interface") -*/
212214
void say_hello(in string str);
213215
/*-- endfilter -*/
214216
```
217+
215218
</details>
216219
217220
### Implement a RPC function
221+
218222
**Exercise** Implement the RPC hello function.
219223
220224
```c
@@ -236,14 +240,15 @@ procedure HelloSimple {
236240
<details markdown='1'>
237241
<summary><em>Quick solution</em></summary>
238242

239-
```
243+
```c
240244
/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="rpc") -*/
241245
/* Implement the RPC function. */
242246
void hello_say_hello(const char *str) {
243247
printf("Component %s saying: %s\n", get_instance_name(), str);
244248
}
245249
/*-- endfilter -*/
246250
```
251+
247252
</details>
248253
249254
### Invoke a RPC function
@@ -266,22 +271,22 @@ void hello_say_hello(const char *str) {
266271
<details markdown='1'>
267272
<summary><em>Quick solution</em></summary>
268273

269-
```
274+
```c
270275
/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="hello") -*/
271276
/* Invoke the RPC function */
272277
char *shello = "hello world";
273278
hello_say_hello(shello);
274279
/*-- endfilter -*/
275280
```
281+
276282
</details>
277283
278284
## Done
279285
280-
Now build and run the project, if it compiles: Congratulations! Be sure to read up on the keywords and
281-
structure of ADL: it's key to understanding CAmkES. And well done on
282-
writing your first CAmkES application.
286+
Now build and run the project. If it compiles: Congratulations!
283287
284288
/*-- filter ExcludeDocs() -*/
289+
285290
```c
286291
/*- filter File("components/Client/src/client.c") --*/
287292
/*
@@ -322,7 +327,7 @@ int run(void) {
322327

323328
```
324329

325-
```
330+
```c
326331
/*- filter File("hello-1.camkes") --*/
327332
/*
328333
* CAmkES tutorial part 1: components with RPC.
@@ -355,7 +360,8 @@ component Echo {
355360
}
356361
/*-- endfilter -*/
357362
```
358-
```
363+
364+
```c
359365
/*- filter File("interfaces/HelloSimple.idl4") --*/
360366
/* Simple RPC interface */
361367
procedure HelloSimple {
@@ -364,7 +370,8 @@ procedure HelloSimple {
364370

365371
/*-- endfilter -*/
366372
```
367-
```
373+
374+
```c
368375
/*- filter TaskCompletion("hello", TaskContentType.ALL) --*/
369376
Component echo saying: hello world
370377
/*-- endfilter -*/
@@ -395,4 +402,5 @@ GenerateCAmkESRootserver()
395402
/*? macros.cmake_check_script(state) ?*/
396403
/*-- endfilter -*/
397404
```
405+
398406
/*-- endfilter -*/

0 commit comments

Comments
 (0)