Jochen Liedtke and L4

Abstract

Jochen Liedtke (1953–2001), a German mathematician turned operating-system designer, showed in 1993 that microkernels did not have to be slow. At the time, sending a short message between processes on a microkernel such as Mach took about 100 microseconds on a 50 MHz processor, and designers were moving services back into the kernel to avoid it. Liedtke’s kernel did it in 5 microseconds, twenty times faster, by designing everything around that one operation. The approach became L4, a kernel of a few kilobytes with a short list of mechanisms and the rule that nothing belongs in the kernel that could be done outside it. Liedtke died suddenly in 2001, aged 48. His design became a family of kernels: one, deployed mostly in Qualcomm modem firmware, had shipped in more than 1.5 billion mobile devices by 2012, Apple’s Secure Enclave runs a customized L4, and seL4, built at NICTA in Sydney, became in 2009 the first operating-system kernel whose implementation was formally proved correct.

Jochen Liedtke. Image: Adelheid Liedtke, CC BY 1.0, via Wikimedia Commons.

Bielefeld and EUMEL

Jochen Liedtke was born on 26 May 1953. He studied mathematics at the University of Bielefeld, and his diploma thesis, completed in 1977, was a compiler for ELAN, a new programming language of the time. ELAN needed a runtime environment on the small Zilog Z80 microcomputers of the time, and Liedtke, who stayed at Bielefeld after his diploma, wrote one. It grew into an operating system, EUMEL.

EUMEL rested on two ideas: persistent processes and data spaces. Every piece of data in the system, including the control blocks of processes and the descriptors of the data spaces themselves, lived in data spaces that could be copied cheaply and atomically by copy-on-write. By copying the “data space of data spaces” every few minutes, the system took a complete snapshot of its own state and wrote it lazily to disk, so that processes survived a restart without the programmer doing anything. Processes communicated only by sending data spaces to each other in synchronous messages, which made a distributed EUMEL easy to build. The paging device, on a cheap computer of the early 1980s, was a floppy disk.

GMD and L3

In 1984 Liedtke moved to the GMD, the German National Research Center for Computer Science at Schloss Birlinghoven near Sankt Augustin, to build a native-code successor to EUMEL for Intel’s 32-bit processors. It was called L3, and it was already a microkernel system: device drivers ran in user mode, as separate processes, a design that remained characteristic of everything Liedtke did afterwards. L3 shipped from 1989; Liedtke’s 1993 paper described it as in daily use at several hundred sites, and his colleagues later put it at about 3,000 installations, most of them in German law practices. Its unusual user and programming interface kept it out of wider use.

The microkernel idea was fashionable in the late 1980s. A small kernel provides only basic mechanisms, address spaces, threads and inter-process communication (IPC), while file systems, network stacks and drivers run as ordinary server processes, isolated from one another, so that a failing driver need not crash the machine. Carnegie Mellon’s Mach was the best-known example (see The macOS Lineage), and Andrew Tanenbaum argued its merits against Linus Torvalds in 1992 (see Andrew Tanenbaum and MINIX). The problem was speed. Every service request became a message to a server and a reply, and in the early 1990s a one-way message on a typical microkernel cost around 100 microseconds, too much to build fast systems on. Vendors and researchers responded by moving drivers and other components back into the kernel; one paper of the period was titled “The Increasing Irrelevance of IPC Performance for Microkernel-Based Operating Systems.” Others argued that slow IPC was an inherent consequence of the microkernel structure.

Improving IPC

Liedtke concluded the opposite. In “Improving IPC by Kernel Design,” presented at the ACM Symposium on Operating Systems Principles (SOSP) in December 1993, he reported a short-message IPC of 5 microseconds on a 50 MHz i486, against the typical 100: about 250 processor cycles. Compared with Mach, the speed-up ranged from a factor of 22 for 8-byte messages to a factor of 3 for 4-kilobyte ones. “There is no single trick to obtaining this high performance,” the abstract said; the gains came from “a synergetic approach in design and implementation on all levels,” guiding the whole design of the kernel by the requirements of IPC.

The techniques were specific. Long messages were copied once, directly from the sender’s to the receiver’s address space, by temporarily mapping the target region into a communication window; the kernel’s data structures were arranged with the processor’s caches and its 32-entry translation lookaside buffer in mind; and Liedtke counted the minimum number of instructions the basic operations needed, twenty, to know how close to the limit he was. It depended on understanding precisely how the processor behaved, down to individual instructions. The 1993 paper described the work on the L3 kernel, which Liedtke was redesigning as he went; he first used the name L4 for the interface version circulated from 1995. The original L4 was written entirely in i486 assembly and soon ported to the Pentium, where by 1997 a one-way message took 121 cycles.

In “On µ-Kernel Construction” (SOSP 1995) Liedtke stated the principle behind the design:

A concept is tolerated inside the µ-kernel only if moving it outside the kernel, i.e. permitting competing implementations, would prevent the implementation of the system’s required functionality.

The 1995 paper also introduced hierarchical external pagers, which let memory management be done by user-level servers that map pages to one another, and argued that the poor performance of earlier microkernels came from their implementations, not from the idea. In 2015 the paper received the ACM SIGOPS Hall of Fame Award. A 1996 article in Communications of the ACM, “Toward Real Microkernels,” carried the argument to a wider audience.

IBM and Dresden

In 1996 Liedtke completed a doctorate at the Technical University of Berlin on guarded page tables, a data structure for sparsely used 64-bit address spaces, and joined IBM’s Thomas J. Watson Research Center in New York, where he continued developing L4 and worked on SawMill, a version of Linux split into multiple servers. He was a frequent visitor to Hermann Härtig’s operating systems group at the Technical University of Dresden, and together they demonstrated L4Linux, a Linux kernel running as a user-level server on L4, at SOSP in 1997. Its overhead compared with native Linux was only a few percent, the measurement that persuaded many researchers that microkernel systems could be practical.

The L4 family tree, from the original L4 through Fiasco, Pistachio, OKL4 and seL4. Image: Wikkiwonkk, CC BY-SA 4.0, via Wikimedia Commons.

Other groups began to reimplement the L4 interface. Dresden and the University of New South Wales built versions for 64-bit Alpha and MIPS processors with sub-microsecond IPC. Because the intellectual-property terms of GMD and IBM proved too restrictive for other researchers, Dresden wrote its own x86 kernel from scratch in 1998, written almost entirely in C++ and named Fiasco after their experience with the licensing issues. It became the oldest L4 code base still maintained.

In April 1999 Liedtke took the chair of system architecture at the University of Karlsruhe (now KIT). His group’s kernel Hazelnut was the first L4 kernel to be ported, rather than rewritten, to a different architecture, from the Pentium to ARM. Students found him an inspiring teacher, and his lectures were among the most popular in the department. On Sunday 10 June 2001, returning from a programme committee meeting for that year’s SOSP, he died unexpectedly at Frankfurt Airport. He was 48. The SOSP 2001 proceedings were dedicated to his memory. His students Volkmar Uhlig, Uwe Dannowski and Espen Skoglund completed the version 4 design he had been working on and released it in 2002 as L4Ka::Pistachio.

Billions of Modems

At NICTA, the Australian research centre in Sydney, Gernot Heiser’s group adapted Pistachio for small embedded systems. In November 2005 NICTA announced that Qualcomm would use its L4 kernel as the protected-mode real-time operating system in the firmware of its mobile-phone modem chips (see Qualcomm). In 2006 Heiser founded Open Kernel Labs to commercialize it as OKL4, and in January 2012 the company announced that its software had shipped in more than 1.5 billion mobile devices, most of them in Qualcomm modems that the phones’ owners never knew existed. A separate commercial clone, PikeOS from Sysgo, was certified for safety-critical avionics and used in aircraft and trains.

Apple’s Secure Enclave, the separate processor in iPhones and Macs that handles keys, biometric data and encryption, runs firmware called sepOS, which Apple describes as “based on an Apple-customised version of the L4 microkernel.” The often repeated claim that L4 runs in “every iPhone’s baseband and Secure Enclave” mixes up two things: the Secure Enclave runs an Apple L4 derivative, while the OKL4 deployments were in Qualcomm modem firmware.

seL4

In 2006 Heiser’s group at NICTA started a new kernel from scratch, designed to be formally verified. seL4 replaced L4’s original access control with capabilities, unforgeable tokens that confer the right to use an object, and its developers wrote a specification of its behaviour in the theorem prover Isabelle/HOL. In 2009 Gerwin Klein and colleagues presented at SOSP a machine-checked proof that the C implementation of seL4 matched its specification, the first complete proof of functional correctness for an operating-system kernel: barring errors in the specification, the compiler and the hardware, the kernel cannot crash or behave other than specified. It was later extended to proofs of security properties and of worst-case execution times. seL4 was released as open source in July 2014, an seL4 Foundation was created under the Linux Foundation in April 2020, and the kernel received the ACM SIGOPS Hall of Fame Award in 2019 and the ACM Software System Award in 2023 (see Secure by Design). DARPA’s HACMS programme on high-assurance cyber-military systems demonstrated it in 2017, and in 2023 the Chinese carmaker Nio announced an seL4-based vehicle operating system for production cars from 2024.

seL4 achieved IPC costs of about 0.1 microseconds on a 2013 Intel processor, about 300 cycles, close to what Liedtke had reached on a 486 twenty years earlier. In a retrospective published in 2013, Kevin Elphinstone and Gernot Heiser concluded that of Liedtke’s principles, the two that had passed the test of time were minimality and high IPC performance: “the fundamental principles of minimality and high IPC performance remain the main drivers of design and implementation decisions.”