Report Number: CS-TR-77-607
Institution: Stanford University, Department of Computer Science
Title: Specifications and proofs for abstract data types in concurrent programs
Author: Owicki, Susan S.
Date: April 1977
Abstract: Shared abstract data types, such as queues and buffers, are useful tools for building well-structured concurrent programs. This paper presents a method for specifying shared types in a way that simplifies concurrent program verification. The specifications describe the operations of the shared type in terms of their effect on variables of the process invoking the operation. This makes it possible to verify the processes independently, reducing the complexity of the proof. The key to defining such specifications is the concept of a private variable: a variable which is part of a shared object but belongs to just one process. Shared types can be implemented using an extended form of monitors; proof rules are given for verifying that a monitor correctly implements its specifications. Finally, it is shown how concurrent programs can be verified using the specifications of their shared types. The specification and proof techniques are illustrated with a number of examples involving a shared bounded buffer.