A Principled Approach to Operating System Construction in Haskell
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.
Last modified: Nov 2007