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-4770/Haswell | 3.4GHz | 1612 | 620 | 626 |
| 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-4770/Haswell | 3.4GHz | gcc GNU 8.4.0 | ../init-build.sh -DPLATFORM=x86_64 -DHARDWARE=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 |