A novel formal theory of concurrent systems that does not assume any atomic operations is introduced. The execution of a concurrent program is modeled as an abstract set of operation executions with two temporal ordering relations: “precedence” and “can causally affect.” A primitive interprocess communication mechanism is then defined.

--From the Author’s Abstract

In this paper, Lamport presents an axiom system for concurrent program execution. His axioms do not assume any atomic operations, which is a radical departure from theories such as [1]. He considers programming models that do assume atomic operations to be unsatisfactory for a fundamental study of mutual exclusion (the main point of his paper), because such models inherently assume some form of underlying mutual exclusion.

Lamport starts by using special relativity theory to motivate consideration of two binary relations on operation executions: temporal precedence (denoted by →) and ability to causally affect (denoted by --→). He then gives four axioms ( A1 - A4) that are satisfied by → and --→ , followed by two additional axioms (A5, A6) that serve to provide the desired properties of “terminating” and “nonterminating” operation executions expressed in terms of → and --→.

Next, Lamport introduces a notion of binary-valued communication variable that can be written by one process (its owner) and read by another, where such a read and a write can be concurrent and are not assumed to be atomic. The desired properties of these communication variables are also given entirely in terms of → and --→(in Axioms C0–C3). Finally, Lamport states in Theorem 1 that an array of such single-reader communication variables can be used to extend the communication variable concept, so as to support multiple readers.

Lamport points out (on p. 321) that communication variables similar to his have been suggested [2], but with the stronger assumption of atomic reads and writes. However, in [2] the authors admit that this assumption of atomicity becomes “less practical” as the number of states of the variable (equivalently, in [2], the number of reader processes) becomes “larger.” On the other hand, Lamport suggests (on p. 324) that the cost of physically implementing his multiple reader communication variable may be essentially independent of the number of readers. Also, it seems that dependence on the atomicity assumption forces [2] to use exactly one (multivalued) communication variable per process in mutual exclusion algorithms. Similarly, the algorithms in [3] use a general test-and-set operation on a single shared variable that is global to the whole system. Both are in sharp contrast to the multiple reader situation associated with Lamport’s communication variable, as shown by Theorem 1.

Lamport’s theory of concurrent programs seems simple and reasonable, and Part II of this paper (see the following review, Rev. 8704-0280) appears to demonstrate its adequacy. However, we feel that the remark in the second paragraph of Section 2.1 does not sufficiently explain why he chose the relativistic, instead of the classical, notion of temporal precedence between events to motivate his axioms (because either notion would have led to his axioms, but the classical notion of precedence would have done so more simply). Perhaps Lamport should have at least mentioned [4] in his motivation, if that paper provided the basis for his choice.