Linux IPC syscall latencies benchmark in the 10s of microseconds typically. SeL4 has worst case execution guarantees that are better than that, even counting the fact that you have to do two syscalls for every one Linux syscall. We’re talking less than a thousand cycles total, which would be less than a single microsecond.

https://www.sel4.systems/About/Performance/home.pml

Does SeL4 have all of of the speculative execution mitigations that Linux has?

Syscall latency also is not the end-all-be-all of performance. Does that actually translate to faster disk and socket I/O on average?

I do believe there are speculative execution mitigations, yes...and from what I remember there was a significant performance impact when they were implemented, and especially so on processors without dedicated code caches.

Syscall latency is definitely not the end-all-be-all of performance, but it is all there is to compare between a monolithic kernel and a microkernel. In both cases, driver code needs to run, and that driver code can be good or shitty just like everything else.

When it comes down to it, the syscall latency that is comparable is the context switch between privileged and unprivileged mode. The holy grail of microkernels isn't to be faster than macrokernels, it is to be just as fast, but a hell of a lot more modular, usable, and secure.

> Syscall latency also is not the end-all-be-all of performance.

That depends on what you're doing. If you're running some digital signage display or whatever, no one cares about a missing display frame or whatever. But if you're running a car's HUD or, worse, its steering system, you absolutely need the execution time guarantees or your code won't make it past certification.

I'm not saying it's not an important space, because it is. But the majority of use cases are not that latency-sensitive. And if you're not that latency-sensitive, it's not obvious that microkernels like SeL4 and QNX are faster than Linux.

And the goalpost moves again.

Could just as well be read as the position of the goalpost gets more precisely specified for each question. The original "performance" was quite ambiguous; this is just a final specification of what was meant by the word.