sel4 benchmarking applications and support library.

To get this project, check out the project manifest: https://github.com/seL4/sel4bench-manifest

We provide multiple applications for benchmarking different paths in the kernel.

This is the driver application: it launches each benchmark in a separate process and collects, processes and outputs results.

This is a hot cache benchmark of the IPC path.

This is a hot cache benchmark of the irq path, measured from inside the kernel. It requires tracepoints to be placed on the irq path where the meaurements are to be taken from.

This is a hot cache benchmark of the irq path, measured from user-level.

This is a hot cache benchmark of a scheduling decision. It works by using a producer-consumer pattern between two notification objects. This benchmark also measures seL4_Yield

This is a hot cache benchmark of the signal path in the kernel, measured from user level.

This is a benchmark measuring mapping, unmapping, protecting and unprotecting a series of pages.

This is an intra-core ipc round-trip benchmark to check overhead of the kernel synchronization on ipc throughput.