diff --git a/Tutorials-old/camkes-vm-crossvm.md b/Tutorials-old/camkes-vm-crossvm.md deleted file mode 100644 index e6a5d8baf0..0000000000 --- a/Tutorials-old/camkes-vm-crossvm.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Camkes Cross-VM communication -tutorial: camkes-vm-crossvm -tutorial-order: vm-2 -description: walkthrough of adding communication between Linux guests in separate VMs. -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-old/camkes-vm-linux.md b/Tutorials-old/camkes-vm-linux.md deleted file mode 100644 index 38225b7050..0000000000 --- a/Tutorials-old/camkes-vm-linux.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Camkes VM Linux -tutorial: camkes-vm-linux -tutorial-order: vm-1 -description: using Linux as a guest in the Camkes VM. -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-old/capabilities.md b/Tutorials-old/capabilities.md deleted file mode 100644 index 657b851250..0000000000 --- a/Tutorials-old/capabilities.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -toc: true -title: Capabilities -tutorial: capabilities -tutorial-order: mechanisms-1 -description: an introduction to capabilities in the seL4 kernel API. -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-old/dynamic-1.md b/Tutorials-old/dynamic-1.md deleted file mode 100644 index 091b71918f..0000000000 --- a/Tutorials-old/dynamic-1.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Dynamic Libraries 1 -tutorial: dynamic-1 -tutorial-order: dynamic-1 -description: system initialisation & threading with seL4_libs. -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-old/dynamic-2.md b/Tutorials-old/dynamic-2.md deleted file mode 100644 index 0795b76fa9..0000000000 --- a/Tutorials-old/dynamic-2.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Dynamic Libraries 2 -tutorial: dynamic-2 -tutorial-order: dynamic-2 -description: IPC with seL4_libs. -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-old/dynamic-3.md b/Tutorials-old/dynamic-3.md deleted file mode 100644 index 2c38d921a1..0000000000 --- a/Tutorials-old/dynamic-3.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Dynamic Libraries 3 -tutorial: dynamic-3 -tutorial-order: dynamic-3 -description: process management with seL4_libs. -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-old/dynamic-4.md b/Tutorials-old/dynamic-4.md deleted file mode 100644 index e66a050f9f..0000000000 --- a/Tutorials-old/dynamic-4.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Dynamic Libraries 4 -tutorial: dynamic-4 -tutorial-order: dynamic-4 -description: timers and timeouts with seL4_libs. -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-old/fault-handlers.md b/Tutorials-old/fault-handlers.md deleted file mode 100644 index 6ad6f1ad46..0000000000 --- a/Tutorials-old/fault-handlers.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -toc: true -title: Faults -tutorial: fault-handlers -tutorial-order: mechanisms-8 -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 %} diff --git a/Tutorials-old/hello-camkes-0.md b/Tutorials-old/hello-camkes-0.md deleted file mode 100644 index e2d52f9d88..0000000000 --- a/Tutorials-old/hello-camkes-0.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Camkes -tutorial: hello-camkes-0 -tutorial-order: camkes-0 -description: an introduction to Camkes concepts. -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-old/hello-camkes-1.md b/Tutorials-old/hello-camkes-1.md deleted file mode 100644 index 2fbbf4786c..0000000000 --- a/Tutorials-old/hello-camkes-1.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Camkes 1 -tutorial: hello-camkes-1 -tutorial-order: camkes-1 -description: an introduction to Camkes concepts. -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-old/hello-camkes-2.md b/Tutorials-old/hello-camkes-2.md deleted file mode 100644 index 4cf55e8411..0000000000 --- a/Tutorials-old/hello-camkes-2.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Camkes 2 -tutorial: hello-camkes-2 -tutorial-order: camkes-2 -description: an introduction to Camkes concepts. -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-old/hello-camkes-timer.md b/Tutorials-old/hello-camkes-timer.md deleted file mode 100644 index bfd34499fc..0000000000 --- a/Tutorials-old/hello-camkes-timer.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Camkes 3 -tutorial: hello-camkes-timer -tutorial-order: camkes-3 -description: introduce Camkes hardware components. -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-old/hello-world.md b/Tutorials-old/hello-world.md deleted file mode 100644 index 1a8adf4dbc..0000000000 --- a/Tutorials-old/hello-world.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -toc: true -title: Hello, World! -tutorial: hello-world -tutorial-order: 0-hello -description: an introduction to seL4 projects and tutorials. -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-old/index.md b/Tutorials-old/index.md deleted file mode 100644 index d8c2c60cf6..0000000000 --- a/Tutorials-old/index.md +++ /dev/null @@ -1,253 +0,0 @@ ---- -toc: true -redirect_from: - - /projects/sel4-tutorials.html - - /projects/sel4-tutorials/ -layout: project -project: sel4-tutorials -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. ---- - -# Tutorials - -{% assign tutorials = site.pages | where_exp: 'page', 'page.tutorial' | sort: 'tutorial-order' %} - -We have developed a series of tutorials to introduce seL4 and -developing systems on seL4. - -## How to use the tutorials - -Depending on your goals and what you want to do with seL4, we suggest -different paths to follow through the tutorial material. Choose the -most relevant category below and follow the tutorials in the suggested -order. - -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) - -### Evaluation - -Goal: - -- You want to understand what seL4 is and what benefits it gives. -- You want to understand how seL4 can be used to develop trustworthy systems. -- You want to get your hands a little dirty and see, compile, and run some code. - -Follow these tutorials: - -1. [seL4 overview](https://sel4.systems/About/seL4-whitepaper.pdf) -2. [Introduction tutorial](#introduction-tutorial) - -### System Building - -Goal: - -- You want to build systems based on seL4. -- You want to know what tools are available to do so and how to use those tools. -- You want experience with how to use seL4 and the tools to build trustworthy systems. - -Follow these tutorials: - -1. [seL4 overview](https://sel4.systems/About/seL4-whitepaper.pdf) -2. [Introduction tutorial](#introduction-tutorial) -3. [CAmkES tutorials](#camkes-tutorials) -4. [Virtualisation tutorials](#virtual-machines) -5. [MCS tutorial](#mcs-extensions) - -### 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: - -1. [seL4 overview](https://sel4.systems/About/seL4-whitepaper.pdf) -2. [Introduction tutorial](#introduction-tutorial) -3. [seL4 mechanisms tutorial](#seL4-mechanisms-tutorials) -4. [Rapid prototyping tutorials](#rapid-prototyping-tutorials) -5. [CAmkES tutorials](#camkes-tutorials) -6. [Virtualisation tutorial](#virtual-machines) -7. [MCS tutorial](#mcs-extensions) - - -### 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](/projects/sel4/kernel-contribution.html) - -Then follow these tutorials: - -1. [seL4 overview](https://sel4.systems/About/seL4-whitepaper.pdf) -2. [Introduction tutorial](#introduction-tutorial) -3. [seL4 mechanisms tutorial](#seL4-mechanisms-tutorials) -4. [MCS tutorial](#mcs-extensions) - -# The Tutorials - -## Prerequisites - -* [set up your machine](/GettingStarted#setting-up-your-machine). - -### Python Dependencies -Additional python dependencies are required to build tutorials. To install you can run: -``` -pip install --user aenum -pip install --user pyelftools -``` - -### Get the code -``` -mkdir sel4-tutorials-manifest -cd sel4-tutorials-manifest -repo init -u https://github.com/seL4/sel4-tutorials-manifest -repo sync -``` - -### Doing the tutorials - -The top of the source tree contains the kernel itself, and the tutorials are found in the subfolder: "`projects/sel4-tutorials`". The tutorial consists of some pre-written sample applications which have been deliberately half-written. You will be guided through filling in the missing portions, and thereby become acquainted with seL4. For each of the sample applications however, there is a completed solution that shows all the correct answers, as a reference. -When completing the tutorials you will be initialising and building your solutions with CMake. The general flow of completing a tutorial exercise involves: -``` -# creating a Tutorial directory -mkdir tutorial -cd tutorial -# initialising the build directory with a tutorial exercise -../init --plat --tut -# building the tutorial exercise -ninja -``` - -After initialising your directory you will be setup with half-written source for you to complete. Additinally, a build -directory will be created based on your directory name eg `tutorial_build`. - -Your job is to follow the tutorial instructions to complete the application in the tutorial folder. - -- The completed sample applications showing the solutions to the - tutorial challenges can be retrieved by initialsing a directory with the `--solution` argument - e.g. `../init --plat --tut --solution` - -## List of tutorials - -### Introduction tutorial - -Before starting tutorials, make sure that you have read through the -[Prerequisites](#prerequisites) and in particular [Doing the -tutorials](#doing-the-tutorials). - -Then, before any other tutorial, do the hello-world tutorial: - -{%- for t in tutorials %} -{%- if t.tutorial-order contains '0-hello' %} -1. [{{t.title}}]({{t.url}}) {{t.description}} -{%- endif %} -{%- endfor %} - -which will ensure your setup is working correctly. - -### seL4 mechanisms tutorials - -This set of tutorials are for people keen to learn about the base mechanisms provided -by the seL4 kernel. You will learn about the kernel API through small exercises -that show basic examples. - -{% assign tutorials = site.pages | where_exp: 'page', 'page.tutorial' | sort: 'tutorial-order' %} -{%- for t in tutorials %} -{%- if t.tutorial-order contains 'mechanisms' %} -1. [{{t.title}}]({{t.url}}) {{t.description}} -{%- endif %} -{%- endfor %} - -### Rapid prototyping tutorials - -This set of tutorials provides walkthroughs and exercises for using the dynamic -libraries provided in [seL4_libs](TODO LINK). These libraries are provided as is, -and have been developed for rapidly prototyping systems on seL4. They have not been -through intensive quality assurance and do have bugs. Contributions are welcome. - -{%- for t in tutorials %} -{%- if t.tutorial-order contains 'dynamic' %} -1. [{{t.title}}]({{t.url}}) {{t.description}} -{%- endif %} -{%- endfor %} - -* The slide presentations to guide you through the tutorials are in the following files: - - - `projects/sel4-tutorials/docs/seL4-Overview.pdf`: This - is an overview of the design and thoughts behind seL4, and - we strongly recommend you read it before starting - the tutorials. - - `projects/sel4-tutorials/docs/seL4-APILib-details.pdf`: This is the actual tutorial. - -### CAmkES tutorials - -These tutorials get you started with our component system CAmkES, which -allows you to configure static systems through components. CAmkES -generates the glue code for interacting with seL4 and is designed for building -high-assurance, static systems. - -These tutorials work similarly to the SEL4 tutorials in that they are -guided by a slide presentation. There are half-completed sample -applications, with a set of slides giving instructions, with TASK -challenges once again. There are also completed sample solutions. - -{%- for t in tutorials %} -{%- if t.tutorial-order contains 'camkes' %} -1. [{{t.title}}]({{t.url}}) {{t.description}} -{%- endif %} -{%- endfor %} - -- The slide presentations to guide you through the tutorials are - in this - file: `projects/sel4-tutorials/docs/CAmkESTutorial.pdf`. - -### Virtual machines - -These tutorials show how to run Linux guests on Camkes and how to communicate between them. -Currently these tutorials are for x86 only. - -{%- for t in tutorials %} -{%- if t.tutorial-order contains 'vm' %} -1. [{{t.title}}]({{t.url}}) {{t.description}} -{%- endif %} -{%- endfor %} - -### MCS extensions - -The MCS extensions are upcoming API changes to seL4. - -{%- for t in tutorials %} -{%- if t.tutorial-order contains 'mcs' %} -1. [{{t.title}}]({{t.url}}) {{t.description}} -{%- endif %} -{%- endfor %} - -## What next? - -You can try building and running [seL4test](../seL4Test). - -Next steps include working on one of our [suggested -projects](/SuggestedProjects.html) or helping to expand the collection -of [libraries and -components](/projects/available-user-components.html) available to -build seL4-based systems. diff --git a/Tutorials-old/interrupts.md b/Tutorials-old/interrupts.md deleted file mode 100644 index ffeb05c281..0000000000 --- a/Tutorials-old/interrupts.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Interrupts -tutorial: interrupts -tutorial-order: mechanisms-7 -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 %} - diff --git a/Tutorials-old/ipc.md b/Tutorials-old/ipc.md deleted file mode 100644 index a7e313dc2c..0000000000 --- a/Tutorials-old/ipc.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -toc: true -title: IPC -tutorial: ipc -tutorial-order: mechanisms-5 -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 %} diff --git a/Tutorials-old/mapping.md b/Tutorials-old/mapping.md deleted file mode 100644 index b3c5136bc7..0000000000 --- a/Tutorials-old/mapping.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -toc: true -title: Mapping -tutorial: mapping -tutorial-order: mechanisms-3 -description: virtual memory in seL4. -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-old/mcs.md b/Tutorials-old/mcs.md deleted file mode 100644 index 64ba2f8382..0000000000 --- a/Tutorials-old/mcs.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: MCS -tutorial: mcs -tutorial-order: mcs-1 -description: an introduction to the seL4 MCS extensions. -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-old/notifications.md b/Tutorials-old/notifications.md deleted file mode 100644 index f4227272cd..0000000000 --- a/Tutorials-old/notifications.md +++ /dev/null @@ -1,11 +0,0 @@ ---- -toc: true -title: Notifications -tutorial: notifications -tutorial-order: mechanisms-6 -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 %} - diff --git a/Tutorials-old/threads.md b/Tutorials-old/threads.md deleted file mode 100644 index 99cadd657c..0000000000 --- a/Tutorials-old/threads.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -toc: true -title: Threads -tutorial: threads -tutorial-order: mechanisms-4 -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 %} diff --git a/Tutorials-old/untyped.md b/Tutorials-old/untyped.md deleted file mode 100644 index 17c1ab3b48..0000000000 --- a/Tutorials-old/untyped.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -toc: true -title: Untyped -tutorial: untyped -tutorial-order: mechanisms-2 -description: user-level memory management. -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. ---- -{% include tutorial.md %}