MirageOS Papers

What if all the software layers in a virtual appliance were compiled within the same safe, high-level language framework?

This fast-moving tutorial introduces you to OCaml, an industrial-strength programming language designed for expressiveness, safety, and speed. Through the book’s many examples, you’ll quickly learn how OCaml stands out as a tool for writing fast, succinct, and readable systems code. Real World OCaml takes you through the concepts of the language at a brisk pace, and then helps you explore the tools and techniques that make OCaml an effective and practical tool. In the book’s third section, you’ll delve deep into the details of the compiler toolchain and OCaml’s simple and efficient runtime system.

We present <em>unikernels</em>, a new approach to deploying cloud services via applications written in high-level source code. Unikernels are single-purpose appliances that are compile-time specialised into standalone kernels, and sealed against modification when deployed to a cloud platform. In return they offer significant reduction in image sizes, improved efficiency and security, and should reduce operational costs. Our MirageOS prototype compiles OCaml code into unikernels that run on commodity clouds and offer an order of magnitude reduction in code size without significant performance penalty. The architecture combines static type-safety with a single address-space layout that can be made immutable via a hypervisor extension. MirageOS contributes a suite of type-safe protocol libraries, and our results demonstrate that the hypervisor is a platform that overcomes the hardware compatibility issues that have made past library operating systems impractical to deploy in the real-world.

...

...

This paper positions work on the Xen backend for MirageOS. It is a decent summary of the idea, although some details such as the filesystem extension are likely to be significantly different in the first release.

...

This is a vision paper that lays out the broader background to the project, including some of the problem areas we are tackling in social networking and scientific computing. The first half is a good introduction to the area, but read the later HotCloud paper instead of the technical second half.

This paper defines the dyntype dynamic typing extension we developed for OCaml, and the SQL mapper that converts ML values directly into SQL calls. The approach is useful as it is purely meta-programming instead of compiler patching, and thus much easier to integrate with other OCaml code.

A small domain-specific language which compiles to both PROMELA (for static model checking) and OCaml (for dynamic enforcement) of state machines. This paper defines the DSL and an example against an SSH server written in pure OCaml.

The original paper that formed the basis of MirageOS. We define MPL, a DSL to express bi-directional packet descriptions and compile them into efficient, type-safe OCaml code. Performance is tested for DNS and SSH servers written in OCaml versus their C counterparts (BIND and OpenSSH

This thesis describes the Main Name System, an approach to centralising DNS for improved reliability. The source code for the MirageOS DNS library is based directly off the data structures described in this thesis.