[vacuity]

Note: IPC performance isn't the only factor in overall OS performance. Especially for a "traditional microkernel", where programs are split up into separate processes liberally, performance degrades due to the sheer number of cross-boundary interactions. A whole system is performant if the design of the whole system, not just the design of the kernel, is aligned with performance. This is not to put down seL4; on the other hand, it continues the trend of L4 microkernels demonstrating the viability of stricter designs. But keep in mind that more time and effort is necessary to implement larger systems well.

[snvzz]

Do not miss the latest seL4 summit's state of seL4 talk by Gernot Heiser[0], which besides providing an update on the work done this year, goes into performance[1].

This is real world throughput and latency seL4 is crushing Linux on, not some synthetic IPC benchmark.

0. https://www.youtube.com/watch?v=wP48V34lDhk

1. https://youtu.be/wP48V34lDhk?t=1199

[vacuity]

I think I've got the gist now. Although I think Gernot Heiser doesn't consider the following to be ideal, I think it's fair to say that true claims have undergone some sensationalization. I don't think people generally lie when they say their product has achieved some impressive performance, but those results exist in the context they are taken under. In the embedded roles LionsOS is being targeted for, I have no doubt that they represent a real improvement over existing Linux systems, and probably any Linux system short of a magical one. However, in a general-purpose OS (which is what I focus on), which is the same as saying that many distinct user bases are simultaneously involved, the kernel is far from being the only load-bearing component. Also note that the functionality compared is not 1:1, nor is Linux the final contender of monolithic systems.

Something I want to explore, and which has some viability in the LionsOS model too, is that a general-purpose system may still liberally cut out unused functionality if highly modular and easily configurable. Like Legos.

In conclusion, props to the people at Trustworthy Systems as always, but it's safe to say that the OS field is still far from settled. My best compliment to seL4 is that it has raised the bar and simultaneously paved the way for future generations of advances. It's a seminal work that was desperately needed.

[vacuity]

I will check those out tomorrow, but in the meantime: I don't mean to say that a microkernel-based system is necessarily worse on performance. However, I think a highly optimized monolithic system will probably always be somewhat faster than a highly optimized microkernel-based system. And note that the seL4 system is probably less mature, and that I have many criticisms of Linux in being a supposedly highly optimized system. I'm all for microkernels. I'm planning to write one myself. But there are some aspects that microkernel-based systems have to work harder on.