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