No, you don’t get to define the benchmarks like that. People use an OS so they can run real-world programs on top of it, not spin it in a loop and see how fast it can do IPC. In a monolithic kernel there’s no need to switch contexts for many things; that’s the entire point of using one. I’m sure that seL4 has a perfectly fast implementation of those operations but that’s because it sits and does those all day as part of its basic functionality. Optimizing overhead doesn’t win you extra points when you’re comparing against an OS that doesn’t have it all.
seL4 is an order of magnitude faster at this "overhead" thing. We're talking nanoseconds vs microseconds difference.
The multiserver architecture does indeed imply an elevated use of IPC, but it does in no way outweigh the difference in IPC cost.
In this model, data sharing, and the implied locking, is minimized, which as a consequence helps SMP scaling.
Dragonfly, while not multiserver proper, took a different direction than Freebsd and Linux by optimizing IPC and not implementing fine-grained locks, and instead favoring concurrent lockless and lockfree servers.
As a consequence, Dragonfly scales much better than Freebsd, and in many benchmarks manages to outperform Linux.
This is despite the tiny development team, particularly so when considered relative to the amount of funding these two systems get.
I am sickened by the effort that's being wasted on a model that we know is bad and does not work. Linux will never be high assurance, secure or scale past a certain point.
Fortunately, no matter how long it'll take, the better technology will win; there's no "performance hack" that a bad system can pull to catch up with the better technology once it's there.
Citation needed.
And by that I mean actual benchmarks of Linux doing the few tasks seL4 does, such as IPC or context switching, faster than seL4.