seL4

Performance

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

Benchmark results

Default

ISA Size Core/Soc/Board Clock IRQ invoke IPC call IPC reply
Armv7 32 A9/i.MX6/Sabre 1GHz 695 302 324
x86_64 64 i7-6700/Skylake ** 3.4GHz 1212 408 406
Armv8 64 A57/Tx1/Jetson 1.9GHz 851 398 385
RISC-V 64 U54-MC/SiFive Freedom U540/Hifive 1.5GHz 1192.5 475 529


** Skylake with no meltdown mitigation.

MCS

ISA Size Core/Soc/Board Clock IRQ invoke IPC call IPC reply
Armv7 32 A9/i.MX6/Sabre 1GHz 853.5 315 342
x86_64 64 i7-4770/Haswell 3.4GHz 1904 632 648
Armv8 64 A57/Tx1/Jetson 1.9GHz 964 396 410
RISC-V 64 U54-MC/SiFive Freedom U540/Hifive 1.5GHz 1714 524 722.5

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

IPC call
Time in cycles for invoking a server in a different address space on the same core.

IPC reply
Time in cycles for a server replying to a client in a different address space on the same core.

Compilation details

ISA Size Core/Soc/Board Clock Compiler Build command Docker image
Armv7 32 A9/i.MX6/Sabre 1GHz arm-linux-gnueabi-gcc GNU 8.3.0 ../init-build.sh -DPLATFORM=sabre -DHARDWARE=TRUE -DAARCH32=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE trustworthysystems/sel4
x86_64 64 i7-6700/Skylake ** 3.4GHz gcc GNU 8.4.0 ../init-build.sh -DPLATFORM=x86_64 -DHARDWARE=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE trustworthysystems/sel4
Armv8 64 A57/Tx1/Jetson 1.9GHz aarch64-linux-gnu-gcc GNU 8.3.0 ../init-build.sh -DPLATFORM=tx1 -DHARDWARE=TRUE -DAARCH64=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE trustworthysystems/sel4
RISC-V 64 U54-MC/SiFive Freedom U540/Hifive 1.5GHz riscv64-unknown-linux-gnu-gcc GNU 10.2.0 ../init-build.sh -DPLATFORM=hifive -DHARDWARE=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE -DRISCV64=TRUE trustworthysystems/sel4-riscv
Armv7 32 A9/i.MX6/Sabre 1GHz arm-linux-gnueabi-gcc GNU 8.3.0 ../init-build.sh -DPLATFORM=sabre -DHARDWARE=TRUE -DAARCH32=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DMCS=TRUE -DFASTPATH=TRUE trustworthysystems/sel4
x86_64 64 i7-4770/Haswell 3.4GHz gcc GNU 8.4.0 ../init-build.sh -DPLATFORM=x86_64 -DRELEASE=TRUE -DFAULT=TRUE -DMCS=TRUE -DHARDWARE=TRUE -DFASTPATH=TRUE trustworthysystems/sel4
Armv8 64 A57/Tx1/Jetson 1.9GHz aarch64-linux-gnu-gcc GNU 8.3.0 ../init-build.sh -DPLATFORM=tx1 -DHARDWARE=TRUE -DAARCH64=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DMCS=TRUE -DFASTPATH=TRUE trustworthysystems/sel4
RISC-V 64 U54-MC/SiFive Freedom U540/Hifive 1.5GHz riscv64-unknown-linux-gnu-gcc GNU 10.2.0 ../init-build.sh -DPLATFORM=hifive -DHARDWARE=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DMCS=TRUE -DFASTPATH=TRUE -DRISCV64=TRUE trustworthysystems/sel4-riscv

Source code

Repository Commit
GitHub sel4bench-manifest 0181ae672eb1026944c1a85e0130e48654d19dd0