Traditionally, the performance metric people care most with microkernels is the basic IPC cost, i.e. the cost for sending a single, minimal-length message betwe en two threads. While it can be debated how meaningful such a microbenchmark is, IPC is the most critical operation of a microkernel.
All figures shown here are measured under the following circumstances:
Kernel | Architecture | Processor | Clock | Latency | Time | Measured | Source | |
---|---|---|---|---|---|---|---|---|
MHz | Cycles | ns | by | year | ||||
seL4 | Intel x86 (32 bit) | Core i7 4770 (Haswell) | 3,400 | 301 | 89 | NICTA | 2013 | SOSP'13 |
seL4 | ARM v7 | Cortex A9 | 1,000 | 316 | 316 | NICTA | 2013 | SOSP'13 |
seL4 | ARMv6 | ARM11 | 532 | 188 | 353 | NICTA | 2013 | SOSP'13 |
NOVA(1) | x86 (32 bit) | Core i7 920 (Bloomfield) | 2,667 | 288 | 108 | TU Dresden | 2010 | EuroSys'10 |
okL4 | ARMv5 | XScale 255 | 400 | 151 | 378 | NICTA | 2007 | NICTA |
okL4 | ARM v4 | StrongARM SA1100 | 206 | 131 | 635 | NICTA | 2007 | NICTA |
L4KA:Pistachio | IA64 | Itanium 2 | 1,500 | 36 | 24 | NICTA | 2005 | Usenix'05 |
L4KA:Pistachio | x86 (64 bit) | AMD Opteron 242 | 1,600 | 230 | 144 | University of Karlsruhe | 2004? | L4Ka site |
Hazelnut | x86 (32 bit) | Pentium 4 | 1,400 | 1,008 | 720 | University of Karlsruhe | 2002 | L4Ka site |
Hazelnut | x86 (32 bit) | Pentium II | 400 | 273 | 683 | University of Karlsruhe | 2002 | L4Ka site |
L4/MIPS(2) | MIPS64 | R4700 | 100 | 86 | 860 | UNSW | 1997 | HotOS'97 |
L4/Alpha(2) | Alpha | 21064 | 433 | 45 | 104 | TU Dresden | 1997 | HotOS'97 |
Original | x86 | Pentium | 166 | 121 | 756 | Liedtke | 1997 | HotOS'97 |
Original | x86 | i486 | 50 | 250 | 5,000 | Liedtke | 1993 | SOSP'93 |