Implementation of an Operating System in ML - PDF | Hacker News Reader

Implementation of an Operating System in ML - PDF

dspace.mit.edu

60 pointsfogus11 comments

If you find this interesting you may want to read about this more current research: http://www.openmirage.org/

To quote from the vision paper http://anil.recoil.org/papers/2010-bcs-visions.pdf

  Mirage is written in the spirit of vertical operating 
  systems such as Nemesis [17] or Exokernel [10], but
  differs in certain aspects: (i) apart from a small runtime,
  the operating system and support code (e.g., threading)
  is entirely written in OCaml; and (ii) is statically
  specialised at compile-time by assembling only required
  components (e.g., a read-only file system which fits
  into memory will be directly linked in as an immutable
  data structure). These features mean that it provides
  a stronger basis for the practical application of formal
  methods such as model checking; and the removal of
  redundant safety system checks greatly improves the
  energy efficiency of the system.

Interesting background of the authors. From Xen (which itself was derived from the Nemesis exokernel, although not directly). XenSource is a heavy OCaml user. And from Cambridge University where Nemesis was developed.

XenSource was bought by Citrix in late 2007. But we are still using OCaml on XenServer. (XenClient started using Haskell.)

a recent video of a talk about mirage:

http://sna-projects.com/blog/2010/10/mirage/

Great video. I don't pretend to understand functional languages but the ideas about memory layout and DSLs for r/w of Ethernet frames seemed really elegant.

This is someone's master thesis from 1998

Here is an abstract for those who don't want to download the full PDF

In this paper I describe the design, implementation, and features of ML/OS, an operating system with an embedded ML compiler. ML/OS supports a continuation-based thread model of concurrency with non-blocking, interrupt-driven input/output. By embedding the ML compiler into the operating system, ML/OS attempts to eliminate levels of abstraction that are present in traditional interactions between compilers and operating systems. By using a continuation-based scheduler, I demonstrate the use of advanced programming language features such as continuations and type safety in system-level programming.

Reminds me of SPIN (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.8...) and Singularity (http://research.microsoft.com/apps/pubs/default.aspx?id=6943...) - putting a compiler in the kernel lets you control what runs on the system without using hardware protection barriers, as well as enables better optimization against the running system.

I know Adobe are forever adding more bloat to Acrobat Reader, but an OS in a PDF? That's just too far!

PostScript was Turing complete. Imagine having a fractal-drawing program in a PDF, and you're not far off from what it can do:

http://www.pvv.ntnu.no/~andersr/fractal/PostScript.html

More system software in ML: http://www.cs.cornell.edu/Info/Projects/HORUS/

"By early in 1997, Ensemble will be an outstanding environment for building Java-based groupware applications that do multimedia conferencing on the Web."

Oh boy, sure brings back memories...

Reply on news.ycombinator.com