Axioms for Concurrent Objects
Abstract
Specification and verification techniques for abstract data types that have been successful for sequential programs can be extended in a natural way to provide the same benefits for concurrent programs. An approach is proposed to specifying and verifying concurrent objects based on a novel correctness condition, which we call linearizability. Linearizability provides the illusion that each operation takes effect instantaneously at some point between its invocation and its response, implying that the meaning of a concurrent objects operations can still be given by pre- and post conditions. This paper defines and discusses linearizability, and then give examples of how to reason about concurrent objects and verify their implementations based on their (sequential) axiomatic specifications.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 1987
- Accession Number
- ADA200584
Entities
People
- Jennette M. Wing
- Maurice P. Herlihy
Organizations
- Carnegie Mellon University