Performance
This page displays the latest benchmark numbers for seL4 from the publicly
available sel4bench repository.
The following times are reported as mean and standard deviation in
the format mean (std dev), both rounded to the nearest integer.
- 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.
- Notify: Time in cycles to send a signal from a process with priority 1 to a higher
priority (255) process in a different address space
Default
ISA |
Mode |
Core/SoC/Board |
Clock |
IRQ Invoke |
IPC call |
IPC reply |
Notify |
Armv7a |
32 |
A9/i.MX6/Sabre |
1.0 GHz |
587 |
(13) |
316 |
(2) |
340 |
(9) |
829 |
(11) |
x86_64 |
64 |
i7-4770/Haswell |
3.4 GHz |
1572 |
(268) |
590 |
(15) |
591 |
(14) |
1338 |
(71) |
x86_64 |
64 |
i7-6700/Skylake (without meltdown mitigation) |
3.4 GHz |
1220 |
(203) |
382 |
(2) |
383 |
(1) |
754 |
(82) |
Armv8a |
64 |
A57/Tx1/Jetson |
1.9 GHz |
668 |
(32) |
423 |
(8) |
409 |
(2) |
948 |
(5) |
RV64IMAC |
64 |
U54-MC/SiFive Freedom U540/Hifive |
1.5 GHz |
957 |
(26) |
470 |
(17) |
669 |
(120) |
1359 |
(72) |
MCS
ISA |
Mode |
Core/SoC/Board |
Clock |
IRQ Invoke |
IPC call |
IPC reply |
Notify |
Armv7a |
32 |
A9/i.MX6/Sabre |
1.0 GHz |
800 |
(17) |
323 |
(2) |
363 |
(2) |
1239 |
(12) |
x86_64 |
64 |
i7-4770/Haswell |
3.4 GHz |
1929 |
(434) |
584 |
(14) |
599 |
(13) |
1588 |
(13) |
x86_64 |
64 |
i7-6700/Skylake (without meltdown mitigation) |
3.4 GHz |
1669 |
(333) |
383 |
(2) |
408 |
(7) |
1056 |
(12) |
Armv8a |
64 |
A57/Tx1/Jetson |
1.9 GHz |
756 |
(23) |
418 |
(16) |
428 |
(5) |
1018 |
(6) |
RV64IMAC |
64 |
U54-MC/SiFive Freedom U540/Hifive |
1.5 GHz |
2993 |
(184) |
675 |
(25) |
877 |
(44) |
3830 |
(133) |
Compilation Details
All benchmarks were built using the trustworthy-systems/sel4
docker image from the seL4
docker file repository
Default
ISA |
Mode |
Core/SoC/Board |
Clock |
Compiler |
Build command |
Armv7a |
32 |
A9/i.MX6/Sabre |
1.0 GHz |
arm-linux-gnueabi-gcc GNU 10.2.1 |
init-build.sh -DFASTPATH=TRUE -DHARDWARE=TRUE -DFAULT=TRUE -DAARCH32=TRUE -DPLATFORM=sabre |
x86_64 |
64 |
i7-4770/Haswell |
3.4 GHz |
gcc GNU 10.2.1 |
init-build.sh -DFASTPATH=TRUE -DHARDWARE=TRUE -DFAULT=TRUE -DPLATFORM=x86_64 |
x86_64 |
64 |
i7-6700/Skylake |
3.4 GHz |
gcc GNU 10.2.1 |
init-build.sh -DKernelSkimWindow=FALSE -DFASTPATH=TRUE -DHARDWARE=TRUE -DFAULT=TRUE -DPLATFORM=x86_64 |
Armv8a |
64 |
A57/Tx1/Jetson |
1.9 GHz |
aarch64-linux-gnu-gcc GNU 10.2.1 |
init-build.sh -DFASTPATH=TRUE -DHARDWARE=TRUE -DFAULT=TRUE -DAARCH64=TRUE -DPLATFORM=tx1 |
RV64IMAC |
64 |
U54-MC/SiFive Freedom U540/Hifive |
1.5 GHz |
riscv64-unknown-elf-gcc GNU 8.3.0 |
init-build.sh -DFASTPATH=TRUE -DHARDWARE=FALSE -DFAULT=FALSE -DRISCV64=TRUE -DPLATFORM=hifive |
MCS
ISA |
Mode |
Core/SoC/Board |
Clock |
Compiler |
Build command |
Armv7a |
32 |
A9/i.MX6/Sabre |
1.0 GHz |
arm-linux-gnueabi-gcc GNU 10.2.1 |
init-build.sh -DFASTPATH=TRUE -DHARDWARE=TRUE -DFAULT=TRUE -DAARCH32=TRUE -DPLATFORM=sabre -DMCS=TRUE |
x86_64 |
64 |
i7-4770/Haswell |
3.4 GHz |
gcc GNU 10.2.1 |
init-build.sh -DFASTPATH=TRUE -DHARDWARE=TRUE -DFAULT=TRUE -DPLATFORM=x86_64 -DMCS=TRUE |
x86_64 |
64 |
i7-6700/Skylake |
3.4 GHz |
gcc GNU 10.2.1 |
init-build.sh -DKernelSkimWindow=FALSE -DMCS=TRUE -DFASTPATH=TRUE -DHARDWARE=TRUE -DFAULT=TRUE -DPLATFORM=x86_64 |
Armv8a |
64 |
A57/Tx1/Jetson |
1.9 GHz |
aarch64-linux-gnu-gcc GNU 10.2.1 |
init-build.sh -DFASTPATH=TRUE -DHARDWARE=TRUE -DFAULT=TRUE -DAARCH64=TRUE -DPLATFORM=tx1 -DMCS=TRUE |
RV64IMAC |
64 |
U54-MC/SiFive Freedom U540/Hifive |
1.5 GHz |
riscv64-unknown-elf-gcc GNU 8.3.0 |
init-build.sh -DFASTPATH=TRUE -DHARDWARE=FALSE -DFAULT=FALSE -DRISCV64=TRUE -DPLATFORM=hifive -DMCS=TRUE |
Source Code
This page was generated on 2024-11-17 for sel4bench-manifest aaf40929.