performance.html

---
# Copyright 2021 seL4 Project a Series of LF Projects, LLC.
# SPDX-License-Identifier: CC-BY-SA-4.0
title: Performance
sub: '
<p>
 seL4 stands apart with its unparalleled formal verification, without any
 compromise in performance. In fact it is <a href="#fastest">fastest operating
 system kernel</a> available on IPC performance. This page explains this claim
 and its significance, while also providing
 <a href="#perf-numbers"> detailed seL4 performance metrics</a>.
 <img src="images/sel4-fast.svg"
      alt="speeding seL4 logo with 2-10x faster byline"
      class="rounded-lg mt-8 w-1/2 mx-auto">
</p>'
redirect_from:
- /About/Performance/home.pml
- /About/Performance/index.html
layout: card
---


<div class="theprose mx-auto">
<h2 id="fastest">The world's fastest kernel</h2>

<p>
  seL4 has been designed for real-world use. From
  the <a href="About/history.html">beginning</a> 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.
</p>

<p>
  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.
</p>
<p>
  By providing both proved security and performance, seL4 is designed to support
  a wide range of real-world <a href="use.html">use cases</a>.
</p>


<h3>Why IPC Benchmarks?</h3>

<p>
  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.
</p>
<p>
  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.
</p>

<h2 id="perf-numbers">Performance numbers</h2>

<p>This section displays the latest benchmark numbers for seL4 from the publicly
available <a href="https://github.com/seL4/sel4bench">sel4bench repository</a>.
The following times are reported as mean and standard deviation in
the format <em>mean (std dev)</em>, both rounded to the nearest integer.</p>
Unless otherwise stated, the client has the FPU enabled, whereas the server
has the FPU disabled.

<ul>
  <li><strong>IRQ invoke</strong>: Time in cycles to invoke a user-level
    interrupt handler running in a different address space as the interrupted
    thread.</li>
  <li><strong>IPC call</strong>: Time in cycles for invoking a server in a
    different address space on the same core.</li>
  <li><strong>IPC reply</strong>: Time in cycles for a server replying to a
    client in a different address space on the same core.</li>
  <li><strong>Notify</strong>: Time in cycles to send a signal from a process
    with priority 1 to a higher priority (255) process in a different address
    space</li>
</ul>
</div>

{% include benchmark-table.html section="Default" %}
{% include benchmark-table.html section="MCS" %}

<div class="theprose mx-auto pt-20">
<h2 id="compil-details">Compilation Details</h2>
<p>All benchmarks were built using the trustworthy-systems/sel4
docker image from the <a href="https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles">seL4
docker file repository</a></p>
</div>

<details>
<summary class="theprose mx-auto">See details on compiler and build commands</summary>
{% include bench-comp-table.html section="Default" %}
{% include bench-comp-table.html section="MCS" %}
</details>

{% if site.data.benchmarks.sha %}
{% assign sha = site.data.benchmarks.sha %}
<div class="theprose mx-auto pb-20">
<h2>Source Code</h2>
<p>This page was generated on {{ "now" | date: "%Y-%m-%d" }} for sel4bench-manifest <a href="https://github.com/seL4/sel4bench-manifest/blob/{{sha}}/default.xml">{{sha}}</a>.</p>
</div>
{% endif %}