sel4/docs

This is the source of the seL4 docs.

The seL4 microkernel

This project contains the source code of seL4 microkernel.

For details about the seL4 microkernel, including details about its formal correctness proof, please see the sel4.systems website and associated FAQ.

DOIs for citing recent releases of this repository:

• 

We welcome contributions to seL4. Please see the website for information on how to contribute.

This repository is usually not used in isolation, but as part of the build system in a larger project.

seL4 Basics

• Tutorials
• Documentation
• seL4 libraries
• seL4Test
• Debugging guide
• Benchmarking guide
• Virtualization on seL4
• Host Build Dependencies
• Porting seL4

Community

• Forums:
  • Discourse
  • seL4 Announce
  • seL4 Devel
• Suggested projects
• Community projects

See the contact links on the seL4 website for the full list.

Reporting security vulnerabilities

If you believe you have found a security vulnerability in seL4 or related software, we ask you to follow our vulnerability disclosure policy.

Manual

A hosted version of the manual for the most recent release can be found here.

A web version of the API can be found here

Repository Overview

• include and src: C and ASM source code of seL4
• tools: build tools
• libsel4: C bindings for the seL4 ABI
• manual: LaTeX sources of the seL4 reference manual

Build Instructions

See the seL4 website for build instructions.

Status

A list of releases and current project status can be found under seL4 releases.

• Roadmap: new features in development
• Hardware Support: information about hardware platform ports
• Kernel Features: information about available kernel features
• Userland Components and Drivers: available device drivers and userland components

License

See the file LICENSE.md.

docs's Issues

Document support of Avnet MaaXBoard Board (i.MX8MQ)

Follow-up from seL4/seL4#829

Document Avnet MaaXBoard Board support and maintainer. Or list this as unmaintained and mention at least that a PR/branch exists with the changes.

merge pages of contribution guidelines

Follow-up from the remark form @lsf37 in today's hangout call. The pages of with the contribution guidelines could be merged into one page. I've just stumbled over these pages

• processes/contributing.md
• processes/doc-contributing.md
  but there might be be even more. Goal is to have one singe page that people can be pointed to then.

camkes-arm-vm project is outdated, should be merged

The Arm VMs have been merged into other repos and the current doc site description is completely outdated, pointing to an archived repo.

It's not clear to me what exactly should replace it or how the description on the docsite should be merged, but it affects the following projects:

• https://docs.sel4.systems/projects/camkes-arm-vm/
• https://docs.sel4.systems/projects/camkes-vm/
• https://docs.sel4.systems/projects/virtualization/

build host dependencies are out of date

The minimum gcc version for building seL4 is 8 (see seL4/seL4#575 and seL4/seL4#574). This means that the currently described build host dependencies are not only out of date, but now insufficient, because Ubuntu 18 comes with gcc 7.5.

We should update the host dependencies to Ubuntu 20LTS and current Debian stable (bullseye) and document minimum gcc and clang versions.

HostDependencies incorrect about CMake version

The current HostDependencies document advises the use of Ubuntu 18.04 in order to have an appropriately current version of CMake.
Ubuntu 18.04 's normal, out-of-the-box repositories (used by apt-get) install version 3.10.2
(at least as of the current date, July 30, 2019)

However, this version seems to be insufficient for building se4L4test. Running init-build.sh:
...
CMake Error at projects/sel4runtime/CMakeLists.txt:20 (cmake_minimum_required):
CMake 3.12.0 or higher is required. You are running version 3.10.2

Choosing the "edit page on github" link for tutorials does not really work

For example:

https://docs.sel4.systems/Tutorials/capabilities.html

takes you to this page:

https://github.com/seL4/docs/edit/master/Tutorials/capabilities.md

Which just has:

{% include tutorial.md %}

It's not clear where the actual tutorial.md source is.

Makefile has:

GIT_REPOS:=$(shell (cd _data/projects && for i in `ls`; do cat $$i | ../../tools/get_repos.py ; done) | sort -u)
REPOSITORY_LIST = sel4 sel4-tutorials capdl
REPOSITORIES = $(GIT_REPOS:%=_repos/%)

But there doesn't appear to be an sel4-tutorials repo available on github.

Docsite: inconsistent links for tutorials

(This may wait for the Information Architecture feedback first)

All the links from the tutorial section on the landing page are wrong, going to the same root Tutorials page

Make supported platforms page more consistent

It's not clear to me whether the page that lists supported platforms (https://docs.sel4.systems/Hardware/) is just for supported hardware or all platforms supported by seL4. E.g on RISC-V the Spike is listed but it's a purely simulated platform (to my knowledge). The page is also not named consistently, the URL is "Hardware", the title is "Supported Platforms" and the navigation bar has it listed as "Supported Hardware"

Please point out which hardware supports simulation

In the big list of devices, I think having a column for simulation supported would be sensible. When starting to tinker, quickly finding out which platform has simulation support is good. Some (most!) of the hardware pages state this individually, but not all are clear on that. For example the Sabre Lite page contains the following phrase in the code example

# If your target binaries can be executed in an emulator/simulator, and if
# our build system happens to support that target emulator, then this script
# might work for you:

Now below, it says:

If you plan to use the ./simulate script, please be sure to add the -DSIMULATION=1 argument when running cmake.

That does not really confirm whether this target has support for simulation, or whether this is generic information on the state of affairs on simulation. Having it all in the overview list once would greatly help to quickly pick a desirable target.

docs/Hardware/index.md

Line 73 in e9e6283

### Simulating seL4

github CI actions should not try to deploy on forks

Follow-up from seL4/ci-actions#185
The github CI actions in this repo should not try to deploy on forks, this will fail anyway. Especially, since this workflow is triggered regularly, the messages with errors can get really annoying after a while ;)

RPi4 Docs missing `fixup4.dat`

According to the RaspberryPI documentation the fixup*.dat are matched pairs together with the start*.elf files. Therefore I conclude that if start4.elf is required (which is explicitly mentioned in the seL4 docs on the RPi4), then the corresponding fixup4.dat is also required. This should be documented in the table marked below:

docs/Hardware/Rpi4.md

Lines 41 to 50 in 796c552

	|Stage |Filename |Description |Source|
	|-|-|-|-|
	|FSBL |- |Mounts SD and loads SSBL |ROM |
	|SSBL |bootcode.bin|Loads GPU firmware and boots GPU|<https://github.com/raspberrypi/firmware/tree/master/boot/bootcode.bin> |
	|GPU firmware |start4.elf |Loads CPU bootloader and boots CPU |<https://github.com/raspberrypi/firmware/tree/master/boot/start4.elf> |
	|Usually the Linux kernel, but could also be U-Boot |u-boot.bin |U-Boot binary| Compiled using the instructions above |
	||config.txt|U-Boot parameters |Add `arm_64bit=1`, `kernel=u-boot.bin`, and `dtoverlay=disable-bt` to the bottom of `config.txt` |
	||uboot.env |U-Boot saved environment |Generated by U-Boot (default environment) bootcmd copied to bootcmd_orig bootcmd and bootdelay removed. This file will not exist when you first setup your SD card. |
	||bcm2711-rpi-4-b.dtb | RPi4 device tree blob |<https://github.com/raspberrypi/firmware/tree/master/boot/bcm2711-rpi-4-b.dtb> |
	||overlays/* | Device tree overlays |<https://github.com/raspberrypi/firmware/tree/master/boot/overlays> |

Tutorials/mcs.html links to master kernel manual instead of mcs kernel

The link is here: https://docs.sel4.systems/Tutorials/mcs.html#getting-help

delete the merged branch 'pingerino-patch-2'

Looks like the branch 'pingerino-patch-2' got merged a while ago, if there is no reason to keep it around it should be deleted.

Missing system calls on API reference page

I've noticed some system calls that appear in the reference manual, don't appear on the API reference page (https://docs.sel4.systems/projects/sel4/api-doc.html).

Specifically:

• seL4_NBSendRecv
• seL4_NBSendWait

There may be more but those are the ones I've noticed so far.

displayed page modification date incorrect

The footer shows site modification and page modification dates, but it looks like they are always the same and might always just be when the site got last generated.

zynq7000 patch is outdated

https://github.com/seL4/docs/blob/5b8af67b8625fd0ccad32ce6bab4ae6021e7e61e/Hardware/ZC706.md?plain=1#L35C1-L35C9

This patch does not apply at all to the current structure found over at https://github.com/Xilinx/u-boot-xlnx

add `xxd` to build dependencies

xxd is needed in elfloader-tool in some configs. See also seL4/seL4-CAmkES-L4v-dockerfiles#70

Docsite: inconsistency between landing page, submenus and pages

(This may wait for the Information Architecture feedback first)

• The landing page has a nice overview but it's not clear that this is just a subset of the docsite content. We should make that clear.

• The order and titles on the landing page and the submenus should be made consistent to avoid confusion. E.g.

  • "Building Dependencies" vs "Set up your machine" vs "Host dependencies"
  • "Hardware and Target platforms" vs "Supported hardware" vs "Supported Platforms"
  • "Contributing" on the landing page goes to the "Processes" page and the "Contributing processes" goes to the "Contributing" page
  • ...

• The Grouping should be consistent; namely "The source code" appears in "Getting started" in the landing page but belongs to "Contributing" submenu

• the "Roles" page appears in the landing page but not in the submenus. There's a question on location of this page versus having it on the website with the TSC information (see also issue 309 on website)

• All the links from the tutorial section on the landing page are wrong, going to the same root Tutorials page (#206)

Multiple Errors

I constructed my simple hello world project according to the first directory structure in your docs.

https://github.com/JonathonAnderson/hello-sel4

When I am in the build directory, I run the following command:

cmake -G Ninja -S ../ -DPLATFORM=x86_64 -DSIMULATION=TRUE

I receive the following output:

---

CMake Error at CMakeLists.txt:9 (include):
include could not find load file:

settings.cmake

-- The C compiler identification is GNU 9.2.1
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- The CXX compiler identification is GNU 9.2.1
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- The ASM compiler identification is GNU
-- Found assembler: /usr/bin/cc
CMake Error at kernel/config.cmake:95 (include):
include could not find load file:

src/arch//config.cmake

Call Stack (most recent call first):
kernel/CMakeLists.txt:54 (include)

CMake Error at kernel/config.cmake:96 (include):
include could not find load file:

include//mode/config.cmake

Call Stack (most recent call first):
kernel/CMakeLists.txt:54 (include)

CMake Error at kernel/CMakeLists.txt:383 (add_custom_command):
add_custom_command Wrong syntax. A TARGET or OUTPUT must be specified.

-- CPIO test cpio_reproducible_flag PASSED
CMake Error at tools/elfloader-tool/CMakeLists.txt:295 (message):
no image start address computed for platform; use platform YAML file or
replace this diagnostic with a CMake custom command to generate a file ""
that hard-codes it; the same goes for ""

-- Configuring incomplete, errors occurred!
See also "/home/jonathon/hello/build/CMakeFiles/CMakeOutput.log".

Intermittent dead links on Hardware/sabreLite.html page

Links for patches or binaries for setting up a sabre u-boot image initially return 404 and only work after waiting a short while:

• https://sel4.systems/Info/Hardware/sabreLite/u-boot.bin
• https://sel4.systems/Info/Hardware/sabreLite/01_android-imx6-uboot-enable_bootelf.patch

They 404'd initially, and then started resolving once I was writing up this issue.

repo sync errors

Hi,

I'm trying to build x86_64 example following instructions from "https://docs.sel4.systems/Hardware/IA32" and after "repo sync" I get lot of errors like:

Aborting
kernel/: leaving master; does not track upstream
error: kernel/: seL4.git checkout ed613d7d490be91f7f164ff98e09d9098de64d6e 
error: Cannot checkout seL4.git
(...)
Aborting
projects/musllibc/: leaving master; does not track upstream
error: projects/musllibc/: musllibc.git checkout 9798aedbc3ee5fa3c1d7f788e9312df9203e7b0b 
error: Cannot checkout musllibc.git
(...)
Aborting
projects/seL4_libs/: leaving master; does not track upstream
error: projects/seL4_libs/: seL4_libs.git checkout 043999f481d8f72f7993eb3d27f3cf3eb66b00a7 
error: Cannot checkout seL4_libs.git
(...)
Aborting
projects/sel4runtime/: leaving master; does not track upstream
error: projects/sel4runtime/: sel4runtime.git checkout d935dd05da0cf959e9fd0140af913dc6fdaa0221 
error: Cannot checkout sel4runtime.git
(...)
Aborting
projects/util_libs/: leaving master; does not track upstream
error: projects/util_libs/: util_libs.git checkout af6b18bd60e4f2e1a10ff1a1e687a46db02fa9db 
error: Cannot checkout util_libs.git
(...)
Aborting
tools/seL4/: leaving master; does not track upstream
error: tools/seL4/: seL4_tools.git checkout df31d5a844993166c88c8a1ccce5dd42018a7296 
error: Cannot checkout seL4_tools.git
Checking out: 100% (10/10), done in 0.576s
error: Unable to fully sync the tree
error: Checking out local projects failed.
Failing repos:
kernel                                                                                                                              
projects/musllibc                                                                                                                   
projects/seL4_libs                                                                                                                  
projects/sel4runtime                                                                                                                
projects/util_libs                                                                                                                  
tools/seL4                                                                                                                          
Try re-running with "-j1 --fail-fast" to exit at the first error.
================================================================================
Repo command failed due to the following `SyncError` errors:
seL4.git checkout ed613d7d490be91f7f164ff98e09d9098de64d6e 
musllibc.git checkout 9798aedbc3ee5fa3c1d7f788e9312df9203e7b0b                                                                      
seL4_libs.git checkout 043999f481d8f72f7993eb3d27f3cf3eb66b00a7                                                                     
sel4runtime.git checkout d935dd05da0cf959e9fd0140af913dc6fdaa0221                                                                   
util_libs.git checkout af6b18bd60e4f2e1a10ff1a1e687a46db02fa9db                                                                     
+1 additional errors...

I have no idea how to deal with this... I'm just following instructions... Any hint?

Edited: I missed this "Checkout the sel4test project using repo as per seL4Test". Now everything is ok, I was able to build a real hardware image for x86_64.

Hello-World tutorial init needs python3

On an Ubuntu 18.04 system, unless python3 dependencies have been installed specifically using pip3 (instead of pip), when the system has both python 2 and python 3 installed, the 'init' script of the hello-world tutorial seems to fail (with missing module errors)

The HostDependencies page instructs that both versions of python-dev and python3-dev be installed (and implicitly thus, python(2) and python3). However, the rest of the page instructs python dependencies to be installed with 'pip' (and not pip3).

This apparently causes a problem when the tutorial init scripts try to run, as this appears in an included script ( seL4-tutorials-manifest/projects/sel4-tutorials/common.py )
#!/usr/bin/env python3

Possible solution:
Once all the commands from HostDependencies were re-run with "pip3" substituted for "pip" (and additionally, the two pip install commands in Tutorials/#get-the-code likewise with pip3 substituted), the tutorial init scripts seemed to run to successful completion

Version of cmake broke the pipe on ubuntu1804

I have tried the build on ubuntu, the version can be install on it is cmake 3.10.x. And another ppa is broken too (unable to find IP). Snap will fix this problem by:

snap install cmake  --classic 

Barrier to entry

I noticed that the entry level documentation pages contain several dead links and the link to the latest manual leads to a manual for v11, not v12 which appears to be the latest release

Hardware/Qemu/index.md is out of date

https://github.com/SEL4PROJ/docs/blob/master/Hardware/Qemu/index.md needs to be updated to reflect current project structure and build system commands

Document support of Pine64 Quartz64 Board (RK3566)

Follow-up from seL4/seL4#727

Document Pine64 Quartz64Board support and maintainer. Or list this an unmaintained and mention at least that a PR/branch exists with the changes.

update build to work with Ubuntu 22.04

As discovered in #163, the docsite build is breaking with the default versions of ruby and bundler on Ubuntu 22.04.

We should update the dependencies such that they are more stable and at least work with both 20.04 and 22.04.

Out of date/old status page

I stumbled upon https://docs.sel4.systems/Status through Google. I haven't been able to find this page any other way. Doesn't seem to be in this repository anywhere. The page itself looks pretty outdated and was probably left over in the process of moving stuff around or something like that.

I'd try remove it myself but I don't know how to and most likely don't have access to do so.

FAQ: immutable OS

Can Sel4 be used to build an immutable system?

Testing.md refers to really old seL4 versions

It talks about 2.0.x.xml
https://github.com/SEL4PROJ/docs/blob/master/Testing.md

RPi4 Docs questionable mentioning of `bootcode.bin`

The RPi4 docs mention bootcode.bin. However, the RaspberryPi documentation mentions that this file is not used on RPi4 and RPi5, so I would guess the file is inert. If that is the case, the seL4 docs should not propose to add it to the SD, that only confuses users (like me).

docs/Hardware/Rpi4.md

Line 44 in 796c552

|SSBL |bootcode.bin|Loads GPU firmware and boots GPU|<https://github.com/raspberrypi/firmware/tree/master/boot/bootcode.bin> |

SMP on Odroid-C2

Is it still not supported as per documentation? PSCI is supported in elfloader, and Amlogic S905 uses PSCI. Short test with setting KernelMaxNumNodes to 4 and specifying affinity in camkes assembly file worked. Not sure how to get the current cpu from the thread though, getcpu syscall seems to be not implemented

How large is seL4?

Heiser and Elphinstone 2016:

The kernel compiles into about 9 k ARM instructions."

The current FAQ:

In terms of executable code size, on the 64-bit RISC-V architecture, the single-core kernel compiles into about 138 KiB. Its RAM size is about 162 KiB, which includes code, static data and the stack. Meta-data for usermode processes, incl. address spaces (page tables), thread-control blocks, capability storage etc, will add to this. (But note that in seL4’s memory-management model, such dynamic memory must be supplied to the kernel by usermode code.)

138 KiB is about 47 K RISC-V instructions, depending on the effectiveness of compression. Is RISC-V that poorly suited (no bitfield instructions, etc) to seL4 or if not what changed since 2016? So I built the spike/riscv64 kernel.

The default build following the Docker quickstart instructions with minimal changes for RISC-V (use the user_sel4-riscv Makefile target, change stack to sudo in the Makefile because the riscv image does not have stack, and configure with -DPLATFORM=spike) produces a 910KiB kernel.elf, unstripped. The size command reports 141KiB of text, very close to the reported number, increasing to 165 KiB including bss and data; I think this is where the numbers came from.

Disassembling and counting gives 20442 instructions occupying 60144 bytes - still a significant apparent regression, but in significant disagreement with the size output. The size output matches the sum of the length of .boot, .text, .srodata, and .rodata; .boot in its entirety is flagged in a text section, and because of the placement of the alignment, the full 64KiB alignment of .text is counted against the size of .boot.

Adjusting the linker script to separate .boot.text and .boot.data and moving the alignment outside of either results in a size measurement of 90 KiB "text" (still includes rodata) and 115 KiB total.

The 64KiB alignment might be a fossil of ARM's large frames; reducing it to 4KiB shrinks the kernel binary by 48 KiB and does not appear to affect sel4test (this does not affect runtime memory use since it's all returned as an untyped).

The bigger problem is that this is a debug build. (For a competitor, this is a listed "benchmarking crime"). The rodata is mostly string error messages.

A -DRELEASE=TRUE build has 14683 instructions (3614 in .boot.text, 11069 in .text) occupying 40952 (10146, 30806) bytes.
The total size of the load image as reported by objdump -p is 46 KiB text and initialized data, 69 KiB including bss (of which 12 KiB is returned as boot memory) This is within a plausible ballpark of the 2016 numbers.

Typo error

I think there's a typo error on the "IA32 Example" where it says:

../init-build.sh -DPLATFORM=ia32 -DRELEASE=TRUE -DSIMULATION=TRUE

should say:

../../init-build.sh -DPLATFORM=ia32 -DRELEASE=TRUE -DSIMULATION=TRUE

It's not a problem at all, but if you are copy-pasting commands it breaks a bit the "magic" of the "user experience" :-)
The more things we can try of seL4, the smoother things work, the more addictive it becomes.

Maintained repo status not in sync

The list on https://docs.sel4.systems/processes/release-process.html does not reflect reality:

• arm-vm-manifest is archived
• mcs-examples is not in CI or tagged
• does sel4webserver have CI?
• sel4tutorials is not a manifest repo

site build is broken

Potentially an unexpectedly recent jekyll version or similar.

See: https://github.com/seL4/docs/actions/runs/3520086041/jobs/5900677174

Liquid Exception: no implicit conversion of Hash into Integer in /home/runner/work/docs/docs/content_collections/_dependencies/l4v.md
                    ------------------------------------------------
      Jekyll 4.0.1   Please append `--trace` to the `build` command 
                     for any additional information or backtrace. 
                    ------------------------------------------------