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.