L4 Microkernels
- 6 April 2016
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Computer Systems
- Vol. 34 (1), 1-29
- https://doi.org/10.1145/2893177
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 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 articles 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.Keywords
Funding Information
- Digital Economy and the Australian Research Council through the ICT Centre of Excellence program
- Australian Government as represented by the Department of Broadband, Communications
This publication has 32 references indexed in Scilit:
- Comprehensive formal verification of an OS microkernelACM Transactions on Computer Systems, 2014
- Making information flow explicit in HiStarCommunications of the ACM, 2011
- seL4 Enforces IntegrityLecture Notes in Computer Science, 2011
- User-Level Device Drivers: Achieved PerformanceJournal of Computer Science and Technology, 2005
- Toward real microkernelsCommunications of the ACM, 1996
- Two years of experience with a μ-Kernel based OSACM SIGOPS Operating Systems Review, 1991
- KeyKOS architectureACM SIGOPS Operating Systems Review, 1985
- A Linear Time Algorithm for Deciding Subject SecurityJournal of the ACM, 1977
- The nucleus of a multiprogramming systemCommunications of the ACM, 1970
- Programming semantics for multiprogrammed computationsCommunications of the ACM, 1966