Various tutorials for using seL4, its libraries, and CAmkES.
Follow the instructions for setting up your host environment on the seL4 docsite.
Starting a tutorial
This tutorial repository is part of a larger collection of repositories, which are required to run the tutorial and are coordinated in a manifest file. See this guide on how to check out a consistent set.
Once you have that, a tutorial is started through the use of the
that is provided in the root directory. Using this script you can specify a
tutorial and target machine and it will create a copy of the tutorial for you to
mkdir build_hello_world cd build_hello_world ../init --plat pc99 --tut hello-world
init script will initialize a build directory in the current directory and at the end
it will print out a list of files that need to be modified to complete the tutorial. Building
is performed simply be invoking
ninja, and once the tutorial compiles it can be tested
in Qemu by using the provided simulation script through
Tutorials and targets
-h switch to the
init script provides a list of different tutorials and targets that
can be provided to
Most tutorials support any target platform, with the exception of hello-camkes-timer, which only supports the zynq7000 platform.
Virtual Machine Image
This appliance is based on VirtualBox 5.1.2. You may also need to install the appropriate VirtualBox extensions available from the same page.
To view the solutions for a tutorial instead of performing the tutorial pass the
mkdir build_hello_world cd build_hello_world ../init --plat pc99 --tut hello-world --solution
After which it will tell you where the solution files are that you can look at. You can then
ninja && ./simulate to build and run the solution.
Reporting issues or bugs in the tutorials:
Please report any issues you find in the tutorials (bugs, outdated API calls, etc) by filing an issue on the public github repository: https://github.com/seL4/sel4-tutorials/issues/
Build system tutorial
Due to custom written additions to the build system specifically for the tutorials they are not appropriate for learning how to create and structure new applications/systems. Future tutorials for this will be forthcoming. For now it is suggested to look at other existing applications for ideas.
A walkthrough of each tutorial is available on the
The slides used for the tutorial are available in
The seL4 manual lives in the kernel source in the
To generate a PDF go into that directory and type
You will need to have LaTeX installed to build it.
A pre-generated PDF version can be found
CAmkES documentation lives in the camkes-tool repository in docs/index.md.