+ Next: Hello world +
diff --git a/Tutorials/hello-camkes-0.md b/Tutorials/hello-camkes-0.md index e2d52f9d88..b42630560a 100644 --- a/Tutorials/hello-camkes-0.md +++ b/Tutorials/hello-camkes-0.md @@ -1,11 +1,10 @@ --- toc: true -title: Camkes +title: Hello CAmkES tutorial: hello-camkes-0 -tutorial-order: camkes-0 -description: an introduction to Camkes concepts. +layout: tutorial +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/hello-camkes-1.md b/Tutorials/hello-camkes-1.md index 2fbbf4786c..02cf5d7266 100644 --- a/Tutorials/hello-camkes-1.md +++ b/Tutorials/hello-camkes-1.md @@ -1,11 +1,10 @@ --- toc: true -title: Camkes 1 +title: Introduction to CAmkES tutorial: hello-camkes-1 -tutorial-order: camkes-1 -description: an introduction to Camkes concepts. +layout: tutorial +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/hello-camkes-2.md b/Tutorials/hello-camkes-2.md index 4cf55e8411..402dc1f5ac 100644 --- a/Tutorials/hello-camkes-2.md +++ b/Tutorials/hello-camkes-2.md @@ -1,11 +1,10 @@ --- toc: true -title: Camkes 2 +title: Events in CAmkES tutorial: hello-camkes-2 -tutorial-order: camkes-2 -description: an introduction to Camkes concepts. +layout: tutorial +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/hello-camkes-timer.md b/Tutorials/hello-camkes-timer.md index bfd34499fc..dfa36c7a27 100644 --- a/Tutorials/hello-camkes-timer.md +++ b/Tutorials/hello-camkes-timer.md @@ -1,11 +1,10 @@ --- toc: true -title: Camkes 3 +title: CAmkES timer tutorial tutorial: hello-camkes-timer -tutorial-order: camkes-3 -description: introduce Camkes hardware components. +layout: tutorial +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/hello-world.md b/Tutorials/hello-world.md index 1a8adf4dbc..3df3848197 100644 --- a/Tutorials/hello-world.md +++ b/Tutorials/hello-world.md @@ -2,9 +2,10 @@ toc: true title: Hello, World! tutorial: hello-world -tutorial-order: 0-hello -description: an introduction to seL4 projects and tutorials. +layout: tutorial +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/how-to.md b/Tutorials/how-to.md new file mode 100644 index 0000000000..c6caf099ec --- /dev/null +++ b/Tutorials/how-to.md @@ -0,0 +1,201 @@ +--- +toc: true +layout: tutorial +description: how-to guide with links to tutorial solutions +SPDX-License-Identifier: CC-BY-SA-4.0 +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 + +{% assign url = "capabilities?tut_expand" %} +### [Capabilities]({{ url }}) + + - [Calculate the size of a CSpace]({{ url }}#how-big-is-your-cspace) + - [Copy a capability between CSlots]({{ url }}#copy-a-capability-between-cslots) + - [Delete a capability]({{ url }}#how-do-you-delete-capabilities) + - [Suspend a thread]({{ url }}#suspend-a-thread) + +{% assign url = "untyped?tut_expand" %} +### [Untyped]({{ url }}) + + - [Create an untyped capability]({{ url }}#create-an-untyped-capability) + - [Create a TCB object]({{ url }}#create-a-tcb-object) + - [Create an endpoint object]({{ url }}#create-an-endpoint-object) + - [Create a notification object]({{ url }}#create-a-notification-object) + - [Delete an object]({{ url }}#delete-the-objects) + +{% assign url = "mapping?tut_expand" %} +### [Mapping]({{ url }}) +- [Map a page directory]({{ url }}#map-a-page-directory) +- [Map a page table]({{ url }}#map-a-page-table) +- [Remap a page]({{ url }}#remap-a-page) +- [Unmap a page]({{ url }}#unmapping-pages) + +{% assign url = "threads?tut_expand" %} +### [Threads]({{ url }}) +- [Configure a TCB]({{ url }}#configure-a-tcb) +- [Change the priority of a thread]({{ url }}#change-priority-via-sel4_tcb_setpriority) +- [Set initial register state]({{ url }}#set-initial-register-state) +- [Start the thread]({{ url }}#start-the-thread) +- [Set the arguments of a thread]({{ url }}#passing-arguments) +- [Resolve a fault]({{ url }}#resolving-a-fault) + +{% assign url = "ipc?tut_expand" %} +### [IPC]({{ url }}) + - [Use capability transfer to send the badged capability]({{ url }}#use-capability-transfer-to-send-the-badged-capability) + - [Get a message]({{ url }}#get-a-message) + - [Reply and wait]({{ url }}#reply-and-wait) + - [Save a reply and store reply capabilities]({{ url }}#save-a-reply-and-store-reply-capabilities) + +{% assign url = "notifications?tut_expand" %} +### [Notifications]({{ url }}) + - [Set up shared memory]({{ url }}#set-up-shared-memory) + - [Signalling]({{ url }}#signal-the-producers-to-go) + - [Differentiate signals]({{ url }}#differentiate-signals) + +{% assign url = "interrupts?tut_expand" %} +### [Interrupts]({{ url }}) + - [Invoke IRQ control]({{ url }}#invoke-irq-control) + - [Set NTFN]({{ url }}#set-ntfn) + - [Acknowledge an interrupt]({{ url }}#acknowledge-an-interrupt) + +{% assign url = "fault-handlers?tut_expand" %} +### [Fault handling]({{ url }}) + - [Set up an endpoint for thread fault IPC messages]({{ url }}#setting-up-the-endpoint-to-be-used-for-thread-fault-ipc-messages) + - [Receive an IPC message from the kernel]({{ url }}#receiving-the-ipc-message-from-the-kernel) + - [Get information about a thread fault]({{ url }}#finding-out-information-about-the-generated-thread-fault) + - [Handle a thread fault]({{ url }}#handling-a-thread-fault) + - [Resume a faulting thread]({{ url }}#resuming-a-faulting-thread) + +{% assign url = "mcs?tut_expand" %} +## [MCS Extensions]({{ url }}) + - [Set up a periodic thread]({{ url }}#periodic-threads) + - [Unbind a scheduling context]({{ url }}#unbinding-scheduling-contexts) + - [Experiment with sporadic tasks]({{ url }}#sporadic-threads) + - [Use passive servers]({{ url }}#passive-servers) + - [Configure fault endpoints]({{ url }}#configuring-a-fault-endpoint-on-the-mcs-kernel) + +{% assign url = "libraries-1?tut_expand" %} +## [Dynamic libraries]({{ url }}) + +### [Initialisation & threading]({{ url }}) + - [Obtain BootInfo]({{ url }}#obtain-bootinfo) + - [Initialise simple]({{ url }}#initialise-simple) + - [Use simple to print BootInfo]({{ url }}#use-simple-to-print-bootinfo) + - [Initialise an allocator]({{ url }}#initialise-an-allocator) + - [Obtain a generic allocation interface (vka)]({{ url }}#obtain-a-generic-allocation-interface-vka) + - [Find the CSpace root cap]({{ url }}#find-the-cspace-root-cap) + - [Find the VSpace root cap]({{ url }}#find-the-vspace-root-cap) + - [Allocate a TCB Object]({{ url }}#allocate-a-tcb-object) + - [Configure the new TCB]({{ url }}#configure-the-new-tcb) + - [Name the new TCB]({{ url }}#name-the-new-tcb) + - [Set the instruction pointer]({{ url }}#set-the-instruction-pointer) + - [Set the stack pointer]({{ url }}#set-the-stack-pointer) + - [Write the registers]({{ url }}#write-the-registers) + - [Start the new thread]({{ url }}#start-the-new-thread) + - [Print]({{ url }}#print-something) + +{% assign url = "libraries-2?tut_expand" %} +### [IPC]({{ url }}) + - [Allocate an IPC buffer]({{ url }}#allocate-an-ipc-buffer) + - [Allocate a page table]({{ url }}#allocate-a-page-table) + - [Map a page table]({{ url }}#map-a-page-table) + - [Map a page]({{ url }}#map-a-page) + - [Allocate an endpoint]({{ url }}#allocate-an-endpoint) + - [Badge an endpoint]({{ url }}#badge-an-endpoint) + - [Set a message register]({{ url }}#message-registers) + - [Send and wait for a reply]({{ url }}#ipc) + - [Receive a reply]({{ url }}#receive-a-reply) + - [Receive an IPC]({{ url }}#receive-an-ipc) + - [Validate a message]({{ url }}#validate-the-message) + - [Write the message registers]({{ url }}#write-the-message-registers) + - [Reply to a message]({{ url }}#reply-to-a-message) + +{% assign url = "libraries-3?tut_expand" %} +### [Processes & Elf loading]({{ url }}) + - [Create a VSpace object]({{ url }}#virtual-memory-management) + - [Configure a process]({{ url }}#configure-a-process) + - [Get a CSpace path]({{ url }}#get-a-cspacepath) + - [Badge a capability]({{ url }}#badge-a-capability) + - [Spawn a process]({{ url }}#spawn-a-process) + - [Receive a message]({{ url }}#receive-a-message) + - [Send a reply]({{ url }}#send-a-reply) + - [Initiate communications by using seL4_Call]({{ url }}#client-call) + +{% assign url = "libraries-4?tut_expand" %} +### [Timer]({{ url }}) + - [Allocate a notification object]({{ url }}#allocate-a-notification-object) + - [Initialise a timer]({{ url }}#initialise-the-timer) + - [Use a timer]({{ url }}#use-the-timer) + - [Handle an interrupt]({{ url }}#handle-the-interrupt) + - [Destroy a timer]({{ url }}#destroy-the-timer) + +## [CAmkES](hello-camkes-0?tut_expand) + +{% assign url = "hello-camkes-1?tut_expand" %} +### [A basic CAmkES application]({{ url }}) + - [Define an instance in the composition section of the ADL]({{ url }}#define-an-instance-in-the-composition-section-of-the-adl) + - [Add a connection]({{ url }}#add-a-connection) + - [Define an interface]({{ url }}#define-an-interface) + - [Implement an RPC function]({{ url }}#implement-a-rpc-function) + - [Invoke a RPC function]({{ url }}#invoke-a-rpc-function) + +{% assign url = "hello-camkes-2?tut_expand" %} +### [Events in CAmkES]({{ url }}) + - [Specify an events interface]({{ url }}#specify-an-events-interface) + - [Add connections]({{ url }}#add-connections) + - [Wait for data to become available]({{ url }}#wait-for-data-to-become-available) + - [Signal that data is available]({{ url }}#signal-that-data-is-available) + - [Register a callback handler]({{ url }}#register-a-callback-handler) + - [Specify dataport interfaces]({{ url }}#specify-dataport-interfaces) + - [Specify dataport connections]({{ url }}#specify-dataport-connections) + - [Copy strings to an untyped dataport]({{ url }}#copy-strings-to-an-untyped-dataport) + - [Read the reply data from a typed dataport]({{ url }}#read-the-reply-data-from-a-typed-dataport) + - [Send data using dataports]({{ url }}#send-data-using-dataports) + - [Read data from an untyped dataport]({{ url }}#read-data-from-an-untyped-dataport) + - [Put data into a typed dataport]({{ url }}#put-data-into-a-typed-dataport) + - [Read data from a typed dataport]({{ url }}#read-data-from-a-typed-dataport) + - [Set component priorities]({{ url }}#set-component-priorities) + - [Restrict access to dataports]({{ url }}#restrict-access-to-dataports) + - [Test the read and write permissions on the dataport]({{ url }}#test-the-read-and-write-permissions-on-the-dataport) + +{% assign url = "hello-camkes-timer?tut_expand" %} +### [CAmkES Timer]({{ url }}) + - [Instantiate a Timer and Timerbase]({{ url }}#instantiate-a-timer-and-timerbase) + - [Connect a timer driver component]({{ url }}#connect-a-timer-driver-component) + - [Configure a timer hardware component instance]({{ url }}#configure-a-timer-hardware-component-instance) + - [Call into a supplied driver to handle the interrupt]({{ url }}#call-into-a-supplied-driver-to-handle-the-interrupt) + - [Stop a timer]({{ url }}#stop-a-timer) + - [Acknowledge an interrupt]({{ url }}#acknowledge-an-interrupt) + - [Get a timer handler]({{ url }}#get-a-timer-handler) + - [Start a timer]({{ url }}#start-a-timer) + - [Implement an RPC interface]({{ url }}#implement-a-rpc-interface) + - [Set a timer interrupt]({{ url }}#set-a-timer-interrupt) + - [Instantiate a TimerDTB component]({{ url }}#instantiate-a-timerdtb-component) + - [Connect interfaces using the seL4DTBHardware connector]({{ url }}#connect-interfaces-using-the-sel4dtbhardware-connector) + - [Configure the TimerDTB component]({{ url }}#configure-the-timerdtb-component) + - [Handle the interrupt]({{ url }}#handle-the-interrupt) + - [Stop the timer]({{ url }}#stop-the-timer) + +{% assign url = "camkes-vm-linux?tut_expand" %} +### [CAmkES VM Linux]({{ url }}) + - [Add a program]({{ url }}#adding-a-program) + - [Add a kernel module]({{ url }}#adding-a-kernel-module) + - [Create a hypercall]({{ url }}#creating-a-hypercall) + +{% assign url = "camkes-vm-crossvm?tut_expand" %} +### [CAmkeES Cross VM Connectors]({{ url }}) + - [Add modules to the guest]({{ url }}#add-modules-to-the-guest) + - [Define interfaces in the VMM]({{ url }}#define-interfaces-in-the-vmm) + - [Define the component interface]({{ url }}#define-the-component-interface) + - [Instantiate the print server]({{ url }}#instantiate-the-print-server) + - [Implement the print server]({{ url }}#implement-the-print-server) + - [Implement the VMM side of the connection]({{ url }}#implement-the-vmm-side-of-the-connection) + - [Update the build system]({{ url }}#update-the-build-system) + - [Add interfaces to the Guest]({{ url }}#add-interfaces-to-the-guest) + - [Create a process]({{ url }}#create-a-process) \ No newline at end of file diff --git a/Tutorials/index.md b/Tutorials/index.md index d8c2c60cf6..4d01dba758 100644 --- a/Tutorials/index.md +++ b/Tutorials/index.md @@ -1,27 +1,31 @@ --- toc: true -redirect_from: - - /projects/sel4-tutorials.html - - /projects/sel4-tutorials/ -layout: project -project: sel4-tutorials +title: Tutorials +layout: tutorial +description: overview of seL4 and related tutorials SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. --- +# Overview -# Tutorials +We have developed a series of tutorials to introduce seL4 and developing systems on seL4. -{% assign tutorials = site.pages | where_exp: 'page', 'page.tutorial' | sort: 'tutorial-order' %} +## List of tutorials +The tutorials are split into a number of broad categories, and have been designed around developer needs. + +- The [seL4 tutorials](setting-up.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) introduces seL4 Mixed-Criticality System 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). + +- [Libraries](libraries-1) provides walkthroughs and exercises for using the libraries provided in `seL4_libs`, which were developed for rapidly prototyping systems on seL4. + +- [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. -We have developed a series of tutorials to introduce seL4 and -developing systems on seL4. +- [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. -## How to use the tutorials +- [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. -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. +**Recommended reading** Note that all of these tutorials require C programming experience and some understanding of operating systems and computer @@ -32,222 +36,17 @@ architecture. Suggested resources for these include: - 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+ Next: Pathways through the tutorials +
\ No newline at end of file diff --git a/Tutorials/interrupts.md b/Tutorials/interrupts.md index ffeb05c281..d061c4a5f0 100644 --- a/Tutorials/interrupts.md +++ b/Tutorials/interrupts.md @@ -2,10 +2,9 @@ toc: true title: Interrupts tutorial: interrupts -tutorial-order: mechanisms-7 -description: receiving and handling interrupts. +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 %} - diff --git a/Tutorials/ipc.md b/Tutorials/ipc.md index a7e313dc2c..6502cd67cb 100644 --- a/Tutorials/ipc.md +++ b/Tutorials/ipc.md @@ -2,8 +2,8 @@ toc: true title: IPC tutorial: ipc -tutorial-order: mechanisms-5 -description: overview of interprocess communication (IPC). +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. --- diff --git a/Tutorials/dynamic-1.md b/Tutorials/libraries-1.md similarity index 72% rename from Tutorials/dynamic-1.md rename to Tutorials/libraries-1.md index 091b71918f..f5ba32ae21 100644 --- a/Tutorials/dynamic-1.md +++ b/Tutorials/libraries-1.md @@ -1,11 +1,10 @@ --- toc: true -title: Dynamic Libraries 1 -tutorial: dynamic-1 -tutorial-order: dynamic-1 +title: Libraries initialisation & threading +tutorial: libraries-1 +layout: tutorial 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/dynamic-2.md b/Tutorials/libraries-2.md similarity index 59% rename from Tutorials/dynamic-2.md rename to Tutorials/libraries-2.md index 0795b76fa9..d1d6f11e74 100644 --- a/Tutorials/dynamic-2.md +++ b/Tutorials/libraries-2.md @@ -1,11 +1,10 @@ --- toc: true -title: Dynamic Libraries 2 -tutorial: dynamic-2 -tutorial-order: dynamic-2 -description: IPC with seL4_libs. +title: Libraries IPC +tutorial: libraries-2 +layout: tutorial +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/dynamic-4.md b/Tutorials/libraries-3.md similarity index 54% rename from Tutorials/dynamic-4.md rename to Tutorials/libraries-3.md index e66a050f9f..fcb922856e 100644 --- a/Tutorials/dynamic-4.md +++ b/Tutorials/libraries-3.md @@ -1,11 +1,10 @@ --- toc: true -title: Dynamic Libraries 4 -tutorial: dynamic-4 -tutorial-order: dynamic-4 -description: timers and timeouts with seL4_libs. +title: Libraries processes & ELF loading +tutorial: libraries-3 +layout: tutorial +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/dynamic-3.md b/Tutorials/libraries-4.md similarity index 55% rename from Tutorials/dynamic-3.md rename to Tutorials/libraries-4.md index 2c38d921a1..19039d7379 100644 --- a/Tutorials/dynamic-3.md +++ b/Tutorials/libraries-4.md @@ -1,11 +1,10 @@ --- toc: true -title: Dynamic Libraries 3 -tutorial: dynamic-3 -tutorial-order: dynamic-3 -description: process management with seL4_libs. +title: Libraries timer tutorial +tutorial: libraries-4 +layout: tutorial +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/mapping.md b/Tutorials/mapping.md index b3c5136bc7..65568bf90f 100644 --- a/Tutorials/mapping.md +++ b/Tutorials/mapping.md @@ -2,8 +2,8 @@ toc: true title: Mapping tutorial: mapping -tutorial-order: mechanisms-3 -description: virtual memory in seL4. +layout: tutorial +description: virtual memory in seL4 SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. --- diff --git a/Tutorials/mcs.md b/Tutorials/mcs.md index 64ba2f8382..4351db75cb 100644 --- a/Tutorials/mcs.md +++ b/Tutorials/mcs.md @@ -2,10 +2,9 @@ toc: true title: MCS tutorial: mcs -tutorial-order: mcs-1 +layout: tutorial 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/notifications.md b/Tutorials/notifications.md index f4227272cd..afe8be243f 100644 --- a/Tutorials/notifications.md +++ b/Tutorials/notifications.md @@ -2,10 +2,9 @@ toc: true title: Notifications tutorial: notifications -tutorial-order: mechanisms-6 -description: using notification objects and signals. +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 %} - diff --git a/Tutorials/pathways.md b/Tutorials/pathways.md new file mode 100644 index 0000000000..cc9264c225 --- /dev/null +++ b/Tutorials/pathways.md @@ -0,0 +1,64 @@ +--- +toc: true +title: Pathways +layout: tutorial +description: pathways through tutorials depending on learning objectives +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2020 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](setting-up.md) +- [Getting the tutorials](get-the-tutorials.md) +- [Hello world](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 + +Recommended tutorials +- [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-vm-crossvm.md) walkthrough of adding communication between Linux guests in separate VMs + + +### Platform Development +Goals +- to contribute to development of the seL4 (user-level) platform +- to develop operating system services and device drivers +- to develop seL4-based frameworks and operating systems + +Recommended tutorials +To gain a comprehensive understanding of seL4, we recommend that you go through all the tutorials in the order listed in the default pathway. + + +### Kernel Development +Goals +- to contribute to the seL4 kernel itself +- to port seL4 to a new platform +- to add new features to the kernel + +Recommended reading +- [Contributing to kernel code](../../projects/sel4/kernel-contribution) + +Recommended tutorials +- Follow the tutorial in the default pathway up to and including MCS. diff --git a/Tutorials/setting-up.md b/Tutorials/setting-up.md new file mode 100644 index 0000000000..ca9582d338 --- /dev/null +++ b/Tutorials/setting-up.md @@ -0,0 +1,155 @@ +--- +toc: true +layout: tutorial +description: guide to machine set-up for tutorials +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC. +--- + +# Setting up your machine + +## Google's Repo tool + +The primary way of obtaining and managing seL4 project sources is through the use of Google's Repo tool. + +To install run: +```sh + sudo apt-get update + sudo apt-get install repo +``` + ++{% assign page_file = page.url | split: '/' | last | remove: ".html" -%} +{%- assign found = false -%} +{%- for item in all_tutes -%} +{%- if found -%} +{%- if item.type == "header" -%} +{%- comment -%} + We include the preceding header name in the "next" link when the link + is an offsite URL, e.g. for Microkit or Rust. +{%- endcomment -%} +{%- assign header_name = item.name -%} +{%- else -%} +{%- case item.type -%} +{%- when "file" -%} +{%- assign url = "/Tutorials/" | append: item.file | relative_url %} + Next: {{ item.name }} +{%- when "url" -%} +{%- else -%} +{%- assign url = "/Tutorials/" | append: item.name | relative_url %} + Next: {{ item.display_name }} +{%- endcase -%} +{%- break -%} +{%- endif -%} +{%- else -%} +{%- case item.type -%} +{%- when "file" -%} +{%- if item.file == page_file -%} +{%- assign found = true -%} +{%- endif -%} +{%- when "url" -%} +{%- when "header" -%} +{%- else -%} +{%- if item.name == page_file -%} +{%- assign found = true -%} +{%- endif -%} +{%- endcase -%} +{%- endif -%} +{%- endfor %} +
+ +{% if page.tutorial -%} + {%- capture path -%} + {{page.tutorial}}/{{page.tutorial}}.md + {%- endcapture -%} + + {%- assign repo_url = 'https://github.com/sel4/sel4-tutorials' -%} + {%- assign view_url = repo_url | append: '/blob/master/tutorials/' | append: path -%} + {%- assign edit_url = repo_url | append: '/edit/master/tutorials/' | append: path -%} +Tutorial included from github repo edit
+{%- endif %} +Information about working with seL4 and its ecosystem
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.
- -Tutorials and other material to learn about seL4.
+