Performance

The world's fastest kernel

seL4 has been designed for real-world use. From the beginning when verification started, the aim was to achieve the highest assurance level through formal proof, without sacrificing more than 10% in performance compared to the fastest kernels at the time.

seL4 not only beat the performance of those earlier kernels, but it now outperforms any microkernels by a factor of 2 to 10 times on key benchmarks. While independent performance comparisons are scarce, the few available studies corroborate our claims. We provide public performance numbers and a public experimental setup to enable repeatable independent benchmarks.

By providing both proved security and performance, seL4 is designed to support a wide range of real-world use cases.

Why IPC Benchmarks?

Microkernel-based systems tend to divide up software into a greater number of components than monolithic systems. Usually these components run in separate address spaces. This is excellent for improving security, but can incur overhead if done wrong.

Components on top of seL4 communicate with IPC (inter-process communication), notifications, and shared memory, where IPC is most commonly used as the mechanism for protected procedure calls. The IPC benchmarks below measure the overhead of these calls and show that they are on the order of normal function calls in monolithic systems. This is the key benchmark for showing that improved security is possible without sacrificing performance.

Performance numbers

This section 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 a different 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