This page displays the latest benchmark numbers for seL4 from the publicly available sel4bench repository.

Benchmark results

HardwareIRQ path cycle countIPC microbenchmark, client→serverIPC microbenchmark, server→client
Sabre I.mx6 (Cortex A9 @1GHz)637301342
SkyLake (IA32 @3.4GHz)1112360354
SkyLake (X64 @3.4GHz)1615629631
SkyLake with no meltdown mitigations (X64 @3.4GHz)1224403404
Jetson TX1 AARCH64 (Cortex A57 @1.9GHz)855.5402385
HiFive Unleashed (RISC-V @1.5GHz)1087.5492622

IRQ path cycle count
Time in cycles to invoke a user-level interrupt handler running in the same address space as the interrupted thread.

IPC benchmark, client→server
Time in cycles for half an IPC between address spaces.

IPC Benchmark, server→client
Time in cycles for the IPC reply between address spaces.

Compilation details

HardwareCompilerBuild commandDocker image
Sabre I.mx6 (Cortex A9 @1GHz)arm-linux-gnueabi-gcc GNU 8.3.0../ -DPLATFORM=sabre -DHARDWARE=TRUE -DAARCH32=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUEtrustworthysystems/sel4
SkyLake (IA32 @3.4GHz)gcc GNU 8.4.0../ -DPLATFORM=ia32 -DHARDWARE=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUEtrustworthysystems/sel4
SkyLake (X64 @3.4GHz)gcc GNU 8.4.0../ -DPLATFORM=x86_64 -DHARDWARE=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUEtrustworthysystems/sel4
SkyLake with no meltdown mitigations (X64 @3.4GHz)gcc GNU 8.4.0../ -DPLATFORM=x86_64 -DKernelArch=x86 -DHARDWARE=TRUE -DKernelSkimWindow=FALSE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUEtrustworthysystems/sel4
Jetson TX1 AARCH64 (Cortex A57 @1.9GHz)aarch64-linux-gnu-gcc GNU 8.3.0../ -DPLATFORM=tx1 -DHARDWARE=TRUE -DAARCH64=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUEtrustworthysystems/sel4
HiFive Unleashed (RISC-V @1.5GHz)riscv64-unknown-linux-gnu-gcc GNU 8.3.0../ -DPLATFORM=hifive -DHARDWARE=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE -DRISCV64=TRUEtrustworthysystems/sel4-riscv

Source code

GitHub sel4bench-manifestb50a0ebcbe2e8821e7f82c0928fe0f18d466f499