Report Number: CSL-TR-77-147
Institution: Stanford University, Computer Systems Laboratory
Title: Verifying concurrent programs with shared date classes
Author: Owicki, Susan S.
Date: August 1977
Abstract: Monitors are a valuable tool for organizing operations on shared data in concurrent programs. In some cases, however, the mutually exclusive procedure calls provided by monitors are overly restrictive. Such applications can be programmed using shared classes, which do not enforce mutual exclusion. This paper presents a method of verifying parallel programs containing shared classes. One first proves that each class procedure performs correctly when executed by itself, then shows that simultaneous execution of other class procedures can not interfere with its correct operation. Once a class has been verified, calls to its procedures may be treated as uninterruptable actions; this simplifies the proof of higher-level program components. Proof rules for classes and procedure calls are given in Hoare's axiomatic style. Several examples are verified, including two versions of the readers and writers problem and a dynamic resource allocator.
http://i.stanford.edu/pub/cstr/reports/csl/tr/77/147/CSL-TR-77-147.pdf