seL4

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 568 (11) 316 (2) 336 (2) 811 (7)
x86_64 64 i7-4770/Haswell 3.4 GHz 1636 (253) 579 (12) 590 (13) 1247 (76)
x86_64 64 i7-6700/Skylake (without meltdown mitigation) 3.4 GHz 1322 (207) 382 (3) 389 (7) 770 (83)
Armv8a 64 A57/Tx1/Jetson 1.9 GHz 668 (37) 404 (6) 418 (8) 905 (15)
RV64IMAC 64 U54-MC/SiFive Freedom U540/Hifive 1.5 GHz 987 (84) 516 (125) 628 (7) 1367 (72)

MCS

ISA Mode Core/SoC/Board Clock IRQ Invoke IPC call IPC reply Notify
Armv7a 32 A9/i.MX6/Sabre 1.0 GHz 817 (17) 325 (6) 363 (2) 1211 (15)
x86_64 64 i7-4770/Haswell 3.4 GHz 2037 (436) 599 (19) 602 (12) 1596 (14)
x86_64 64 i7-6700/Skylake (without meltdown mitigation) 3.4 GHz 1738 (336) 388 (2) 411 (5) 1067 (6)
Armv8a 64 A57/Tx1/Jetson 1.9 GHz 759 (29) 433 (5) 429 (4) 957 (12)
RV64IMAC 64 U54-MC/SiFive Freedom U540/Hifive 1.5 GHz 1964 (39) 729 (114) 885 (97) 2588 (89)

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-03-27 for sel4bench-manifest 014a7f86.