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 the seL4 Foundation 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 the seL4 Foundation 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 seL4 Foundation
Hardware benchmarks Application to benchmark hardware-related operations active seL4 Foundation
IPC benchmarks Application to benchmark seL4 IPC active seL4 Foundation
IRQ kernel-mode benchmarks Application to benchmark seL4 IRQs from inside the kernel active seL4 Foundation
IRQ user-mode benchmarks Application to benchmark seL4 IRQs without modification to the kernel active seL4 Foundation
Page mapping benchmarks Application to benchmark seL4 mapping a series of pages active seL4 Foundation
Scheduler benchmarks Application to benchmark seL4 scheduler without modification to the kernel active seL4 Foundation
Signal benchmarks Application to benchmark seL4 signals without modification to the kernel active seL4 Foundation
SMP benchmarks Application to benchmark SMP operations and IPC active seL4 Foundation
Synchronisation library benchmarks Application to benchmark the seL4 sync library active seL4 Foundation
Aarch64 VCPU benchmarks Application to benchmark seL4 VCPU performance active seL4 Foundation

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

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) seL4 Foundation
HARDWARE (BOOL) Configuration for sel4bench hardware app (Default: OFF) seL4 Foundation
FAULT (BOOL) Configuration sel4bench fault app (Default: OFF) seL4 Foundation
VCPU (BOOL) Whether or not to run the VCPU benchmarks (Default: OFF) seL4 Foundation
SMP (BOOL) Configuration sel4bench smp app (Default: OFF) seL4 Foundation
PLATFORM (STRING) Platform to test (Default: x86_64) seL4 Foundation
FASTPATH (BOOL) Turn fastpath on or off (Default: ON) seL4 Foundation
ARM_HYP (BOOL) ARM EL2 hypervisor features on or off (Default: OFF) seL4 Foundation