seL4

Performance

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

BenchmarkSabre I.mx6 (Cortex A9 @1GHz)IA32 SkyLake @3.4GHzX64 SkyLake @3.4GHzJetson TK1 (Cortex A15 @700MHz)
IRQ path cycle count1859.59071102912
IPC microbenchmark, client->server288397354573
IPC microbenchmark, server->client304386358538

RepositoryCommit
GitHub sel4bench-manifest9c5b970c2dc7d4fb768d26b41b06cfa63135a31d
GitHub seL4dc24cdea0486527ca189a4b90f95ceaa0539f95e
GitHub seL4_tools7223b43dd0151933e64bca509b2a471770ccff05
GitHub muslclib (branch: sel4)558c9df056bac7b08863b2c3d64b06022a2dc49f
GitHub seL4_libsda16411463cdeb3188ba47f5cc620aa479de9530
GitHub util_libs9deb65ea5315c0781cbda238aae813d54e1fbe94
GitHub projects_libs8147869d485093eaaa4ccd322295d3675802673e
GitHub seL4bencha701fa344df10fac9b45d74e0c8702a29945d070
IRQ path cycle count
Time in cycles to deliver an interrupt to user space, where a context switch is not needed
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