Specifying and Verifying Imperative Models of Operating System Structures

Abstract

Discovering bugs in complex, concurrent systems is challenging, even with extensive testing. Model checking—the process of exhaustively verifying the correctness of a finite-state representation of a system—is one technique used to contend with this challenge. Despite model checking’s power, it has several drawbacks which prevent its more widespread use. One challenge is that the leading tools that exist for specifying checkable models are difficult to use. TLA+, a leading model specification language, uses syntax inspired by mathematical notation, which is very different from the syntax of common programming languages. PlusCal is a model specification language that compiles to TLA+. Unlike TLA+, however, PlusCal code much more closely resembles common imperative programming languages, allowing programmers to more easily create models of their systems. While PlusCal is a powerful tool, its functionality is limited compared to TLA+. There is no module system, all variables have global scope, and the syntax has confusing restrictions. Operating systems are one class of complex concurrent systems for which model checking is particularly attractive. In this thesis, we seek to improve the PlusCal language and use it to validate the correctness of operating system components. Specifically, we make the following contributions:

First, we present the design and implementation of the PlusCal Preprocessor, or PCalPP, a language which compiles to PlusCal. PCalPP makes several changes to PlusCal. It removes PlusCal’s strict formatting requirements, introduces a module system, and adds support for local variables. Next, we leverage PCalPP’s modularity to implement a “standard library”—a set of basic components which can be reused in other models. These are designed to facilitate the modeling of operating system components. Specifically, we provide models for locks and schedulers. Finally, we leverage this standard library to write a PCalPP model of the waitqueue abstraction from the Chickadee teaching operating system, used in Harvard’s CS161: Operating Systems course. The waitqueue allows processes to “block” while awaiting conditions. We show that the TLC model checker can successfully verify that our model conforms to its specifications, thereby proving the correctness of our implementation, and that model checking can detect subtle bugs in incorrect waitqueue designs that traditional testing is unlikely to catch. We hope that future CS161 students will be able to use our tooling to verify the correctness of their own waitqueue designs.