A Principled Approach to Operating System Construction in Haskell

A Principled Approach to Operating System Construction in Haskell

Thomas Hallgren, Mark Jones, Andrew Tolmach, and Rebekah Leslie. In Proceedings of the International Conference on Functional Programming (ICFP 2005), Tallinn, Estonia, September 2005.


Abstract:

We describe a monadic interface to low-level hardware features that is a suitable basis for building operating systems in Haskell. The interface includes primitives for controlling memory management hardware, user-mode process execution, and low-level device I/O. The interface enforces memory safety in nearly all circumstances. Its behavior is specified in part by formal assertions written in a programming logic called P-Logic. The interface has been implemented on bare IA32 hardware using the Glasgow Haskell Compiler (GHC) runtime system. We show how a variety of simple O/S kernels can be constructed on top of the interface, including a simple separation kernel and a demonstration system in which the kernel, window system, and all device drivers are written in Haskell.


Available by http in pdf.