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.

Features

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 Data61 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 Data61
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. Data61

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. Data61
default.xml seL4test project manifest with all repositories pinned to last versions that passed all tests. active. This gets updated automatically by continuous integration. Data61

Configurations

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) Data61
RELEASE (BOOL) Performance optimized build (Default: OFF) Data61
VERIFICATION (BOOL) Only verification friendly kernel features (Default: OFF) Data61
BAMBOO (BOOL) Enable machine parseable output (Default: OFF) Data61
DOMAINS (BOOL) Test multiple domains (Default: OFF) Data61
SMP (BOOL) (if supported) Test SMP kernel (Default: OFF) Data61
NUM_NODES (STRING) (if SMP) the number of nodes) (Default: 4) Data61
PLATFORM (STRING) Platform to test (Default: x86_64) Data61
ARM_HYP (BOOL) Hyp mode for ARM platforms (Default: OFF) Data61
MCS (BOOL) MCS kernel (Default: OFF) Data61
KernelSel4Arch (STRING) aarch32, aarch64, arm_hyp, ia32, x86_64, riscv32, riscv64 (Default: Usually set by PLATFORM) Data61
LibSel4TestPrinterRegex (STRING) A POSIX regex pattern used to filter tests (Default: .*) Data61
LibSel4TestPrinterHaltOnTestFailure (BOOL) Halt on the first test failure (Default: OFF) Data61