The sel4bench Suite

sel4bench is an application and support library for benchmarking the performance of the seL4 kernel.

A selection of benchmarking results are continually updated on the main seL4 website. The page also shows the build options used to obtain those results.

Sources:

• https://github.com/seL4/sel4bench-manifest
• https://github.com/seL4/sel4bench

Getting the code

First make sure you have set up your machine. Then run the following.

mkdir sel4bench
cd sel4bench
repo init -u https://github.com/seL4/sel4bench-manifest.git
repo sync

This clones the seL4 kernel, the benchmarking suite including libraries, and tools used in the build process. By default, the current master branch of the kernel is cloned. To clone a specific version of the kernel and compatible libraries and tools, replace the line

repo init https://github.com/seL4/sel4bench-manifest.git

above with e.g.:

repo init -u https://github.com/seL4/sel4bench-manifest.git -b refs/tags/13.0.0

This example clones version 13.0.0 of the kernel. For more information on version numbers, see the release page and the list of seL4 releases.

Building and running sel4bench

Configuration

The CMake build environment supports a number of platforms. For information on which ones these are and their corresponding CMake configuration arguments, see the Supported Platforms page.

For the available meta configuration options, see below.

For example, to enable the optional Fault benchmark set and build for the sabre platform, we would use the following invocation.

# create build directory
mkdir build
cd build
# configure build directory
../init-build.sh -DPLATFORM=sabre -DFAULT=ON

Building

After you have configured the system, you can build it by running:

ninja

Running it

The build step above will produce a bootable image file in the images/ directory. Please refer to the documentation of the respective build platform for how to boot the specific board with such an image.

Available Benchmarks

The following table lists the available benchmark sets. Measured from user space means that the benchmark is not instrumenting the kernel. This means it measures unmodified kernel code, but may consequently have lower precision than some of the other benchmarks.

Configuration Options

Kernel configuration settings can have a large effect on the end results reported by the benchmarks. Some benchmarks will only work in certain configurations. To make it easier to configure a build of seL4bench that has the right configuration values set, use the meta-configuration options listed below.

RELEASE

HARDWARE

FAULT

VCPU

SMP

PLATFORM

FASTPATH

ARM_HYP

RELEASE

HARDWARE

FAULT

VCPU

SMP

PLATFORM

FASTPATH

ARM_HYP

Implementation

Benchmark runner

seL4bench must be started directly by seL4 as the root-task in the system. This is the sel4bench binary, which 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 completed.

Benchmarking environment

Each benchmark runs in a separate process environment. Currently there is only a single kind of 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. It also provides the configuration options for each benchmark. Each benchmark can provide an init function and a parse_results function that will get called in the main sel4bench app. Otherwise all benchmark functionality runs in the environment.

The libsel4benchsupport library provides environment functions that the benchmarks can call.

Adding a new benchmark

For adding new benchmarks see the sel4bench repository README.