From L3 to seL4 What Have We Learnt in 20 Years …

1 From L3 to seL4 What Have We Learnt in 20 years of l4 microkernels ?Kevin Elphinstone and Gernot HeiserNICTA and UNSW, L4 microkernel has undergone 20 Years of use andevolution. It has an active user and developer commu-nity, and there are commercial versions which are de-ployed on a large scale and in safety-critical this paper we examine the lessons Learnt in those 20years about microkernel design and implementation. Werevisit the L4 design papers, and examine the evolutionof design and implementation from the original L4 to thelatest generation of L4 kernels, especially seL4, whichhas pushed the L4 model furthest and was the first OSkernel to undergo a complete formal verification of itsimplementation as well as a sound analysis of worst-caseexecution times.

2 We demonstrate that while much haschanged, the fundamental principles of minimality andhigh IPC performance remain the main drivers of designand implementation IntroductionTwenty Years ago, Liedtke [1993a] demonstrated withhis L4 kernel that microkernel IPC could be fast, a factor10 20 faster than other contemporary minimize the functionality that is pro-vided by the kernel: the kernel provides a set of generalmechanisms, while user-mode servers implement the ac-tual operating system (OS) services [Levin et al., 1975].User code obtains a system service by communicatingwith servers via an inter-process communication (IPC)mechanism, typically message passing. Hence, IPC isPermission to make digital or hard copies of part or all of this work forpersonal or classroom use is granted without fee provided that copiesare not made or distributed for profit or commercial advantage and thatcopies bear this notice and the full citation on the first page.

3 Copyrightsfor third-party components of this work must be honored. For all otheruses, contact the is held by the Owner/Author(s).SOSP 13, Nov. 3 6, 2013, Farmington, Pennsylvania, 978-1-4503-2388-8/13 the critical path of any service invocation, and lowIPC costs are the early 90s, IPC performance had become theachilles heel of microkernels : typical cost for a one-way message was around 100 s, which was too highfor building performant systems, with a resulting trendto move core services back into the kernel [Condictet al., 1994]. There were also arguments that high IPCcosts were an (inherent?) consequence of the structure ofmicrokernel-based systems [Chen and Bershad, 1993].In this context, the order-of-magnitude improvementof IPC costs Liedtke demonstrated was quite remark-able.

4 It was followed by work discussing the philoso-phy and mechanisms of L4 [Liedtke, 1995, 1996], thedemonstration of a para-virtualized Linux on L4 withonly a few percent overhead [H artig et al., 1997], thedeployment of L4 kernels on billions of mobile devicesand in safety-critical systems, and, finally, the world sfirst functional correctness proof of an OS kernel [Kleinet al., 2009]. It also had a strong influence on otherresearch systems, such as Barrelfish [Baumann et al.,2009].In this paper we examine the development of L4 overthe last 20 Years . Specifically we look at what makesmodern L4 kernels tick, how this relates to Liedtke soriginal design and implementation, and which of hismicrokernel essentials have passed the test of specifically examine how the lessons of the past haveinfluenced the design of the latest generation of L4 mi-crokernels, exemplified byseL4[Klein et al.]

5 , 2009], butpoint out where other current L4 versions have made dif-ferent design The L4 Microkernel FamilyL4 developed out of an earlier system, called L3, de-veloped by Liedtke [1993b] in the early 1980s on i386platforms. L3 was a complete OS with built-in persis-tence, and it already featured user-mode drivers, still a13393 94 95 96 97 98 99 00 01 02 03 04 05 06 07 08 09 10 11 12 13 L3 L4 X Hazelnut Pistachio L4/Alpha L4/MIPS seL4 OKL4 Kernel OKL4 Microvisor Codezero P4 PikeOS Fiasco L4-embed. NOVA GMD/IBM/Karlsruhe UNSW/NICTA Dresden Commercial Clone OK Labs Figure 1: The L4 family tree (simplified). Black arrows indicate code, green arrows ABI inheritance. Boxcolours indicate origin as per key at the bottom of L4 microkernels .

6 It was commerciallydeployed in a few thousand installations (mainly schoolsand legal practices). Like all microkernels at the time,L3 suffered from IPC costs of the order of 100 initially used L3 to try out new ideas, andwhat he referred to as L3 in early publications[Liedtke, 1993a] was actually an interim version of aradical re-design. He first used the name L4 with the V2 ABI circulated in the community from the following we refer to this version as the orig-inal L4 . Liedtke implemented it completely in assem-bler on i486-based PCs and soon ported it to the initial work triggered a twenty- year evolution,with multiple ABI revisions and from-scratch imple-mentations, as depicted in Figure 1.

7 It started withTU Dresden and UNSW re-implementing the ABI (withnecessary adaptations) on 64-bit Alpha and MIPS pro-cessors, the latter implemented all longer-running oper-ations in C. Both kernels achieved sub-microsecond IPCperformance [Liedtke et al., 1997a] and were releasedas open source. The UNSW Alpha kernel was the firstmultiprocessor version of , who had moved from GMD to IBM Wat-son, kept experimenting with the ABI in what be-came known asVersion X. GMD and IBM imposedan IP regime which proved too restrictive for other re-searchers, prompting Dresden to implement a new x86version from scratch, calledFiascoin reference to theirexperience in trying to deal with IP issues. The open-source Fiasco was the first L4 version written almostcompletely in a higher-level language (C++) and is theoldest L4 codebase still actively maintained.

8 It was thefirst L4 kernel with significant commercial use (esti-mated shipments up to 100,000).After Liedtke s move to Karlsruhe, he and his stu-dents did their own from-scratch implementation (inC),Hazelnut, which was the first L4 kernel that wasported (rather than re-implemented) to another architec-ture (from Pentium to ARM).Karlsruhe s experience with Version X and Hazelnutresulted in a major ABI revision, V4, aimed at improv-ing kernel and application portability, multi-processorsupport and addressing various other shortcomings. Af-ter Liedtke s tragic death in 2001, his students im-plemented the design in a new open-source kernel,L4Ka::Pistachio( Pistachio for short). It was writ-ten in C++, originally on x86 and PowerPC, and atUNSW/NICTA we soon after ported it to MIPS, Alpha,64-bit PowerPC and most of these ports, lessthan 10% of the code NICTA we soon re-targeted Pistachio for usein resource-constrained embedded systems, resultingin a fork calledNICTA::Pistachio-embedded( L4-embedded ).

9 It saw massive-scale commercially deploy-ment when Qualcomm adopted it as a protected-modereal-time OS for the firmware of their wireless modemprocessors. The NICTA spinout Open Kernel Labs tookon the support and further development of the kernel, re-1 There were also Itanium [Gray et al., 2005] and SPARC versions,but they were never 41,4002, 21, i7 (Bloomfield) 32-bit2, i7 4770 (Haswell) 32-bit3, A91, 1: One-way IPC cost of various L4 theOKL4 deployed ver-sion is PikeOS, a commercial V2 clone by Sysgo, cer-tified for use in safety-critical avionics and deployed inaircraft and influence of EROS [Shapiro et al., 1999] and in-creasing security focus resulted in a move to capabil-ities [Dennis and Van Horn, 1966] for access control,first with the release of OKL4 (2008) and soon fol-lowed by Fiasco ( ).

10 Aiming for for-mal verification, which seemed infeasible for a codebase not designed for the purpose, we instead opted fora from-scratch implementation for our last few Years also saw two new designs specifi-cally aimed to support virtualization as the primary con-cern,NOVA[Steinberg and Kauer, 2010] from Dresdenand theOKL4 Microvisor[Heiser and Leslie, 2010] fromOK common thread throughout those two decades istheminimality principleintroduced in Section , and astrong focus on the performance of the critical IPC op-eration; kernel implementors generally aim to stay closeto the limits set by the micro-architecture, as shown inTable 1. Consequently, the L4 community tends to mea-sure IPC latencies in cycles rather than microseconds,as this better relates to the hardware limits.