I have a very vague memory of either a research paper or talk in which a “port” of Linux to use (Se?)L4 for process switching (???) resulted in a speedup. I’m certain that this is a wildly inaccurate memory and the closest I can come up with is L4Linux.
Does this ring any bells to anyone? Or is this just a memory that has bit-rotted to the point of meaninglessness?
This was before seL4. IIRC it was an older L4 kernel (a re-implementation at UNSW) together with a para-virtualised Linux (called Wombat). The main thing that was going on there was that L4 used fast ARM context switching code which Linux at that time did not implement. This meant that the para-virtualised Linux on L4 did indeed run faster (about 30x improved context switching time) than plain native Linux.
Would this no longer be true with SeL4? I remember Gernot saying something about how context switching on Linux is slow but his suggested changes were rejected as being too complicated. Was that in relation to Wombat or SeL4? Is SeL4 context switching no longer an “order of magnitude” faster than with Linux?
It is still true that seL4’s context switching is an order of magnitude faster than Linux (just saw benchmark results for that today in the seL4 summit again). That does not mean that Linux running on top of seL4 automatically gets faster. seL4 runs fully virtualised unmodified Linux VMs, whereas Wombat back then was para-virtualised (i.e. slightly modified) which made it possible to use the underlying L4 context switching instead of the Linux default context switching.
So, while any seL4 calls and context switches will be very fast, the Linux context switching runs at original Linux speed.