Paper Info
Title
From L3 to seL4 what have we learnt in 20 years of L4 microkernels?
Abstract
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.
Year
DOI
Venue
2013
10.1145/2517349.2522720
SOSP
Keywords
Field
DocType
l4 microkernels,l4 model furthest,active user,commercial version,l4 design paper,complete formal verification,os kernel,l4 microkernel,l4 kernel,implementation decision,microkernel design,iommu,hypervisor,operating systems,virtualization
Virtualization,Computer science,Hypervisor,Microkernel,Real-time computing,Micro kernel,Os kernel,Operating system,Sound analysis,Embedded system,Formal verification
Conference
Citations 
PageRank 
References 
42
1.27
30
Authors
2
Name
Order
Citations
PageRank
K. Elphinstone1119065.76
Gernot Heiser22525137.42