seL4bench Project Status

This project status page lists the status for currently supported features, components and configurations for seL4bench and who is responsible for maintaining them. Some benchmark results are regularly updated on the sel4.systems website.

Features

Benchmark runner

seL4bench requires itself to be started directly by seL4 as the root-task in the system. This is the sel4bench binary and it then also serves as the main benchmark runner. It runs the configured benchmarks and sets up a new environment for each benchmark to run in. When a benchmark completes, it reports the results back to the runner and the runner prints the results out as JSON once all the benchmarks have run. sel4bench is maintained by Data61 and is currently the only benchmark runner that is expected to run benchmarks targeting sel4bench.

Benchmarking environment

Each benchmark runs in a separate process environment. Currently there is only a single environment that all benchmarking apps are expected to execute in. This environment defines the set of system resources that each benchmark is given to run with, and also provides the configuration options for each benchmark. Each benchmark is able to provide an init function and parse results function that will get called in the main sel4bench app. Otherwise all benchmark functionality runs in the environment.

The libsel4benchsupport is a library that provides the environment functions that the benchmarks can call. This library is maintained by Data61 and is extended to support new features as new benchmarks are added.

Benchmarks

Components Description Status Maintained by
Fault benchmarks Application to benchmark seL4 faults without modification to the kernel active Data61
Hardware benchmarks Application to benchmark hardware-related operations active Data61
IPC benchmarks Application to benchmark seL4 IPC active Data61
IRQ kernel-mode benchmarks Application to benchmark seL4 IRQs from inside the kernel active Data61
IRQ user-mode benchmarks Application to benchmark seL4 IRQs without modification to the kernel active Data61
Page mapping benchmarks Application to benchmark seL4 mapping a series of pages active Data61
Scheduler benchmarks Application to benchmark seL4 scheduler without modification to the kernel active Data61
Signal benchmarks Application to benchmark seL4 signals without modification to the kernel active Data61
SMP benchmarks Application to benchmark SMP operations and IPC active Data61
Synchronisation library benchmarks Application to benchmark the seL4 sync library active Data61
Aarch64 VCPU benchmarks Application to benchmark seL4 VCPU performance active Data61

Project manifests

Components Description Status Maintained by
master.xml seL4bench project manifest with all repositories from master branches. active. Updated whenever project repository structure changes. Data61
default.xml seL4bench project manifest with all repositories pinned to last versions that successfully produced benchmark results. active. This gets updated automatically by continuous integration. Data61

Configurations

Different configurations can have a large effect on the end results reported by the benchmarks. Some benchmarks also won’t work unless certain configurations are set. To make it easier to configure a build of seL4bench that has the right configuration values set there is a selection of meta-configuration options that are specific to seL4bench. These options are listed below and will be interpreted by seL4bench and used to set sensible default configuration values.

Configurations Description Status Maintained by
RELEASE (BOOL) Performance optimized build (Default: ON) Data61
HARDWARE (BOOL) Configuration for sel4bench hardware app (Default: OFF) Data61
FAULT (BOOL) Configuration sel4bench fault app (Default: OFF) Data61
VCPU (BOOL) Whether or not to run the VCPU benchmarks (Default: OFF) Data61
SMP (BOOL) Configuration sel4bench smp app (Default: OFF) Data61
PLATFORM (STRING) Platform to test (Default: x86_64) Data61
FASTPATH (BOOL) Turn fastpath on or off (Default: ON) Data61
ARM_HYP (BOOL) ARM EL2 hypervisor features on or off (Default: OFF) Data61