seL4test Project Status

This project status page lists the status for currently supported features, components and configurations for seL4Test and who is responsible for maintaining them.


Test runner

seL4test requires itself to be started directly by seL4 as the root-task in the system. This is the sel4test-driver binary and it then also serves as the main test runner. It runs the configured tests and sets up the required test environment for each test. It prints out test results over a serial connection. sel4test-driver is maintained by the seL4 Foundation and is currently the only test runner that is expected to run tests defined for seL4test.

Test environments

Each test runs in a test environment. This environment provides the test with an expected set of system resources required for it to run. There are currently two test environments, listed below. It is possible for more test environments to be defined in the future. The usual motivation for different test environments is different system dependencies of the tests.

Components Description Status Maintained by
BASIC test type General test type where test is launched in own process and can report test results to driver over IPC. active seL4 Foundation
BOOTSTRAP test type Bootstrapping test type where each test is called in the same address space as the test driver. Used for testing functionality required for BASIC test type. active. seL4 Foundation

Test declarations

Tests can be declared in any library that can be linked with sel4test applications. A test is defined by using a preprocessor macro defined by its test environment. This will place the test into a named linker section that the test runner will use to launch the test at runtime inside it’s requested environment.

Project manifests

Components Description Status Maintained by
master.xml seL4test project manifest with all repositories from master branches. active. Updated whenever project repository structure changes. seL4 Foundation
default.xml seL4test project manifest with all repositories pinned to last versions that passed all tests. active. This gets updated automatically by continuous integration. seL4 Foundation


The set of tests that get run will be different for different kernel configurations. Each test is able to specify a config requirement that will prevent the test from being run if a certain config option isn’t set in a compatible way. This means that changing the build configuration can change which tests will be run. To make it easier to configure a build of seL4test that enables the right coverage of tests there is a selection of meta-configuration options that are specific to seL4test. These options are listed below and will be interpreted by seL4test and used to set sensible default configuration values.

Configurations Description Status Maintained by
SIMULATION (BOOL) Include only simulation compatible tests (Default: OFF) seL4 Foundation
RELEASE (BOOL) Performance optimized build (Default: OFF) seL4 Foundation
VERIFICATION (BOOL) Only verification friendly kernel features (Default: OFF) seL4 Foundation
BAMBOO (BOOL) Enable machine parseable output (Default: OFF) seL4 Foundation
DOMAINS (BOOL) Test multiple domains (Default: OFF) seL4 Foundation
SMP (BOOL) (if supported) Test SMP kernel (Default: OFF) seL4 Foundation
NUM_NODES (STRING) (if SMP) the number of nodes) (Default: 4) seL4 Foundation
PLATFORM (STRING) Platform to test (Default: x86_64) seL4 Foundation
ARM_HYP (BOOL) Hyp mode for ARM platforms (Default: OFF) seL4 Foundation
MCS (BOOL) MCS kernel (Default: OFF) seL4 Foundation
KernelSel4Arch (STRING) aarch32, aarch64, arm_hyp, ia32, x86_64, riscv32, riscv64 (Default: Usually set by PLATFORM) seL4 Foundation
LibSel4TestPrinterRegex (STRING) A POSIX regex pattern used to filter tests (Default: .*) seL4 Foundation
LibSel4TestPrinterHaltOnTestFailure (BOOL) Halt on the first test failure (Default: OFF) seL4 Foundation