Anil Madhavapeddy on MirageOS and the Evolution of Operating Systems

Ron Minsky welcomes Anil Madhavapeddy, a systems researcher, engineer and longtime collaborator with whom he and Jason Hickey wrote Real World OCaml. They begin with MirageOS, a project Madhavapeddy developed while exploring safer ways to build internet infrastructure.

Madhavapeddy recalls the early 2000s, when internet worms exploited buffer overflows and other memory errors in systems largely written in C. As a Cambridge graduate student, he wanted to rewrite common internet protocols in a high-level language while retaining the practical characteristics of Unix programming.

He chose OCaml for native compilation, easy debugging and a thin interface to the operating system. He rewrote DNS and SSH in OCaml and found that they could perform comparably to C implementations while allowing high-level reasoning with model checking and early verification techniques.

But the compiler still produced an application that depended on a much larger operating system. Madhavapeddy asks why an application carefully built in a safe language should need to bring along the millions of lines of C in a general-purpose kernel.

MirageOS extends compilation to operating-system components. Application logic and configuration are combined with OCaml libraries for networking, storage and drivers to produce a specialized bootable system: a unikernel. It is built for the particular application rather than including every service of a general-purpose OS.

The project grew from a research experiment into a community with many protocol and filesystem implementations. Minsky calls the idea an operating system as a library, then asks what an operating system actually does.

Madhavapeddy explains that a conventional kernel mediates access to hardware and gives processes isolated access to resources. A library OS instead supplies system functionality as linked libraries. This makes sense for a specialized application with exclusive access to its environment, but a conventional OS remains better suited to a desktop running many mutually untrusted applications.

Minsky places MirageOS in a broader shift away from the original multi-user OS ideal. Virtual machines and containers often bundle and reproduce the entire software stack for an application, rather than simply sharing a single operating system among users. Once the environment changes that much, he asks, why keep all the original abstractions?

Madhavapeddy sees the change as layers of abstraction evolving with need. Xen began with the goal of running multiple isolated operating-system instances on one physical machine with little overhead, without requiring applications such as databases to be rewritten.

Xen used paravirtualization: parts of the guest kernel were adapted to work with a hypervisor that mediated access to real hardware. Multiple operating-system stacks could then share a physical server, consolidating machines that were individually underused. In this view, the user became the person booting an entire operating system.

Xen itself began as a Cambridge pub bet that Keir Fraser could not modify Linux over a weekend. The resulting prototype became a larger project; Madhavapeddy later worked at XenSource on making it a product, including Windows and Linux drivers and the many compatibility edge cases.

To test Xen without the baggage of full Windows or Linux installations, the team built a minimal operating system that exercised low-level facilities. Madhavapeddy and Thomas Gazagnaire linked in the OCaml runtime for more complex tests, then added TCP/IP and HTTP libraries. MirageOS grew organically from those experiments.

Madhavapeddy argues that a stunt can test a research hypothesis before the hard work of productizing it. He says MirageOS libraries subsequently reached large numbers of users through infrastructure, although they often run invisibly as part of other systems.

Minsky asks whether the abstractions created through these historical accidents are the right ones. Madhavapeddy says the Mirage team never considers its interfaces finished. OCaml's module signatures describe types and operations, while separate implementations satisfy those signatures, enabling interfaces and implementations to evolve.

For example, a Mirage networking interface called a flow can be implemented using a Linux socket or a pure OCaml TCP/IP stack. The application can use the same interface while choosing a different backend. As hardware, security models and distributed-system requirements change, the team can revise interfaces and adapt implementations incrementally.

Minsky emphasizes that a Mirage program need not always run as a standalone kernel: it can also use an ordinary host operating system. The same abstractions let an application be deployed in multiple environments, from a conventional Unix process to a specialized target.

Madhavapeddy gives a solar-powered website as an example. The team first developed a web server on Raspberry Pi using ordinary OCaml and Linux, then measured its energy use. By moving toward a constrained Mirage interface requiring fewer operating-system services, the application could target smaller devices such as an ESP32 with a lower energy budget and fewer capabilities.

He says this iterative approach also removes some mystique from kernel development: a programmer can write OCaml and produce a custom bootable kernel. Minsky values the ability to use rich language abstractions and omit unneeded components, producing a smaller system and potentially reducing its attack surface.

Minsky notes that most programmers depend on their language tools without much ability to change them. Working with a language community can make it possible to improve those foundations. Madhavapeddy wants systems that can last, and contrasts continually refreshed systems with the ambition to build durable ones with well-understood properties.

Minsky asks about a clear drawback: if everything must be written in OCaml, how can a system use the broader world of software? Madhavapeddy agrees that multiple languages are necessary. He values stable semantics and the ability to compile old OCaml code, and points to foreign interfaces and emerging WebAssembly interoperability as ways to connect languages.

Minsky cautions that interoperability can undermine simplicity when languages must accommodate one another's complexity. Madhavapeddy agrees that end-to-end guarantees require care. In work on Tezos unikernels, for example, OCaml's garbage-collected model and Rust's lifetime-oriented model have to be layered and connected deliberately; this is not a magic build-system switch.

Docker for Mac and Windows provides another Mirage use. Madhavapeddy describes translation layers that connect Linux containers to host filesystem and networking services. By translating traffic into ordinary host calls, the system can avoid some of the friction of bridging networks through enterprise firewall and antivirus configurations.

He says support calls fell sharply after deployment, but emphasizes the engineering required to make Go and OCaml values interoperate safely. Minsky sees this as another example of Mirage's flexibility: its components can form a shim between operating systems rather than only a complete bare-metal kernel.

Madhavapeddy recounts how developers wrote an OCaml TLS stack after Heartbleed and created a Bitcoin piñata: a public unikernel holding private keys, with the reward available to anyone who could break in. He says it withstood many attacks, restarted quickly after denial-of-service crashes, and the Bitcoin was eventually donated to charity.

Minsky asks about the reach of systems Madhavapeddy worked on. Madhavapeddy points to Xen management infrastructure and Docker's desktop products, while distinguishing those installations from OCaml-derived code compiled to JavaScript for web applications. He also describes plans to use Mirage in climate-sensing devices and secure network infrastructure.

Asked how he entered computing, Madhavapeddy says he trained as an engineer and originally expected to work in electrical engineering. A programmable online MUD led to a party and, unexpectedly, an internship associated with NASA's Mars Polar Lander project.

He helped set up infrastructure for the anticipated public interest in the landing. After the initial Solaris machines were compromised, he switched to OpenBSD, found bugs while operating it, and contributed patches. Having those patches accepted drew him further into open-source systems work.

The lander was lost, and Madhavapeddy returned to Cambridge for a PhD. There he worked on Xen and used OCaml more seriously for the protocol stacks he described. Open-source code became a portable set of tools he could carry among academic, industrial and government projects.

Cambridge taught ML-family languages and exposed students to OCaml as a way to learn data structures, recursion and foundations. Madhavapeddy also found it practical for Unix systems work in the early 2000s. As a body of reusable code accumulated, extending it became increasingly attractive compared with rewriting everything in another language.

Minsky challenges the claim that OCaml was the obvious systems language when C dominated the field. Madhavapeddy agrees and says he wishes he had promoted OCaml earlier. Around 2005 progress slowed and limited tooling made adoption difficult, even within XenSource.

After XenSource was acquired by Citrix, Madhavapeddy returned to academia with funding and the ambition to build MirageOS. He also saw that the OCaml compiler team needed help with bug reports, tooling and maintenance. Improving the language ecosystem would directly support Mirage, so he helped establish OCaml Labs at Cambridge.

Cambridge's intellectual-property arrangements made it easier for staff to release open-source code. Minsky credits the university for supporting difficult coordination and maintenance work that does not always resemble conventional academic research or directly lead to tenure.

Minsky describes OCaml Labs as connective tissue across projects: Merlin, OCamlFormat and Dune originated in different places, but collaboration helped turn them into shared, maintained tools. Madhavapeddy adds that universities train people who then move into other organizations, keeping knowledge and contributors flowing through the ecosystem.

They turn to multicore OCaml. At the time of the conversation, running multiple OCaml threads in parallel on a shared heap was a long-standing goal. Minsky asks why it has taken so long; Madhavapeddy says extending an existing language while preserving its semantics exposes an extraordinary number of edge cases.

An early plan in 2013 proved too optimistic. Industrial users later pressed the team to define a memory model explaining what happens when concurrent threads access the same value. The resulting research on local data-race freedom gave the multicore design a clearer semantic foundation.

The garbage collector was another major challenge: multiple cores may trigger collection, and type safety must hold throughout. The team compared alternative designs while protecting existing single-core code from substantial slowdowns. Madhavapeddy says an initial 10–20% performance penalty was reduced to a few percent over years of work.

The team incrementally upstreamed pieces across OCaml releases rather than creating an incompatible fork. Madhavapeddy's goal for the future OCaml 5.0 release was that nearly all existing code would compile with little performance loss, while domains would provide shared-heap parallelism.

Minsky asks what working programmers would gain compared with Java. Madhavapeddy hopes for a less surprising memory model and familiar high-level parallel libraries. He notes that language semantics are difficult to retract once programs depend on them, so the team studied earlier designs before choosing its model.

On data races, Madhavapeddy contrasts C++ undefined behavior with the guarantees he describes for OCaml: a race has consequences, but their effects are bounded in space and time rather than spreading arbitrarily through the program. Minsky observes that making buggy code easier to reason about is valuable because real codebases contain bugs.

Asked for a date, Madhavapeddy says an experimental domains-enabled compiler is already available through opam alongside the stable compiler. Developers can try existing projects and report bugs. He also describes a more experimental branch with effect handlers for managing operations such as blocking I/O.

The 2021 roadmap he outlines aims for domains in OCaml 5.0, followed by runtime support for effects and eventually language-level effect handlers. He presents this as a multiyear plan, not a fixed release schedule, and asks users to test the open-source branches.

Minsky distinguishes parallel domains, roughly associated with physical cores, from many lightweight concurrent tasks within them. Madhavapeddy calls those tasks fibers: effect handlers allow scheduling logic to be written in OCaml, potentially letting applications choose policies suited to their own workloads.

He connects the work back to MirageOS. An experimental direct-style I/O stack, Eio, uses effect handlers and platform facilities such as Linux io_uring, Apple's Grand Central Dispatch and Windows IOCP behind ordinary-looking OCaml code. He presents its performance comparisons as observations about the work at that time.

Minsky closes by noting the connection between MirageOS and the newest OCaml work. Madhavapeddy's account brings the conversation back to the same theme: moving system abstractions into reusable, programmable components while preserving the ability to run practical applications.