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.
Would a paravirtualized Linux built on seL4 see a perf benefit like that of Wombat? Or has Linux already adopted the tricks that made Wombat faster?
I don’t know, but I would hope that something has moved in that part of Linux in the last 15 years.
The main reason to not continue that project was that it is very high effort to keep maintaining a paravirtualised Linux kernel for all that time when you can run an unmodified fully virtualised one instead.
What confuses me is that all y’all have produced a lot of slides with block diagrams showing seL4 as a hypervisor for Linux. It would be nice to be able to make the flat claim that a seL4 hypervisor or a paravirtualized Linux based on seL4 would be faster than the Linux equivalent.
But until there is a benchmark for that, perhaps it would be best to avoid such claims.
No one is claiming that virtualised Linux on top of seL4 makes Linux context switching faster than on native Linux, what are you talking about?
Apparently there was a paravirtualised Linux running on top of a seL4 predecessor using a more efficient calling convention or whatever resulting in faster context switches for a virtualised Linux. Although interesting, it’s not relevant to today’s Linux and seL4.
I have the feeling you are mixing up different things: Claims about seL4 context switch versus Linux context switch speed, and the earlier mentioned Linux context switch speed when running virtualised on top of seL4.