the history of microkernels

 

Microkernels: the idea and the first generation

The core idea goes back to Per Brinch Hansen's RC 4000 "nucleus" (1969): the kernel should provide only a mechanism for processes to communicate, and everything else — file systems, drivers, network stacks — should live in ordinary user processes. Carnegie Mellon's Hydra (1970s) added capability-based protection.

The 1980s produced the first real generation. Mach (CMU, from 1985, led by Rick Rashid and Avie Tevanian) was the most influential; it was BSD-derived and became the base for NeXTSTEP and later XNU in macOS/iOS, plus the OSF/1 and GNU Hurd efforts. Alongside it: Chorus in France, Amoeba (Tanenbaum, distributed), QNX (1982, commercial and real-time, descended from Waterloo's Thoth), and MINIX (Tanenbaum, 1987), which set off the famous 1992 Usenet argument with Linus Torvalds over monolithic versus microkernel design.

Mach also gave microkernels a bad reputation. It was slow — IPC cost hundreds of microseconds, and cache footprint was terrible. By the mid-90s the consensus was that the design was elegant but impractical.

Second generation: L4

Jochen Liedtke at GMD in Germany disagreed, and argued the problem was implementation, not concept. His L3 kernel (1993) and then L4 (1995), hand-written in assembly, achieved IPC roughly 10–20× faster than Mach. His 1995 SOSP paper "On µ-kernel construction" laid out the minimality principle: a feature belongs in the kernel only if moving it out would prevent the system from meeting a functional requirement.

L4 spawned a family — Fiasco (Dresden), L4Ka::Pistachio (Karlsruhe), Pistachio-derived OKL4 from Open Kernel Labs, which shipped in billions of phone basebands and Qualcomm modems. Liedtke died in 2001; his students carried the work forward.

seL4

Gernot Heiser, one of Liedtke's collaborators, moved to UNSW Sydney and later NICTA (now CSIRO's Data61, with the team called Trustworthy Systems). Around 2004 they started asking whether an L4-style kernel could be small enough to formally prove correct — the argument being that the whole point of a microkernel is a tiny trusted computing base, and a tiny TCB is one you can actually verify.

seL4 was a redesign, not just a verification of existing L4. It replaced ad-hoc memory management with a capability system in which all kernel memory is explicitly accounted for by user level, so the kernel never allocates dynamically. In 2009, Gerwin Klein and colleagues published the functional correctness proof at SOSP: a machine-checked Isabelle/HOL proof that ~8,700 lines of C matched its abstract specification. Later work added binary-level proofs (removing the compiler from the trusted base), plus integrity, confidentiality, and worst-case execution time analysis.

The sources and proofs were released as open source by NICTA in July 2014, and the seL4 Foundation was launched on 7 April 2020 for governance and stewardship, initially hosted under the Linux Foundation. DARPA's HACMS program gave it a public demonstration when a Boeing Unmanned Little Bird running seL4-based software resisted a red team that had root on a non-critical partition. Verification continues: the AArch64 port recently gained a proof of confidentiality enforcement, after functional correctness and integrity, showing that an application on top of seL4 cannot learn information without authorisation. The Foundation is now moving out of the Linux Foundation to become its own Swiss association. Wikipedia + 3

HarmonyOS

Huawei began work on what became the HongMeng kernel around 2016–17, and the project got urgent after the U.S. Entity List placement in May 2019 threatened Android access. HarmonyOS launched in 2019 and was described from the start as microkernel-based with Android app support, reaching phones and tablets with version 2.0 in 2021. AppInChina

The microkernel claim was contested for years, and fairly: HarmonyOS 1.x–4.x on phones ran a Linux kernel with AOSP compatibility layers, and the microkernel ("LiteOS-M"/HongMeng) shipped mainly on watches, IoT devices, and TEE contexts. Gernot Heiser and others publicly criticised the marketing. The open-source portion, OpenHarmony, was donated to the OpenAtom Foundation in 2020.

That changed with HarmonyOS NEXT, announced at HDC on 4 August 2023 and released in October 2024, which drops the AOSP layer entirely and cannot run APKs. Shipped as HarmonyOS 5, it uses the HongMeng microkernel and is based on OpenHarmony rather than AOSP. Huawei published a technical paper at OSDI 2024 describing HongMeng as a capability-based multi-server microkernel engineered for general-purpose performance and Linux ABI compatibility — the first serious attempt to put a microkernel under a mass-market consumer phone. All new Huawei devices in China now ship it, with international expansion targeted for 2026, and HarmonyOS 6 is the current line. Wikipedia + 4

The lineage connection to seL4 is intellectual rather than direct: HongMeng borrows the capability model and formal-verification ambitions that seL4 established, and Huawei's formal methods teams cite that literature, but it's a separate codebase and its verification claims cover components rather than the whole kernel to seL4's standard.

One footnote on naming: there was an earlier, unrelated Harmony — a real-time multiprocessor operating system built at Canada's National Research Council in the 1980s, descended from the same Thoth family that produced QNX and the V system. If that's the Harmony you meant rather than Huawei's, say so and I'll go into it.

The thread ran in comp.os.minix from late January to mid-February 1992, and it's worth reading because almost nobody in it argued the way the legend says they did.

The opening shot

Tanenbaum posted on 29 January 1992 under the subject line "LINUX is obsolete." His argument had two prongs. First, architecture: he laid out the monolithic-versus-microkernel distinction, listed RC4000, Amoeba, Chorus, Mach and the unreleased Windows NT as microkernel examples, and declared that among people who actually design operating systems the debate was essentially over and microkernels had won — citing Rick Rashid's Mach 3.0 performance papers as evidence that the old performance objection was dead. Writing a monolithic kernel in 1991 was "a giant step back into the 1970s", he said, comparing it to rewriting a working C program in BASIC. O'ReillyWikipedia

Second, portability. He predicted RISC chips would displace the x86 line, so tying a kernel to the 386 was a mistake. MINIX had been ported to 68000, SPARC and NS32016; Linux hadn't been ported anywhere. He closed by suggesting people wanting a modern free OS wait for something microkernel-based, "like maybe GNU."

Torvalds' reply

Torvalds answered the same day, and the reply is nastier than people remember. He went at the "MINIX is my hobby" framing first: Tanenbaum made money from MINIX while Linux was given away free. On the professor line, he said being a professor and researcher was an excellent excuse for MINIX's brain damage. He conceded the architecture point immediately — microkernels are nicer, and on theoretical and aesthetic grounds Linux loses — but argued MINIX didn't actually do the microkernel thing well, pointing to its single-threaded file system and lack of real kernel multitasking, and noting that much of the good 386 code in MINIX had come from Bruce Evans anyway.

On portability he made the distinction that mattered: the Linux API was portable because it followed Unix and POSIX, while the implementation was 386-specific by choice. He also pointed out that the entire Linux kernel source was smaller than just the i386-dependent portion of Mach.

Tanenbaum's rejoinder defended MINIX's constraints as pedagogical (it had to run on a diskless 4.77 MHz PC), dismissed multithreaded file systems as a performance hack, and delivered the famous jab that Torvalds should be thankful he wasn't his student, because the design wouldn't earn a high grade. He extended the grading metaphor: a second F for the term, with a chance to pass on the final.

Torvalds posted an apology the next day, admitting he'd replied with no thought for netiquette and signing off as a hothead in his first and hopefully last flamefest.

The parts people forget

The thread's most interesting content came from third parties, and the technical objections to Tanenbaum were sharper than Torvalds'.

Ted Ts'o cited Brent Welch's argument that the file system is a mature enough abstraction to belong in the kernel, and raised context-switch and copying costs in OSF/1 Mach for network traffic — the exact problem that would later sink Mach commercially. Lawrence Foard complained that OS theorists never tested their ideas; Tanenbaum replied that he was mortally insulted and not a theorist, and pointed at OSF, Chorus at USL, Amoeba, and QNX's 200,000 installed systems. Peter da Silva defended microkernels from an entirely different direction — AmigaOS was a message-passing microkernel design shipping on three million machines and beating everything else on the PC for response time.

Ken Thompson posted a short, characteristically dry note: microkernels were probably the future, but a monolithic kernel is easier to implement — and easier to turn into a mess as it's modified. Several people, including David Megginson and Douglas Graham, questioned whether MINIX was really a microkernel at all in the sense Mach was.

Tanenbaum then broadened it with a second post, "Unhappy campers," which is where the debate stopped being about kernels. He identified three sticking points, the third being whether software ought to be free, defended MINIX's $169 price, and questioned whether Torvalds would ever let Linux out of his control. Torvalds' answer was two words: he wouldn't. He'd already floated the idea of a kernel mailing list to make release decisions, and the only thing his copyright forbade was selling it without source. Tanenbaum invoked Harlan Mills' surgical-team model and said a widely dispersed group hacking on complicated code without one person in charge means anarchy. That exchange, more than the microkernel argument, is what the thread ended up testing over the next thirty years.

About Bill Jolitz

I want to be straight with you: I can't find Jolitz in the "LINUX is obsolete" thread. The canonical archive of the debate — the one reprinted as Appendix A of Open Sources (1999) — has posts from Tanenbaum, Torvalds, Ken Thompson, Ted Ts'o, Peter MacDonald, David Miller, Kevin Brown, Lawrence Foard, Richard Tobin, Charles Hedrick, peter da silva and a dozen others, but no Jolitz. That archive isn't necessarily the complete thread, so I can't rule it out entirely, but he wasn't one of the notable voices in it.

What you may be thinking of is that Jolitz's famous 1992 Usenet post came seven weeks later and was about something else entirely. On 19 March 1992 he posted "The Road Not Taken" to comp.unix.bsd, a bitter account of his split from Berkeley Software Design after leaving in December 1991 — his position being that BSDI intended to sell what should have been free, and that CSRG had unilaterally cut Berkeley's involvement in 386BSD and claimed his post-Net/2 work as university property. Rob Kolstad and Mike Karels of BSDI both posted rebuttals disputing his account of events. He also posted "386BSD, a guided tour" in late April.

386BSD is nonetheless directly relevant to the debate, in two ways. It was the free BSD that half the posters in the Tanenbaum thread were waiting for — Charles Hedrick and Richard Tobin both said they'd jump ship the moment a free BSD or GNU appeared. And 386BSD 0.0 shipped on 12 March 1992, six weeks after Tanenbaum's post, taking the wind out of the "there is no alternative" argument Torvalds had leaned on. Torvalds himself said in later years that if 386BSD had existed when he started, he probably wouldn't have bothered writing Linux.

Architecturally, Jolitz sat in neither camp. 386BSD was a monolithic BSD kernel, but its stated innovations included a modular, loadable kernel design and role-based security — the loadable-module middle path that Linux itself adopted in 1995 and that made the pure monolithic-versus-microkernel framing obsolete in practice. His writing on kernel design ran in Dr. Dobb's Journal from January 1991 to July 1992 as the "Porting UNIX to the 386" series, which Torvalds has said he was reading while starting Linux.

If you have a specific Jolitz quote in mind, or you meant Lynne Jolitz — she wrote frequently on this history afterward