Simpler Proofs for Concurrent Reading and Writing
Abstract
In most computing systems, hardware ensures that read and write operations to some basic unit of memory can be considered mutually exclusive. As a result, a read that overlaps with a write is serialized and will appear either to precede that write or to follow it. Operations that make multiple accesses to memory are not serialized by the hardware. Therefore, the programmer must ensure that when such operations overlap, they produce meaningful results. This paper gives simplified proofs for some protocols proposed by Lamport to coordinate read and write operations that involve multiple accesses to memory. The two key theorems in Lamport's work are long and intricate. Here, we prove each in only a few lines. Our facility with proofs and the use of formalism in problem solving has improved significantly in a little over 15 years. This is due, in part, to the influence of Edsger Dijkstra.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 13, 1989
- Accession Number
- ADA212600
Entities
People
- Fred B. Schneider
Organizations
- Cornell University