From L3 to seL4 what have we learnt in 20 years of L4 microkernels?

The L4 microkernel has undergone 20 years of use and evolution. It has an active user and developer community, and there are commercial versions which are deployed on a large scale and in safety-critical systems. In this paper we examine the lessons learnt in those 20 years about microkernel design and implementation. We revisit the L4 design papers, and examine the evolution of design and implementation from the original L4 to the latest generation of L4 kernels, especially seL4, which has pushed the L4 model furthest and was the first OS kernel to undergo a complete formal verification of its implementation as well as a sound analysis of worst-case execution times. We demonstrate that while much has changed, the fundamental principles of minimality and high IPC performance remain the main drivers of design and implementation decisions.
In the ACM Digital Library: dl.acm.org/cita...

[@biggusmunkusthegreat]

I've been designing a microkernel for 7 years now and to hear many of the ideas I've had over the years put so succinctly is so satisfying. Clear, direct, amazing talk. Thank you SO MUCH for posting this.

[@jlxip]

This is awesome, thank you for posting it on RUclips.

[@inkbunnybunny]

I have a question would it be possible to have more than just User and Kernel space?

[@doBobro]

Ah those sweet pre-SPECTRE times full of hopes.

[@jochenliedtke6910]

OMG that old dude is still around!! Garnot Heiser is an old man long past his prime and long past his time. He should have been put out to pasture all long time ago.

[@teclishighelf5787]

Yes, I agree Heiser and his research group should definitely put away their laptops and take up knitting.

[@afakeaccountofcourse.8463]

gee, why so much hate? Be constructive.

[@teclishighelf5787]

Heiser is busted! I found a darknet site with sel4 exploits and they all work on the version of seL4 that apple used.......

[@qwertyplm13does51]

teclis High Elf does Apple use sel4?