Operating Systems

Abstract

Current research in the field of operating systems has been very systems-oriented and result driven. Little theoretical research has been done in considering the formal ramifications of these systems level decisions, or in mapping out the topology of the standard operating system. Because of this, it is often difficult in operating systems work to get a clear picture of the high-level interactions between different OS services, or to apportion programming efforts across well-defined interfaces. Formal specification of the operating system structure and methodology would provide a framework for clearer study, discussion, and implementation of operating systems.

We present a formal method for modelling an operating system as a distributed system of state machines. Drawing the connection between the various independent services of an oeprating system and the independent agents of distributed systems, we model each service of the operating system as an asynchronous I/O Automaton. Demonstrating both the instructional and functional value of this modelling technique, we present here two views of the operaitng system. The first view, the User Level model, provides a simplified abstraction of the operating system. This acts as a operating syystem interface specification as well as an easy first step for teaching students in the field. The second view, or Kernel Level model, provides an implementation of the User Level abstract specification, and unveils many of the realities which were abstracted away in the User Level model. It provides a framework for research in formalizing operating systems, as well as providing a clear and concise description of many of today's oeprating system elements. Finally, using the powerful mathematical tools developed for I/O Automata, we make two formal modifications to the Kernel Level model and prove that it in fact does implement the User Level specification. We thereby assert that the two models are, from the perspective of the processes, functionally equivalent.

Daniel Yates, Nancy Lynch, Victor Luchangco, and Margo Seltzer. I/O Automaton Model of Operating System Primitives Masters thesis, Harvard University and Massachusetts Institute of Technology, May 1999. Thesis (.ps)

TOC / LCS / MIT Last modified: Fri. March 17 15:05:35 2000	Comments?