From 502c045155d773236d2a635712d64ebc312fb30b Mon Sep 17 00:00:00 2001
From: Birgit Brecknell Tutorials and other material to learn about seL4.
+ seL4 is a third-generation microkernel. It is broadly based on L4 and influenced by EROS. Like L4 it features abstractions for virtual address spaces, threads, IPC, and, unlike most earlier L4 kernels, an explicit in-kernel memory management model and capabilities for authorisation.
+
+ Authority in seL4 is conferred by possession of a capability. Capabilities are segregated and stored in capability address spaces composed of capability container objects called CNodes. seL4 has six system calls, of which five require possession of a capability (the sixth is a yield to the scheduler). The five system calls are IPC primitives that are used either to invoke services implemented by other processes (using capabilities to port-like endpoints that facilitate message passing), or invoke kernel services (using capabilities to kernel objects, such as a thread control block (TCB)). While the number of system calls is small, the kernel’s effective API is the sum of all the interfaces presented by all kernel object types.
+
+ Kernel memory management in seL4 is explicit. All kernel data structures are either statically allocated at boot time, or are dynamically-allocated first-class objects in the API. Kernel objects thus act as both inkernel data structures, and user-invoked fine-grained kernel services. Kernel objects include TCBs, CNodes, and level-1 and level-2 page tables (termed PageDirectories and PageTables).
+
+ Authority over free memory is encapsulated in an untyped memory object. Creating new kernel objects explicitly involves invoking the retype method of an untyped
+memory object, which allocates the memory for the object, initialises it, and returns a capability to the new object.
+
+ Virtual address spaces are formed by explicit manipulation of virtual-memoryrelated kernel objects: PageDirectories, PageTables, ASIDPools and Frames (mappable physical memory). As such, address spaces have no kernel-defined structure (except for a protected region reserved for the seL4 kernel itself). Whether the userlevel system is Exokernel like, a multi-server, or a para-virtualised monolithic OS is determined by user-level via a map and unmap interface to Frames and PageTables. The distribution of authority to the kernel virtual memory (VM) objects ultimately determines the scope of influence over virtual and physical memory.
+
+ Threads are the active entity in seL4. By associating a CNode and a virtual address space with a thread, user-level policies create high-level abstractions, such as processes or virtual machines.
+
+ IPC is supported in two forms: synchronous message passing via endpoints (portlike destinations without in-kernel buffering), and asynchronous notification via asynchronous endpoints (rendezvous objects consisting of a single in-kernel word that is used to combine IPC sends using a logical or). Remote procedure call semantics are facilitated over synchronous IPC via reply capabilities. Send capabilities are minted from an initial endpoint capability. Send capabilities feature an immutable badge which is used by the specific endpoint’s IPC recipients to distinguish which send capability (and thus which authority) was used to send a message. The unforgeable badge, represented by an integer value, is delivered with the message.
+
+ Exceptions are propagated via synchronous IPC to each thread’s exception handler (registered in the TCB via a capability to an endpoint). Similarly, page faults are also propagated using synchronous IPC to a thread’s page fault handler. Non-native system calls are treated as exceptions to support virtualisation.
+
+ Device Drivers run as user-mode applications that have access to device registers and memory, either by mapping the device into the virtual address space, or by controlled access to device ports on x86 hardware. seL4 provides a mechanism to receive notification of interrupts (via asynchronous IPC) and acknowledge their receipt.
+
+ The seL4 kernel runs on multiple platforms, and runs on common architectures like ARM and RiscV.
+
+ Because sel4 is small, a lot more needs to be done in user space and there are a lot more choices about how to do that. We'll start by building a simple system using the seL4 Microkit, which is a software development kit for building static systems on seL4.
+
+ Next: The seL4 microkit
+ Tutorials and other material to learn about seL4.
+ The seL4 Microkit is an operating system framework on top of seL4 provides a small set of simple abstractions that ease the design and implementation of statically structured systems on seL4, while still leveraging the kernel’s benefits of security and performance.
+
+ The Microkit is distributed as an SDK that integrates with the build system of your choice, significantly reducing the barrier to entry for new users of seL4.
+
+ Go to the Microkit tutorial
+
+
+ Previous: About seL4
+
+
+ Next: The seL4 microkit
+
@@ -35,5 +41,5 @@ memory object, which allocates the memory for the object, initialises it, and re
Because sel4 is small, a lot more needs to be done in user space and there are a lot more choices about how to do that. We'll start by building a simple system using the seL4 Microkit, which is a software development kit for building static systems on seL4.
- Next: The seL4 microkit
+ Next: seL4 microkit tutorial
The seL4 Microkit is an operating system framework on top of seL4 provides a small set of simple abstractions that ease the design and implementation of statically structured systems on seL4, while still leveraging the kernel’s benefits of security and performance.
- The Microkit is distributed as an SDK that integrates with the build system of your choice, significantly reducing the barrier to entry for new users of seL4.
+ The Microkit is distributed as an SDK that integrates with the build system of your choice, significantly reducing the barrier to entry for new users of seL4. We recommend it as the first tutorial, to familiarise new users with seL4 concepts.
- Go to the Microkit tutorial
+ After completing the Microkit tutorial, go to seL4 kernel tutorials for a deep dive into seL4 concepts.
+ Go to the Microkit tutorial
+
- Previous: About seL4
+ Previous: About seL4
- Next: The seL4 microkit
+ Next: seL4 kernel tutorials
+ Previous: Hello world
+
+ Next: Untyped
+
diff --git a/TutorialsReworked/seL4Kernel/hello-world.md b/TutorialsReworked/seL4Kernel/hello-world.md
index a365b07163..0a255af4a5 100644
--- a/TutorialsReworked/seL4Kernel/hello-world.md
+++ b/TutorialsReworked/seL4Kernel/hello-world.md
@@ -2,43 +2,16 @@
toc: true
layout: api
SPDX-License-Identifier: CC-BY-SA-4.0
-SPDX-FileCopyrightText: 2023 seL4 Project a Series of LF Projects, LLC.
+SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC.
---
# Hello, world!
-Outcomes
-
In this tutorial you will
- Run Hello, World! to ensure your setup is working correctly
- Become familiar with the jargon *root task*
- Build and simulate a seL4 project
- Have a basic understanding of the role of the `CMakeLists.txt` file in applications
-## Prerequisites
-
-- [Set up your machine](setting-up-your-machine).
-
-## Python Dependencies
-Additional python dependencies are required to build [tutorials](ReworkedTutorials). To install you can run:
-```
-pip install --user aenum
-pip install --user pyelftools
-```
-*Hint:* This step only needs to be done once, i.e. before doing your first tutorial
-
-## Get the code
-```
-mkdir sel4-tutorials-manifest
-cd sel4-tutorials-manifest
-repo init -u https://github.com/seL4/sel4-tutorials-manifest
-repo sync
-```
-
-`repo sync` may take a few moments to run
-
-*Hint:* The **Get the code** step only needs to be done once, i.e. before doing your first tutorial
-
-
## Building your first program
seL4 is a microkernel, not an operating system, and as a result only provides very minimal services.
@@ -54,20 +27,36 @@ all you need to do is build and run the tutorial.
```
cd sel4-tutorials-manifest
./init --tut hello-world
-
```
This step creates two new directories in `sel4-tutorials-manifest`, namely `hello-world` and `hello-world_build`
-We will now use two terminals, as described in [Setting up your machine](setting-up-your-machine#mapping-a-container).
+
+ Previous: Setting up your machine
+
+
+ Next: Capabilities
+
+ Previous: Untyped
+
+ Next: Threads
+
diff --git a/TutorialsReworked/seL4Kernel/overview.md b/TutorialsReworked/seL4Kernel/overview.md
new file mode 100644
index 0000000000..bdb2cbaa16
--- /dev/null
+++ b/TutorialsReworked/seL4Kernel/overview.md
@@ -0,0 +1,41 @@
+---
+layout: home
+title: seL4 Docs
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC.
+---
+
+
+ Previous: Microkit tutorial
+
+
+ Next: Setting up your machine
+
+ Previous: Overview
+
+
+ Next: Hello world
+
+ Previous: Capabilities
+
+ Next: Mapping
+
diff --git a/index.md b/index.md
index aba01de625..bb0a1c39ab 100644
--- a/index.md
+++ b/index.md
@@ -83,13 +83,14 @@ This documentation site is for cooperatively developing and sharing documentatio
More on Docker
+
+
+ **Available images**
+
+ All the prebuilt docker images are available on [DockerHub here](https://hub.docker.com/u/trustworthysystems)
+
+ These images are used by the Trustworthy Systems Continuous Integration (CI) software, and so represent a standard software setup we use.
+ The CI software always uses the `latest` docker image, but images are also tagged with the date they were built.
+
+ **More information**
+
+ You can find the dockerfiles and supporting Makefile [here](https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles)
+
+More on Repo
+
+[More details about on installing Repo](https://source.android.com/setup/develop#installing-repo).
+
+[seL4 Repo cheatsheet](../projects/buildsystem/repo-cheatsheet)
+More on host dependencies
+
+[A detailed guide on host dependencies](../projects/buildsystem/host-dependencies)
+Tutorials
+
+
+
+
+
+
+
+
+ About seL4
+
+Tutorials
-
The seL4 Microkit
+About seL4
The seL4 Microkit
+---
+layout: home
+title: seL4 Docs
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC.
+---
+The seL4 Microkit tutorial
Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut capabilities
+```
+Answers are also available in drop down menus under each section.
+Quick solution
+```c
+ size_t initial_cnode_object_size_bytes = initial_cnode_object_size * (1u << seL4_SlotBits);
+```
+Quick solution
+```c
+ /* use seL4_CNode_Copy to make another copy of the initial TCB capability to the last slot in the CSpace */
+ error = seL4_CNode_Copy(seL4_CapInitThreadCNode, last_slot, seL4_WordBits,
+ seL4_CapInitThreadCNode, first_free_slot, seL4_WordBits, seL4_AllRights);
+ ZF_LOGF_IF(error, "Failed to copy cap!");
+```
+Quick solution
+```c
+ // delete the created TCB capabilities
+ seL4_CNode_Revoke(seL4_CapInitThreadCNode, seL4_CapInitThreadTCB, seL4_WordBits);
+```
+Quick solution
+```c
+ // suspend the current thread
+ seL4_TCB_Suspend(seL4_CapInitThreadTCB);
+```
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut hello-world
+```
+This will generate another `hello-world` directory and `hello-world_build` directory, with unique names, e.g. `hello-world44h1po5q` and `hello-world44h1po5q_build`.
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut mapping
+```
+Answers are also available in drop down menus under each section.
+Overview
+We have developed a series of tutorials to on seL4 concepts. These assume a basic understanding of seL4, e.g. by having done the Microkit tutorial.
+
+Prerequisites
+Note that all of these tutorials require C programming
+experience and some understanding of operating systems and computer
+architecture. Suggested resources for these include:
+
+- C programming language
+ - [C tutorial](https://www.cprogramming.com/tutorial/c-tutorial.html)
+- Operating Systems:
+ - [Modern Operating Systems (book)](https://www.amazon.com/Modern-Operating-Systems-Andrew-Tanenbaum/dp/013359162X)
+ - [COMP3231 at UNSW](http://www.cse.unsw.edu.au/~cs3231)
+- Computer Architecture
+ - [Computer Architecture (wikipedia)](https://en.wikipedia.org/wiki/Computer_architecture)
+ - [Instruction Set Architecture (wikipedia)](https://en.wikipedia.org/wiki/Instruction_set_architecture)
+
+Resources
+We recommend having access to the seL4 manual and the API references.
+
+
+Getting help
+* [FAQ](https://docs.sel4.systems/FrequentlyAskedQuestions)
+* [Debugging guide](https://docs.sel4.systems/DebuggingGuide.html)
+* [seL4 Discourse forum](https://sel4.discourse.group)
+* [Developer's mailing list](https://lists.sel4.systems/postorius/lists/devel.sel4.systems/)
+* [Mattermost Channel](https://mattermost.trustworthy.systems/sel4-external/)
+
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut untyped
+```
+Answers are also available in drop down menus under each section.
+Quick solution
+```c
+ // seL4_EndpointBits and seL4_NotificationBits are both less than seL4_TCBBits, which
+ // means that all objects together fit into the size of two TCBs, or 2^(seL4_TCBBits + 1):
+ seL4_Word untyped_size_bits = seL4_TCBBits + 1;
+```
+Quick solution
+```c
+ /* create a TCB in CSlot child_tcb */
+ seL4_Untyped_Retype(child_untyped, seL4_TCBObject, 0, seL4_CapInitThreadCNode, 0, 0, child_tcb, 1);
+```
+Quick solution
+```c
+ /* create an endpoint in CSlot child_ep */
+ seL4_Untyped_Retype(child_untyped, seL4_EndpointObject, 0, seL4_CapInitThreadCNode, 0, 0, child_ep, 1);
+```
+Quick solution
+```c
+ // create a notification object in CSlot child_ntfn
+ seL4_Untyped_Retype(child_untyped, seL4_NotificationObject, 0, seL4_CapInitThreadCNode, 0, 0, child_ntfn, 1);
+```
+Quick solution
+```c
+ // revoke the child untyped
+ error = seL4_CNode_Revoke(seL4_CapInitThreadCNode, child_untyped, seL4_WordBits);
+ assert(error == seL4_NoError);
+```
+
+
{% endif %}
+
+{% if page_url[1] == "TutorialsReworked" %}
+
+{% endif %}
+
From c6e88b037bae950350d1f70f92cc97b400d395e1 Mon Sep 17 00:00:00 2001
From: Birgit Brecknell Quick solution
+```c
+ // TODO map a page directory object
+ error = seL4_X86_PageDirectory_Map(pd,seL4_CapInitThreadVSpace, TEST_VADDR, seL4_X86_Default_VMAttributes);
+ assert(error == seL4_NoError);
+```
+Quick solution
+```c
+ // map a page table object
+ error = seL4_X86_PageTable_Map(pt, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_X86_Default_VMAttributes);
+ assert(error == seL4_NoError);
+```
+Quick solution
+```c
+ // remap the page
+ error = seL4_X86_Page_Map(frame, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_ReadWrite, seL4_X86_Default_VMAttributes);
+ assert(error == seL4_NoError);
+```
+
- Next: seL4 microkit tutorial + Next tutorial: seL4 microkit tutorial
\ No newline at end of file diff --git a/TutorialsReworked/GettingStarted/microkit.md b/TutorialsReworked/GettingStarted/microkit.md index 6b78b95314..4df6163097 100644 --- a/TutorialsReworked/GettingStarted/microkit.md +++ b/TutorialsReworked/GettingStarted/microkit.md @@ -1,6 +1,6 @@ --- -layout: home -title: seL4 Docs +toc: true +layout: project SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. --- @@ -18,8 +18,5 @@ SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. Go to the Microkit tutorial- Previous: About seL4 -
-
- Next: seL4 kernel tutorials + Next tutorial: seL4 kernel tutorials
\ No newline at end of file diff --git a/TutorialsReworked/seL4Kernel/capabilities.md b/TutorialsReworked/seL4Kernel/capabilities.md index b3ef3468fa..67d2d736bf 100644 --- a/TutorialsReworked/seL4Kernel/capabilities.md +++ b/TutorialsReworked/seL4Kernel/capabilities.md @@ -374,8 +374,5 @@ to become more familiar with CSpaces.- Previous: Hello world -
-- Next: Untyped + Next tutorial: Untyped
diff --git a/TutorialsReworked/seL4Kernel/hello-world.md b/TutorialsReworked/seL4Kernel/hello-world.md index 54cdb74595..aac5611519 100644 --- a/TutorialsReworked/seL4Kernel/hello-world.md +++ b/TutorialsReworked/seL4Kernel/hello-world.md @@ -204,8 +204,5 @@ Hello, World! Second hello ```
- Previous: Setting up your machine -
-
- Next: Capabilities + Next tutorial: Capabilities
\ No newline at end of file diff --git a/TutorialsReworked/seL4Kernel/mapping.md b/TutorialsReworked/seL4Kernel/mapping.md index ae4bdb9322..73ca8e4e3e 100644 --- a/TutorialsReworked/seL4Kernel/mapping.md +++ b/TutorialsReworked/seL4Kernel/mapping.md @@ -240,8 +240,5 @@ to become more familiar with virtual memory management on seL4. * Create a generic function for converting from `seL4_MappingFailedLookupLevel` to the required seL4 object.- Previous: Untyped -
-- Next: Threads + Next tutorial: Threads
diff --git a/TutorialsReworked/seL4Kernel/overview.md b/TutorialsReworked/seL4Kernel/overview.md index bdb2cbaa16..ce8982d496 100644 --- a/TutorialsReworked/seL4Kernel/overview.md +++ b/TutorialsReworked/seL4Kernel/overview.md @@ -1,6 +1,6 @@ --- -layout: home -title: seL4 Docs +toc: true +layout: project SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. --- @@ -34,8 +34,5 @@ We recommend having access to the Microkit tutorial -
-
- Next: Setting up your machine + Next tutorial: Setting up your machine
\ No newline at end of file diff --git a/TutorialsReworked/seL4Kernel/setting-up.md b/TutorialsReworked/seL4Kernel/setting-up.md index e495e62a35..e28fc657c6 100644 --- a/TutorialsReworked/seL4Kernel/setting-up.md +++ b/TutorialsReworked/seL4Kernel/setting-up.md @@ -254,10 +254,6 @@ repo sync *Hint:* The **Get the code** step only needs to be done once, i.e. before doing your first tutorial. - -- Previous: Overview -
- Next: Hello world + Next tutorial: Hello world
diff --git a/TutorialsReworked/seL4Kernel/untyped.md b/TutorialsReworked/seL4Kernel/untyped.md index 40c4c7f454..2959cd1faf 100644 --- a/TutorialsReworked/seL4Kernel/untyped.md +++ b/TutorialsReworked/seL4Kernel/untyped.md @@ -356,8 +356,5 @@ to become more familiar with untyped objects and memory allocation in seL4. * Create a simple object allocator for allocating seL4 objects.- Previous: Capabilities -
-- Next: Mapping + Next tutorial: Mapping
diff --git a/_includes/nav-sidebar.html b/_includes/nav-sidebar.html index f43bfab129..82c6176a39 100644 --- a/_includes/nav-sidebar.html +++ b/_includes/nav-sidebar.html @@ -11,7 +11,7 @@
@@ -60,7 +60,7 @@ {% assign tutorials = site.pages | where_exp: 'page', 'page.tutorial' | sort: 'tutorial-order' %} {% for t in tutorials %}- Next tutorial: Untyped -
+Next tutorial: Untyped diff --git a/TutorialsReworked/seL4Kernel/hello-world.md b/TutorialsReworked/seL4Kernel/hello-world.md index aac5611519..3547daa7ca 100644 --- a/TutorialsReworked/seL4Kernel/hello-world.md +++ b/TutorialsReworked/seL4Kernel/hello-world.md @@ -203,6 +203,5 @@ On success, you should see the following: Hello, World! Second hello ``` -
- Next tutorial: Capabilities -
\ No newline at end of file + +Next tutorial: Capabilities \ No newline at end of file diff --git a/TutorialsReworked/seL4Kernel/ipc.md b/TutorialsReworked/seL4Kernel/ipc.md index e69de29bb2..ae8314e0fd 100644 --- a/TutorialsReworked/seL4Kernel/ipc.md +++ b/TutorialsReworked/seL4Kernel/ipc.md @@ -0,0 +1,363 @@ +--- +toc: true +layout: project +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +--- +# IPC +This tutorial is about interprocess communication (IPC), the microkernel mechanism for synchronous transmission of small amounts of data. + +You will learn +1. How to use IPC to send data and capabilities between processes. +2. The jargon *cap transfer*. +3. How to to differentiate requests via badged capabilities. +4. Design protocols that use the IPC fastpath. + + +## Initialising + +```sh +# For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/#get-the-code +# +# Follow these instructions to initialise the tutorial +# initialising the build directory with a tutorial exercise +./init --tut ipc +# building the tutorial exercise +cd ipc_build +ninja +``` + +- Next tutorial: Threads -
+Next tutorial: Threads
diff --git a/TutorialsReworked/seL4Kernel/notifications.md b/TutorialsReworked/seL4Kernel/notifications.md
index e69de29bb2..142a3b6fe7 100644
--- a/TutorialsReworked/seL4Kernel/notifications.md
+++ b/TutorialsReworked/seL4Kernel/notifications.md
@@ -0,0 +1,224 @@
+---
+toc: true
+layout: project
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC.
+---
+
+# Notifications and shared memory
+This tuotorial covers notification objects.
+
+You will learn how to:
+1. Set up shared memory between tasks.
+2. Use notification objects for synchronisation between tasks.
+3. Use badges to differentiate notifications.
+
+## Initialising
+
+```sh
+# For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/#get-the-code
+#
+# Follow these instructions to initialise the tutorial
+# initialising the build directory with a tutorial exercise
+./init --tut notifications
+# building the tutorial exercise
+cd notifications_build
+ninja
+```
+
+
- Next tutorial: Mapping
-
+Next tutorial: Mapping
diff --git a/_includes/nav-sidebar.html b/_includes/nav-sidebar.html
index 82c6176a39..f3f74ddf81 100644
--- a/_includes/nav-sidebar.html
+++ b/_includes/nav-sidebar.html
@@ -105,5 +105,10 @@
The seL4 Microkit is an operating system framework on top of seL4 provides a small set of simple abstractions that ease the design and implementation of statically structured systems on seL4, while still leveraging the kernel’s benefits of security and performance.
Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut notifications
+```
+Answers are also available in drop down menus under each section.
+Get CapDL
+The capDL loader parses
+a static description of the system and the relevant ELF binaries.
+It is primarily used in [Camkes](https://docs.sel4.systems/CAmkES/) projects
+but we also use it in the tutorials to reduce redundant code.
+The program that you construct will end up with its own CSpace and VSpace, which are separate
+from the root task, meaning CSlots like `seL4_CapInitThreadVSpace` have no meaning
+in applications loaded by the capDL loader.
+
+More information about CapDL projects can be found [here](https://docs.sel4.systems/CapDL.html).
+
+For this tutorial clone the [CapDL repo](https://github.com/sel4/capdl). This can be added in a directory that is adjacent to the tutorials-manifest directory.
+Quick solution
+```c
+ error = seL4_CNode_Copy(cnode, mapping_2, seL4_WordBits,
+ cnode, buf2_frame_cap, seL4_WordBits, seL4_AllRights);
+ ZF_LOGF_IFERR(error, "Failed to copy cap");
+```
+Quick solution
+```c
+ seL4_Signal(buf1_empty);
+ seL4_Signal(buf2_empty);
+```
+Quick solution
+```c
+ if (badge & 0b01) {
+ assert(*buf1 == 1);
+ *buf1 = 0;
+ seL4_Signal(buf1_empty);
+ }
+ if (badge & 0b10) {
+ assert(*buf2 == 2);
+ *buf2 = 0;
+ seL4_Signal(buf2_empty);
+ }
+```
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut threads
+```
+Answers are also available in drop down menus under each section.
+Quick solution
+```c
+ seL4_Error result = seL4_Untyped_Retype(tcb_untyped, seL4_TCBObject, seL4_TCBBits, root_cnode, 0, 0, tcb_cap_slot, 1);
+```
+Quick solution
+```c
+ result = seL4_TCB_Configure(tcb_cap_slot, seL4_CapNull, root_cnode, 0, root_vspace, 0, (seL4_Word) thread_ipc_buff_sym, tcb_ipc_frame);
+```
+Quick solution
+```c
+ result = seL4_TCB_SetPriority(tcb_cap_slot, root_tcb, 254);
+```
+Quick solution
+```c
+ // use valid instruction pointer
+ sel4utils_set_instruction_pointer(®s, (seL4_Word) new_thread);
+ // use valid stack pointer
+ sel4utils_set_stack_pointer(®s, tcb_stack_top);
+ // fix parameters to this invocation
+ error = seL4_TCB_WriteRegisters(tcb_cap_slot, 0, 0, sizeof(regs)/sizeof(seL4_Word), ®s);
+```
+Quick solution
+```c
+ error = seL4_TCB_Resume(tcb_cap_slot);
+```
+Quick solution
+```c
+ sel4utils_arch_init_local_context((void*)new_thread,
+ (void *)1, (void *)2, (void *)3,
+ (void *)tcb_stack_top, ®s);
+ error = seL4_TCB_WriteRegisters(tcb_cap_slot, 0, 0, sizeof(regs)/sizeof(seL4_Word), ®s);
+
+```
+Quick solution
+Fix `sel4utils_arch_init_local_context`
+```c
+ sel4utils_arch_init_local_context((void*)new_thread,
+ (void *)1, (void *)&data, (void *)3,
+ (void *)tcb_stack_top, ®s);
+```
+Quick solution
+Create a new function
+```c
+ int call_once(int arg) {
+ printf("Hello 3 %d\n", arg);
+ }
+
+```
+and fix `sel4utils_arch_init_local_context`
+```c
+ sel4utils_arch_init_local_context((void*)new_thread,
+ (void *)call_once, (void *)&data, (void *)3,
+ (void *)tcb_stack_top, ®s);
+```
+
+
{% endif %}
From f918f4af7e5697b5681d033cc5eca3706597b9dd Mon Sep 17 00:00:00 2001
From: Birgit Brecknell Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut dynamic-1
+```
+Answers are also available in drop down menus under each section.
+Quick solution
+```c
+ info = platsupport_get_bootinfo();
+ ZF_LOGF_IF(info == NULL, "Failed to get bootinfo.");
+```
+Quick solution
+```c
+ simple_default_init_bootinfo(&simple, info);
+```
+Quick solution
+```c
+ simple_print(&simple);
+```
+Quick solution
+```c
+ allocman = bootstrap_use_current_simple(&simple, ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool);
+ ZF_LOGF_IF(allocman == NULL, "Failed to initialize alloc manager.\n"
+ "\tMemory pool sufficiently sized?\n"
+ "\tMemory pool pointer valid?\n");
+```
+Quick solution
+```c
+ allocman_make_vka(&vka, allocman);
+```
+Quick solution
+```c
+ cspace_cap = simple_get_cnode(&simple);
+```
+Quick solution
+```c
+ pd_cap = simple_get_pd(&simple);
+```
+Quick solution
+```c
+ error = vka_alloc_tcb(&vka, &tcb_object);
+ ZF_LOGF_IFERR(error, "Failed to allocate new TCB.\n"
+ "\tVKA given sufficient bootstrap memory?");
+```
+Quick solution
+```c
+ error = seL4_TCB_Configure(tcb_object.cptr, seL4_CapNull, cspace_cap, seL4_NilData, pd_cap, seL4_NilData, 0, 0);
+ ZF_LOGF_IFERR(error, "Failed to configure the new TCB object.\n"
+ "\tWe're running the new thread with the root thread's CSpace.\n"
+ "\tWe're running the new thread in the root thread's VSpace.\n"
+ "\tWe will not be executing any IPC in this app.\n");
+```
+Quick solution
+```c
+ NAME_THREAD(tcb_object.cptr, "dynamic-1: thread_2");
+```
+Quick solution
+```c
+ sel4utils_set_instruction_pointer(®s, (seL4_Word)thread_2);
+
+```
+Quick solution
+```c
+ sel4utils_set_stack_pointer(®s, thread_2_stack_top);
+```
+Quick solution
+```c
+ error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, ®s);
+ ZF_LOGF_IFERR(error, "Failed to write the new thread's register set.\n"
+ "\tDid you write the correct number of registers? See arg4.\n");
+```
+Quick solution
+```c
+ error = seL4_TCB_Resume(tcb_object.cptr);
+ ZF_LOGF_IFERR(error, "Failed to start new thread.\n");
+```
+Quick solution
+```c
+ printf("thread_2: hallo wereld\n");
+```
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut dynamic-2
+```
+Answers are also available in drop down menus under each section.
+Quick solution
+```c
+ error = vka_alloc_frame(&vka, IPCBUF_FRAME_SIZE_BITS, &ipc_frame_object);
+ ZF_LOGF_IFERR(error, "Failed to alloc a frame for the IPC buffer.\n"
+ "\tThe frame size is not the number of bytes, but an exponent.\n"
+ "\tNB: This frame is not an immediately usable, virtually mapped page.\n")
+```
+Quick solution
+```c
+ error = seL4_ARCH_Page_Map(ipc_frame_object.cptr, pd_cap, ipc_buffer_vaddr,
+ seL4_AllRights, seL4_ARCH_Default_VMAttributes);
+```
+Quick solution
+```c
+ error = vka_alloc_page_table(&vka, &pt_object);
+ ZF_LOGF_IFERR(error, "Failed to allocate new page table.\n");
+```
+Quick solution
+```c
+ error = seL4_ARCH_PageTable_Map(pt_object.cptr, pd_cap,
+ ipc_buffer_vaddr, seL4_ARCH_Default_VMAttributes);
+ ZF_LOGF_IFERR(error, "Failed to map page table into VSpace.\n"
+ "\tWe are inserting a new page table into the top-level table.\n"
+ "\tPass a capability to the new page table, and not for example, the IPC buffer frame vaddr.\n")
+```
+Quick solution
+```c
+ error = seL4_ARCH_Page_Map(ipc_frame_object.cptr, pd_cap,
+ ipc_buffer_vaddr, seL4_AllRights, seL4_ARCH_Default_VMAttributes);
+ ZF_LOGF_IFERR(error, "Failed again to map the IPC buffer frame into the VSpace.\n"
+ "\t(It's not supposed to fail.)\n"
+ "\tPass a capability to the IPC buffer's physical frame.\n"
+ "\tRevisit the first seL4_ARCH_Page_Map call above and double-check your arguments.\n");
+```
+Quick solution
+```c
+ error = vka_alloc_endpoint(&vka, &ep_object);
+ ZF_LOGF_IFERR(error, "Failed to allocate new endpoint object.\n");
+```
+Quick solution
+```c
+ error = vka_mint_object(&vka, &ep_object, &ep_cap_path, seL4_AllRights,
+ EP_BADGE);
+ ZF_LOGF_IFERR(error, "Failed to mint new badged copy of IPC endpoint.\n"
+ "\tseL4_Mint is the backend for vka_mint_object.\n"
+ "\tseL4_Mint is simply being used here to create a badged copy of the same IPC endpoint.\n"
+ "\tThink of a badge in this case as an IPC context cookie.\n");
+```
+Quick solution
+```c
+ tag = seL4_MessageInfo_new(0, 0, 0, 1);
+ seL4_SetMR(0, MSG_DATA);
+```
+Quick solution
+```c
+ tag = seL4_Call(ep_cap_path.capPtr, tag);
+```
+Quick solution
+```c
+ msg = seL4_GetMR(0);
+```
+Quick solution
+```c
+ tag = seL4_Recv(ep_object.cptr, &sender_badge);
+```
+Quick solution
+```c
+ ZF_LOGF_IF(sender_badge != EP_BADGE,
+ "Badge on the endpoint was not what was expected.\n");
+
+ ZF_LOGF_IF(seL4_MessageInfo_get_length(tag) != 1,
+ "Length of the data send from root thread was not what was expected.\n"
+ "\tHow many registers did you set with seL4_SetMR, within the root thread?\n");
+```
+Quick solution
+```c
+ msg = seL4_GetMR(0);
+ printf("thread_2: got a message %#" PRIxPTR " from %#" PRIxPTR "\n", msg, sender_badge);
+```
+Quick solution
+```c
+ seL4_SetMR(0, msg);
+```
+Quick solution
+```c
+ seL4_ReplyRecv(ep_object.cptr, tag, &sender_badge);
+```
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut dynamic-3
+```
+Answers are also available in drop down menus under each section.
+Quick solution
+```c
+ error = sel4utils_bootstrap_vspace_with_bootinfo_leaky(&vspace,
+ &data, simple_get_pd(&simple), &vka, info);
+ ZF_LOGF_IFERR(error, "Failed to prepare root thread's VSpace for use.\n"
+ "\tsel4utils_bootstrap_vspace_with_bootinfo reserves important vaddresses.\n"
+ "\tIts failure means we can't safely use our vaddrspace.\n");
+```
+Quick solution
+```c
+ sel4utils_process_t new_process;
+
+ sel4utils_process_config_t config = process_config_default_simple(&simple, APP_IMAGE_NAME, APP_PRIORITY);
+ error = sel4utils_configure_process_custom(&new_process, &vka, &vspace, config);
+ ZF_LOGF_IFERR(error, "Failed to spawn a new thread.\n"
+ "\tsel4utils_configure_process expands an ELF file into our VSpace.\n"
+ "\tBe sure you've properly configured a VSpace manager using sel4utils_bootstrap_vspace_with_bootinfo.\n"
+ "\tBe sure you've passed the correct component name for the new thread!\n");
+```
+Quick solution
+```c
+ cspacepath_t ep_cap_path;
+ seL4_CPtr new_ep_cap = 0;
+ vka_cspace_make_path(&vka, ep_object.cptr, &ep_cap_path);
+```
+Quick solution
+```c
+ new_ep_cap = sel4utils_mint_cap_to_process(&new_process, ep_cap_path,
+ seL4_AllRights, EP_BADGE);
+
+ ZF_LOGF_IF(new_ep_cap == 0, "Failed to mint a badged copy of the IPC endpoint into the new thread's CSpace.\n"
+ "\tsel4utils_mint_cap_to_process takes a cspacepath_t: double check what you passed.\n");
+```
+Quick solution
+```c
+ new_ep_cap = sel4utils_mint_cap_to_process(&new_process, ep_cap_path,
+ seL4_AllRights, EP_BADGE);
+ seL4_Word argc = 1;
+ char string_args[argc][WORD_STRING_SIZE];
+ char* argv[argc];
+ sel4utils_create_word_args(string_args, argv, argc, new_ep_cap);
+
+ error = sel4utils_spawn_process_v(&new_process, &vka, &vspace, argc, (char**) &argv, 1);
+ ZF_LOGF_IFERR(error, "Failed to spawn and start the new thread.\n"
+ "\tVerify: the new thread is being executed in the root thread's VSpace.\n"
+ "\tIn this case, the CSpaces are different, but the VSpaces are the same.\n"
+ "\tDouble check your vspace_t argument.\n");
+```
+Quick solution
+```c
+ tag = seL4_Recv(ep_cap_path.capPtr, &sender_badge);
+ /* make sure it is what we expected */
+ ZF_LOGF_IF(sender_badge != EP_BADGE,
+ "The badge we received from the new thread didn't match our expectation.\n");
+
+ ZF_LOGF_IF(seL4_MessageInfo_get_length(tag) != 1,
+ "Response data from the new process was not the length expected.\n"
+ "\tHow many registers did you set with seL4_SetMR within the new process?\n");
+```
+Quick solution
+```c
+ seL4_ReplyRecv(ep_cap_path.capPtr, tag, &sender_badge);
+```
+Quick solution
+```c
+ seL4_CPtr ep = (seL4_CPtr) atol(argv[0]);
+ tag = seL4_Call(ep, tag);
+```
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut fault-handlers
+```
+Get CapDL
+The capDL loader parses
+a static description of the system and the relevant ELF binaries.
+It is primarily used in [Camkes](https://docs.sel4.systems/CAmkES/) projects
+but we also use it in the tutorials to reduce redundant code.
+The program that you construct will end up with its own CSpace and VSpace, which are separate
+from the root task, meaning CSlots like `seL4_CapInitThreadVSpace` have no meaning
+in applications loaded by the capDL loader.
+
+More information about CapDL projects can be found [here](https://docs.sel4.systems/CapDL.html).
+
+For this tutorial clone the [CapDL repo](https://github.com/sel4/capdl). This can be added in a directory that is adjacent to the tutorials-manifest directory.
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut interrupts
+```
+Answers are also available in drop down menus under each section.
+Get CapDL
+The capDL loader parses
+a static description of the system and the relevant ELF binaries.
+It is primarily used in [Camkes](https://docs.sel4.systems/CAmkES/) projects
+but we also use it in the tutorials to reduce redundant code.
+The program that you construct will end up with its own CSpace and VSpace, which are separate
+from the root task, meaning CSlots like `seL4_CapInitThreadVSpace` have no meaning
+in applications loaded by the capDL loader.
+
+More information about CapDL projects can be found [here](https://docs.sel4.systems/CapDL.html).
+
+For this tutorial clone the [CapDL repo](https://github.com/sel4/capdl). This can be added in a directory that is adjacent to the tutorials-manifest directory.
+Quick solution
+```c
+ error = seL4_IRQControl_Get(irq_control, TTC0_TIMER1_IRQ, cnode, irq_handler, seL4_WordBits);
+ ZF_LOGF_IF(error, "Failed to get IRQ capability");
+```
+Quick solution
+```c
+ error = seL4_IRQHandler_SetNotification(irq_handler, ntfn);
+ ZF_LOGF_IF(error, "Failed to set notification");
+```
+Quick solution
+```c
+ error = seL4_IRQHandler_Ack(irq_handler);
+ ZF_LOGF_IF(error, "Failed to ack irq");
+```
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut hello-camkes-1
+```
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut dynamic-4
+```
+Answers are also available in drop down menus under each section.
+Quick solution
+```c
+ error = vka_alloc_notification(&vka, &ntfn_object);
+ assert(error == 0);
+```
+Quick solution
+```c
+ error = ltimer_default_init(&timer, ops, NULL, NULL);
+ assert(error == 0);
+```
+Quick solution
+```c
+ error = ltimer_set_timeout(&timer, NS_IN_MS, TIMEOUT_PERIODIC);
+ assert(error == 0);
+```
+Quick solution
+```c
+ seL4_Word badge;
+ seL4_Wait(ntfn_object.cptr, &badge);
+ sel4platsupport_irq_handle(&ops.irq_ops, MINI_IRQ_INTERFACE_NTFN_ID, badge);
+ count++;
+ if (count == 1000 * msg) {
+ break;
+ }
+```
+Quick solution
+```c
+ ltimer_destroy(&timer);
+```
+The seL4 Microkit tutorial
+Using the seL4 Microkit tutorial to get started with seL4
Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut mcs
+```
+Quick solution
+```c
+ error = seL4_SchedControl_Configure(sched_control, sched_context, 0.9 * US_IN_S, 1 * US_IN_S, 0, 0);
+ ZF_LOGF_IF(error != seL4_NoError, "Failed to configure schedcontext");
+```
+Quick solution
+```c
+ error = seL4_SchedContext_Unbind(sched_context);
+ ZF_LOGF_IF(error, "Failed to unbind sched_context");
+```
+Quick solution
+```c
+ error = seL4_SchedContext_Bind(sched_context, sender_tcb);
+ ZF_LOGF_IF(error != seL4_NoError, "Failed to bind schedcontext");
+```
+Quick solution
+```c
+ error = seL4_SchedControl_Configure(sched_control, sched_context, 0.9 * US_IN_S, 1 * US_IN_S, 6, 0);
+ ZF_LOGF_IF(error != seL4_NoError, "Failed to configure schedcontext");
+```
+Quick solution
+```c
+ error = seL4_SchedContext_Bind(sched_context, server_tcb);
+ ZF_LOGF_IF(error != seL4_NoError, "Failed to bind sched_context to server_tcb");
+```
+Quick solution
+```c
+ error = seL4_SchedControl_Configure(sched_control, sched_context, 500, US_IN_S, 0, 5);
+ ZF_LOGF_IF(error != seL4_NoError, "Failed to configure sched_context");
+```
+Quick solution
+```c
+```
+
diff --git a/index.md b/index.md
index 34b8221502..7c0114d88e 100644
--- a/index.md
+++ b/index.md
@@ -83,7 +83,7 @@ This documentation site is for cooperatively developing and sharing documentatio
+
From a311549bf14acaf9c1847510eac864ba4507fced Mon Sep 17 00:00:00 2001
From: Birgit Brecknell
From cb2fc679bf5cf0965056b1c825a030ba9f5f097c Mon Sep 17 00:00:00 2001
From: Birgit Brecknell Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut hello-camkes-1
+```
+
+
+ Quick solution
+```
+ assembly {
composition {
component EmptyComponent empty;
component Client client;
component Echo echo;
```
+Quick solution
+```
+ connection seL4RPCCall hello_con(from client.hello, to echo.hello);
+```
+Quick solution
+```
+ void say_hello(in string str);
+```
+Quick solution
+```
void hello_say_hello(const char *str) {
printf("Component %s saying: %s\n", get_instance_name(), str);
}
```
+Quick solution
+```
+ char *shello = "hello world";
+ hello_say_hello(shello);
+```
+Quick solution
+```
+```
+
All tutorials come with complete solutions. To get solutions run:
```
-./init --solution --tut hello-camkes-1
+./init --solution --tut hello-camkes-2
+```
+Quick solution
+```
```
Quick solution
+```c
+ /* TASK 10: emit event to signal that the data is available */
+ /* hint 1: use the function Quick solution
+```c
+ /* TASK 11: wait to get an event back signalling that the reply data is avaialble */
+ /* hint 1: use the function Quick solution
+```c
+ /* TASK 14: emit event to signal that the data is available */
+ /* hint 1: we've already done this before */
+
+ echo_emit();
+```
+Quick solution
+```c
+ /* TASK 15: wait to get an event back signalling that data has been read */
+ /* hint 1: we've already done this before */
+
+ client_wait();
+```
+Quick solution
+```c
+ /* TASK 22: notify the client that there is new data available for it */
+ /* hint 1: use the function Quick solution
+```c
+ /* TASK 25: notify the client that we are done reading the data */
+ /* hint 1: use the function Quick solution
+```c
+ /* this function is invoked to initialise the echo event interface before it
+ * becomes active. */
+ /* TASK 17: replace "echo" with the actual name of the "consumes" event interface */
+ /* hint 1: use the interface name as defined in Echo.camkes.
+ * For example if you defined it as "consumes TheEvent c_event" then you would use "c_event".
+ */
+ void echo__init(void) {
+ /* TASK 18: register the first callback handler for this interface */
+ /* hint 1: use the function Quick solution
+```c
+ /* TASK 21: register the second callback for this event. */
+ /* hint 1: use the function Quick solution
+```c
+ /* TASK 24: register the original callback handler for this event */
+ /* hint 1: use the function Quick solution
+```
+```
+Quick solution
+```
+```
+Quick solution
+```
+```
+Quick solution
+```c
+ /* TASK 9: copy strings to an untyped dataport */
+ /* hint 1: use the "Buf" dataport as defined in the Client.camkes file
+ * hint 2: to access the dataport use the interface name as defined in Client.camkes.
+ * For example if you defined it as "dataport Buf d" then you would use "d" to refer to the dataport in C.
+ * hint 3: first write the number of strings (NUM_STRINGS) to the dataport
+ * hint 4: then copy all the strings from "s_arr" to the dataport.
+ * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+ */
+
+ int *n = (int*)d;
+ *n = NUM_STRINGS;
+ char *str = (char*)(n + 1);
+ for (int i = 0; i < NUM_STRINGS; i++) {
+ strcpy(str, s_arr[i]);
+ str += strlen(str) + 1;
+ }
+
+```
+Quick solution
+```
+ /* 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
+ * hint 2: to access the dataport use the interface name as defined in Client.camkes.
+ * For example if you defined it as "dataport str_buf_t d_typed" then you would use "d_typed" to refer to the dataport in C.
+ * hint 3: for the definition of "str_buf_t" see "str_buf.h".
+ * hint 4: use the "n" field to determine the number of strings in the dataport
+ * hint 5: print out the specified number of strings from the "str" field
+ * hint 6: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+ */
+
+ for (int i = 0; i < d_typed->n; i++) {
+ printf("%s: string %d (%p): \"%s\"\n", get_instance_name(), i, d_typed->str[i], d_typed->str[i]);
+ }
+```
+Quick solution
+```
+ /* TASK 13: send the data over again, this time using two dataports, one
+ * untyped dataport containing the data, and one typed dataport containing
+ * dataport pointers pointing to data in the untyped, dataport.
+ */
+ /* hint 1: for the untyped dataport use the "Buf" dataport as defined in the Client.camkes file
+ * hint 2: for the typed dataport use the "ptr_buf_t" dataport as defined in the Client.camkes file
+ * hint 3: for the definition of "ptr_buf_t" see "str_buf.h".
+ * hint 4: copy all the strings from "s_arr" into the untyped dataport
+ * hint 5: use the "n" field of the typed dataport to specify the number of dataport pointers (NUM_STRINGS)
+ * hint 6: use the "ptr" field of the typed dataport to store the dataport pointers
+ * hint 7: use the function "dataport_wrap_ptr()" to create a dataport pointer from a regular pointer
+ * hint 8: the dataport pointers should point into the untyped dataport
+ * hint 9: for more information about dataport pointers see: https://github.com/seL4/camkes-tool/blob/master/docs/index.md
+ */
+
+ d_ptrs->n = NUM_STRINGS;
+ str = (char*)d;
+ for (int i = 0; i < NUM_STRINGS; i++) {
+ strcpy(str, s_arr[i]);
+ d_ptrs->ptr[i] = dataport_wrap_ptr(str);
+ str += strlen(str) + 1;
+ }
+```
+Quick solution
+```c
+ /* TASK 19: read some data from the untyped dataport */
+ /* hint 1: use the "Buf" dataport as defined in the Echo.camkes file
+ * hint 2: to access the dataport use the interface name as defined in Echo.camkes.
+ * For example if you defined it as "dataport Buf d" then you would use "d" to refer to the dataport in C.
+ * hint 3: first read the number of strings from the dataport
+ * hint 4: then print each string from the dataport
+ * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+ */
+
+ int *n = (int*)d;
+ char *str = (char*)(n + 1);
+ for (int i = 0; i < *n; i++) {
+ printf("%s: saying (%p): \"%s\"\n", get_instance_name(), str, str);
+ str += strlen(str) + 1;
+ }
+```
+Quick solution
+```c
+ /* TASK 20: put a modified copy of the data from the untyped dataport into the typed dataport */
+ /* hint 1: modify each string by making it upper case, use the function "uppercase"
+ * hint 2: read from the "Buf" dataport as above
+ * hint 3: write to the "str_buf_t" dataport as defined in the Echo.camkes file
+ * hint 4: to access the dataport use the interface name as defined in Echo.camkes.
+ * For example if you defined it as "dataport str_buf_t d_typed" then you would use "d_typed" to refer to the dataport in C.
+ * hint 5: for the definition of "str_buf_t" see "str_buf.h"
+ * hint 6: use the "n" field to specify the number of strings in the dataport
+ * hint 7: copy the specified number of strings from the "Buf" dataport to the "str" field
+ * hint 8: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+ * hint 9: you could combine this TASK with the previous one in a single loop if you want
+ */
+
+ n = (int*)d;
+ str = (char*)(n + 1);
+ for (int i = 0, j = *n - 1; i < *n; i++, j--) {
+ strncpy(d_typed->str[j], str, STR_LEN);
+ uppercase(d_typed->str[j]);
+ str += strlen(str) + 1;
+ }
+ d_typed->n = *n;
+```
+Quick solution
+```c
+ /* TASK 23: read some data from the dataports. specifically:
+ * read a dataport pointer from one of the typed dataports, then use
+ * that pointer to access data in the untyped dataport.
+ */
+ /* hint 1: for the untyped dataport use the "Buf" dataport as defined in the Echo.camkes file
+ * hint 2: for the typed dataport use the "ptr_buf_t" dataport as defined in the Echo.camkes file
+ * hint 3: for the definition of "ptr_buf_t" see "str_buf.h".
+ * hint 4: the "n" field of the typed dataport specifies the number of dataport pointers
+ * hint 5: the "ptr" field of the typed dataport contains the dataport pointers
+ * hint 6: use the function "dataport_unwrap_ptr()" to create a regular pointer from a dataport pointer
+ * hint 7: for more information about dataport pointers see: https://github.com/seL4/camkes-tool/blob/master/docs/index.md
+ * hint 8: print out the string pointed to by each dataport pointer
+ */
+
+ char *str;
+ for (int i = 0; i < d_ptrs->n; i++) {
+ str = dataport_unwrap_ptr(d_ptrs->ptr[i]);
+ printf("%s: dptr saying (%p): \"%s\"\n", get_instance_name(), str, str);
+ }
+```
+Quick solution
+```
+```
+Quick solution
+```
+```
+Quick solution
+```
+```
+
-
Quick solution
```
+ /* TASK 1: the event interfaces */
+ /* hint 1: specify 2 interfaces: one "emits" and one "consumes"
+ * hint 2: you can use an arbitrary string as the interface type (it doesn't get used)
+ * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
+ */
+ emits TheEvent echo;
+ consumes TheEvent client;
```
Quick solution
```c
@@ -76,6 +76,7 @@ application to transparently interact with these events.
echo_emit();
```
Quick solution
```c
@@ -215,12 +216,29 @@ in the shared mem communication. We will then link them together using a
Quick solution
```
+ /* TASK 2: the dataport interfaces */
+ /* hint 1: specify 3 interfaces: one of type "Buf", one of type "str_buf_t" and one of type "ptr_buf_t"
+ * hint 2: for the definition of these types see "str_buf.h".
+ * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+ */
+
+ dataport Buf d;
+ dataport str_buf_t d_typed;
+ dataport ptr_buf_t d_ptrs;
```
Quick solution
```
+ /* TASK 4: the dataport interfaces */
+ /* hint 1: specify 3 interfaces: one of type "Buf", one of type "str_buf_t" and one of type "ptr_buf_t"
+ * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+ */
+
+ dataport Buf d;
+ dataport str_buf_t d_typed;
+ dataport ptr_buf_t d_ptrs;
```
Quick solution
```
+ /* TASK 6: Dataport connections */
+ /* hint 1: connect the corresponding dataport interfaces of the components to each other
+ * hint 2: use seL4SharedData as the connector
+ * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+ */
+
+ connection seL4SharedData data_conn(from client.d, to echo.d);
+ connection seL4SharedData typed_data_conn(from client.d_typed, to echo.d_typed);
+ connection seL4SharedData ptr_data_conn(from client.d_ptrs, to echo.d_ptrs);
```
Quick solution
```
+ /* TASK 7: set component priorities */
+ /* hint 1: component priority is specified as an attribute with the name Quick solution
```
+ /* TASK 8: restrict access to dataports */
+ /* hint 1: use attribute Quick solution
```
+ /* 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.
+ */
+ /* hint 1: try to assign a value to a field of the "str_buf_t" dataport */
+
+ d_typed->n = 0;
```
Quick solution
```c
@@ -72,45 +72,44 @@ application to transparently interact with these events.
/* hint 1: use the function Quick solution
```c
- /* TASK 11: wait to get an event back signalling that the reply data is avaialble */
+ /* TASK 11: wait to get an event back signalling that the reply data is available */
/* hint 1: use the function Quick solution
```c
/* TASK 14: emit event to signal that the data is available */
/* hint 1: we've already done this before */
-
echo_emit();
```
Quick solution
```c
/* TASK 15: wait to get an event back signalling that data has been read */
/* hint 1: we've already done this before */
-
client_wait();
```
Quick solution
```c
@@ -118,11 +117,11 @@ application to transparently interact with these events.
/* hint 1: use the function Quick solution
```c
@@ -130,7 +129,6 @@ application to transparently interact with these events.
/* hint 1: use the function Quick solution
```c
@@ -158,13 +157,13 @@ instance. These steps help you to become familiar with this approach.
* hint 3: pass NULL as the extra argument to the callback
* hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
*/
-
int error = echo_reg_callback(callback_handler_1, NULL);
ZF_LOGF_IF(error != 0, "Failed to register callback");
}
```
Quick solution
```c
@@ -174,12 +173,12 @@ instance. These steps help you to become familiar with this approach.
* hint 3: pass NULL as the extra argument to the callback
* hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
*/
-
int error = echo_reg_callback(callback_handler_2, NULL);
ZF_LOGF_IF(error != 0, "Failed to register callback");
```
Quick solution
```c
@@ -189,7 +188,6 @@ instance. These steps help you to become familiar with this approach.
* hint 3: pass NULL as the extra argument to the callback
* hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
*/
-
int error = echo_reg_callback(callback_handler_1, NULL);
ZF_LOGF_IF(error != 0, "Failed to register callback");
```
@@ -213,6 +211,7 @@ interface instances on each of the components that will be participating
in the shared mem communication. We will then link them together using a
"seL4SharedData" connector later on.
+#### Specify dataport interfaces
Quick solution
```
@@ -221,13 +220,13 @@ in the shared mem communication. We will then link them together using a
* hint 2: for the definition of these types see "str_buf.h".
* hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
*/
-
dataport Buf d;
dataport str_buf_t d_typed;
dataport ptr_buf_t d_ptrs;
```
Quick solution
```
@@ -235,7 +234,6 @@ in the shared mem communication. We will then link them together using a
/* hint 1: specify 3 interfaces: one of type "Buf", one of type "str_buf_t" and one of type "ptr_buf_t"
* hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
*/
-
dataport Buf d;
dataport str_buf_t d_typed;
dataport ptr_buf_t d_ptrs;
@@ -248,6 +246,7 @@ 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
Quick solution
```
@@ -256,7 +255,6 @@ proceed.
* hint 2: use seL4SharedData as the connector
* hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
*/
-
connection seL4SharedData data_conn(from client.d, to echo.d);
connection seL4SharedData typed_data_conn(from client.d_typed, to echo.d_typed);
connection seL4SharedData ptr_data_conn(from client.d_ptrs, to echo.d_ptrs);
@@ -268,6 +266,7 @@ proceed.
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
Quick solution
```c
@@ -279,7 +278,6 @@ to access and manipulate the data in the shared memory mapping
* hint 4: then copy all the strings from "s_arr" to the dataport.
* hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
*/
-
int *n = (int*)d;
*n = NUM_STRINGS;
char *str = (char*)(n + 1);
@@ -287,10 +285,10 @@ to access and manipulate the data in the shared memory mapping
strcpy(str, s_arr[i]);
str += strlen(str) + 1;
}
-
```
Quick solution
```
@@ -303,13 +301,13 @@ to access and manipulate the data in the shared memory mapping
* hint 5: print out the specified number of strings from the "str" field
* hint 6: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
*/
-
for (int i = 0; i < d_typed->n; i++) {
printf("%s: string %d (%p): \"%s\"\n", get_instance_name(), i, d_typed->str[i], d_typed->str[i]);
}
```
Quick solution
```
@@ -327,7 +325,6 @@ to access and manipulate the data in the shared memory mapping
* hint 8: the dataport pointers should point into the untyped dataport
* hint 9: for more information about dataport pointers see: https://github.com/seL4/camkes-tool/blob/master/docs/index.md
*/
-
d_ptrs->n = NUM_STRINGS;
str = (char*)d;
for (int i = 0; i < NUM_STRINGS; i++) {
@@ -343,6 +340,7 @@ to access and manipulate the data in the shared memory mapping
code to access and manipulate the data in the shared memory mapping
(Dataport) of the server.
+#### Read data from an untyped dataport
Quick solution
```c
@@ -354,7 +352,6 @@ code to access and manipulate the data in the shared memory mapping
* hint 4: then print each string from the dataport
* hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
*/
-
int *n = (int*)d;
char *str = (char*)(n + 1);
for (int i = 0; i < *n; i++) {
@@ -364,6 +361,7 @@ code to access and manipulate the data in the shared memory mapping
```
Quick solution
```c
@@ -379,7 +377,6 @@ code to access and manipulate the data in the shared memory mapping
* hint 8: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
* hint 9: you could combine this TASK with the previous one in a single loop if you want
*/
-
n = (int*)d;
str = (char*)(n + 1);
for (int i = 0, j = *n - 1; i < *n; i++, j--) {
@@ -391,6 +388,7 @@ code to access and manipulate the data in the shared memory mapping
```
Quick solution
```c
@@ -407,7 +405,6 @@ code to access and manipulate the data in the shared memory mapping
* hint 7: for more information about dataport pointers see: https://github.com/seL4/camkes-tool/blob/master/docs/index.md
* hint 8: print out the string pointed to by each dataport pointer
*/
-
char *str;
for (int i = 0; i < d_ptrs->n; i++) {
str = dataport_unwrap_ptr(d_ptrs->ptr[i]);
@@ -420,14 +417,14 @@ code to access and manipulate the data in the shared memory mapping
This is an introduction to CAmkES attributes: you're
being asked to set the priority of the components.
+#### Set component priorities
Quick solution
```
/* TASK 7: set component priorities */
/* hint 1: component priority is specified as an attribute with the name Quick solution
```
@@ -448,7 +446,6 @@ our constraints when mapping those Dataports.
* hint 4: make the "Buf" dataport read only for the Echo component
* hint 3: make the "str_buf_t" dataport read only for the Client component
*/
-
echo.d_access = "R";
client.d_access = "W";
echo.d_typed_access = "W";
@@ -456,6 +453,7 @@ our constraints when mapping those Dataports.
```
Quick solution
```
diff --git a/TutorialsReworked/CAmkES/camkes3.md b/TutorialsReworked/CAmkES/camkes3.md
index e69de29bb2..2f7de071cf 100644
--- a/TutorialsReworked/CAmkES/camkes3.md
+++ b/TutorialsReworked/CAmkES/camkes3.md
@@ -0,0 +1,443 @@
+# CAmkES Timer Tutorial
+
+This tutorial guides you through setting up a sample timer driver component in
+CAmkES and using it to delay for 2 seconds. For this tutorial, we will be using
+the ZYNQ7000 ARM-based platform. This platform can be simulated via QEMU so it
+is not a problem if you do not have access to the actual physical board.
+
+The tutorial also has two parts to it. The first part will teach you how to
+manually define hardware details to configure the hardware component and
+initialise hardware resources. The second part will teach you how to use a
+CAmkES connector to initialise hardware resources automatically for you.
+
+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
+
+```sh
+# For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/#get-the-code
+#
+# Follow these instructions to initialise the tutorial
+# initialising the build directory with a tutorial exercise
+./init --tut hello-camkes-timer
+# building the tutorial exercise
+cd hello-camkes-timer_build
+ninja
+```
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut hello-camkes-timer
+```
+Quick solution
+```
+ /* Part 1, TASK 1: component instances */
+ /* hint 1: one hardware component and one driver component
+ * hint 2: look at
+ * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
+ */
+ component Timerbase timerbase;
+ component Timer timer;
+```
+Quick solution
+```
+ /* Part 1, TASK 2: connections */
+ /* hint 1: use seL4HardwareMMIO to connect device memory
+ * hint 2: use seL4HardwareInterrupt to connect interrupt
+ * hint 3: look at
+ * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
+ */
+ connection seL4HardwareMMIO timer_mem(from timer.reg, to timerbase.reg);
+ connection seL4HardwareInterrupt timer_irq(from timerbase.irq, to timer.irq);
+```
+Quick solution
+```
+ /* Part 1, TASK 3: hardware resources */
+ /* Timer and Timerbase:
+ * hint 1: find out the device memory address and IRQ number from the hardware data sheet
+ * hint 2: look at
+ * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#hardware-components
+ */
+ timerbase.reg_paddr = 0xF8001000; // paddr of mmio registers
+ timerbase.reg_size = 0x1000; // size of mmio registers
+ timerbase.irq_irq_number = 42; // timer irq number
+```
+Quick solution
+```c
+ /* Part 1, TASK 4: call into the supplied driver to handle the interrupt. */
+ /* hint: timer_handle_irq
+ */
+ timer_handle_irq(&timer_drv);
+```
+Quick solution
+```c
+ /* Part 1, TASK 5: stop the timer. */
+ /* hint: timer_stop
+ */
+ timer_stop(&timer_drv);
+```
+Quick solution
+```c
+ /* Part 1, TASK 6: acknowledge the interrupt */
+ /* hint 1: use the function Quick solution
+```c
+ /* Part 1, TASK 7: call into the supplied driver to get the timer handler */
+ /* hint1: timer_init
+ * hint2: The timer ID is supplied as a #define in this file
+ * hint3: The register's variable name is the same name as the dataport in the Timer component
+ */
+ int error = timer_init(&timer_drv, DEFAULT_TIMER_ID, reg);
+ assert(error == 0);
+```
+Quick solution
+```c
+ /* Part 1, TASK 8: start the timer
+ * hint: timer_start
+ */
+ error = timer_start(&timer_drv);
+ assert(error == 0);
+```
+Quick solution
+```c
+ /* part 1, TASK 9: implement the rpc function. */
+ /* hint 1: the name of the function to implement is a composition of an interface name and a function name:
+ * i.e.: Quick solution
+```c
+ * Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */
+ /* hint1: timer_set_timeout
+ * hint2: periodic should be set to false
+ */
+ error = timer_set_timeout(&timer_drv, sec * NS_IN_SECOND, false);
+ assert(error == 0);
+```
+Quick solution
+```
+ /* Part 2, TASK 1: component instances */
+ /* hint 1: a single TimerDTB component
+ * hint 2: look at
+ * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
+ */
+ component TimerDTB timer;
+```
+Quick solution
+```
+ /* Part 2, TASK 2: connections */
+ /* hint 1: connect the dummy_source and timer interfaces
+ * hint 2: the dummy_source should be the 'from' end
+ * hint 3: look at
+ * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
+ */
+ connection seL4DTBHardware timer_dtb(from timer.dummy_source, to timer.tmr);
+```
+Quick solution
+```
+ /* Part 2, TASK 3: hardware resources */
+ /* TimerDTB:
+ * hint 1: look in the DTB/DTS for the path of a timer
+ * hint 2: set the 'dtb' setting for the tmr interface in the TimerDTB component,
+ * e.g. foo.dtb = dtb({"path" : "/bar"});
+ * hint 3: set the 'generate_interrupts' setting to 1
+ */
+ tmr.dtb = dtb({"path" : "/amba/timer@f8001000"}); // path of the timer in the DTB
+ tmr.generate_interrupts = 1; // tell seL4DTBHardware to init interrupts
+```
+Quick solution
+```c
+ /* Part 2, TASK 4: call into the supplied driver to handle the interrupt. */
+ /* hint: timer_handle_irq
+ */
+ timer_handle_irq(&timer_drv);
+```
+Quick solution
+```c
+ /* Part 2, TASK 5: stop the timer. */
+ /* hint: timer_stop
+ */
+ timer_stop(&timer_drv);
+```
+Quick solution
+```
+ /* Part 2, TASK 7: call into the supplied driver to get the timer handler */
+ /* hint1: timer_init
+ * hint2: The timer ID is supplied as a #define in this file
+ * hint3: The register's name is follows the format of Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut camkes-vm-crossvm
+```
+Hint: tutorial solutions
+
+All tutorials come with complete solutions. To get solutions run:
+```
+./init --solution --tut camkes-vm-linux
+```
+Hint: tutorial solutions
All tutorials come with complete solutions. To get solutions run:
+
```
./init --solution --tut capabilities
```
+
Answers are also available in drop down menus under each section.
Quick solution
+
```c
size_t initial_cnode_object_size_bytes = initial_cnode_object_size * (1u << seL4_SlotBits);
```
+
Quick solution
+
```c
/* use seL4_CNode_Copy to make another copy of the initial TCB capability to the last slot in the CSpace */
error = seL4_CNode_Copy(seL4_CapInitThreadCNode, last_slot, seL4_WordBits,
seL4_CapInitThreadCNode, first_free_slot, seL4_WordBits, seL4_AllRights);
ZF_LOGF_IF(error, "Failed to copy cap!");
```
+
Quick solution
+
```c
// suspend the current thread
seL4_TCB_Suspend(seL4_CapInitThreadTCB);
diff --git a/TutorialsReworked/seL4Kernel/hello-world.md b/TutorialsReworked/seL4Kernel/hello-world.md
index 3547daa7ca..4443711290 100644
--- a/TutorialsReworked/seL4Kernel/hello-world.md
+++ b/TutorialsReworked/seL4Kernel/hello-world.md
@@ -7,7 +7,7 @@ SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC.
# Hello, world!
-In this tutorial you will
+In this tutorial you will:
- Run Hello, World! to ensure your setup is working correctly
- Become familiar with the jargon *root task*
- Build and simulate a seL4 project
@@ -23,7 +23,7 @@ When the root task starts there are no available drivers, however a minimal C li
The tutorial is already set up to print "Hello, world!", so at this point
all you need to do is build and run the tutorial.
-### Initialise the build directory
+### Initialising
```
cd sel4-tutorials-manifest
@@ -35,13 +35,15 @@ This step creates two new directories in `sel4-tutorials-manifest`, namely `hell
Hint: tutorial solutions
All tutorials come with complete solutions. To get solutions run:
+
```
./init --solution --tut hello-world
```
+
This will generate another `hello-world` directory and `hello-world_build` directory, with unique names, e.g. `hello-world44h1po5q` and `hello-world44h1po5q_build`.
From d63b96f87e1dac197e21202f207e0f8089fd948f Mon Sep 17 00:00:00 2001
From: Birgit Brecknell
- Next tutorial: seL4 microkit tutorial + Next: Get started with the seL4 microkit tutorial
\ No newline at end of file diff --git a/TutorialsReworked/GettingStarted/overview.md b/TutorialsReworked/GettingStarted/overview.md new file mode 100644 index 0000000000..b644b150c0 --- /dev/null +++ b/TutorialsReworked/GettingStarted/overview.md @@ -0,0 +1,12 @@ +We have developed a series of tutorials to introduce seL4 and +developing systems on seL4. + +The tutorials are split into a number of broad categories: + +- [About seL4](about) and [Getting started with the Microkit tutorial](microkit) are introductions to seL4 concepts +- The [seL4 Kernel tutorials] are a deep dive into seL4 concepts +- [MCS] introduces seL4 MCS extensions +- [Dynamic Libraries] covers the libraries found in `seL4_libs` +- [CAmkES], a platform for building componentised systems for embedded platforms +- [Microkit], an operating system framework on top of seL4 provides a small set of simple abstractions that ease the design and implementation of statically structured systems on seL4 +- [Rust], crates for supporting the use of Rust in seL4 userspace diff --git a/TutorialsReworked/seL4Kernel/overview.md b/TutorialsReworked/seL4Kernel/overview.md index ce8982d496..616ce76f7b 100644 --- a/TutorialsReworked/seL4Kernel/overview.md +++ b/TutorialsReworked/seL4Kernel/overview.md @@ -23,15 +23,10 @@ architecture. Suggested resources for these include: - [Instruction Set Architecture (wikipedia)](https://en.wikipedia.org/wiki/Instruction_set_architecture)Next tutorial: Setting up your machine diff --git a/_includes/nav-sidebar.html b/_includes/nav-sidebar.html index c1e33b6e3e..d805773d84 100644 --- a/_includes/nav-sidebar.html +++ b/_includes/nav-sidebar.html @@ -71,6 +71,7 @@
Information about working with seL4 and its ecosystem
Tutorials and other material to learn about seL4.
List and details of all the projects that make up the seL4 platform.
- -List and details of all the projects that make up the seL4 platform.
+ +Tutorials and other material to learn about seL4.
-Links to tutorial solutions as quick references for seL4 calls and methods.
+Tutorials and other material to learn about seL4.
+Tutorials and other material to learn about seL4.
- Virtual address spaces are formed by explicit manipulation of virtual-memoryrelated kernel objects: PageDirectories, PageTables, ASIDPools and Frames (mappable physical memory). As such, address spaces have no kernel-defined structure (except for a protected region reserved for the seL4 kernel itself). Whether the userlevel system is Exokernel like, a multi-server, or a para-virtualised monolithic OS is determined by user-level via a map and unmap interface to Frames and PageTables. The distribution of authority to the kernel virtual memory (VM) objects ultimately determines the scope of influence over virtual and physical memory. + Virtual address spaces are formed by explicit manipulation of virtual-memory related kernel objects: PageDirectories, PageTables, ASIDPools and Frames (mappable physical memory). As such, address spaces have no kernel-defined structure (except for a protected region reserved for the seL4 kernel itself). Whether the userlevel system is Exokernel like, a multi-server, or a para-virtualised monolithic OS is determined by user-level via a map and unmap interface to Frames and PageTables. The distribution of authority to the kernel virtual memory (VM) objects ultimately determines the scope of influence over virtual and physical memory.
Threads are the active entity in seL4. By associating a CNode and a virtual address space with a thread, user-level policies create high-level abstractions, such as processes or virtual machines. From c22a3e6628c0edb2f0cf2678beb76263c9be9a37 Mon Sep 17 00:00:00 2001 From: Birgit Brecknell Date: Fri, 17 May 2024 10:09:03 +1000 Subject: [PATCH 033/111] fix href target blank Signed-off-by: Birgit Brecknell --- Tutorials/GettingStarted/microkit.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Tutorials/GettingStarted/microkit.md b/Tutorials/GettingStarted/microkit.md index 0003ac8a30..1bf5969301 100644 --- a/Tutorials/GettingStarted/microkit.md +++ b/Tutorials/GettingStarted/microkit.md @@ -15,7 +15,7 @@ SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. After completing the Microkit tutorial, go to seL4 kernel tutorials for a deep dive into seL4 concepts.
- Go to the Microkit tutorial + Go to the Microkit tutorial
Next tutorial: seL4 kernel tutorials
From 61f321cf8f3fc6d95f51e71504d2febcf21baa63 Mon Sep 17 00:00:00 2001
From: Birgit Brecknell
Date: Fri, 17 May 2024 10:10:39 +1000
Subject: [PATCH 034/111] fix link
Signed-off-by: Birgit Brecknell
---
Tutorials/seL4Kernel/overview.md | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Tutorials/seL4Kernel/overview.md b/Tutorials/seL4Kernel/overview.md
index dfaa2fe556..e1c9794ed0 100644
--- a/Tutorials/seL4Kernel/overview.md
+++ b/Tutorials/seL4Kernel/overview.md
@@ -23,7 +23,7 @@ architecture. Suggested resources for these include:
- [Instruction Set Architecture (wikipedia)](https://en.wikipedia.org/wiki/Instruction_set_architecture)
Resources
-We recommend having access to the seL4 manual and the API references.
+We recommend having access to the seL4 manual and the API references.
The How to page provides links to tutorial solutions as quick references for seL4 calls and methods.
From cd34825994578147571d2a958f6ef8f52dcfa098 Mon Sep 17 00:00:00 2001
From: Birgit Brecknell
Date: Mon, 20 May 2024 12:06:20 +1000
Subject: [PATCH 035/111] expand solutions if using how-to page
Signed-off-by: Birgit Brecknell
---
Tutorials/CAmkES/camkes-vm-crossvm.md | 1 +
Tutorials/CAmkES/camkes-vm-linux.md | 1 +
Tutorials/CAmkES/hello-camkes-0.md | 1 +
Tutorials/CAmkES/hello-camkes-1.md | 1 +
Tutorials/CAmkES/hello-camkes-2.md | 1 +
Tutorials/CAmkES/hello-camkes-timer.md | 1 +
Tutorials/DynamicLibraries/dynamic-1.md | 1 +
Tutorials/DynamicLibraries/dynamic-2.md | 1 +
Tutorials/DynamicLibraries/dynamic-3.md | 1 +
Tutorials/DynamicLibraries/dynamic-4.md | 1 +
Tutorials/MCS/mcs.md | 1 +
Tutorials/Resources/how-to.md | 3 +++
Tutorials/seL4Kernel/capabilities.md | 1 +
Tutorials/seL4Kernel/fault-handlers.md | 1 +
Tutorials/seL4Kernel/hello-world.md | 1 +
Tutorials/seL4Kernel/interrupts.md | 1 +
Tutorials/seL4Kernel/ipc.md | 1 +
Tutorials/seL4Kernel/mapping.md | 1 +
Tutorials/seL4Kernel/notifications.md | 1 +
Tutorials/seL4Kernel/threads.md | 1 +
Tutorials/seL4Kernel/untyped.md | 1 +
assets/js/toggle-markdown.js | 16 ++++++++++++++++
22 files changed, 39 insertions(+)
create mode 100644 assets/js/toggle-markdown.js
diff --git a/Tutorials/CAmkES/camkes-vm-crossvm.md b/Tutorials/CAmkES/camkes-vm-crossvm.md
index 3fc835fb72..1138a4b58d 100644
--- a/Tutorials/CAmkES/camkes-vm-crossvm.md
+++ b/Tutorials/CAmkES/camkes-vm-crossvm.md
@@ -9,3 +9,4 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
diff --git a/Tutorials/CAmkES/camkes-vm-linux.md b/Tutorials/CAmkES/camkes-vm-linux.md
index 9c8a032c8a..00641bda65 100644
--- a/Tutorials/CAmkES/camkes-vm-linux.md
+++ b/Tutorials/CAmkES/camkes-vm-linux.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: CAmkES Cross VM
diff --git a/Tutorials/CAmkES/hello-camkes-0.md b/Tutorials/CAmkES/hello-camkes-0.md
index 1ed57a311e..eed9ce1d72 100644
--- a/Tutorials/CAmkES/hello-camkes-0.md
+++ b/Tutorials/CAmkES/hello-camkes-0.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: CAmkES 1: Introduction to CAmkES
diff --git a/Tutorials/CAmkES/hello-camkes-1.md b/Tutorials/CAmkES/hello-camkes-1.md
index f981d02ef9..608b55d2f8 100644
--- a/Tutorials/CAmkES/hello-camkes-1.md
+++ b/Tutorials/CAmkES/hello-camkes-1.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: CAmkES 2: Events
\ No newline at end of file
diff --git a/Tutorials/CAmkES/hello-camkes-2.md b/Tutorials/CAmkES/hello-camkes-2.md
index 935e1896f6..964054e427 100644
--- a/Tutorials/CAmkES/hello-camkes-2.md
+++ b/Tutorials/CAmkES/hello-camkes-2.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: CAmkES 3: Timer
diff --git a/Tutorials/CAmkES/hello-camkes-timer.md b/Tutorials/CAmkES/hello-camkes-timer.md
index 021b449d5f..9da8e28c2f 100644
--- a/Tutorials/CAmkES/hello-camkes-timer.md
+++ b/Tutorials/CAmkES/hello-camkes-timer.md
@@ -9,6 +9,7 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: CAmkES VM
diff --git a/Tutorials/DynamicLibraries/dynamic-1.md b/Tutorials/DynamicLibraries/dynamic-1.md
index ce60d43856..e80493f5cc 100644
--- a/Tutorials/DynamicLibraries/dynamic-1.md
+++ b/Tutorials/DynamicLibraries/dynamic-1.md
@@ -9,6 +9,7 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: IPC
diff --git a/Tutorials/DynamicLibraries/dynamic-2.md b/Tutorials/DynamicLibraries/dynamic-2.md
index ce1486f7fe..21dad15c03 100644
--- a/Tutorials/DynamicLibraries/dynamic-2.md
+++ b/Tutorials/DynamicLibraries/dynamic-2.md
@@ -9,6 +9,7 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: Processes & Elf loading
diff --git a/Tutorials/DynamicLibraries/dynamic-3.md b/Tutorials/DynamicLibraries/dynamic-3.md
index 0e90c0733a..814d1b2ac2 100644
--- a/Tutorials/DynamicLibraries/dynamic-3.md
+++ b/Tutorials/DynamicLibraries/dynamic-3.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: Timer
diff --git a/Tutorials/DynamicLibraries/dynamic-4.md b/Tutorials/DynamicLibraries/dynamic-4.md
index f3984c190e..a3e2acdf91 100644
--- a/Tutorials/DynamicLibraries/dynamic-4.md
+++ b/Tutorials/DynamicLibraries/dynamic-4.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: Hello CAmkES
diff --git a/Tutorials/MCS/mcs.md b/Tutorials/MCS/mcs.md
index d7c5d29197..972ff6b45b 100644
--- a/Tutorials/MCS/mcs.md
+++ b/Tutorials/MCS/mcs.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: Dynamic libraries
diff --git a/Tutorials/Resources/how-to.md b/Tutorials/Resources/how-to.md
index 39e3458421..d70584a15c 100644
--- a/Tutorials/Resources/how-to.md
+++ b/Tutorials/Resources/how-to.md
@@ -7,6 +7,9 @@ SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC.
# How to: A quick solutions guide
This guide provides links to tutorial solutions as quick references for seL4 calls and methods.
+[//]: # (Show me some foo)
+
+
## The seL4 kernel
### [Capabilities](../seL4Kernel/capabilities)
diff --git a/Tutorials/seL4Kernel/capabilities.md b/Tutorials/seL4Kernel/capabilities.md
index c7ca44aa25..df7f392372 100644
--- a/Tutorials/seL4Kernel/capabilities.md
+++ b/Tutorials/seL4Kernel/capabilities.md
@@ -10,5 +10,6 @@ SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: Untyped
diff --git a/Tutorials/seL4Kernel/fault-handlers.md b/Tutorials/seL4Kernel/fault-handlers.md
index a5321f4752..b41cf80df9 100644
--- a/Tutorials/seL4Kernel/fault-handlers.md
+++ b/Tutorials/seL4Kernel/fault-handlers.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: MCS
diff --git a/Tutorials/seL4Kernel/hello-world.md b/Tutorials/seL4Kernel/hello-world.md
index df1711d74c..0b16f833a1 100644
--- a/Tutorials/seL4Kernel/hello-world.md
+++ b/Tutorials/seL4Kernel/hello-world.md
@@ -10,5 +10,6 @@ SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: Capabilities
\ No newline at end of file
diff --git a/Tutorials/seL4Kernel/interrupts.md b/Tutorials/seL4Kernel/interrupts.md
index 8b04dc03a3..a200651425 100644
--- a/Tutorials/seL4Kernel/interrupts.md
+++ b/Tutorials/seL4Kernel/interrupts.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: Fault handling
diff --git a/Tutorials/seL4Kernel/ipc.md b/Tutorials/seL4Kernel/ipc.md
index d7494b3f3c..026e22585c 100644
--- a/Tutorials/seL4Kernel/ipc.md
+++ b/Tutorials/seL4Kernel/ipc.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: Notifications
diff --git a/Tutorials/seL4Kernel/mapping.md b/Tutorials/seL4Kernel/mapping.md
index 9de492e6d7..ee63720c14 100644
--- a/Tutorials/seL4Kernel/mapping.md
+++ b/Tutorials/seL4Kernel/mapping.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: Threads
diff --git a/Tutorials/seL4Kernel/notifications.md b/Tutorials/seL4Kernel/notifications.md
index 928ffb76ff..ab2fd58b57 100644
--- a/Tutorials/seL4Kernel/notifications.md
+++ b/Tutorials/seL4Kernel/notifications.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: Interrupts
diff --git a/Tutorials/seL4Kernel/threads.md b/Tutorials/seL4Kernel/threads.md
index 5b480cdde9..6e715ef39a 100644
--- a/Tutorials/seL4Kernel/threads.md
+++ b/Tutorials/seL4Kernel/threads.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: IPC
\ No newline at end of file
diff --git a/Tutorials/seL4Kernel/untyped.md b/Tutorials/seL4Kernel/untyped.md
index 4ea4aa181b..6bcfc2f746 100644
--- a/Tutorials/seL4Kernel/untyped.md
+++ b/Tutorials/seL4Kernel/untyped.md
@@ -9,5 +9,6 @@ SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---
{% include tutorial.md %}
+
Next tutorial: Mapping
diff --git a/assets/js/toggle-markdown.js b/assets/js/toggle-markdown.js
new file mode 100644
index 0000000000..5f8a867977
--- /dev/null
+++ b/assets/js/toggle-markdown.js
@@ -0,0 +1,16 @@
+// Open all solutions if previous link was how-to page
+
+let text = document.referrer;
+let result = text.includes("Tutorials/Resources/how-to");
+
+if (result==true){
+ document.body.querySelectorAll('details')
+ .forEach((e) => {(e.hasAttribute('open')) ?
+ e.removeAttribute('open') : e.setAttribute('open',true);
+ console.log(e.hasAttribute('open'))
+ })
+}
+
+
+
+
From 74e041337557a5fb99a37ebb78415d32458d3779 Mon Sep 17 00:00:00 2001
From: Birgit Brecknell
Date: Mon, 20 May 2024 13:21:27 +1000
Subject: [PATCH 036/111] add css space after solution boxes
Signed-off-by: Birgit Brecknell
---
assets/css/style.scss | 5 +++++
assets/js/toggle-markdown.js | 2 +-
2 files changed, 6 insertions(+), 1 deletion(-)
diff --git a/assets/css/style.scss b/assets/css/style.scss
index 7e224e395c..5abd29f1a8 100644
--- a/assets/css/style.scss
+++ b/assets/css/style.scss
@@ -291,3 +291,8 @@ a[href*="//"]:not([href*="{{site.url}}"],.skip-icon):after {
.flex-grid-thirds .col {
width: 32%;
}
+
+/* add margin below tutorials solutions boxes */
+details {
+ padding-bottom: 20px;
+}
diff --git a/assets/js/toggle-markdown.js b/assets/js/toggle-markdown.js
index 5f8a867977..d55457deca 100644
--- a/assets/js/toggle-markdown.js
+++ b/assets/js/toggle-markdown.js
@@ -1,4 +1,4 @@
-// Open all solutions if previous link was how-to page
+// Expand all solutions if previous link was how-to page
let text = document.referrer;
let result = text.includes("Tutorials/Resources/how-to");
From f159026cb320c4acd0d7277531bbc65147a2176f Mon Sep 17 00:00:00 2001
From: Birgit Brecknell
Date: Mon, 20 May 2024 13:29:27 +1000
Subject: [PATCH 037/111] separate instructions for getting tutes manifest
Signed-off-by: Birgit Brecknell
---
Tutorials/seL4Kernel/get-the-tutorials.md | 32 +++++++++++++++++++++++
Tutorials/seL4Kernel/setting-up.md | 24 +----------------
_includes/nav-sidebar.html | 1 +
3 files changed, 34 insertions(+), 23 deletions(-)
create mode 100644 Tutorials/seL4Kernel/get-the-tutorials.md
diff --git a/Tutorials/seL4Kernel/get-the-tutorials.md b/Tutorials/seL4Kernel/get-the-tutorials.md
new file mode 100644
index 0000000000..fe8c2e285c
--- /dev/null
+++ b/Tutorials/seL4Kernel/get-the-tutorials.md
@@ -0,0 +1,32 @@
+---
+toc: true
+layout: tutorial
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC.
+---
+
+# Tutorials
+## Python Dependencies
+Additional python dependencies are required to build [tutorials](ReworkedTutorials). To install you can run:
+```
+pip install --user aenum
+pip install --user pyelftools
+```
+*Hint:* This step only needs to be done once, i.e. before doing your first tutorial
+
+## Get the code
+All tutorials are in the sel4-tutorials-manifest. Get the code with:
+```
+mkdir sel4-tutorials-manifest
+cd sel4-tutorials-manifest
+repo init -u https://github.com/seL4/sel4-tutorials-manifest
+repo sync
+```
+
+`repo sync` may take a few moments to run
+
+*Hint:* The **Get the code** step only needs to be done once, i.e. before doing your first tutorial.
+
+
+ Next: Hello world +
diff --git a/Tutorials/seL4Kernel/setting-up.md b/Tutorials/seL4Kernel/setting-up.md index b8a742c00e..bff2d66292 100644 --- a/Tutorials/seL4Kernel/setting-up.md +++ b/Tutorials/seL4Kernel/setting-up.md @@ -232,28 +232,6 @@ That's it! seL4 is running. To quit QEMU: `Ctrl+a, x` -# Tutorials -## Python Dependencies -Additional python dependencies are required to build [tutorials](ReworkedTutorials). To install you can run: -``` -pip install --user aenum -pip install --user pyelftools -``` -*Hint:* This step only needs to be done once, i.e. before doing your first tutorial - -## Get the code -All tutorials are in the sel4-tutorials-manifest. Get the code with: -``` -mkdir sel4-tutorials-manifest -cd sel4-tutorials-manifest -repo init -u https://github.com/seL4/sel4-tutorials-manifest -repo sync -``` - -`repo sync` may take a few moments to run - -*Hint:* The **Get the code** step only needs to be done once, i.e. before doing your first tutorial. -- Next tutorial: Hello world + Next: Get the tutorials
diff --git a/_includes/nav-sidebar.html b/_includes/nav-sidebar.html index 44841591c6..4f7eeae5cb 100644 --- a/_includes/nav-sidebar.html +++ b/_includes/nav-sidebar.html @@ -68,6 +68,7 @@- seL4 is a third-generation microkernel. It is broadly based on L4 and influenced by EROS. Like L4 it features abstractions for virtual address spaces, threads, IPC, and, unlike most earlier L4 kernels, an explicit in-kernel memory management model and capabilities for authorisation. -
-- Authority in seL4 is conferred by possession of a capability. Capabilities are segregated and stored in capability address spaces composed of capability container objects called CNodes. seL4 has six system calls, of which five require possession of a capability (the sixth is a yield to the scheduler). The five system calls are IPC primitives that are used either to invoke services implemented by other processes (using capabilities to port-like endpoints that facilitate message passing), or invoke kernel services (using capabilities to kernel objects, such as a thread control block (TCB)). While the number of system calls is small, the kernel’s effective API is the sum of all the interfaces presented by all kernel object types. -
-- Kernel memory management in seL4 is explicit. All kernel data structures are either statically allocated at boot time, or are dynamically-allocated first-class objects in the API. Kernel objects thus act as both inkernel data structures, and user-invoked fine-grained kernel services. Kernel objects include TCBs, CNodes, and level-1 and level-2 page tables (termed PageDirectories and PageTables). -
-- Authority over free memory is encapsulated in an untyped memory object. Creating new kernel objects explicitly involves invoking the retype method of an untyped -memory object, which allocates the memory for the object, initialises it, and returns a capability to the new object. -
-- Virtual address spaces are formed by explicit manipulation of virtual-memory related kernel objects: PageDirectories, PageTables, ASIDPools and Frames (mappable physical memory). As such, address spaces have no kernel-defined structure (except for a protected region reserved for the seL4 kernel itself). Whether the userlevel system is Exokernel like, a multi-server, or a para-virtualised monolithic OS is determined by user-level via a map and unmap interface to Frames and PageTables. The distribution of authority to the kernel virtual memory (VM) objects ultimately determines the scope of influence over virtual and physical memory. -
-- Threads are the active entity in seL4. By associating a CNode and a virtual address space with a thread, user-level policies create high-level abstractions, such as processes or virtual machines. -
-- IPC is supported in two forms: synchronous message passing via endpoints (portlike destinations without in-kernel buffering), and asynchronous notification via asynchronous endpoints (rendezvous objects consisting of a single in-kernel word that is used to combine IPC sends using a logical or). Remote procedure call semantics are facilitated over synchronous IPC via reply capabilities. Send capabilities are minted from an initial endpoint capability. Send capabilities feature an immutable badge which is used by the specific endpoint’s IPC recipients to distinguish which send capability (and thus which authority) was used to send a message. The unforgeable badge, represented by an integer value, is delivered with the message. -
-- Exceptions are propagated via synchronous IPC to each thread’s exception handler (registered in the TCB via a capability to an endpoint). Similarly, page faults are also propagated using synchronous IPC to a thread’s page fault handler. Non-native system calls are treated as exceptions to support virtualisation. -
-- Device Drivers run as user-mode applications that have access to device registers and memory, either by mapping the device into the virtual address space, or by controlled access to device ports on x86 hardware. seL4 provides a mechanism to receive notification of interrupts (via asynchronous IPC) and acknowledge their receipt. -
-- The seL4 kernel runs on multiple platforms, and runs on common architectures like ARM and RiscV. -
-- Because sel4 is small, a lot more needs to be done in user space and there are a lot more choices about how to do that. We'll start by building a simple system using the seL4 Microkit, which is a software development kit for building static systems on seL4. -
-- Next: Get started with the seL4 microkit tutorial -
\ No newline at end of file diff --git a/Tutorials/GettingStarted/microkit.md b/Tutorials/GettingStarted/microkit.md deleted file mode 100644 index 1bf5969301..0000000000 --- a/Tutorials/GettingStarted/microkit.md +++ /dev/null @@ -1,22 +0,0 @@ ---- -toc: true -layout: overview -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. ---- -- The seL4 Microkit is an operating system framework on top of seL4 provides a small set of simple abstractions that ease the design and implementation of statically structured systems on seL4, while still leveraging the kernel’s benefits of security and performance. -
-- The Microkit is distributed as an SDK that integrates with the build system of your choice, significantly reducing the barrier to entry for new users of seL4. We recommend it as the first tutorial, to familiarise new users with seL4 concepts. -
-- After completing the Microkit tutorial, go to seL4 kernel tutorials for a deep dive into seL4 concepts. -
-- Go to the Microkit tutorial -
-- Next tutorial: seL4 kernel tutorials -
\ No newline at end of file diff --git a/Tutorials/GettingStarted/overview.md b/Tutorials/GettingStarted/overview.md new file mode 100644 index 0000000000..5e13aee069 --- /dev/null +++ b/Tutorials/GettingStarted/overview.md @@ -0,0 +1,44 @@ +--- +toc: true +title: Overview +layout: tutorial +redirect_from: + - /tutorials/ +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +--- +# Overview + +We have developed a series of tutorials to introduce seL4 and developing systems on seL4. + +## List of tutorials +The tutorials are split into a number of broad categories, and have been designed around developer needs. + +- The [seL4 tutorials](seL4/overview.md) are for people keen to learn about the base mechanisms provided by the seL4 kernel. The kernel API is explained with short exercises that show basic examples. + +- [MCS](MCS/mcs) introduces seL4 MCS extensions, which are detailed in this [paper](https://trustworthy.systems/publications/full_text/Lyons_MAH_18.pdf) and [PhD](https://github.com/pingerino/phd/blob/master/phd.pdf). + +- [Dynamic Libraries](DynamicLibraries/dynamic-1) provides walkthroughs and exercises for using the dynamic libraries provided in `seL4_libs`, which were developed for rapidly prototyping systems on seL4. + +- [CAmkES](CAmkES/hello-camkes-0) generates the glue code for interacting with seL4 and is designed for building high-assurance, static systems. These tutorials demonstrate how to configure static systems through components. + +- [Microkit](https://trustworthy.systems/projects/microkit/tutorial/) enables system designers to create static software systems based on the seL4 microkernel. We recommend this as a potential introduction to seL4, bearing in mind that the Microkit hides many of the seL4 mechanisms - it is designed that way, to make building on top of seL4 easier. + +- [Rust](https://github.com/seL4/rust-sel4) allows people to write safer user-level code on top of seL4 without needing full formal verification, with a language that is receiving increasing interest and that aligns extremely well with security and safety critical embedded systems programming. + +## Resources +Additional resources to assist with learning: +- The [seL4 manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf) +- [API references](projects/sel4/api-doc) +- The [How to](Resources/how-to) page provides links to tutorial solutions as quick references for seL4 calls and methods. +- The [seL4 white paper](https://sel4.systems/About/seL4-whitepaper.pdf) +- [FAQs](projects/sel4/frequently-asked-questions) +- [Debugging guide](projects/sel4-tutorials/debugging-guide) +- [Discourse forum](https://sel4.discourse.group/) +- [Developer mailing list](https://lists.sel4.systems/postorius/lists/devel.sel4.systems/) +- [Mattermost channel](https://mattermost.trustworthy.systems/sel4-external/channels/web-doc-revamp) + + ++ Next: Pathways through the tutorials +
\ No newline at end of file diff --git a/Tutorials/GettingStarted/pathways.md b/Tutorials/GettingStarted/pathways.md new file mode 100644 index 0000000000..6c7a55665d --- /dev/null +++ b/Tutorials/GettingStarted/pathways.md @@ -0,0 +1,80 @@ +--- +toc: true +title: Tutorial pathways +layout: tutorial +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +--- + +# Pathways through tutorials +The tutorials can be approached in a number of different ways. Our recommended approach for newcomers is to begin the [Microkit](https://trustworthy.systems/projects/microkit/tutorial/), bearing in mind that the Microkit hides many of the seL4 mechanisms - it is designed that way, to make building on top of seL4 easier. Having built a small system on top of seL4, the developer can delve into the concepts in the order list in the navigation bar to the left. + +## Alternate pathways +Alternate pathways through the tutorials depend on development goals. + +### Evaluation +Goals: +- to understand seL4 and its benefits +- to learn how to use seL4 to develop trustworthy systems +- to see, compile, and run some code + +Recommended tutorials +- [Setting up your machine](../seL4Kernel/setting-up) +- [Getting the tutorials](../seL4Kernel/get-the-tutorials.md) +- [Hello world](../seL4Kernel/hello-world.md) + +### System Building +Goals: +- to build systems based on seL4 +- to know which tools are available to build systems, and how to use those tools +- to build trustworthy systems +- +Follow these tutorials: +Recommended tutorials +- [Setting up your machine](../seL4Kernel/setting-up) +- [Getting the tutorials](../seL4Kernel/get-the-tutorials.md) +- [Hello world](../seL4Kernel/hello-world.md) + +**up to here** + +seL4 overview +Introduction tutorial +CAmkES tutorials +Virtualisation tutorials +MCS tutorial + +Platform Development +Goal: + +You want to contribute to development of the seL4 (user-level) platform. +You want to develop operating system services and device drivers. +You want to develop seL4-based frameworks and operating systems. +Follow these tutorials: + +seL4 overview +Introduction tutorial +seL4 mechanisms tutorial +Rapid prototyping tutorials +CAmkES tutorials +Virtualisation tutorial +MCS tutorial +Kernel Development +Goal: + +You want to contribute to the seL4 kernel itself. +You want to port seL4 to a new platform. +You want to add new features to the kernel. +Read this first: + +Contributing to kernel code +Then follow these tutorials: + +seL4 overview +Introduction tutorial +seL4 mechanisms tutorial +MCS tutorial + + ++ Next tutorial: seL4 kernel tutorials +
\ No newline at end of file diff --git a/Tutorials/index.md b/Tutorials/index.md index 15fb25580f..def57a79e0 100644 --- a/Tutorials/index.md +++ b/Tutorials/index.md @@ -1,32 +1,6 @@ --- toc: true -layout: overview +layout: tutorial SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. --- -# Tutorials about seL4 - -We have developed a series of tutorials to introduce seL4 and -developing systems on seL4. - -- Next tutorial: seL4 kernel tutorials + Next tutorial: seL4 tutorials
\ No newline at end of file diff --git a/Tutorials/seL4/capabilities.md b/Tutorials/seL4/capabilities.md new file mode 100644 index 0000000000..df7f392372 --- /dev/null +++ b/Tutorials/seL4/capabilities.md @@ -0,0 +1,15 @@ +--- +toc: true +title: Capabilities +tutorial: capabilities +tutorial-order: mechanisms-1 +description: an introduction to capabilities in the seL4 kernel API. +layout: tutorial +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +--- + +{% include tutorial.md %} + + +Next tutorial: Untyped diff --git a/Tutorials/seL4/fault-handlers.md b/Tutorials/seL4/fault-handlers.md new file mode 100644 index 0000000000..2ac8f3a755 --- /dev/null +++ b/Tutorials/seL4/fault-handlers.md @@ -0,0 +1,14 @@ +--- +toc: true +title: Faults +tutorial: fault-handlers +tutorial-order: mechanisms-8 +layout: tutorial +description: fault (e.g virtual memory fault) handling and fault endpoints. +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. +--- +{% include tutorial.md %} + + +Next tutorial: MCS diff --git a/Tutorials/seL4/get-the-tutorials.md b/Tutorials/seL4/get-the-tutorials.md new file mode 100644 index 0000000000..ea9d6a079d --- /dev/null +++ b/Tutorials/seL4/get-the-tutorials.md @@ -0,0 +1,33 @@ +--- +toc: true +title: Getting the tutorials +layout: tutorial +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +--- + +# Getting the tutorials +## Python Dependencies +Additional python dependencies are required to build [tutorials](ReworkedTutorials). To install you can run: +``` +pip install --user aenum +pip install --user pyelftools +``` +*Hint:* This step only needs to be done once, i.e. before doing your first tutorial + +## Get the code +All tutorials are in the sel4-tutorials-manifest. Get the code with: +``` +mkdir sel4-tutorials-manifest +cd sel4-tutorials-manifest +repo init -u https://github.com/seL4/sel4-tutorials-manifest +repo sync +``` + +`repo sync` may take a few moments to run + +*Hint:* The **Get the code** step only needs to be done once, i.e. before doing your first tutorial. + ++ Next: Hello world +
diff --git a/Tutorials/seL4/hello-world.md b/Tutorials/seL4/hello-world.md new file mode 100644 index 0000000000..0b16f833a1 --- /dev/null +++ b/Tutorials/seL4/hello-world.md @@ -0,0 +1,15 @@ +--- +toc: true +title: Hello, World! +tutorial: hello-world +tutorial-order: 0-hello +description: an introduction to seL4 projects and tutorials. +layout: tutorial +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +--- + +{% include tutorial.md %} + + +Next tutorial: Capabilities \ No newline at end of file diff --git a/Tutorials/seL4/interrupts.md b/Tutorials/seL4/interrupts.md new file mode 100644 index 0000000000..90412cab2c --- /dev/null +++ b/Tutorials/seL4/interrupts.md @@ -0,0 +1,14 @@ +--- +toc: true +title: Interrupts +tutorial: interrupts +tutorial-order: mechanisms-7 +layout: tutorial +description: receiving and handling interrupts. +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. +--- +{% include tutorial.md %} + + +Next tutorial: Fault handling diff --git a/Tutorials/seL4/ipc.md b/Tutorials/seL4/ipc.md new file mode 100644 index 0000000000..026e22585c --- /dev/null +++ b/Tutorials/seL4/ipc.md @@ -0,0 +1,14 @@ +--- +toc: true +title: IPC +tutorial: ipc +tutorial-order: mechanisms-5 +layout: tutorial +description: overview of interprocess communication (IPC). +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. +--- +{% include tutorial.md %} + + +Next tutorial: Notifications diff --git a/Tutorials/seL4/mapping.md b/Tutorials/seL4/mapping.md new file mode 100644 index 0000000000..ee63720c14 --- /dev/null +++ b/Tutorials/seL4/mapping.md @@ -0,0 +1,14 @@ +--- +toc: true +title: Mapping +tutorial: mapping +tutorial-order: mechanisms-3 +description: virtual memory in seL4. +layout: tutorial +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. +--- +{% include tutorial.md %} + + +Next tutorial: Threads diff --git a/Tutorials/seL4/notifications.md b/Tutorials/seL4/notifications.md new file mode 100644 index 0000000000..ab2fd58b57 --- /dev/null +++ b/Tutorials/seL4/notifications.md @@ -0,0 +1,14 @@ +--- +toc: true +title: Notifications +tutorial: notifications +tutorial-order: mechanisms-6 +layout: tutorial +description: using notification objects and signals. +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. +--- +{% include tutorial.md %} + + +Next tutorial: Interrupts diff --git a/Tutorials/seL4/overview.md b/Tutorials/seL4/overview.md new file mode 100644 index 0000000000..a732f87862 --- /dev/null +++ b/Tutorials/seL4/overview.md @@ -0,0 +1,38 @@ +--- +toc: true +layout: tutorial +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +--- + +# Overview +The [seL4 tutorials](seL4/overview.md) are for people keen to learn about the base mechanisms provided by the seL4 kernel. The kernel API is explained with short exercises that show basic examples. +We have developed a series of tutorials to on seL4 concepts. + +Recommended reading: +- the [seL4 white paper](https://sel4.systems/About/seL4-whitepaper.pdf) + + ++ Next tutorial: Setting up your machine +
\ No newline at end of file diff --git a/Tutorials/seL4/setting-up.md b/Tutorials/seL4/setting-up.md new file mode 100644 index 0000000000..4a281b7556 --- /dev/null +++ b/Tutorials/seL4/setting-up.md @@ -0,0 +1,237 @@ +--- +toc: true +layout: tutorial +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +--- + +# Setting up your machine +**Overview** +- Set up your machine - install dependencies required to run seL4`` +- Run seL4test on a simulator +- Gain awareness of terminology used for seL4 + + + +## Docker +To compile and use seL4, it is recommended that you use Docker to isolate the dependencies from your machine. + +These instructions assume you are using Debian (or a derivative, such as Ubuntu), and are using Bash for your shell. However, it should be informative enough for users of other distros/shells to adapt. + +These instructions are intended for Ubuntu LTS versions 20.04 and 22.04. + +To begin, you will need at least these two programs: + + * make (`sudo apt install make`) + * docker (See [here](https://get.docker.com) or [here](https://docs.docker.com/engine/installation) for installation instructions) + +For convenience, add your account to the docker group: + +```bash +sudo usermod -aG docker $(whoami) +``` + ++ Next: Get the tutorials +
diff --git a/Tutorials/seL4/threads.md b/Tutorials/seL4/threads.md new file mode 100644 index 0000000000..6e715ef39a --- /dev/null +++ b/Tutorials/seL4/threads.md @@ -0,0 +1,14 @@ +--- +toc: true +title: Threads +tutorial: threads +tutorial-order: mechanisms-4 +layout: tutorial +description: how to start a thread using the seL4 API. +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. +--- +{% include tutorial.md %} + + +Next tutorial: IPC \ No newline at end of file diff --git a/Tutorials/seL4/untyped.md b/Tutorials/seL4/untyped.md new file mode 100644 index 0000000000..6bcfc2f746 --- /dev/null +++ b/Tutorials/seL4/untyped.md @@ -0,0 +1,14 @@ +--- +toc: true +title: Untyped +tutorial: untyped +tutorial-order: mechanisms-2 +description: user-level memory management. +layout: tutorial +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. +--- +{% include tutorial.md %} + + +Next tutorial: Mapping From 9b3284ca196bace637efc0cb1f7ddd565b69aa27 Mon Sep 17 00:00:00 2001 From: Birgit Brecknell Date: Mon, 15 Jul 2024 08:28:23 +1000 Subject: [PATCH 051/111] finish addressing Gerwin high-level issues Signed-off-by: Birgit Brecknell --- Hardware/HiKey/index.md | 2 +- Hardware/IA32.md | 6 +- Hardware/VMware/index.md | 2 +- Hardware/jetsontk1.md | 2 +- Makefile | 2 +- Resources.md | 7 +- Tutorials/GettingStarted/overview.md | 2 +- Tutorials/Resources/how-to.md | 102 ++++----- Tutorials/seL4/overview.md | 21 +- Tutorials/seL4Kernel/capabilities.md | 15 -- Tutorials/seL4Kernel/fault-handlers.md | 14 -- Tutorials/seL4Kernel/get-the-tutorials.md | 33 --- Tutorials/seL4Kernel/hello-world.md | 15 -- Tutorials/seL4Kernel/interrupts.md | 14 -- Tutorials/seL4Kernel/ipc.md | 14 -- Tutorials/seL4Kernel/mapping.md | 14 -- Tutorials/seL4Kernel/notifications.md | 14 -- Tutorials/seL4Kernel/overview.md | 37 --- Tutorials/seL4Kernel/setting-up.md | 237 -------------------- Tutorials/seL4Kernel/threads.md | 14 -- Tutorials/seL4Kernel/untyped.md | 14 -- _data/sidebar.yml | 8 +- _includes/header.html | 2 +- _includes/nav-sidebar.html | 30 ++- index.md | 31 +-- projects/buildsystem/index.md | 2 +- projects/sel4/documentation.md | 2 +- projects/sel4/frequently-asked-questions.md | 2 +- 28 files changed, 112 insertions(+), 546 deletions(-) delete mode 100644 Tutorials/seL4Kernel/capabilities.md delete mode 100644 Tutorials/seL4Kernel/fault-handlers.md delete mode 100644 Tutorials/seL4Kernel/get-the-tutorials.md delete mode 100644 Tutorials/seL4Kernel/hello-world.md delete mode 100644 Tutorials/seL4Kernel/interrupts.md delete mode 100644 Tutorials/seL4Kernel/ipc.md delete mode 100644 Tutorials/seL4Kernel/mapping.md delete mode 100644 Tutorials/seL4Kernel/notifications.md delete mode 100644 Tutorials/seL4Kernel/overview.md delete mode 100644 Tutorials/seL4Kernel/setting-up.md delete mode 100644 Tutorials/seL4Kernel/threads.md delete mode 100644 Tutorials/seL4Kernel/untyped.md diff --git a/Hardware/HiKey/index.md b/Hardware/HiKey/index.md index 1317f9cf2f..8e659cb92e 100644 --- a/Hardware/HiKey/index.md +++ b/Hardware/HiKey/index.md @@ -23,7 +23,7 @@ SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. - One HiKey Board. See [Hikey 96Board](http://www.96boards.org/products/ce/hikey/) - Fully working development environment. See - [Working with seL4](/Working-with-seL4) + [Resources](/Resources) ### Getting Started The Hikey board is based around the diff --git a/Hardware/IA32.md b/Hardware/IA32.md index 21e0056b7c..071715628a 100644 --- a/Hardware/IA32.md +++ b/Hardware/IA32.md @@ -29,7 +29,7 @@ menuentry "Load seL4 VM" --class os { insmod part_msdos insmod ext2 set root='(hd0,msdos2)' - multiboot /boot/sel4kernel + multiboot /boot/seL4 module /boot/sel4rootserver } ``` @@ -59,13 +59,13 @@ install-mbr /dev/sdb syslinux --install /dev/sdb1 mount /dev/sdb1 /mnt cp images/sel4test-driver-image-ia32-pc99 /mnt/rootserver -cp images/kernel-ia32-pc99 /mnt/sel4kernel +cp images/kernel-ia32-pc99 /mnt/seL4 cat > /mnt/syslinux.cfg <Next tutorial: Setting up your machine diff --git a/Tutorials/seL4Kernel/capabilities.md b/Tutorials/seL4Kernel/capabilities.md deleted file mode 100644 index df7f392372..0000000000 --- a/Tutorials/seL4Kernel/capabilities.md +++ /dev/null @@ -1,15 +0,0 @@ ---- -toc: true -title: Capabilities -tutorial: capabilities -tutorial-order: mechanisms-1 -description: an introduction to capabilities in the seL4 kernel API. -layout: tutorial -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. ---- - -{% include tutorial.md %} - - -Next tutorial: Untyped diff --git a/Tutorials/seL4Kernel/fault-handlers.md b/Tutorials/seL4Kernel/fault-handlers.md deleted file mode 100644 index 2ac8f3a755..0000000000 --- a/Tutorials/seL4Kernel/fault-handlers.md +++ /dev/null @@ -1,14 +0,0 @@ ---- -toc: true -title: Faults -tutorial: fault-handlers -tutorial-order: mechanisms-8 -layout: tutorial -description: fault (e.g virtual memory fault) handling and fault endpoints. -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. ---- -{% include tutorial.md %} - - -Next tutorial: MCS diff --git a/Tutorials/seL4Kernel/get-the-tutorials.md b/Tutorials/seL4Kernel/get-the-tutorials.md deleted file mode 100644 index ea9d6a079d..0000000000 --- a/Tutorials/seL4Kernel/get-the-tutorials.md +++ /dev/null @@ -1,33 +0,0 @@ ---- -toc: true -title: Getting the tutorials -layout: tutorial -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. ---- - -# Getting the tutorials -## Python Dependencies -Additional python dependencies are required to build [tutorials](ReworkedTutorials). To install you can run: -``` -pip install --user aenum -pip install --user pyelftools -``` -*Hint:* This step only needs to be done once, i.e. before doing your first tutorial - -## Get the code -All tutorials are in the sel4-tutorials-manifest. Get the code with: -``` -mkdir sel4-tutorials-manifest -cd sel4-tutorials-manifest -repo init -u https://github.com/seL4/sel4-tutorials-manifest -repo sync -``` - -`repo sync` may take a few moments to run - -*Hint:* The **Get the code** step only needs to be done once, i.e. before doing your first tutorial. - -
- Next: Hello world -
diff --git a/Tutorials/seL4Kernel/hello-world.md b/Tutorials/seL4Kernel/hello-world.md deleted file mode 100644 index 0b16f833a1..0000000000 --- a/Tutorials/seL4Kernel/hello-world.md +++ /dev/null @@ -1,15 +0,0 @@ ---- -toc: true -title: Hello, World! -tutorial: hello-world -tutorial-order: 0-hello -description: an introduction to seL4 projects and tutorials. -layout: tutorial -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. ---- - -{% include tutorial.md %} - - -Next tutorial: Capabilities \ No newline at end of file diff --git a/Tutorials/seL4Kernel/interrupts.md b/Tutorials/seL4Kernel/interrupts.md deleted file mode 100644 index 90412cab2c..0000000000 --- a/Tutorials/seL4Kernel/interrupts.md +++ /dev/null @@ -1,14 +0,0 @@ ---- -toc: true -title: Interrupts -tutorial: interrupts -tutorial-order: mechanisms-7 -layout: tutorial -description: receiving and handling interrupts. -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. ---- -{% include tutorial.md %} - - -Next tutorial: Fault handling diff --git a/Tutorials/seL4Kernel/ipc.md b/Tutorials/seL4Kernel/ipc.md deleted file mode 100644 index 026e22585c..0000000000 --- a/Tutorials/seL4Kernel/ipc.md +++ /dev/null @@ -1,14 +0,0 @@ ---- -toc: true -title: IPC -tutorial: ipc -tutorial-order: mechanisms-5 -layout: tutorial -description: overview of interprocess communication (IPC). -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. ---- -{% include tutorial.md %} - - -Next tutorial: Notifications diff --git a/Tutorials/seL4Kernel/mapping.md b/Tutorials/seL4Kernel/mapping.md deleted file mode 100644 index ee63720c14..0000000000 --- a/Tutorials/seL4Kernel/mapping.md +++ /dev/null @@ -1,14 +0,0 @@ ---- -toc: true -title: Mapping -tutorial: mapping -tutorial-order: mechanisms-3 -description: virtual memory in seL4. -layout: tutorial -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. ---- -{% include tutorial.md %} - - -Next tutorial: Threads diff --git a/Tutorials/seL4Kernel/notifications.md b/Tutorials/seL4Kernel/notifications.md deleted file mode 100644 index ab2fd58b57..0000000000 --- a/Tutorials/seL4Kernel/notifications.md +++ /dev/null @@ -1,14 +0,0 @@ ---- -toc: true -title: Notifications -tutorial: notifications -tutorial-order: mechanisms-6 -layout: tutorial -description: using notification objects and signals. -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. ---- -{% include tutorial.md %} - - -Next tutorial: Interrupts diff --git a/Tutorials/seL4Kernel/overview.md b/Tutorials/seL4Kernel/overview.md deleted file mode 100644 index b6167a9044..0000000000 --- a/Tutorials/seL4Kernel/overview.md +++ /dev/null @@ -1,37 +0,0 @@ ---- -toc: true -layout: tutorial -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. ---- - -- Next tutorial: Setting up your machine -
\ No newline at end of file diff --git a/Tutorials/seL4Kernel/setting-up.md b/Tutorials/seL4Kernel/setting-up.md deleted file mode 100644 index 4a281b7556..0000000000 --- a/Tutorials/seL4Kernel/setting-up.md +++ /dev/null @@ -1,237 +0,0 @@ ---- -toc: true -layout: tutorial -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. ---- - -# Setting up your machine -**Overview** -- Set up your machine - install dependencies required to run seL4`` -- Run seL4test on a simulator -- Gain awareness of terminology used for seL4 - - - -## Docker -To compile and use seL4, it is recommended that you use Docker to isolate the dependencies from your machine. - -These instructions assume you are using Debian (or a derivative, such as Ubuntu), and are using Bash for your shell. However, it should be informative enough for users of other distros/shells to adapt. - -These instructions are intended for Ubuntu LTS versions 20.04 and 22.04. - -To begin, you will need at least these two programs: - - * make (`sudo apt install make`) - * docker (See [here](https://get.docker.com) or [here](https://docs.docker.com/engine/installation) for installation instructions) - -For convenience, add your account to the docker group: - -```bash -sudo usermod -aG docker $(whoami) -``` - -- Next: Get the tutorials -
diff --git a/Tutorials/seL4Kernel/threads.md b/Tutorials/seL4Kernel/threads.md deleted file mode 100644 index 6e715ef39a..0000000000 --- a/Tutorials/seL4Kernel/threads.md +++ /dev/null @@ -1,14 +0,0 @@ ---- -toc: true -title: Threads -tutorial: threads -tutorial-order: mechanisms-4 -layout: tutorial -description: how to start a thread using the seL4 API. -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. ---- -{% include tutorial.md %} - - -Next tutorial: IPC \ No newline at end of file diff --git a/Tutorials/seL4Kernel/untyped.md b/Tutorials/seL4Kernel/untyped.md deleted file mode 100644 index 6bcfc2f746..0000000000 --- a/Tutorials/seL4Kernel/untyped.md +++ /dev/null @@ -1,14 +0,0 @@ ---- -toc: true -title: Untyped -tutorial: untyped -tutorial-order: mechanisms-2 -description: user-level memory management. -layout: tutorial -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. ---- -{% include tutorial.md %} - - -Next tutorial: Mapping diff --git a/_data/sidebar.yml b/_data/sidebar.yml index d7c287b8a9..716b413a53 100644 --- a/_data/sidebar.yml +++ b/_data/sidebar.yml @@ -2,11 +2,11 @@ # Copyright 2020 seL4 Project a Series of LF Projects, LLC. toc: - - title: Working with seL4 - url: /Working-with-seL4.html + - title: Resources + url: /Resources.html subfolderitems: - - page: Working with seL4 - url: /Working-with-seL4.html + - page: Resources + url: /Resources.html - page: seL4 Documentation url: /projects/sel4/documentation.html - page: seL4 FAQ diff --git a/_includes/header.html b/_includes/header.html index 277700d72d..fe57493654 100644 --- a/_includes/header.html +++ b/_includes/header.html @@ -16,7 +16,7 @@Information about working with seL4 and its ecosystem
List and details of all the projects that make up the seL4 platform.
@@ -56,17 +58,20 @@ This documentation site is for cooperatively developing and sharing documentatioTutorials and other material to learn about seL4.
-Links to tutorial solutions as quick references for seL4 calls and methods.
-Next: Pathways through the tutorials From 3e2f994957baa0d078039a8f4e600e21350bbcda Mon Sep 17 00:00:00 2001 From: Birgit Brecknell Date: Wed, 17 Jul 2024 16:42:26 +1000 Subject: [PATCH 058/111] revert to old tutorials structure Signed-off-by: Birgit Brecknell --- Makefile | 2 +- Tutorials/GettingStarted/overview.md | 41 --- Tutorials/Resources/how-to.md | 338 +++++++++--------- Tutorials/{CAmkES => }/camkes-vm-crossvm.md | 0 Tutorials/{CAmkES => }/camkes-vm-linux.md | 0 Tutorials/{seL4 => }/capabilities.md | 0 Tutorials/{DynamicLibraries => }/dynamic-1.md | 0 Tutorials/{DynamicLibraries => }/dynamic-2.md | 0 Tutorials/{DynamicLibraries => }/dynamic-3.md | 0 Tutorials/{DynamicLibraries => }/dynamic-4.md | 2 +- Tutorials/{seL4 => }/fault-handlers.md | 2 +- Tutorials/{seL4 => }/get-the-tutorials.md | 0 Tutorials/{CAmkES => }/hello-camkes-0.md | 0 Tutorials/{CAmkES => }/hello-camkes-1.md | 0 Tutorials/{CAmkES => }/hello-camkes-2.md | 0 Tutorials/{CAmkES => }/hello-camkes-timer.md | 0 Tutorials/{seL4 => }/hello-world.md | 0 Tutorials/index.md | 32 ++ Tutorials/{seL4 => }/interrupts.md | 0 Tutorials/{seL4 => }/ipc.md | 0 Tutorials/{seL4 => }/mapping.md | 0 Tutorials/{MCS => }/mcs.md | 2 +- Tutorials/{seL4 => }/notifications.md | 0 Tutorials/{GettingStarted => }/pathways.md | 20 +- .../{seL4/overview.md => sel4-overview.md} | 2 +- Tutorials/{seL4 => }/setting-up.md | 2 +- Tutorials/{seL4 => }/threads.md | 0 Tutorials/{seL4 => }/untyped.md | 0 _includes/nav-sidebar.html | 62 ++-- index.md | 8 +- 30 files changed, 251 insertions(+), 262 deletions(-) delete mode 100644 Tutorials/GettingStarted/overview.md rename Tutorials/{CAmkES => }/camkes-vm-crossvm.md (100%) rename Tutorials/{CAmkES => }/camkes-vm-linux.md (100%) rename Tutorials/{seL4 => }/capabilities.md (100%) rename Tutorials/{DynamicLibraries => }/dynamic-1.md (100%) rename Tutorials/{DynamicLibraries => }/dynamic-2.md (100%) rename Tutorials/{DynamicLibraries => }/dynamic-3.md (100%) rename Tutorials/{DynamicLibraries => }/dynamic-4.md (80%) rename Tutorials/{seL4 => }/fault-handlers.md (87%) rename Tutorials/{seL4 => }/get-the-tutorials.md (100%) rename Tutorials/{CAmkES => }/hello-camkes-0.md (100%) rename Tutorials/{CAmkES => }/hello-camkes-1.md (100%) rename Tutorials/{CAmkES => }/hello-camkes-2.md (100%) rename Tutorials/{CAmkES => }/hello-camkes-timer.md (100%) rename Tutorials/{seL4 => }/hello-world.md (100%) rename Tutorials/{seL4 => }/interrupts.md (100%) rename Tutorials/{seL4 => }/ipc.md (100%) rename Tutorials/{seL4 => }/mapping.md (100%) rename Tutorials/{MCS => }/mcs.md (78%) rename Tutorials/{seL4 => }/notifications.md (100%) rename Tutorials/{GettingStarted => }/pathways.md (76%) rename Tutorials/{seL4/overview.md => sel4-overview.md} (94%) rename Tutorials/{seL4 => }/setting-up.md (97%) rename Tutorials/{seL4 => }/threads.md (100%) rename Tutorials/{seL4 => }/untyped.md (100%) diff --git a/Makefile b/Makefile index 074e4253cd..ee65a3a866 100644 --- a/Makefile +++ b/Makefile @@ -51,7 +51,7 @@ _repos/tutes: _repos/tutes/%.md: _repos/sel4proj/sel4-tutorials/tutorials/% _repos/tutes PYTHONPATH=_repos/sel4/capdl/python-capdl-tool _repos/sel4proj/sel4-tutorials/template.py --docsite --out-dir _repos/tutes --tut-file $$(@F) -TUTORIALS:= $(filter-out index.md overview.md setting-up.md get-the-tutorials.md,$(notdir $(wildcard Tutorials/seL4/*.md Tutorials/CAmkES/*.md Tutorials/DynamicLibraries/*.md Tutorials/MCS/*.md))) +TUTORIALS:= $(filter-out index.md get-the-tutorials.md pathways.md sel4-overview.md setting-up.md,$(notdir $(wildcard Tutorials/*.md))) tutorials: ${TUTORIALS:%=_repos/tutes/%} _generate_api_pages: $(REPOSITORIES) diff --git a/Tutorials/GettingStarted/overview.md b/Tutorials/GettingStarted/overview.md deleted file mode 100644 index c313a2c84d..0000000000 --- a/Tutorials/GettingStarted/overview.md +++ /dev/null @@ -1,41 +0,0 @@ ---- -toc: true -title: Overview -layout: tutorial -redirect_from: - - /tutorials/ -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. ---- -# Overview - -We have developed a series of tutorials to introduce seL4 and developing systems on seL4. - -## List of tutorials -The tutorials are split into a number of broad categories, and have been designed around developer needs. - -- The [seL4 tutorials](../seL4/overview.md) are for people keen to learn about the base mechanisms provided by the seL4 kernel. The kernel API is explained with short exercises that show basic examples. - -- [MCS](../MCS/mcs) introduces seL4 MCS extensions, which are detailed in this [paper](https://trustworthy.systems/publications/full_text/Lyons_MAH_18.pdf) and [PhD](https://github.com/pingerino/phd/blob/master/phd.pdf). - -- [Dynamic Libraries](../DynamicLibraries/dynamic-1) provides walkthroughs and exercises for using the dynamic libraries provided in `seL4_libs`, which were developed for rapidly prototyping systems on seL4. - -- [CAmkES](../CAmkES/hello-camkes-0) generates the glue code for interacting with seL4 and is designed for building high-assurance, static systems. These tutorials demonstrate how to configure static systems through components. - -- [Microkit](https://trustworthy.systems/projects/microkit/tutorial/) enables system designers to create static software systems based on the seL4 microkernel. We recommend this as a potential introduction to seL4, bearing in mind that the Microkit hides many of the seL4 mechanisms - it is designed that way, to make building on top of seL4 easier. - -- [Rust](https://github.com/seL4/rust-sel4) allows people to write safer user-level code on top of seL4 without needing full formal verification, with a language that is receiving increasing interest and that aligns extremely well with security and safety critical embedded systems programming. - -## Resources -Additional resources to assist with learning: -- The [seL4 manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf) -- [API references](../../projects/sel4/api-doc) -- The [How to](../Resources/how-to) page provides links to tutorial solutions as quick references for seL4 calls and methods. -- The [seL4 white paper](https://sel4.systems/About/seL4-whitepaper.pdf) -- [FAQs](../../projects/sel4/frequently-asked-questions) -- [Debugging guide](../../projects/sel4-tutorials/debugging-guide) -- [Contact](../../Resources#contact) - -
- Next: Pathways through the tutorials -
\ No newline at end of file diff --git a/Tutorials/Resources/how-to.md b/Tutorials/Resources/how-to.md index 01fdd64ae9..b7a9d29054 100644 --- a/Tutorials/Resources/how-to.md +++ b/Tutorials/Resources/how-to.md @@ -12,172 +12,172 @@ This guide provides links to tutorial solutions as quick references for seL4 cal ## The seL4 kernel -### [Capabilities](../seL4/capabilities) - - - [Calculate the size of a CSpace](../seL4/capabilities#how-big-is-your-cspace) - - [Copy a capability between CSlots](../seL4/capabilities#copy-a-capability-between-cslots) - - [Delete a capability](../seL4/capabilities#how-do-you-delete-capabilities) - - [Suspend a thread](../seL4/capabilities#suspend-a-thread) - -### [Untyped](../seL4/untyped) - - - [Create an untyped capability](../seL4/untyped#create-an-untyped-capability) - - [Create a TCB object](../seL4/untyped#create-a-tcb-object) - - [Create an endpoint object](../seL4/untyped#create-an-endpoint-object) - - [Create a notification object](../seL4/untyped#create-a-notification-object) - - [Delete an object](../seL4/untyped#delete-the-objects) - -### [Mapping](../seL4/mapping) -- [Map a page directory](../seL4/mapping#map-a-page-directory) -- [Map a page table](../seL4/mapping#map-a-page-table) -- [Remap a page](../seL4/mapping#remap-a-page) -- [Unmap a page](../seL4/mapping#unmapping-pages) - -### [Threads](../seL4/threads) -- [Configure a TCB](../seL4/threads#configure-a-tcb) -- [Change the priority of a thread](../seL4/threads#change-priority-via-sel4_tcb_setpriority) -- [Set initial register state](../seL4/threads#set-initial-register-state) -- [Start the thread](../seL4/threads#start-the-thread) -- [Set the arguments of a thread](../seL4/threads#passing-arguments) -- [Resolve a fault](../seL4/threads#resolving-a-fault) - -### [IPC](../seL4/ipc) - - [Use capability transfer to send the badged capability](../seL4/ipc#use-capability-transfer-to-send-the-badged-capability) - - [Get a message](../seL4/ipc#get-a-message) - - [Reply and wait](../seL4/ipc#reply-and-wait) - - [Save a reply and store reply capabilities](../seL4/ipc#save-a-reply-and-store-reply-capabilities) - -### [Notifications](../seL4/notifications) - - [Set up shared memory](../seL4/notifications#set-up-shared-memory) - - [Signalling](../seL4/notifications#signal-the-producers-to-go) - - [Differentiate signals](../seL4/notifications#differentiate-signals) - -### [Interrupts](../seL4/interrupts) - - [Invoke IRQ control](../seL4/interrupts#invoke-irq-control) - - [Set NTFN](../seL4/interrupts#set-ntfn) - - [Acknowledge an interrupt](../seL4/interrupts#acknowledge-an-interrupt) - -### [Fault handling](../seL4/fault-handlers) - - [Set up an endpoint for thread fault IPC messages](../seL4/fault-handlers#setting-up-the-endpoint-to-be-used-for-thread-fault-ipc-messages) - - [Receive an IPC message from the kernel](../seL4/fault-handlers#receiving-the-ipc-message-from-the-kernel) - - [Get information about a thread fault](../seL4/fault-handlers#finding-out-information-about-the-generated-thread-fault) - - [Handle a thread fault](../seL4/fault-handlers#handling-a-thread-fault) - - [Resume a faulting thread](../seL4/fault-handlers#resuming-a-faulting-thread) - -## [MCS Extensions](../MCS/mcs) - - [Set up a periodic thread](../MCS/mcs#periodic-threads) - - [Unbind a scheduling context](../MCS/mcs#unbinding-scheduling-contexts) - - [Experiment with sporadic tasks](../MCS/mcs#sporadic-threads) - - [Use passive servers](../MCS/mcs#passive-servers) - - [Configure fault endpoints](../MCS/mcs#configuring-a-fault-endpoint-on-the-mcs-kernel) - -## [Dynamic libraries](../DynamicLibraries/dynamic-1) - -### [Initiliasation & threading](../DynamicLibraries/dynamic-1) - - [Obtain BootInfo](../DynamicLibraries/dynamic-1#obtain-bootinfo) - - [Initialise simple](../DynamicLibraries/dynamic-1#initialise-simple) - - [Use simple to print BootInfo](../DynamicLibraries/dynamic-1#use-simple-to-print-bootinfo) - - [Initialise an allocator](../DynamicLibraries/dynamic-1#initialise-an-allocator) - - [Obtain a generic allocation interface (vka)](../DynamicLibraries/dynamic-1#obtain-a-generic-allocation-interface-vka) - - [Find the CSpace root cap](../DynamicLibraries/dynamic-1#find-the-cspace-root-cap) - - [Find the VSpace root cap](../DynamicLibraries/dynamic-1#find-the-vspace-root-cap) - - [Allocate a TCB Object](../DynamicLibraries/dynamic-1#allocate-a-tcb-object) - - [Configure the new TCB](../DynamicLibraries/dynamic-1#configure-the-new-tcb) - - [Name the new TCB](../DynamicLibraries/dynamic-1#name-the-new-tcb) - - [Set the instruction pointer](../DynamicLibraries/dynamic-1#set-the-instruction-pointer) - - [Set the stack pointer](../DynamicLibraries/dynamic-1#set-the-stack-pointer) - - [Write the registers](../DynamicLibraries/dynamic-1#write-the-registers) - - [Start the new thread](../DynamicLibraries/dynamic-1#start-the-new-thread) - - [Print](../DynamicLibraries/dynamic-1#print-something) - -### [IPC](../DynamicLibraries/dynamic-2) - - [Allocate an IPC buffer](../DynamicLibraries/dynamic-2#allocate-an-ipc-buffer) - - [Allocate a page table](../DynamicLibraries/dynamic-2#allocate-a-page-table) - - [Map a page table](../DynamicLibraries/dynamic-2#map-a-page-table) - - [Map a page](../DynamicLibraries/dynamic-2#map-a-page) - - [Allocate an endpoint](../DynamicLibraries/dynamic-2#allocate-an-endpoint) - - [Badge an endpoint](../DynamicLibraries/dynamic-2#badge-an-endpoint) - - [Set a message register](../DynamicLibraries/dynamic-2#message-registers) - - [Send and wait for a reply](../DynamicLibraries/dynamic-2#ipc) - - [Receive a reply](../DynamicLibraries/dynamic-2#receive-a-reply) - - [Receive an IPC](../DynamicLibraries/dynamic-2#receive-an-ipc) - - [Validate a message](../DynamicLibraries/dynamic-2#validate-the-message) - - [Write the message registers](../DynamicLibraries/dynamic-2#write-the-message-registers) - - [Reply to a message](../DynamicLibraries/dynamic-2#reply-to-a-message) - -### [Processes & Elf loading](../DynamicLibraries/dynamic-3) - - [Create a VSpace object](../DynamicLibraries/dynamic-3#virtual-memory-management) - - [Configure a process](../DynamicLibraries/dynamic-3#configure-a-process) - - [Get a cspacepath](../DynamicLibraries/dynamic-3#get-a-cspacepath) - - [Badge a capability](../DynamicLibraries/dynamic-3#badge-a-capability) - - [Spawn a process](../DynamicLibraries/dynamic-3#spawn-a-process) - - [Receive a message](../DynamicLibraries/dynamic-3#receive-a-message) - - [Send a reply](../DynamicLibraries/dynamic-3#send-a-reply) - - [Initiate communications by using seL4_Call](../DynamicLibraries/dynamic-3#client-call) - -### [Timer](../DynamicLibraries/dynamic-4) - - [Allocate a notification object](../DynamicLibraries/dynamic-4#allocate-a-notification-object) - - [Initialise a timer](../DynamicLibraries/dynamic-4#initialise-the-timer) - - [Use a timer](../DynamicLibraries/dynamic-4#use-the-timer) - - [Handle an interrupt](../DynamicLibraries/dynamic-4#handle-the-interrupt) - - [Destroy a timer](../DynamicLibraries/dynamic-4#destroy-the-timer) - -## [CAmkES](../CAmkES/hello-camkes-0) - -### [A basic CAmkES application](../CAmkES/hello-camkes-1) - - [Define an instance in the composition section of the ADL](../CAmkES/hello-camkes-1#define-an-instance-in-the-composition-section-of-the-adl) - - [Add a connection](../CAmkES/hello-camkes-1#add-a-connection) - - [Define an interface](../CAmkES/hello-camkes-1#define-an-interface) - - [Implement a RPC function](../CAmkES/hello-camkes-1#implement-a-rpc-function) - - [Invoke a RPC function](../CAmkES/hello-camkes-1#invoke-a-rpc-function) - -### [Events in CAmkES](../CAmkES/hello-camkes-2) - - [Specify an events interface](../CAmkES/hello-camkes-2#specify-an-events-interface) - - [Add connections](../CAmkES/hello-camkes-2#add-connections) - - [Wait for data to become available](../CAmkES/hello-camkes-2#wait-for-data-to-become-available) - - [Signal that data is available](../CAmkES/hello-camkes-2#signal-that-data-is-available) - - [Register a callback handler](../CAmkES/hello-camkes-2#register-a-callback-handler) - - [Specify dataport interfaces](../CAmkES/hello-camkes-2#specify-dataport-interfaces) - - [Specify dataport connections](../CAmkES/hello-camkes-2#specify-dataport-connections) - - [Copy strings to an untyped dataport](../CAmkES/hello-camkes-2#copy-strings-to-an-untyped-dataport) - - [Read the reply data from a typed dataport](../CAmkES/hello-camkes-2#read-the-reply-data-from-a-typed-dataport) - - [Send data using dataports](../CAmkES/hello-camkes-2#send-data-using-dataports) - - [Read data from an untyped dataport](../CAmkES/hello-camkes-2#read-data-from-an-untyped-dataport) - - [Put data into a typed dataport](../CAmkES/hello-camkes-2#put-data-into-a-typed-dataport) - - [Read data from a typed dataport](../CAmkES/hello-camkes-2#read-data-from-a-typed-dataport) - - [Set component priorities](../CAmkES/hello-camkes-2#set-component-priorities) - - [Restrict access to dataports](../CAmkES/hello-camkes-2#restrict-access-to-dataports) - - [Test the read and write permissions on the dataport](../CAmkES/hello-camkes-2#test-the-read-and-write-permissions-on-the-dataport) - -### [CAmkES Timer](../CAmkES/hello-camkes-timer) - - [Instantiate a Timer and Timerbase](../CAmkES/hello-camkes-timer#instantiate-a-timer-and-timerbase) - - [Connect a timer driver component](../CAmkES/hello-camkes-timer#connect-a-timer-driver-component) - - [Configure a timer hardware component instance](../CAmkES/hello-camkes-timer#configure-a-timer-hardware-component-instance) - - [Call into a supplied driver to handle the interrupt](../CAmkES/hello-camkes-timer#call-into-a-supplied-driver-to-handle-the-interrupt) - - [Stop a timer](../CAmkES/hello-camkes-timer#stop-a-timer) - - [Acknowledge an interrupt](../CAmkES/hello-camkes-timer#acknowledge-an-interrupt) - - [Get a timer handler](../CAmkES/hello-camkes-timer#get-a-timer-handler) - - [Start a timer](../CAmkES/hello-camkes-timer#start-a-timer) - - [Implement a RPC interface](../CAmkES/hello-camkes-timer#implement-a-rpc-interface) - - [Set a timer interrupt](../CAmkES/hello-camkes-timer#set-a-timer-interrupt) - - [Instantiate a TimerDTB component](../CAmkES/hello-camkes-timer#instantiate-a-timerdtb-component) - - [Connect interfaces using the seL4DTBHardware connector](../CAmkES/hello-camkes-timer#connect-interfaces-using-the-sel4dtbhardware-connector) - - [Configure the TimerDTB component](../CAmkES/hello-camkes-timer#configure-the-timerdtb-component) - - [Handle the interrupt](../CAmkES/hello-camkes-timer#handle-the-interrupt) - - [Stop the timer](../CAmkES/hello-camkes-timer#stop-the-timer) - -### [CAmkES VM Linux](../CAmkES/camkes-vm-linux) - - [Add a program](../CAmkES/camkes-vm-linux#adding-a-program) - - [Add a kernel module](../CAmkES/camkes-vm-linux#adding-a-kernel-module) - - [Create a hypercall](../CAmkES/camkes-vm-linux#creating-a-hypercall) - -### [CAmkeES Cross VM Connectors](../CAmkES/camkes-vm-crossvm) - - [Add modules to the guest](../CAmkES/camkes-vm-crossvm#add-modules-to-the-guest) - - [Define interfaces in the VMM](../CAmkES/camkes-vm-crossvm#define-interfaces-in-the-vmm) - - [Define the component interface](../CAmkES/camkes-vm-crossvm#define-the-component-interface) - - [Instantiate the print server](../CAmkES/camkes-vm-crossvm#instantiate-the-print-server) - - [Implement the print server](../CAmkES/camkes-vm-crossvm#implement-the-print-server) - - [Implement the VMM side of the connection](../CAmkES/camkes-vm-crossvm#implement-the-vmm-side-of-the-connection) - - [Update the build system](../CAmkES/camkes-vm-crossvm#update-the-build-system) - - [Add interfaces to the Guest](../CAmkES/camkes-vm-crossvm#add-interfaces-to-the-guest) - - [Create a process](../CAmkES/camkes-vm-crossvm#create-a-process) \ No newline at end of file +### [Capabilities](../capabilities.md) + + - [Calculate the size of a CSpace](../capabilities.md#how-big-is-your-cspace) + - [Copy a capability between CSlots](../capabilities.md#copy-a-capability-between-cslots) + - [Delete a capability](../capabilities.md#how-do-you-delete-capabilities) + - [Suspend a thread](../capabilities.md#suspend-a-thread) + +### [Untyped](../untyped.md) + + - [Create an untyped capability](../untyped.md#create-an-untyped-capability) + - [Create a TCB object](../untyped.md#create-a-tcb-object) + - [Create an endpoint object](../untyped.md#create-an-endpoint-object) + - [Create a notification object](../untyped.md#create-a-notification-object) + - [Delete an object](../untyped.md#delete-the-objects) + +### [Mapping](../mapping.md) +- [Map a page directory](../mapping.md#map-a-page-directory) +- [Map a page table](../mapping.md#map-a-page-table) +- [Remap a page](../mapping.md#remap-a-page) +- [Unmap a page](../mapping.md#unmapping-pages) + +### [Threads](../threads.md) +- [Configure a TCB](../threads.md#configure-a-tcb) +- [Change the priority of a thread](../threads.md#change-priority-via-sel4_tcb_setpriority) +- [Set initial register state](../threads.md#set-initial-register-state) +- [Start the thread](../threads.md#start-the-thread) +- [Set the arguments of a thread](../threads.md#passing-arguments) +- [Resolve a fault](../threads.md#resolving-a-fault) + +### [IPC](../ipc.md) + - [Use capability transfer to send the badged capability](../ipc.md#use-capability-transfer-to-send-the-badged-capability) + - [Get a message](../ipc.md#get-a-message) + - [Reply and wait](../ipc.md#reply-and-wait) + - [Save a reply and store reply capabilities](../ipc.md#save-a-reply-and-store-reply-capabilities) + +### [Notifications](../notifications.md) + - [Set up shared memory](../notifications.md#set-up-shared-memory) + - [Signalling](../notifications.md#signal-the-producers-to-go) + - [Differentiate signals](../notifications.md#differentiate-signals) + +### [Interrupts](../interrupts.md) + - [Invoke IRQ control](../interrupts.md#invoke-irq-control) + - [Set NTFN](../interrupts.md#set-ntfn) + - [Acknowledge an interrupt](../interrupts.md#acknowledge-an-interrupt) + +### [Fault handling](../fault-handlers.md) + - [Set up an endpoint for thread fault IPC messages](../fault-handlers.md#setting-up-the-endpoint-to-be-used-for-thread-fault-ipc-messages) + - [Receive an IPC message from the kernel](../fault-handlers.md#receiving-the-ipc-message-from-the-kernel) + - [Get information about a thread fault](../fault-handlers.md#finding-out-information-about-the-generated-thread-fault) + - [Handle a thread fault](../fault-handlers.md#handling-a-thread-fault) + - [Resume a faulting thread](../fault-handlers.md#resuming-a-faulting-thread) + +## [MCS Extensions](../mcs.md) + - [Set up a periodic thread](../mcs.md#periodic-threads) + - [Unbind a scheduling context](../mcs.md#unbinding-scheduling-contexts) + - [Experiment with sporadic tasks](../mcs.md#sporadic-threads) + - [Use passive servers](../mcs.md#passive-servers) + - [Configure fault endpoints](../mcs.md#configuring-a-fault-endpoint-on-the-mcs-kernel) + +## [Dynamic libraries](../dynamic-1.md) + +### [Initiliasation & threading](../dynamic-1.md) + - [Obtain BootInfo](../dynamic-1.md#obtain-bootinfo) + - [Initialise simple](../dynamic-1.md#initialise-simple) + - [Use simple to print BootInfo](../dynamic-1.md#use-simple-to-print-bootinfo) + - [Initialise an allocator](../dynamic-1.md#initialise-an-allocator) + - [Obtain a generic allocation interface (vka)](../dynamic-1.md#obtain-a-generic-allocation-interface-vka) + - [Find the CSpace root cap](../dynamic-1.md#find-the-cspace-root-cap) + - [Find the VSpace root cap](../dynamic-1.md#find-the-vspace-root-cap) + - [Allocate a TCB Object](../dynamic-1.md#allocate-a-tcb-object) + - [Configure the new TCB](../dynamic-1.md#configure-the-new-tcb) + - [Name the new TCB](../dynamic-1.md#name-the-new-tcb) + - [Set the instruction pointer](../dynamic-1.md#set-the-instruction-pointer) + - [Set the stack pointer](../dynamic-1.md#set-the-stack-pointer) + - [Write the registers](../dynamic-1.md#write-the-registers) + - [Start the new thread](../dynamic-1.md#start-the-new-thread) + - [Print](../dynamic-1.md#print-something) + +### [IPC](../dynamic-2.md) + - [Allocate an IPC buffer](../dynamic-2.md#allocate-an-ipc-buffer) + - [Allocate a page table](../dynamic-2.md#allocate-a-page-table) + - [Map a page table](../dynamic-2.md#map-a-page-table) + - [Map a page](../dynamic-2.md#map-a-page) + - [Allocate an endpoint](../dynamic-2.md#allocate-an-endpoint) + - [Badge an endpoint](../dynamic-2.md#badge-an-endpoint) + - [Set a message register](../dynamic-2.md#message-registers) + - [Send and wait for a reply](../dynamic-2.md#ipc) + - [Receive a reply](../dynamic-2.md#receive-a-reply) + - [Receive an IPC](../dynamic-2.md#receive-an-ipc) + - [Validate a message](../dynamic-2.md#validate-the-message) + - [Write the message registers](../dynamic-2.md#write-the-message-registers) + - [Reply to a message](../dynamic-2.md#reply-to-a-message) + +### [Processes & Elf loading](../dynamic-3.md) + - [Create a VSpace object](../dynamic-3.md#virtual-memory-management) + - [Configure a process](../dynamic-3.md#configure-a-process) + - [Get a cspacepath](../dynamic-3.md#get-a-cspacepath) + - [Badge a capability](../dynamic-3.md#badge-a-capability) + - [Spawn a process](../dynamic-3.md#spawn-a-process) + - [Receive a message](../dynamic-3.md#receive-a-message) + - [Send a reply](../dynamic-3.md#send-a-reply) + - [Initiate communications by using seL4_Call](../dynamic-3.md#client-call) + +### [Timer](../dynamic-4.md) + - [Allocate a notification object](../dynamic-4.md#allocate-a-notification-object) + - [Initialise a timer](../dynamic-4.md#initialise-the-timer) + - [Use a timer](../dynamic-4.md#use-the-timer) + - [Handle an interrupt](../dynamic-4.md#handle-the-interrupt) + - [Destroy a timer](../dynamic-4.md#destroy-the-timer) + +## [CAmkES](../hello-camkes-0.md) + +### [A basic CAmkES application](../hello-camkes-1.md) + - [Define an instance in the composition section of the ADL](../hello-camkes-1.md#define-an-instance-in-the-composition-section-of-the-adl) + - [Add a connection](../hello-camkes-1.md#add-a-connection) + - [Define an interface](../hello-camkes-1.md#define-an-interface) + - [Implement a RPC function](../hello-camkes-1.md#implement-a-rpc-function) + - [Invoke a RPC function](../hello-camkes-1.md#invoke-a-rpc-function) + +### [Events in CAmkES](../hello-camkes-2.md) + - [Specify an events interface](../hello-camkes-2.md#specify-an-events-interface) + - [Add connections](../hello-camkes-2.md#add-connections) + - [Wait for data to become available](../hello-camkes-2.md#wait-for-data-to-become-available) + - [Signal that data is available](../hello-camkes-2.md#signal-that-data-is-available) + - [Register a callback handler](../hello-camkes-2.md#register-a-callback-handler) + - [Specify dataport interfaces](../hello-camkes-2.md#specify-dataport-interfaces) + - [Specify dataport connections](../hello-camkes-2.md#specify-dataport-connections) + - [Copy strings to an untyped dataport](../hello-camkes-2.md#copy-strings-to-an-untyped-dataport) + - [Read the reply data from a typed dataport](../hello-camkes-2.md#read-the-reply-data-from-a-typed-dataport) + - [Send data using dataports](../hello-camkes-2.md#send-data-using-dataports) + - [Read data from an untyped dataport](../hello-camkes-2.md#read-data-from-an-untyped-dataport) + - [Put data into a typed dataport](../hello-camkes-2.md#put-data-into-a-typed-dataport) + - [Read data from a typed dataport](../hello-camkes-2.md#read-data-from-a-typed-dataport) + - [Set component priorities](../hello-camkes-2.md#set-component-priorities) + - [Restrict access to dataports](../hello-camkes-2.md#restrict-access-to-dataports) + - [Test the read and write permissions on the dataport](../hello-camkes-2.md#test-the-read-and-write-permissions-on-the-dataport) + +### [CAmkES Timer](../hello-camkes-timer.md) + - [Instantiate a Timer and Timerbase](../hello-camkes-timer.md#instantiate-a-timer-and-timerbase) + - [Connect a timer driver component](../hello-camkes-timer.md#connect-a-timer-driver-component) + - [Configure a timer hardware component instance](../hello-camkes-timer.md#configure-a-timer-hardware-component-instance) + - [Call into a supplied driver to handle the interrupt](../hello-camkes-timer.md#call-into-a-supplied-driver-to-handle-the-interrupt) + - [Stop a timer](../hello-camkes-timer.md#stop-a-timer) + - [Acknowledge an interrupt](../hello-camkes-timer.md#acknowledge-an-interrupt) + - [Get a timer handler](../hello-camkes-timer.md#get-a-timer-handler) + - [Start a timer](../hello-camkes-timer.md#start-a-timer) + - [Implement a RPC interface](../hello-camkes-timer.md#implement-a-rpc-interface) + - [Set a timer interrupt](../hello-camkes-timer.md#set-a-timer-interrupt) + - [Instantiate a TimerDTB component](../hello-camkes-timer.md#instantiate-a-timerdtb-component) + - [Connect interfaces using the seL4DTBHardware connector](../hello-camkes-timer.md#connect-interfaces-using-the-sel4dtbhardware-connector) + - [Configure the TimerDTB component](../hello-camkes-timer.md#configure-the-timerdtb-component) + - [Handle the interrupt](../hello-camkes-timer.md#handle-the-interrupt) + - [Stop the timer](../hello-camkes-timer.md#stop-the-timer) + +### [CAmkES VM Linux](../camkes-vm-linux.md) + - [Add a program](../camkes-vm-linux.md#adding-a-program) + - [Add a kernel module](../camkes-vm-linux.md#adding-a-kernel-module) + - [Create a hypercall](../camkes-vm-linux.md#creating-a-hypercall) + +### [CAmkeES Cross VM Connectors](../camkes-vm-crossvm.md) + - [Add modules to the guest](../camkes-vm-crossvm.md#add-modules-to-the-guest) + - [Define interfaces in the VMM](../camkes-vm-crossvm.md#define-interfaces-in-the-vmm) + - [Define the component interface](../camkes-vm-crossvm.md#define-the-component-interface) + - [Instantiate the print server](../camkes-vm-crossvm.md#instantiate-the-print-server) + - [Implement the print server](../camkes-vm-crossvm.md#implement-the-print-server) + - [Implement the VMM side of the connection](../camkes-vm-crossvm.md#implement-the-vmm-side-of-the-connection) + - [Update the build system](../camkes-vm-crossvm.md#update-the-build-system) + - [Add interfaces to the Guest](../camkes-vm-crossvm.md#add-interfaces-to-the-guest) + - [Create a process](../camkes-vm-crossvm.md#create-a-process) \ No newline at end of file diff --git a/Tutorials/CAmkES/camkes-vm-crossvm.md b/Tutorials/camkes-vm-crossvm.md similarity index 100% rename from Tutorials/CAmkES/camkes-vm-crossvm.md rename to Tutorials/camkes-vm-crossvm.md diff --git a/Tutorials/CAmkES/camkes-vm-linux.md b/Tutorials/camkes-vm-linux.md similarity index 100% rename from Tutorials/CAmkES/camkes-vm-linux.md rename to Tutorials/camkes-vm-linux.md diff --git a/Tutorials/seL4/capabilities.md b/Tutorials/capabilities.md similarity index 100% rename from Tutorials/seL4/capabilities.md rename to Tutorials/capabilities.md diff --git a/Tutorials/DynamicLibraries/dynamic-1.md b/Tutorials/dynamic-1.md similarity index 100% rename from Tutorials/DynamicLibraries/dynamic-1.md rename to Tutorials/dynamic-1.md diff --git a/Tutorials/DynamicLibraries/dynamic-2.md b/Tutorials/dynamic-2.md similarity index 100% rename from Tutorials/DynamicLibraries/dynamic-2.md rename to Tutorials/dynamic-2.md diff --git a/Tutorials/DynamicLibraries/dynamic-3.md b/Tutorials/dynamic-3.md similarity index 100% rename from Tutorials/DynamicLibraries/dynamic-3.md rename to Tutorials/dynamic-3.md diff --git a/Tutorials/DynamicLibraries/dynamic-4.md b/Tutorials/dynamic-4.md similarity index 80% rename from Tutorials/DynamicLibraries/dynamic-4.md rename to Tutorials/dynamic-4.md index 75e3a9b9b0..7dac922784 100644 --- a/Tutorials/DynamicLibraries/dynamic-4.md +++ b/Tutorials/dynamic-4.md @@ -11,4 +11,4 @@ SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. {% include tutorial.md %} -Next tutorial: Hello CAmkES +Next tutorial: Hello CAmkES diff --git a/Tutorials/seL4/fault-handlers.md b/Tutorials/fault-handlers.md similarity index 87% rename from Tutorials/seL4/fault-handlers.md rename to Tutorials/fault-handlers.md index cd508d663c..50f844a4f0 100644 --- a/Tutorials/seL4/fault-handlers.md +++ b/Tutorials/fault-handlers.md @@ -11,4 +11,4 @@ SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. {% include tutorial.md %} -Next tutorial: MCS +Next tutorial: MCS diff --git a/Tutorials/seL4/get-the-tutorials.md b/Tutorials/get-the-tutorials.md similarity index 100% rename from Tutorials/seL4/get-the-tutorials.md rename to Tutorials/get-the-tutorials.md diff --git a/Tutorials/CAmkES/hello-camkes-0.md b/Tutorials/hello-camkes-0.md similarity index 100% rename from Tutorials/CAmkES/hello-camkes-0.md rename to Tutorials/hello-camkes-0.md diff --git a/Tutorials/CAmkES/hello-camkes-1.md b/Tutorials/hello-camkes-1.md similarity index 100% rename from Tutorials/CAmkES/hello-camkes-1.md rename to Tutorials/hello-camkes-1.md diff --git a/Tutorials/CAmkES/hello-camkes-2.md b/Tutorials/hello-camkes-2.md similarity index 100% rename from Tutorials/CAmkES/hello-camkes-2.md rename to Tutorials/hello-camkes-2.md diff --git a/Tutorials/CAmkES/hello-camkes-timer.md b/Tutorials/hello-camkes-timer.md similarity index 100% rename from Tutorials/CAmkES/hello-camkes-timer.md rename to Tutorials/hello-camkes-timer.md diff --git a/Tutorials/seL4/hello-world.md b/Tutorials/hello-world.md similarity index 100% rename from Tutorials/seL4/hello-world.md rename to Tutorials/hello-world.md diff --git a/Tutorials/index.md b/Tutorials/index.md index def57a79e0..2e05d14237 100644 --- a/Tutorials/index.md +++ b/Tutorials/index.md @@ -4,3 +4,35 @@ layout: tutorial SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. --- +# Overview + +We have developed a series of tutorials to introduce seL4 and developing systems on seL4. + +## List of tutorials +The tutorials are split into a number of broad categories, and have been designed around developer needs. + +- The [seL4 tutorials](../sel4-overview) are for people keen to learn about the base mechanisms provided by the seL4 kernel. The kernel API is explained with short exercises that show basic examples. + +- [MCS](../MCS/mcs) introduces seL4 MCS extensions, which are detailed in this [paper](https://trustworthy.systems/publications/full_text/Lyons_MAH_18.pdf) and [PhD](https://github.com/pingerino/phd/blob/master/phd.pdf). + +- [Dynamic Libraries](../DynamicLibraries/dynamic-1) provides walkthroughs and exercises for using the dynamic libraries provided in `seL4_libs`, which were developed for rapidly prototyping systems on seL4. + +- [CAmkES](../CAmkES/hello-camkes-0) generates the glue code for interacting with seL4 and is designed for building high-assurance, static systems. These tutorials demonstrate how to configure static systems through components. + +- [Microkit](https://trustworthy.systems/projects/microkit/tutorial/) enables system designers to create static software systems based on the seL4 microkernel. We recommend this as a potential introduction to seL4, bearing in mind that the Microkit hides many of the seL4 mechanisms - it is designed that way, to make building on top of seL4 easier. + +- [Rust](https://github.com/seL4/rust-sel4) allows people to write safer user-level code on top of seL4 without needing full formal verification, with a language that is receiving increasing interest and that aligns extremely well with security and safety critical embedded systems programming. + +## Resources +Additional resources to assist with learning: +- The [seL4 manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf) +- [API references](../../projects/sel4/api-doc) +- The [How to](../Resources/how-to) page provides links to tutorial solutions as quick references for seL4 calls and methods. +- The [seL4 white paper](https://sel4.systems/About/seL4-whitepaper.pdf) +- [FAQs](../../projects/sel4/frequently-asked-questions) +- [Debugging guide](../../projects/sel4-tutorials/debugging-guide) +- [Contact](../../Resources#contact) + ++ Next: Pathways through the tutorials +
\ No newline at end of file diff --git a/Tutorials/seL4/interrupts.md b/Tutorials/interrupts.md similarity index 100% rename from Tutorials/seL4/interrupts.md rename to Tutorials/interrupts.md diff --git a/Tutorials/seL4/ipc.md b/Tutorials/ipc.md similarity index 100% rename from Tutorials/seL4/ipc.md rename to Tutorials/ipc.md diff --git a/Tutorials/seL4/mapping.md b/Tutorials/mapping.md similarity index 100% rename from Tutorials/seL4/mapping.md rename to Tutorials/mapping.md diff --git a/Tutorials/MCS/mcs.md b/Tutorials/mcs.md similarity index 78% rename from Tutorials/MCS/mcs.md rename to Tutorials/mcs.md index d6fb87e678..b4ab1a24fb 100644 --- a/Tutorials/MCS/mcs.md +++ b/Tutorials/mcs.md @@ -11,4 +11,4 @@ SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. {% include tutorial.md %} -Next tutorial: Dynamic libraries +Next tutorial: Dynamic libraries diff --git a/Tutorials/seL4/notifications.md b/Tutorials/notifications.md similarity index 100% rename from Tutorials/seL4/notifications.md rename to Tutorials/notifications.md diff --git a/Tutorials/GettingStarted/pathways.md b/Tutorials/pathways.md similarity index 76% rename from Tutorials/GettingStarted/pathways.md rename to Tutorials/pathways.md index 37cffbf2d4..7ff2c72c33 100644 --- a/Tutorials/GettingStarted/pathways.md +++ b/Tutorials/pathways.md @@ -19,9 +19,9 @@ Goals - to see, compile, and run some code Recommended tutorials -- [Setting up your machine](../seL4/setting-up) -- [Getting the tutorials](../seL4/get-the-tutorials.md) -- [Hello world](../seL4/hello-world.md) +- [Setting up your machine](setting-up.md) +- [Getting the tutorials](get-the-tutorials.md) +- [Hello world](hello-world.md) ### System Building Goals @@ -30,14 +30,14 @@ Goals - to build trustworthy systems Recommended tutorials -- [Setting up your machine](../seL4/setting-up) -- [Getting the tutorials](../seL4/get-the-tutorials.md) -- [Hello world](../seL4/hello-world.md) -- [MCS](../MCS/mcs.md) -- The CAmkES tutorials beginning with [Hello CAmkES](../CAmkES/hello-camkes-0.md) +- [Setting up your machine](setting-up.md) +- [Getting the tutorials](get-the-tutorials.md) +- [Hello world](hello-world.md) +- [MCS](mcs.md) +- The CAmkES tutorials beginning with [Hello CAmkES](hello-camkes-0.md) - Virtualisation tutorials - [CAmkES VM](../CAmkES/camkes-vm-linux) using Linux as a guest in the CAmkES VM; and - - [CAmkES Cross-VM communication](../CAmkES/camkes-vm-crossvm.md) walkthrough of adding communication between Linux guests in separate VMs + - [CAmkES Cross-VM communication](camkes-vm-crossvm.md) walkthrough of adding communication between Linux guests in separate VMs ### Platform Development @@ -63,5 +63,5 @@ Recommended tutorials - Follow the tutorial in the default pathway up to and including MCS.- Next tutorial: seL4 tutorials + Next tutorial: seL4 tutorials
\ No newline at end of file diff --git a/Tutorials/seL4/overview.md b/Tutorials/sel4-overview.md similarity index 94% rename from Tutorials/seL4/overview.md rename to Tutorials/sel4-overview.md index ca19081899..ae94d873a4 100644 --- a/Tutorials/seL4/overview.md +++ b/Tutorials/sel4-overview.md @@ -27,5 +27,5 @@ architecture. Suggested resources for these include: - [COMP3231 at UNSW](http://www.cse.unsw.edu.au/~cs3231)- Next tutorial: Setting up your machine + Next tutorial: Setting up your machine
\ No newline at end of file diff --git a/Tutorials/seL4/setting-up.md b/Tutorials/setting-up.md similarity index 97% rename from Tutorials/seL4/setting-up.md rename to Tutorials/setting-up.md index 41f981f125..dd6639698e 100644 --- a/Tutorials/seL4/setting-up.md +++ b/Tutorials/setting-up.md @@ -81,7 +81,7 @@ Hello, welcome to the seL4/CAmkES/L4v docker build environment ``` ### Mapping a container -To run the container from other directories (e.g. starting a container for the [Hello World](hello-world) tutorial, which we'll do next), you can setup a bash alias such as this: +To run the container from other directories (e.g. starting a container for the [Hello World](hello-world.md) tutorial, which we'll do next), you can setup a bash alias such as this: ```bash echo $'alias container=\'make -C /Tutorials and other material to learn about seL4.
- Next tutorial: seL4 tutorials + Next tutorial: Setting up your machine
\ No newline at end of file diff --git a/Tutorials/sel4-overview.md b/Tutorials/sel4-overview.md deleted file mode 100644 index cd3c49af22..0000000000 --- a/Tutorials/sel4-overview.md +++ /dev/null @@ -1,31 +0,0 @@ ---- -toc: true -layout: tutorial -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. ---- - -# Overview -The seL4 tutorials are for people keen to learn about the base mechanisms provided by the seL4 kernel. The kernel API is explained with short exercises that show basic examples. - -While doing these tutorials, we recommend having access to the -- [seL4 white paper](https://sel4.systems/About/seL4-whitepaper.pdf) -- the seL4 manual -- the API references -- the [How to page](how-to), which provides links to tutorial solutions as quick references for seL4 calls and methods - -**Recommended reading** - -Note that all of these tutorials require C programming -experience and some understanding of operating systems and computer -architecture. Suggested resources for these include: - -- C programming language - - [C tutorial](https://www.cprogramming.com/tutorial/c-tutorial.html) -- Operating Systems: - - [Modern Operating Systems (book)](https://www.amazon.com/Modern-Operating-Systems-Andrew-Tanenbaum/dp/013359162X) - - [COMP3231 at UNSW](http://www.cse.unsw.edu.au/~cs3231) - -- Next tutorial: Setting up your machine -
\ No newline at end of file diff --git a/_data/tutorials-sidebar.yml b/_data/tutorials-sidebar.yml index 8c45afeff0..50918a4050 100644 --- a/_data/tutorials-sidebar.yml +++ b/_data/tutorials-sidebar.yml @@ -8,7 +8,7 @@ - name: Getting started type: header -- name: Overview of tutorials +- name: Overview file: "" type: file - name: Tutorial pathways @@ -17,9 +17,6 @@ - name: seL4 type: header -- name: Overview - file: sel4-overview - type: file - name: Setting up your machine file: setting-up type: file diff --git a/index.md b/index.md index 564c57ee72..c205f58261 100644 --- a/index.md +++ b/index.md @@ -63,7 +63,6 @@ This documentation site is for cooperatively developing and sharing documentatioTutorials and other material to learn about seL4.
- Next tutorial: Setting up your machine -
\ No newline at end of file diff --git a/Tutorials/threads.md b/Tutorials/threads.md index 38aaadc5d4..7a1d2f1d8d 100644 --- a/Tutorials/threads.md +++ b/Tutorials/threads.md @@ -7,6 +7,3 @@ SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. --- {% include tutorial.md %} - - -Next tutorial: IPC \ No newline at end of file diff --git a/Tutorials/untyped.md b/Tutorials/untyped.md index 26c74348f9..5948a7a492 100644 --- a/Tutorials/untyped.md +++ b/Tutorials/untyped.md @@ -7,6 +7,3 @@ SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. --- {% include tutorial.md %} - - -Next tutorial: Mapping diff --git a/camkes-vm-crossvm/camkes-vm-crossvm.md b/camkes-vm-crossvm/camkes-vm-crossvm.md new file mode 100644 index 0000000000..72b0e2162c --- /dev/null +++ b/camkes-vm-crossvm/camkes-vm-crossvm.md @@ -0,0 +1,650 @@ + + +/*? declare_task_ordering([ + 'crossvm' +]) ?*/ + +# CAmkES VM: Cross VM Connectors + +This tutorial provides an introduction to using the cross virtual machine (VM) connector mechanisms +provided by seL4 and Camkes in order to connect processes in a guest Linux instance to Camkes components. + +In this tutorial you will learn how to: + +* Configure processes in a Linux guest VM to communicate with CAmkES components + +## Prerequisites +1. [Set up your machine](https://docs.sel4.systems/tutorials/setting-up) +2. [CAmkES VM Linux tutorial](https://docs.sel4.systems/tutorials/camkes-vm-linux) + +*Note that the instructions for this tutorial are for Linux only.* + +## Initialising + +/*? macros.tutorial_init("camkes-vm-crossvm") ?*/ + +- Next: Get the tutorials -
From c6adfe6c06bc94c2ae3ad3e3c1549f0b64395830 Mon Sep 17 00:00:00 2001 From: Birgit Brecknell Date: Fri, 4 Oct 2024 10:29:53 +1000 Subject: [PATCH 105/111] add comment about filtered tut pages Signed-off-by: Birgit Brecknell --- Makefile | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Makefile b/Makefile index 167ed6b3ba..0863471a5e 100644 --- a/Makefile +++ b/Makefile @@ -51,6 +51,9 @@ _repos/tutes: _repos/tutes/%.md: _repos/sel4proj/sel4-tutorials/tutorials/% _repos/tutes PYTHONPATH=_repos/sel4/capdl/python-capdl-tool _repos/sel4proj/sel4-tutorials/template.py --docsite --out-dir _repos/tutes --tut-file $$(@F) +# Make tutorials +# Filter out index.md; get-the-tutorials.md; how-to.md pathways.md; setting-up.md +# which are docsite pages, and not in the tutorials repo TUTORIALS:= $(filter-out index.md get-the-tutorials.md how-to.md pathways.md setting-up.md,$(notdir $(wildcard Tutorials/*.md))) tutorials: ${TUTORIALS:%=_repos/tutes/%} From 6258219f30d86eea44bed25d0c7b9c749a591447 Mon Sep 17 00:00:00 2001 From: Birgit Brecknell Date: Fri, 4 Oct 2024 10:31:35 +1000 Subject: [PATCH 106/111] revert copyright year Signed-off-by: Birgit Brecknell --- Tutorials/hello-world.md | 2 +- Tutorials/index.md | 2 +- Tutorials/setting-up.md | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Tutorials/hello-world.md b/Tutorials/hello-world.md index cb029650f6..0abae7c64f 100644 --- a/Tutorials/hello-world.md +++ b/Tutorials/hello-world.md @@ -4,7 +4,7 @@ title: Hello, World! tutorial: hello-world layout: tutorial SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. --- {% include tutorial.md %} diff --git a/Tutorials/index.md b/Tutorials/index.md index 3f9b635e76..594fd5fbd7 100644 --- a/Tutorials/index.md +++ b/Tutorials/index.md @@ -3,7 +3,7 @@ toc: true title: Tutorials layout: tutorial SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. --- # Overview diff --git a/Tutorials/setting-up.md b/Tutorials/setting-up.md index 20c0bf07cd..1332e61164 100644 --- a/Tutorials/setting-up.md +++ b/Tutorials/setting-up.md @@ -2,7 +2,7 @@ toc: true layout: tutorial SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. --- # Setting up your machine From e20dd4754423a9d8603b18da69b400ac83a3791c Mon Sep 17 00:00:00 2001 From: Birgit Brecknell Date: Fri, 4 Oct 2024 12:51:48 +1000 Subject: [PATCH 107/111] add relative_url for github preview Signed-off-by: Birgit Brecknell --- _includes/header.html | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/_includes/header.html b/_includes/header.html index 54d86f4fe2..f8d2186f76 100644 --- a/_includes/header.html +++ b/_includes/header.html @@ -16,10 +16,10 @@ From a2a59cd8c6afdf2303064db78893f0e23c014194 Mon Sep 17 00:00:00 2001 From: Birgit Brecknell Date: Fri, 4 Oct 2024 17:55:16 +1000 Subject: [PATCH 108/111] fix js code for markdown expansions Signed-off-by: Birgit Brecknell --- Tutorials/how-to.md | 41 ++++++++++++++++++------------------ assets/js/toggle-markdown.js | 18 ++++++---------- 2 files changed, 27 insertions(+), 32 deletions(-) diff --git a/Tutorials/how-to.md b/Tutorials/how-to.md index 4f01cd7d4a..626a1df74d 100644 --- a/Tutorials/how-to.md +++ b/Tutorials/how-to.md @@ -9,17 +9,16 @@ This guide provides links to tutorial solutions as quick references for seL4 cal [//]: # (Show me some foo) - ## The seL4 kernel -### [Capabilities](capabilities.md) +### [Capabilities](capabilities?tut_expand) - [Calculate the size of a CSpace](capabilities.md#how-big-is-your-cspace) - [Copy a capability between CSlots](capabilities.md#copy-a-capability-between-cslots) - [Delete a capability](capabilities.md#how-do-you-delete-capabilities) - [Suspend a thread](capabilities.md#suspend-a-thread) -### [Untyped](untyped.md) +### [Untyped](untyped?tut_expand) - [Create an untyped capability](untyped.md#create-an-untyped-capability) - [Create a TCB object](untyped.md#create-a-tcb-object) @@ -27,13 +26,13 @@ This guide provides links to tutorial solutions as quick references for seL4 cal - [Create a notification object](untyped.md#create-a-notification-object) - [Delete an object](untyped.md#delete-the-objects) -### [Mapping](mapping.md) +### [Mapping](mapping?tut_expand) - [Map a page directory](mapping.md#map-a-page-directory) - [Map a page table](mapping.md#map-a-page-table) - [Remap a page](mapping.md#remap-a-page) - [Unmap a page](mapping.md#unmapping-pages) -### [Threads](threads.md) +### [Threads](threads?tut_expand) - [Configure a TCB](threads.md#configure-a-tcb) - [Change the priority of a thread](threads.md#change-priority-via-sel4_tcb_setpriority) - [Set initial register state](threads.md#set-initial-register-state) @@ -41,39 +40,39 @@ This guide provides links to tutorial solutions as quick references for seL4 cal - [Set the arguments of a thread](threads.md#passing-arguments) - [Resolve a fault](threads.md#resolving-a-fault) -### [IPC](ipc.md) +### [IPC](ipc?tut_expand) - [Use capability transfer to send the badged capability](ipc.md#use-capability-transfer-to-send-the-badged-capability) - [Get a message](ipc.md#get-a-message) - [Reply and wait](ipc.md#reply-and-wait) - [Save a reply and store reply capabilities](ipc.md#save-a-reply-and-store-reply-capabilities) -### [Notifications](notifications.md) +### [Notifications](notifications?tut_expand) - [Set up shared memory](notifications.md#set-up-shared-memory) - [Signalling](notifications.md#signal-the-producers-to-go) - [Differentiate signals](notifications.md#differentiate-signals) -### [Interrupts](interrupts.md) +### [Interrupts](interrupts?tut_expand) - [Invoke IRQ control](interrupts.md#invoke-irq-control) - [Set NTFN](interrupts.md#set-ntfn) - [Acknowledge an interrupt](interrupts.md#acknowledge-an-interrupt) -### [Fault handling](fault-handlers.md) +### [Fault handling](fault-handlers?tut_expand) - [Set up an endpoint for thread fault IPC messages](fault-handlers.md#setting-up-the-endpoint-to-be-used-for-thread-fault-ipc-messages) - [Receive an IPC message from the kernel](fault-handlers.md#receiving-the-ipc-message-from-the-kernel) - [Get information about a thread fault](fault-handlers.md#finding-out-information-about-the-generated-thread-fault) - [Handle a thread fault](fault-handlers.md#handling-a-thread-fault) - [Resume a faulting thread](fault-handlers.md#resuming-a-faulting-thread) -## [MCS Extensions](mcs.md) +## [MCS Extensions](mcs?tut_expand) - [Set up a periodic thread](mcs.md#periodic-threads) - [Unbind a scheduling context](mcs.md#unbinding-scheduling-contexts) - [Experiment with sporadic tasks](mcs.md#sporadic-threads) - [Use passive servers](mcs.md#passive-servers) - [Configure fault endpoints](mcs.md#configuring-a-fault-endpoint-on-the-mcs-kernel) -## [Dynamic libraries](libraries-1.md) +## [Dynamic libraries](libraries-1?tut_expand) -### [Initialisation & threading](libraries-1.md) +### [Initialisation & threading](libraries-1?tut_expand) - [Obtain BootInfo](libraries-1.md#obtain-bootinfo) - [Initialise simple](libraries-1.md#initialise-simple) - [Use simple to print BootInfo](libraries-1.md#use-simple-to-print-bootinfo) @@ -90,7 +89,7 @@ This guide provides links to tutorial solutions as quick references for seL4 cal - [Start the new thread](libraries-1.md#start-the-new-thread) - [Print](libraries-1.md#print-something) -### [IPC](libraries-2.md) +### [IPC](libraries-2?tut_expand) - [Allocate an IPC buffer](libraries-2.md#allocate-an-ipc-buffer) - [Allocate a page table](libraries-2.md#allocate-a-page-table) - [Map a page table](libraries-2.md#map-a-page-table) @@ -105,7 +104,7 @@ This guide provides links to tutorial solutions as quick references for seL4 cal - [Write the message registers](libraries-2.md#write-the-message-registers) - [Reply to a message](libraries-2.md#reply-to-a-message) -### [Processes & Elf loading](libraries-3.md) +### [Processes & Elf loading](libraries-3?tut_expand) - [Create a VSpace object](libraries-3.md#virtual-memory-management) - [Configure a process](libraries-3.md#configure-a-process) - [Get a CSpace path](libraries-3.md#get-a-cspacepath) @@ -115,23 +114,23 @@ This guide provides links to tutorial solutions as quick references for seL4 cal - [Send a reply](libraries-3.md#send-a-reply) - [Initiate communications by using seL4_Call](libraries-3.md#client-call) -### [Timer](libraries-4.md) +### [Timer](libraries-4?tut_expand) - [Allocate a notification object](libraries-4.md#allocate-a-notification-object) - [Initialise a timer](libraries-4.md#initialise-the-timer) - [Use a timer](libraries-4.md#use-the-timer) - [Handle an interrupt](libraries-4.md#handle-the-interrupt) - [Destroy a timer](libraries-4.md#destroy-the-timer) -## [CAmkES](hello-camkes-0.md) +## [CAmkES](hello-camkes-0?tut_expand) -### [A basic CAmkES application](hello-camkes-1.md) +### [A basic CAmkES application](hello-camkes-1?tut_expand) - [Define an instance in the composition section of the ADL](hello-camkes-1.md#define-an-instance-in-the-composition-section-of-the-adl) - [Add a connection](hello-camkes-1.md#add-a-connection) - [Define an interface](hello-camkes-1.md#define-an-interface) - [Implement an RPC function](hello-camkes-1.md#implement-a-rpc-function) - [Invoke a RPC function](hello-camkes-1.md#invoke-a-rpc-function) -### [Events in CAmkES](hello-camkes-2.md) +### [Events in CAmkES](hello-camkes-2?tut_expand) - [Specify an events interface](hello-camkes-2.md#specify-an-events-interface) - [Add connections](hello-camkes-2.md#add-connections) - [Wait for data to become available](hello-camkes-2.md#wait-for-data-to-become-available) @@ -149,7 +148,7 @@ This guide provides links to tutorial solutions as quick references for seL4 cal - [Restrict access to dataports](hello-camkes-2.md#restrict-access-to-dataports) - [Test the read and write permissions on the dataport](hello-camkes-2.md#test-the-read-and-write-permissions-on-the-dataport) -### [CAmkES Timer](hello-camkes-timer.md) +### [CAmkES Timer](hello-camkes-timer?tut_expand) - [Instantiate a Timer and Timerbase](hello-camkes-timer.md#instantiate-a-timer-and-timerbase) - [Connect a timer driver component](hello-camkes-timer.md#connect-a-timer-driver-component) - [Configure a timer hardware component instance](hello-camkes-timer.md#configure-a-timer-hardware-component-instance) @@ -166,12 +165,12 @@ This guide provides links to tutorial solutions as quick references for seL4 cal - [Handle the interrupt](hello-camkes-timer.md#handle-the-interrupt) - [Stop the timer](hello-camkes-timer.md#stop-the-timer) -### [CAmkES VM Linux](camkes-vm-linux.md) +### [CAmkES VM Linux](camkes-vm-linux?tut_expand) - [Add a program](camkes-vm-linux.md#adding-a-program) - [Add a kernel module](camkes-vm-linux.md#adding-a-kernel-module) - [Create a hypercall](camkes-vm-linux.md#creating-a-hypercall) -### [CAmkeES Cross VM Connectors](camkes-vm-crossvm.md) +### [CAmkeES Cross VM Connectors](camkes-vm-crossvm?tut_expand) - [Add modules to the guest](camkes-vm-crossvm.md#add-modules-to-the-guest) - [Define interfaces in the VMM](camkes-vm-crossvm.md#define-interfaces-in-the-vmm) - [Define the component interface](camkes-vm-crossvm.md#define-the-component-interface) diff --git a/assets/js/toggle-markdown.js b/assets/js/toggle-markdown.js index 34bcfb04af..8e45bd629a 100644 --- a/assets/js/toggle-markdown.js +++ b/assets/js/toggle-markdown.js @@ -1,15 +1,11 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright 2024 seL4 Project a Series of LF Projects, LLC. -// Expand all solutions if previous link was how-to page +// Expand all solutions +let param = new URLSearchParams(window.location.search); -let text = document.referrer; -let result = text.includes("Tutorials/how-to"); - -if (result==true){ - document.body.querySelectorAll('details') - .forEach((e) => {(e.hasAttribute('open')) ? - e.removeAttribute('open') : e.setAttribute('open',true); - console.log(e.hasAttribute('open')) - }) -} \ No newline at end of file +if (param.has('tut_expand')) { + document.body.querySelectorAll('details').forEach((e) => { + e.setAttribute('open', true); + }) +} From 0bc8c027ea4b0fbbb8014125cd69e25bd66376dd Mon Sep 17 00:00:00 2001 From: Indan Zupancic