Thomas Hallgren
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.
- F. Bellard. QEMU. http://fabrice.bellard.free.fr/qemu/.Google Scholar
- E. Biagioni, R. Harper, and P. Lee. A Network Protocol Stack in Standard ML. Higher Order Symbol. Comput., 14(4):309--356, 2001. Google ScholarDigital Library
- L. Cardelli, J. Donahue, L. Glassman, M. Jordan, B. Kalsow, and G. Nelson. Modula-3: Language definition. http://www.research.compaq.com/SRC/m3defn/html/complete.html.Google Scholar
- S. Carlier and J. Bobbio. hOp. http://www.macs.hw.ac.uk/~sebc/hOp/, 2004.Google Scholar
- A. Cheadle, T. Field, S. Marlow, S. Peyton Jones, and L. While. Exploring the Barrier to Entry: Incremental Generational Garbage Collection for Haskell. In Int. Symp. on Memory Management, pages 163--174, 2004. Google ScholarDigital Library
- J. Cupitt. A brief walk thourgh KAOS. Techical Report 58, Computing Laboratory, Univ. of Kent at Canterbury, February 1989.Google Scholar
- Cyclone. http://www.research.att.com/projects/cyclone/.Google Scholar
- K. Fraser, S. Hand, R. Neugebauer, I. Pratt, A. Warfield, and M. Williamson. Safe hardware access with the Xen virtual machine monitor. In Proc. OASIS ASPLOS Workshop, 2004.Google Scholar
- G. Fu. Design and implementation of an operating system in Standard ML. Master's thesis, University of Hawaii, August 1999.Google Scholar
- Glasgow haskell compiler. http://www.haskell.org/ghc.Google Scholar
- Grub. http://www.gnu.org/software/grub/.Google Scholar
- T. Hallgren. The House web page. http://www.cse.ogi.edu/~hallgren/House/, 2004.Google Scholar
- Intel Corp. IA-32 Intel Architecture Software Developer's Manual Volume 3: System Programming Guide, 2004.Google Scholar
- T. Jim, G. Morrisett, D. Grossman, M. Hicks, J. Cheney, and Y.Wang. Cyclone: A Safe Dialect of C. In USENIX Annual Technical Conference, pages 275--288, June 2002. Google ScholarDigital Library
- M. P. Jones. Functional programming with overloading and higherorder polymorphism. In Advanced Functional Programming, 1st Int. Spring School on Advanced Functional Programming Techniques-Tutorial Text, pages 97--136, London, UK, 1995. Springer-Verlag. Google ScholarDigital Library
- M. P. Jones. Bare Metal: A Programatica model of hardware. In High Confidence Software and Systems Conference, Baltimore, MD, March 2005.Google Scholar
- K. Karlsson. Nebula: A functional operating system. Technical report, Programing Methodology Group, University of Göteborg and Chalmers University of Technology, 1981.Google Scholar
- R. B. Kieburtz. P-logic: Property verification for Haskell programs. ftp://ftp.cse.ogi.edu/pub/pacsoft/papers/Plogic.pdf, August 2002.Google Scholar
- S. Liang, P. Hudak, and M. Jones. Monad transformers and modular interpreters. In POPL '95: Proc. 22nd ACM Symp. on Principles of programming languages, pages 333--343, 1995. Google ScholarDigital Library
- R. Noble. Lazy Functional Components for Graphical User Interface. PhD thesis, University of York, November 1995.Google Scholar
- The OSKit Project. http://www.cs.utah.edu/flux/oskit/.Google Scholar
- The Programatica Project home page. www.cse.ogi.edu/PacSoft/projects/programatica/, 2002.Google Scholar
- The SPIN project. http://www.cs.washington.edu/research/projects/spin/www/, 1997.Google Scholar
- W. Stoye. Message-based functional operating systems. Science of Computer Programming, 6:291--311, 1986. Google ScholarDigital Library
- L. Team. L4 eXperimental Kernel Reference Manual, January 2005.Google Scholar
- Video Electronics Standards Association. VESA BIOS EXTENSION (VBE) - Core Functions Standard, Version: 3.0, September 1998. www.vesa.org.Google Scholar
- M. Wallace. Functional Programming and Embedded Systems. PhD thesis, Dept of Computer Science, Univ. of York, UK, January 1995.Google Scholar
- M. Wallace and C. Runciman. Lambdas in the Liftshaft - Functional Programming and an Embedded Architecture. In FPCA '95: Proc. 7th Int. Conf. on Functional Programming Languages and Computer Architecture, pages 249--258, 1995. Google ScholarDigital Library
Index Terms
- A principled approach to operating system construction in Haskell
Recommendations
A principled approach to operating system construction in Haskell
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingWe 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 ...
Strength Induction in a Haskell Program Verifier
Haskell employs a melange of strict and non-strict evaluation semantics, hence a Haskell verifier should be capable of checking assumptions that program variables may or may not denote well-defined values. The paper introduces a new strategy, called ...
The Intel labs Haskell research compiler
Haskell '13The Glasgow Haskell Compiler (GHC) is a well supported optimizing compiler for the Haskell programming language, along with its own extensions to the language and libraries. Haskell's lazy semantics imposes a runtime model which is in general difficult ...
Comments