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. Categories and Subject Descriptors D.3.2 [Programming Languages]: Language Classifications--Applicative (functional) languages; D.4.0 [Operating Systems]: Organization and Design; D.4.5 [Operating Systems]: Reliability...

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: Thomas Hallgren, Mark P. Jones, Rebekah Leslie, Andrew P. Tolmach
• Keywords: Hardware Interface, ICFP 2005, Interface Enforces Memory, Interface Includes Primitives, Programming Languages