A history of microkernels

Most operating systems people use are monolithic. The kernel is a single large program running with full authority over the hardware, containing the scheduler, the memory manager, the file systems, the network stack, and the device drivers all in one address space. Linux is monolithic. So was classic Unix, and so is Windows in most respects that matter.

The microkernel is the alternative that has been proposed, abandoned, and revived roughly once per decade for over fifty years. The idea is to strip the kernel down to almost nothing — address spaces, threads, and a way for processes to talk to each other — and run everything else as ordinary user-level programs. A file system becomes a server. A disk driver becomes a process. If it crashes, it crashes alone.

This is the story of how that idea developed, why it kept failing, and what changed.

1969–1980: the nucleus

The first statement of the concept came from Per Brinch Hansen, working on the RC 4000 at Regnecentralen in Denmark. His 1969 system had what he called a nucleus, which deliberately implemented no policy at all. It provided a mechanism for processes to exchange messages and nothing more. Scheduling policy, resource allocation, and anything resembling an operating system were left to processes running above it. Brinch Hansen's 1970 paper describing it is the origin document for the whole tradition.

Through the 1970s, Carnegie Mellon's Hydra project on the C.mmp multiprocessor added the other half of the modern picture: capability-based protection. Rather than the kernel consulting a global table to decide whether a process may touch an object, the process holds an unforgeable token granting that specific right. Hydra also drew a hard line between mechanism and policy. Both ideas were absorbed into everything that followed.

The term "microkernel" itself did not come into common use until the late 1980s. The early systems were just called kernels or nuclei.

1980–1990: the first generation

The 1980s produced the first substantial crop of message-passing systems, and they came from quite different worlds.

Thoth and its descendants. David Cheriton's Thoth at the University of Waterloo (late 1970s) was a portable message-passing system that seeded two lineages. Cheriton took the ideas to Stanford and built the V System. Separately, Waterloo alumni Gordon Bell and Dan Dodge founded Quantum Software Systems and shipped QNX in 1982, a commercial real-time microkernel that is still in production more than forty years later. Canada's National Research Council also built Harmony, a real-time multiprocessor system from the same family, which is why "Harmony" occasionally causes confusion in this history.

Amoeba. Andrew Tanenbaum's group at the Vrije Universiteit in Amsterdam built Amoeba from around 1981 as a distributed system: a pool of processors presented to the user as a single machine, with capabilities used to name and protect objects across the network.

Chorus. Started at INRIA in France in 1979, later commercialised by Chorus Systèmes, and eventually acquired by Sun. Chorus was designed for distributed and real-time use and ended up in telecoms equipment.

Mach. The most consequential of the group, developed at CMU from 1985 under Rick Rashid and Avie Tevanian, and descended in part from the earlier Accent system. Mach's design goals were multiprocessor support and Unix compatibility, and it was funded heavily by DARPA. Critically, Mach was derived from BSD rather than written from scratch, and early versions still contained the entire BSD kernel inside the kernel address space. Only Mach 3.0, around 1990, moved the Unix personality out into user space and became a true microkernel.

MINIX. Tanenbaum wrote MINIX in 1987 as a teaching system to accompany his textbook Operating Systems: Design and Implementation. It was a microkernel with the file system and memory manager as separate processes, small enough that its full source could be printed in a book, and it ran on an 8088 with floppy disks and no hard drive.

AmigaOS. Often left out of academic accounts, but Commodore's AmigaOS (1985) was a message-passing microkernel design that shipped on millions of consumer machines and had better interactive response than anything else on a personal computer at the time. It achieved this by omitting memory protection entirely, which is a large asterisk, but it demonstrated that message passing need not be slow.

1988–1994: adoption, and the performance problem

For a few years it looked like the microkernel had won on the merits.

The Open Software Foundation chose Mach 3.0 as the base for OSF/1. Unix System Laboratories bet on Chorus. IBM planned the Workplace OS around Mach. NeXT built NeXTSTEP on Mach 2.5. The Free Software Foundation chose Mach as the base for the GNU Hurd, a multi-server Unix built from independent servers. Rashid published performance figures arguing that microkernel systems could match monolithic ones.

Then the measurements came in from everyone else.

Mach's IPC was slow, on the order of hundreds of microseconds, and its cache footprint was punishing. Every attempt to run a full Unix personality on top of Mach 3.0 produced something noticeably slower than the monolithic kernel it had replaced, and the overhead showed up worst in exactly the workloads that mattered commercially: network traffic and file I/O, where each operation crossed protection boundaries multiple times.

The consequences were structural. NeXTSTEP never moved to Mach 3.0's split design, and its descendant XNU — the kernel in macOS and iOS today — keeps Mach and BSD together in kernel space, making it a hybrid rather than a microkernel. Windows NT, designed in the same period with an executive layer that looks microkernel-shaped, moved the graphics subsystem into kernel mode in NT 4.0 for performance. IBM's Workplace OS was cancelled. The Hurd never reached production.

By the mid-1990s the field's working consensus was that the microkernel was architecturally correct and practically unaffordable.

1992: the Tanenbaum–Torvalds debate

The best-known artefact of this period is a Usenet argument that ran in comp.os.minix between late January and mid-February 1992.

Tanenbaum opened on 29 January under the subject "LINUX is obsolete," arguing that among people who design operating systems the microkernel debate was essentially settled, that writing a monolithic kernel in 1991 was a giant step back into the 1970s, and that tying a kernel to the 386 was a mistake because RISC would displace x86.

Torvalds replied the same day. He conceded the architectural point immediately — microkernels are nicer, and on theoretical grounds Linux loses — but argued that MINIX did not implement the concept well, and that a portable API mattered more than a portable implementation. Tanenbaum's rejoinder included the line about Torvalds being lucky not to be his student.

The thread is more interesting for its other participants. Ted Ts'o raised the context-switch and copying costs in OSF/1 Mach that were already sinking it commercially. Ken Thompson posted a brief note saying microkernels were probably the future but monolithic kernels were easier to build and easier to turn into a mess. Peter da Silva pointed out that AmigaOS had been shipping a message-passing design on three million machines while everyone argued about research systems. Several people questioned whether MINIX was really a microkernel in the sense Mach was.

The debate settled nothing technically. Its lasting significance is as a snapshot of what the field believed in 1992, and for the argument it drifted into later about whether distributed development without a single controlling architect could work.

1993–2000: the second generation

Jochen Liedtke at GMD in Germany rejected the conclusion that microkernels were inherently slow. His position was that Mach's overhead was an implementation artefact, and he demonstrated it empirically.

L3 (1993) and then L4 (1995) were written largely in hand-tuned assembly, with the design driven by cache behaviour rather than abstraction. L4's IPC was roughly ten to twenty times faster than Mach's. Liedtke's 1995 SOSP paper "On µ-kernel construction" supplied the field with its governing principle: a concept belongs inside the kernel only if moving it outside would prevent the implementation of required system functionality. Not if it is faster inside, not if it is convenient. Only if the system otherwise cannot work.

L4 became a family rather than a product. Fiasco was developed at TU Dresden, along with L4Linux, which ran a paravirtualised Linux kernel as a user-level server and demonstrated single-digit percentage overhead. L4Ka::Pistachio came from Karlsruhe, where Liedtke had moved. Hermann Härtig's group published the 1997 SOSP paper "The performance of µ-kernel-based systems," which put numbers behind the claim that the second generation had fixed the problem.

Liedtke died in 2001. His students carried the work forward, and one commercial descendant, OKL4 from Open Kernel Labs, went on to ship in billions of mobile phone basebands and Qualcomm modems — meaning that for much of the 2000s, most people carrying a phone were carrying a microkernel without knowing it.

Meanwhile the first generation persisted in places that valued isolation over benchmarks. QNX moved into automotive and industrial control. Green Hills shipped INTEGRITY for avionics. SYSGO shipped PikeOS for certified safety-critical use. These systems were never fashionable and never went away.

2000–2015: capabilities and proofs

The third generation of microkernels is distinguished by capability-based access control done properly, and by an ambition that would have seemed absurd earlier: proving the kernel correct.

Gernot Heiser, who had collaborated with Liedtke, moved to UNSW Sydney and later NICTA, where the group became Trustworthy Systems. Around 2004 they began asking whether an L4-style kernel could be made small enough to formally verify. The reasoning followed directly from Liedtke's minimality principle. The point of a microkernel is a tiny trusted computing base, and a tiny base is one you might actually be able to prove things about.

seL4 was a redesign rather than a verification of an existing kernel. Its central change was that the kernel never allocates memory dynamically: all kernel memory is explicitly accounted for through capabilities held at user level, which removes an entire class of behaviour that would otherwise be intractable to reason about.

In 2009, Gerwin Klein and colleagues published the functional correctness proof at SOSP — a machine-checked Isabelle/HOL proof that roughly 8,700 lines of C conformed to an abstract specification. Later work extended this to the compiled binary, removing the C compiler from the trusted base, and added proofs of integrity and confidentiality plus sound worst-case execution time analysis. NICTA released the sources and the proofs as open source in July 2014.

Tanenbaum, meanwhile, had returned to the subject from a different direction. MINIX 3, released in 2005, abandoned the teaching mission for a reliability one: drivers run as isolated user processes, and a reincarnation server detects a crashed driver and restarts it without taking down the system. MINIX 3 later acquired an unexpected distinction when researchers established that a version of it runs inside the Intel Management Engine on essentially every modern Intel chipset, arguably making it the most widely deployed operating system in the world.

Other third-generation work from this period includes NOVA, a capability-based hypervisor microkernel from Dresden, and the Barrelfish multikernel from ETH Zurich and Microsoft Research.

2015–present: back in production

Three things happened more or less at once.

seL4 moved from research to deployment. DARPA's HACMS program provided the public demonstration: a Boeing Unmanned Little Bird running seL4-based software resisted a red team that had been given root access on a non-critical partition and still could not reach the flight controls. The seL4 Foundation launched on 7 April 2020 under the Linux Foundation, and is now becoming an independent Swiss association. Verification has continued, with the AArch64 port recently gaining a proof of confidentiality enforcement on top of functional correctness and integrity.

Google built Fuchsia. Its Zircon kernel is a capability-based microkernel descended from the LK embedded kernel, and Fuchsia shipped commercially on the Nest Hub in 2021, though its longer-term role at Google has never been entirely clear.

Huawei put one under a phone. Work on the HongMeng kernel began around 2016 or 2017 and became urgent after the May 2019 Entity List placement threatened Android access. Early HarmonyOS versions were marketed as microkernel-based but ran a Linux kernel with AOSP compatibility layers on phones, with the actual microkernel confined to watches, IoT devices, and trusted execution environments — a gap that Heiser among others criticised publicly.

HarmonyOS NEXT closed it. Announced in August 2023 and released in October 2024 as HarmonyOS 5, it drops the AOSP layer entirely, cannot run Android APKs, and runs on the HongMeng microkernel over OpenHarmony. Huawei's OSDI 2024 paper describes HongMeng as a capability-based multi-server microkernel engineered for general-purpose performance and Linux ABI compatibility. All new Huawei devices in China now ship it. It is the first serious attempt to put a microkernel under a mass-market consumer smartphone, and its results will matter regardless of how they turn out.

Where things stand

The microkernel never won the general-purpose desktop or server market and shows no sign of doing so. Linux is monolithic and dominant. But the design has quietly become the default in the places where isolation is worth paying for: avionics, automotive, industrial control, secure separation kernels, phone basebands, and hardware security modules. Loadable kernel modules, which Linux adopted in 1995, absorbed enough of the modularity argument to remove the pressure elsewhere.

The more interesting shift is in what the argument is about. In 1992 it was performance and portability. Liedtke settled the performance question by 1997. What replaced it is assurance: how small can the part of the system you have to trust be made, and can you prove anything about it. That is a question a monolithic kernel cannot even ask, and it is the reason the idea is still alive fifty-five years after Brinch Hansen described it.

---

Further reading. Brinch Hansen's "The nucleus of a multiprogramming system" (CACM, 1970). Liedtke's "On µ-kernel construction" (SOSP, 1995). Klein et al., "seL4: Formal verification of an OS kernel" (SOSP, 2009). The 1992 Usenet thread is reprinted as Appendix A of Open Sources: Voices from the Open Source Revolution (O'Reilly, 1999).