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 |