L4 Microkernels: The Lessons from 20 Years of Research and Deployment

Select |




Print


Heiser, Gernot; Elphinstone, Kevin

Heiser, Gernot; Elphinstone, Kevin


2016-04-07


Journal Article


ACM Transactions on Computer Systems


34


1


1:1-1:29


The L4 microkernel has undergone 20 years of use and evolution. It has an active user and developer community, and there are commercial versions that are deployed on a large scale and in safety-critical systems. In this article 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. We specifically look at 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, generality and high inter-process communication (IPC) performance remain the main drivers of design and implementation decisions.


https://doi.org/10.1145/2893177


nicta:8988


Heiser, Gernot; Elphinstone, Kevin. L4 Microkernels: The Lessons from 20 Years of Research and Deployment. ACM Transactions on Computer Systems. 2016-04-07; 34(1):1:1-1:29. https://doi.org/10.1145/2893177



Loading citation data...

Citation counts
(Requires subscription to view)