A principled approach to operating system construction in Haskell

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A principled approach to operating system construction in Haskell

Full text

Pdf (155 KB)

Source

International Conference on Functional Programming archive
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming table of contents

Tallinn, Estonia

SESSION: Session 4 table of contents

Pages: 116 - 128

Year of Publication: 2005

ISBN:1-59593-064-7

Also published in ...

Authors

Thomas Hallgren	Oregon Health & Science University
Mark P. Jones	Oregon Health & Science University
Rebekah Leslie	Portland State University
Andrew Tolmach	Portland State University

Sponsors

ACM: Association for Computing Machinery
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 9, Downloads (12 Months): 69, Citation Count: 16

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1086365.1086380 What is a DOI?

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	F. Bellard. QEMU. http://fabrice.bellard.free.fr/qemu/.
	2	Edoardo Biagioni , Robert Harper , Peter Lee, A Network Protocol Stack in Standard ML, Higher-Order and Symbolic Computation, v.14 n.4, p.309-356, December 2001 [doi>10.1023/A:1014403914699]
	3	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.
	4	S. Carlier and J. Bobbio. hOp. http://www.macs.hw.ac.uk/~sebc/hOp/, 2004.
	5	A. M. Cheadle , A. J. Field , S. Marlow , S. L. Peyton Jones , R. L. While, Exploring the barrier to entry: incremental generational garbage collection for Haskell, Proceedings of the 4th international symposium on Memory management, October 24-25, 2004, Vancouver, BC, Canada [doi>10.1145/1029873.1029893]
	6	J. Cupitt. A brief walk thourgh KAOS. Techical Report 58, Computing Laboratory, Univ. of Kent at Canterbury, February 1989.
	7	Cyclone. http://www.research.att.com/projects/cyclone/.
	8	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.
	9	G. Fu. Design and implementation of an operating system in Standard ML. Master's thesis, University of Hawaii, August 1999.
	10	Glasgow haskell compiler. http://www.haskell.org/ghc.
	11	Grub. http://www.gnu.org/software/grub/.
	12	T. Hallgren. The House web page. http://www.cse.ogi.edu/~hallgren/House/, 2004.
	13	Intel Corp. IA-32 Intel Architecture Software Developer's Manual Volume 3: System Programming Guide, 2004.
	14	Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
	15	Mark P. Jones, Functional Programming with Overloading and Higher-Order Polymorphism, Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text, p.97-136, May 24-30, 1995
	16	M. P. Jones. Bare Metal: A Programatica model of hardware. In High Confidence Software and Systems Conference, Baltimore, MD, March 2005.
	17	K. Karlsson. Nebula: A functional operating system. Technical report, Programing Methodology Group, University of Göteborg and Chalmers University of Technology, 1981.
	18	R. B. Kieburtz. P-logic: Property verification for Haskell programs. ftp://ftp.cse.ogi.edu/pub/pacsoft/papers/Plogic.pdf, August 2002.
	19	Sheng Liang , Paul Hudak , Mark Jones, Monad transformers and modular interpreters, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.333-343, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199528]
	20	R. Noble. Lazy Functional Components for Graphical User Interface. PhD thesis, University of York, November 1995.
	21	The OSKit Project. http://www.cs.utah.edu/flux/oskit/.
	22	The Programatica Project home page. www.cse.ogi.edu/PacSoft/projects/programatica/, 2002.
	23	The SPIN project. http://www.cs.washington.edu/research/projects/spin/www/, 1997.
	24	W Stoye, Message-based functional operating systems, Science of Computer Programming, v.6 n.3, p.291-311, May 1986
	25	L. Team. L4 eXperimental Kernel Reference Manual, January 2005.
	26	Video Electronics Standards Association. VESA BIOS EXTENSION (VBE) - Core Functions Standard, Version: 3.0, September 1998. www.vesa.org.
	27	M. Wallace. Functional Programming and Embedded Systems. PhD thesis, Dept of Computer Science, Univ. of York, UK, January 1995.
	28	Malcolm Wallace , Colin Runciman, Lambdas in the liftshaft—functional programming and an embedded architecture, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.249-258, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224213]

CITED BY 16

	Rui Shi, Implementing reliable Linux device drivers in ATS, Proceedings of the 2007 workshop on Programming languages meets program verification, October 05-05, 2007, Freiburg, Germany
	Eelco Dolstra , Armijn Hemel, Purely functional system configuration management, Proceedings of the 11th USENIX workshop on Hot topics in operating systems, p.1-6, May 07-09, 2007, San Diego, CA
	Kevin Elphinstone , Gerwin Klein , Philip Derrin , Timothy Roscoe , Gernot Heiser, Towards a practical, verified kernel, Proceedings of the 11th USENIX workshop on Hot topics in operating systems, p.1-6, May 07-09, 2007, San Diego, CA
	Iavor S. Diatchki , Mark P. Jones, Strongly typed memory areas programming systems-level data structures in a functional language, Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, September 17-17, 2006, Portland, Oregon, USA
	Jonathan Shapiro, Programming language challenges in systems codes: why systems programmers still use C, and what to do about it, Proceedings of the 3rd workshop on Programming languages and operating systems: linguistic support for modern operating systems, p.9-es, October 22-22, 2006, San Jose, California
	Philip Derrin , Kevin Elphinstone , Gerwin Klein , David Cock , Manuel M. T. Chakravarty, Running the manual: an approach to high-assurance microkernel development, Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, September 17-17, 2006, Portland, Oregon, USA
	Malcolm Dowse , Andrew Butterfield, Modelling deterministic concurrent I/O, ACM SIGPLAN Notices, v.41 n.9, September 2006
	Paul Hudak , John Hughes , Simon Peyton Jones , Philip Wadler, A history of Haskell: being lazy with class, Proceedings of the third ACM SIGPLAN conference on History of programming languages, p.12-1-12-55, June 09-10, 2007, San Diego, California
	Iavor S. Diatchki , Thomas Hallgren , Mark P. Jones , Rebekah Leslie , Andrew Tolmach, Writing systems software in a functional language: an experience report, Proceedings of the 4th workshop on Programming languages and operating systems, October 18-18, 2007, Stevenson, Washington
	Marius Nita , Dan Grossman , Craig Chambers, A theory of platform-dependent low-level software, ACM SIGPLAN Notices, v.43 n.1, January 2008
	John Criswell , Andrew Lenharth , Dinakar Dhurjati , Vikram Adve, Secure virtual architecture: a safe execution environment for commodity operating systems, ACM SIGOPS Operating Systems Review, v.41 n.6, December 2007
	Peng Li , Simon Marlow , Simon Peyton Jones , Andrew Tolmach, Lightweight concurrency primitives for GHC, Proceedings of the ACM SIGPLAN workshop on Haskell workshop, September 30-30, 2007, Freiburg, Germany
	Kevin Bierhoff , Chris Hawblitzel, Checking the hardware-software interface in spec#, Proceedings of the 4th workshop on Programming languages and operating systems, October 18-18, 2007, Stevenson, Washington
	Eelco Dolstra , Andres Löh, NixOS: a purely functional Linux distribution, ACM SIGPLAN Notices, v.43 n.9, September 2008
	Daniel Frampton , Stephen M. Blackburn , Perry Cheng , Robin J. Garner , David Grove , J. Eliot B. Moss , Sergey I. Salishev, Demystifying magic: high-level low-level programming, Proceedings of the 2009 ACM SIGPLAN/SIGOPS international conference on Virtual execution environments, March 11-13, 2009, Washington, DC, USA
	Yoshihiro Oyama , Yoshiki Kaneko , Hideya Iwasaki, Kenro: a virtual machine monitor mostly described in Haskell, Proceedings of the 2009 ACM symposium on Applied Computing, March 08-12, 2009, Honolulu, Hawaii