A New Approach to Proving the Correctness of Multiprocess Programs

A corrigendum was published in ACM Transactions on Programming Languages and Systems 2, 1 (January 1980), 134 and is available here.

Like everyone else at the time, when I began studying concurrent algorithms, I reasoned about them behaviorally. Such reasoning typically involved arguments based on the order in which events occur. I discovered that proofs can be made simpler, more elegant, and more mathematical by reasoning about operations (which can be composed of multiple events) and two relations on them: precedes (denoted by a solid arrow) and can affect (denoted by a dashed arrow). Operation A precedes operation B if all the events of A precede all the events of B; and A can affect B if some event in A precedes some event in B. These relations obey some simple rules that can reduce behavioral reasoning to mathematical symbol pushing.

This paper introduced the method of reasoning with the two arrow relations and applied it to a variant of the bakery algorithm. In the spring of 1976 I spent a month working with Carel Scholten at the Philips Nat Lab in Eindhoven. Scholten was a colleague and friend of Dijkstra, and the three of us spent one afternoon a week working, talking, and drinking beer at Dijkstra’s house. The algorithm emerged from one of those afternoons. I think I was its primary author, but as I mention in the paper, the beer and the passage of time made it impossible for me to be sure of who was responsible for what.

The solid and dashed arrow formalism provides very elegant proofs for tiny algorithms such as the bakery algorithm. But, like all behavioral reasoning, it is hard to make completely formal, and it collapses under the weight of a complex problem. You should use assertional methods to reason about complex algorithms. However, standard assertional reasoning requires that the algorithm be written in terms of its atomic operations. The only assertional approach to reasoning directly about nonatomic operations (without translating them into sequences of atomic operations) is the one in [86], which is not easy to use. The two-arrow formalism is still good for a small class of problems.

The formalism seems to have been almost completely ignored, even among the theoretical concurrency community. I find this ironic. There is a field of research known by the pretentious name of “true concurrency”. Its devotees eschew assertional methods that are based on interleaving models because such models are not truly concurrent. Instead, they favor formalisms based on modeling a system as a partial ordering of events, which they feel is the only truly concurrent kind of model. Yet, those formalisms assume that events are atomic and indivisible. Atomic events don’t overlap in time the way real concurrent operations do. The two-arrow formalism is the only one I know that is based on nonatomic operations and could therefore be considered truly concurrent. But, as far as I know, the true concurrency community has paid no attention to it.