This page lists any publications, technical reports and related work to MirageOS. If you know of any work that should be listed here, please contact us.
Anil Madhavapeddy and David Scott
In Communications of the ACM, January 2014.
What if all the software layers in a virtual appliance were compiled within the same safe, high-level language framework?
Anil Madhavapeddy, Yaron Minsky and Jason Hickey
Published by O'Reilly Associates, 510 pages, Nov 2013.
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.
Anil Madhavapeddy, Richard Mortier, Charalampos Rotsos, David Scott, Balraj Singh, Thomas Gazagnaire, Steven Smith, Steven Hand and Jon Crowcroft
Proceedings of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems>ASPLOS '13, April, 2013.
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.
Richard Mortier, Charalampos Rotsos, Anil Madhavapeddy, Balraj Singh and Andrew Moore
Proceedings of IEEE ICC Software Defined Networking workshop, June 2012.
Jon Crowcroft, Anil Madhavapeddy, Malte Schwarzkopf, Theo Hong and Richard Mortier
Proceedings of 12th International Conference on Distributed Computing and Networking >ICDCN '11, January 2011. Invited paper.
Anil Madhavapeddy, Richard Mortier, Ripduman Sohan, Thomas Gazagnaire, Steven Hand, Tim Deegan, Derek McAuley and Jon Crowcroft
2nd USENIX Workshop on Hot Topics in Cloud Computing HotCloud '10, June 2010.
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.
Richard Mortier, Anil Madhavapeddy, Theo Hong, Derek Murray and Malte Schwarzkopf
Proceedings of the 18th International Workshop on Security Protocols (IWSP), April 2010
Anil Madhavapeddy, Richard Mortier, Jon Crowcroft and Steven Hand
ACM/BCS Visions of Computer Science, April 2010
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.
Thomas Gazagnaire and Anil Madhavapeddy
Workshop on Generative Technologies, April 2010
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.
International Conference on Formal Engineering Methods ICFEM, December 2009.
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.
Anil Madhavapeddy, Alex Ho, Tim Deegan, David Scott and Ripduman Sohan
>EuroSys 2007, March 2007.
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
PhD Thesis, University of Cambridge, 2006.
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.