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 |