Pretending Atomicity
Abstract
This document presents a theorem for deriving properties of a concurrent program by reasoning about a simpler, coarser-grained version. The theorem generalizes a result that Lipton proved for partial correctness and deadlock-freedom. Our theorem applies to all safety properties. Keywords: Reduction theorem.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 14, 1989
- Accession Number
- ADA208995
Entities
People
- Fred B. Schneider
- Leslie Lamport
Organizations
- Cornell University