On 13 Apr 2020, at 09:37, Leo Gaspard mailto:sel4@leo.gaspard.io> wrote:
Hello,
I come wondering: the FAQ claims that seL4 is “the world's fastest
microkernel”. However, I can only find benchmarks of just seL4, without
comparison to other operating systems running on the same machine.
Would you happen to have such comparative benchmarks? I'd be
particularly interested by something against L4Re, as it'd probably
allow me to guess at the performance of something similar to L4Linux
ported to seL4.
We benchmark our own system and publish the results in an easy to reproduce way. No-one else does, for good reason (because no-one is keen to demonstrate how much slower they are). If we published our own measurements of other systems’ performance, people might not believe them, or we might even not tweak the other systems to get the best out of them. So the best thing for us to do is to be open about our own performance, make the claim of being the fastest, and leave it to others to challenge this (with reproducible numbers, of course).
However, there is a recent peer-reviewed paper that does compare the performance of sel4, Fiasco.OC (aka L4Re) and Zircon. It shows that seL4 performance is within 10–20% of the hardware limit, while Fiasco.OC is about a factor two slower (i.e. >100% above the hardware limit), and Zircon is way slower than that: https://dl.acm.org/doi/pdf/10.1145/3302424.3303946
Gernot
