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.