Formal Methods: A Practical Tool for OS Implementors

Patrick Tullmann, Jeff Turner, John McCorquodale, Jay Lepreau, Aday Chitturi, Godmar Back
{tullmann, sjt, mcq, lepreau, chitturi, gback}@cs.utah.edu

University of Utah Department of Computer Science
3190 MEB, Salt Lake City, Utah 84112

Abstract

The formal methods community has long known about the need to formally analyze concurrent software, but the OS community has been slow to adopt such methods. The foremost reasons for this are the cultural and knowledge gaps between formalists and OS hackers, fostered by three beliefs: inaccessibility of the tools, the disabling gap between the validated model and actual implementation, and the intractable size of operating systems. In this paper, we show these beliefs to be untrue for appropriately structured operating systems.

We applied formal methods to verify properties of the implementation of the Fluke microkernel's IPC subsystem, a major component of the kernel. In particular, we have verified, in many scenarios, the lack of deadlock and certain liveness properties, with results that apply to both SMP and uniprocessor environments. The SPIN model checker provided an exhaustive concurrency analysis of the IPC subsystem, unattainable through traditional OS testing methods. SPIN is easily accessible to programmers inexperienced with formal methods. We present our results as a starting point for a more comprehensive inclusion of formal methods in practical OS development.

Full paper presented at and appears in Proceedings of the Sixth IEEE Workshop on Hot Topics in Operating Systems, May 1997.