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