Abstract
A multiprocess program executing on a modern multiprocessor must issue explicit commands to synchronize memory accesses. A method is proposed for deriving the necessary commands from a correctness proof of the underlying algorithm in a formalism based on temporal relations among operation executions.
A multiprocess program executing on a modern multiprocessor must issue explicit commands to synchronize memory accesses. A method is proposed for deriving the necessary commands from a correctness proof of the underlying algorithm in a formalism based on temporal relations among operation executions.
Motivation
Accessing a single memory location in a multiprocessor is traditionally assumed to be atomic. Such atomicity is a fiction; a memory access consists of a number of hardware actions, and different accesses may be executed concurrently. Early multiprocessors maintained this fiction, but more modern ones usually do not. Instead, they provide special commands with which processes themselves can synchronize memory accesses. The programmer must determine, for each particular computer, what synchronization commands are needed to make his program correct.
We derive the synchronization commands from a proof of correctness of the algorithm. The method of extracting synchronization commands from a proof is described by an example a simple mutual exclusion algorithm.
The Mutual Exclusion example
The example of the mutual exclusion algorithm illustrates how a set of properties sufficient to guarantee correctness can be extracted directly from a correctness proof. Implementations of the algorithm on different memory architectures can be derived from the assumptions, with no further reasoning about the algorithm. An implementation will be efficient only if the architecture provides synchronization primitives that efficiently implement the assumed properties.
Background
Sequential Consistency
The atomicity condition traditionally assumed for multiprocess programs is sequential consistency, meaning that the program behaves as if the memory accesses of all processes were interleaved and then executed sequentially (seen by all nodes of the system in the same order).
It has been proposed that, when sequential consistency is not provided by the memory system, it can be achieved by a constrained style of programming. Synchronization commands are added either explicitly by the programmer, or automatically from hints he provides.
Strict Consistency
Strict consistency is stronger than sequential consistency. This demands that operations are seen in order in which they were actually issued - which is essentially impossible to secure in distributed system, where deciding global time is virtually impossible.
Causal Consistency
Causal consistency is weaker than sequential consistency. This demands that writes that potentially are causally related are seen by every node of the system in the same order. Concurrent writes may be seen in different order by different nodes. When a node performs a read followed later by a write, the two operations are said to be causally related because the value stored by the write may have been dependent upon the result of the read. Similarly, a read operation is causally related to an earlier write that stored the data retrieved by the read. Operations that are not causally related are said to be concurrent.
ContributionsCausal Consistency
Causal consistency is weaker than sequential consistency. This demands that writes that potentially are causally related are seen by every node of the system in the same order. Concurrent writes may be seen in different order by different nodes. When a node performs a read followed later by a write, the two operations are said to be causally related because the value stored by the write may have been dependent upon the result of the read. Similarly, a read operation is causally related to an earlier write that stored the data retrieved by the read. Operations that are not causally related are said to be concurrent.
Most multiprocess programs for modern multiprocessors are best written in terms of higher-level abstractions. The method presented here can be applied to the algorithms that implement these abstractions and to those algorithms, usually in the depths of the operating system, where efficiency and correctness are crucial.
