NOTE: This transcription was contributed by Martin P.M. van der Burgt, who has devised a process for producing transcripts automatically. Although its markup is incomplete, we believe it serves a useful purpose by virtue of its searchability and its accessibility to text-reading software. It will be replaced by a fully marked-up version when time permits. —HR

**Finding the correctness proof of a concurrent program**.

(Those who have seen EWD622 will recognize the following as an improved treatment of one of the versions of the concurrent program developed in that report. The main improvement consists of the heuristics for finding the correctness proof: the heuristics effectively buffer the shock of invention which, in EWD622 - 11, was indicated by “A bold guess is to interpret....”.

For the benefit of those who have not seen EWD622, this note is written as a self-contained text that fully redescribes the problem. They have furthermore the advantage that they won’t be confused by changed notations and meanings of variables.)

In the following y denotes a vector of N components y[i] for 0 ≤ i < N . with the identifier f we shall denote a vector-valued function of a vector-valued argument, and the algorithm concerned solves the equation

y = f(y) | (1) |

y[i] = fi(y) for 0 ≤ i < N . | (2) |

It is assumed that the initial value of y and the function f are such that the repeated assignments of the form

<y[i]:= fi(y) > | (3) |

For the purpose of this note it suffices to know that functions f
exist such that with a proper value of y equation (1) will be solved by a
finite number of assignments (3). How for a given f and initial value y
this property can be established is **not** the subject of this paper. (He who
refuses to assume that the function f has that delightful property is free
to do so: he can, again, read the following as a proof of partial correctness
that states that **when** our concurrent program has terminated, (1) is
satisfied.)

Besides the global vector y there is a global boolean array h , with elements h[i] for 0 ≤ i < N , all of which are true to start with. we now consider the following program of N-fold concurrency, in which each atomic action modifies at most one global array element. We give the program first and shall explain the notation afterwards.

The concurrent program we are considering consists of the following N components (0 ≤ i < N):

comp.i: | ||||

L0: |
do < (E j: h[j]) > → | |||

L1: |
< if y[i] = fi(y) → h[i]:= false > | |||

▯ y[i] ≠ fi(y) → y[i]:= fi(y) > ; | ||||

L2j: |
(A j: < h[j]:= true > ) | |||

fi | ||||

od |

__E__j: h[j]) is an abbreviation for (

__E__j: 0 ≤ j < N: h[j]) ; for the sake of brevity we shall use this abbreviation throughout this note. By writing < (

__E__j: h[j]) > in the guard we have made the inspection whether a true h[j] can be found into an atomic action. The opening angle bracket “ < ” in L1 has two corresponding closing brackets, corresponding to the two “atomic alternatives”; it means that in the same atomic action the guards are evaluated and either “h[i]:= false” or “y[i]:= fi(y)” is executed. In the latter case, N separate atomic actions follow, each setting an h[j] to true: in line L2j we have used the abbreviation (

__A__j: < h[j]:= true > ) for the program that performs the N atomic actions < h[0]:= true > through < h[N-1]:= true > in some order which we don’t specify any further. Our target state is that y is a solution of (1), or, more explicitly

(A j: y[j] = fj(y)) . | (4) |

non (E j: h[j]) and (A j: y[j] = fj(y)) | (5) |

(A j: non h[j]) and (A j: y[j] = fj(y)) | (5’) |

__A__j:

**non**h[j]). When (4) holds, the assumption of fair random order implies that within a finite number of steps (5) will hold. But then the guards of the repetitive constructs are false, and all components will terminate nicely with (4) holding. The critical point is: can we guarantee that none of the components terminates too soon? In order to prove that termination implies that (4) holds, we have to prove the universal truth of

(E j: h[j]) or (A j: y[j] = fj(y)) . | (6) |

We get a hint of the kind of difficulties we may expect when trying to prove the invariance of (6) as soon as we realize that the first term is a compact notation for

h[0] or h[1] or h[2] or ... or h[N-1] |

**last**true h[j] disappears. That is ugly!

Proving a mathematical theorem is often only feasible by proving a
stronger —but, somehow, more manageable— theorem instead. In direct analogy:
instead of trying to prove the invariant truth of (6) we shall try to prove
the invariant truth of a stronger assertion that we get by replacing the
conditions y[j] = fj(y) by stronger ones. Because under the universal truth
of (Q **or** R) , the relation non R is stronger than Q , we can strengthen
(6) into

(E j= h[j]) or (A j: non Rj) | (7) |

(A j: y[j] = fj(y) or Rj) | (8) |

What have we gained by the introduction of the N predicates Rj? Well: the freedom to choose them! More precisely: the freedom to define them in such a way that we can prove the universal truth of (8) —which is structurally quite pleasant— while the universal truth of (7) —which is structurally equally “ugly” as (6)— follows more or less directly from the definition of the Rj’s : that is the way in which we may hope that (7) is more “manageable” than the original (6).

In order to find a proper definition of the Rj’s , we analyse our
obligation to **prove** the invariance of (8).

If we only looked at the invariance of (8), one might think, that a definition of the Rj’s in terms of y:

Rj = (y[j] ≠ fj(y)) |

For two reasons we are looking for a definition of the Rj’s in which the
y does not occur: firstly, it is then that we can expect the proof of the
universal truth of (8) to amount to something —and, therefore, to contribute
to the argument— , secondly, we would like to conclude the universal truth
of (7) —which does not mention y at all— from the definition of the Rj’s.
In other words, we propose a **definition** of the Rj’s which does not refer
to y at all: only with such a definition the replacement of (6) by (7) and
(8) localizes our dealing with y completely to the proof of the universal
truth of (8).

Because we want to define the Rj’s independently of y , because initially we cannot assume that for some j-value y[j] = fj(y) holds, and because (8) must hold initially, we must assume that initially

(A j: Rj) | (9) |

(E j: non h[j]) or (A j: Rj) . | (10) |

(A j: non h[j] or Rj) | (11) |

From (11) it follows that the algorithm will start with all the Rj’s true. From (8) it follows that the truth of Rj can be appreciated as “the equation y[j] = fj(y) need not be satisfied”, and from (7) it follows that in our final state we want to have all the Rj’s equal to false.

Let us now look at the alternative construct

L1: |
<if y[i] = fi(y) → h[i]:= false > | ||

▯ y[i] ≠ fi(y) → y[i]:= f(y) >; | |||

L2j: |
(A j: < h[j]:= true >) | ||

fi |

**may**become false, but that in the second alternative as a whole, all Rj’s

**must**become true.

Let us now confront the two atomic alternatives with (8). Because, when the first alternative is selected, only y[i] = fi(y) has been observed, the universal truth of (8) is not destroyed by it, provided:

In the execution of the first atomic alternative

< y[i] = fi(y) -. h[i]:= false > | ||

no Rj for j ≠ i may change from true to false. | (12) |

Confronting the second atomic alternative

<y[i] ≠ fi(y) → y[i]:= fi(y)> |

with (8), and observing that upon its completion

**none**of the relations y[j] = fj(y) needs to hold, we conclude that the second atomic alternative itself must already cause a final state in which all the Rj’s are true, in spite of the fact that the subsequent assignments h[j]:= true —which would each force an Rj to true on account of (11)— have not been executed yet. In short: in our definition for the Rj’s we must include besides (11) another reason why an Rj should be defined to be true.

As it stands, the second atomic alternative only modifies y , but we:
had decided that the definition of the Rj’s would not be expressed in terms
of y ! The only way in which we can formulate the additional reason for
an Rj to be true is in terms of an **auxiliary** variable (to me introduced in
a moment), whose value is changed in conjunction with the assignment to y[i] .
It has to force each Rj to true until the subsequent assignment
< h[j]:= true > does so via (11). Because the second atomic alternative is
followed by N subsequent, separate atomic actions < h[j]:= true > —one
for each value of j — it stands to reason that we introduce for comp.i
an auxiliary local boolean array ri with elements ri[j] for 0 ≤ j < N .
Their initial (and “neutral”) value is true. The second atomic alternative of
L1 sets them all to false, the atomic statements L2j will reset them to true
one at a time.

In the following annotated version of comp.i we have inserted local
assertions between braces. In order to understand the local assertions about
ri it suffices to remember that L1 is local to comp.i . The local assertion
Ri in the second atomic alternative of L1 is justified by the guard
y[i] ≠ fi(y) in conjunction with (8). We have further incorporated in our,
annotation the consequence of (12) and the fact that the execution of a second
alternative will never cause an Rj to become false: a true Ri can only
become false by virtue of the execution of the first atomic alternative of
L1 by comp.i itself! Hence, Ri is true all through the execution of the
second alternative of comp.i .

comp.i:

L0: |
do < (E j: h[j]) >→ {(A j: ri[j])} | |||

L1: |
<if y[i] = fi(y) → h[i]:= false > {(A j: ri[j])} | |||

▯ y[i] ≠ fi(y) → | ||||

{Ri} y[i]:= fi(y); | ||||

(A j: ri[j]:= false) > {Ri and (A j: non ri[j])}; | ||||

(A j:{Ri and non ri[j]} < h[j]:= true; ri[j]:= true ≠ ) | ||||

L2j: |
fi {(A j: ri[j])} . | |||

od | ||||

On account of (11) Rj will be true upon completion of L2j. But the second atomic alternative of L1 ,should already have made Rj true, and it should remain so until L2j is executed. The precondition of L2j, as given in the annotation, hence tells us the ”other reason besides

(A j: non h[j] or Rj) | (11) |

(A i, j: non Ri or ri[j] or Rj) . | (13) |

**define**the Rj’s as the

**minimal**solution of (11) and (13), minimal in the sense of: as few Rj’s true as possible.

A second look shows how the minimal solution is found. It is a sort of
transitive closure: starting with the set of Rj’s forced true by (11) —on
account of falsity of **non** h[j]— , if necessary we extend this set —possibly
in cascades— with the Rj’s forced true by (13) —on account of falsity of
**non** Ri **or** ri[j]— .

For a value of i , for which

(A j: ri[j]) | (14) |

We have proved the universal truth of (8) by defining the Rj’s as the minimal solution of (11) and (13). The universal truth of (7) , however, is now obvious. If the leFt-hand term of (7) is false, we have

(A j:non h[j]), |

(A j: non Rj) | , |

**Acknowledgements**. I would like to express my gratitude to both IFIP WG2.3 and
”The Tuesday Afternoon Club“, where I had the opportunity to discuss this
problem. Those familiar with the long history that led to this note, however,
know that in this case I am indebted to C.S.Scholten more than to anyone
else.

**Reference **

EWD622 ”On making solutions more and more fine-grained.“ by Edsger W.Dijkstra.

Plataanstraat 5 | prof.dr.Edsger W.Dijkstra |

5671 AL NUENEN | Burroughs Research Fellow |

The Netherlands |

Transcribed by Martin P.M. van der Burgt

Last revision