Misra’s proof of Lamport’s mutual exclusion

Misra's proof for lamport's mutual exclusion

Consider for $i \geq 1$ -legenda will follow the program

$$ \begin{array}{l} \begin{array}{r}\underline {{d o}} \quad t r u e \rightarrow {\neg s. i }\end{array} \ ; b. i := t r u e {7 s. i \wedge b. i } \ ; x := i \left{\neg s. i \land b. i \right} \ ; i f y = 0 \rightarrow s. i := t r u e f _ {i} {s. i \wedge b. i } \ ; y := i {s. i \wedge b. i \wedge (y \neq 0 \vee x \neq i) } \ i f x = i \rightarrow z := i {P _ {i} } \ \int f r u e \rightarrow \ \end{array} $$

$$ \begin{array}{l} b. i := \mathrm {f a l s e} {s. i } \ ; (\underline {{A}} h: i f \neg b. h \rightarrow s k i p {\underline {{i}}) {s. i \wedge (W \vee y \neq i) } \ i f y = i \rightarrow s k i p f _ {i} {P, i } \ \end{array} $$

$$ \begin{array}{l} \underline {{f _ {i}}} \end{array} \left{\underline {{P _ {i}}} \right}; \mathrm {c r i t i c a l s e c t i o n} \left{\underline {{P _ {i}}} \right} $$

$$ ; y, s. i := 0, f a l s e {\neg s. i } $$

$$ ; b. i := \text {f a l s e} {7 5. i } $$

od

Here $x$ and $y$ are shared integers and the b.i are shared booleans, one for each program; $z$ is an integer thought variable, the s.i are boolean thought variables, one for each program. The setting of a thought variable occurs in the same atomic action as the assignment or (successful) test written in the same line. Statements "if $B \rightarrow S$ i" represent operationally a possible delay.

For the annotation we introduce the abbreviations $W, H,$ and $P$ , for all $i$ given by

$$ w \equiv (\underline {{A}} k: \neg (b. k \land s. k)) \quad (0) $$

$$ H _ {i} = b _ {i} \wedge (x = i \vee 7 5. x) \tag {1} $$

$$ P _ {i} \equiv s. i \wedge y \neq 0 \wedge ((z = i \wedge H. i) \vee (y = i \wedge W)) \quad (2) $$

From (0) $W \land {s}{i} \Rightarrow \neg {b}{i}$ ,hence From(1)

$$ P _ {i} \land P _ {j} \land W \Rightarrow y = i \land y = j $$

From (2) all by itself

$$ P _ {i} \land P _ {j} \land \neg W \Rightarrow z = i \land z = j \tag {4} $$

As the right-hand sides of (3) and (4) imply $i = j$

$$ P _ {i} \land P _ {j} \Rightarrow i = j \tag {5} $$

Furthermore we observe

$$ s. i \wedge b. i \wedge x = i $$

$$ \begin{array}{l} \Rightarrow {\operatorname {f r a m} (0) } \ 7 W \wedge x = i \wedge S. i \ = {\mathrm {p r e d . c a l c} } \ I W \wedge x = i \wedge S. x \ \Rightarrow {(1) } \ (A k: k \neq i: \neg W \land \neg H. k) \ \Rightarrow {(2) } \ (A k: k \neq i: \neg P. k) \tag {6} \ \end{array} $$

We now check the validity of the annotations. The programs are defined to start with $n$ s.i. The post conditions of the next three statements are trivially established and not falsified by other programs. Let $k \neq i$ .

The postcondition of $y \mathrel{\text{:=}} i$ is established by this assignment because $i \neq 0$ . We can rewrite (6) as

$$ s. i \wedge b. i \wedge P. k \Rightarrow x \neq i $$

so, if program $k$ falsifies $y \neq 0$ ,it does so while $x \neq i$ . Because $k \neq i$ ,program $k$ never falsifies

The assignment $z = i$ is executed under $S.i \land b.i \land y \neq 0 \land x = i$ , hence establishes $P.i$ . Next we have to verify that program $k$ does not falsify $P.i$ .

(i) Program $k$ does not falsify. s.i since $k \neq i$ . (ii) Program $k$ does not falsify $y \neq 0\;$ on account (iii) Program $k$ does not falsify $z = i$ ,since its $z = k$ is executed under s.k A b.k A $x = k$ , which, on account of (6) implies ? P.i since i≠k. (iv) Program $k$ does not falsify $H.i$ because, firstly, it does not falsify b.i. since $i \neq k -$ , and, secondly, falsification of $(x = i \lor 7.s.x)$ does not occur: $x := k$ is harmless since it establishes $7.s.x$ , and truthification of $s.x$ is ruled out under $y \neq 0$ .

(v) Program $k$ does not falsify $y = i \land W$ since, firstly, the precondition of $y \mathrel{\text{:=}} k$ implies $\neg W$ and, secondly, $W$ is only falsified under $y = 0$ .

Statement (A h : i f ¬b.h → skip fi) establishes for each program $h$ (i included) in some irrelevant order ¬b.h and hence the weaker ¬(b.h ∧ s.h) v y≠i . Falsification of the first disjunct only occurs under $y = 0$ , which implies the second disjunct, while no program k falsifies $y \neq i$ . Hence the quantified statement establishes the stable $W \vee y \neq i$ .

From the annotation we now see that the test $y = i$ establishes $(s.i \land (W \lor y \neq i)) \land y = i$ , i.e. $s.i \land W \land y = i$ , which on account of (2) and $i \neq 0$ implies $P_{i}$ .

On account of (5), this concludes the proof

The above program has been extracted from

$$ \text {s t a r t :} \langle b [ i ] := \text {t r u e} \rangle ; $$

$$ \langle x := i \rangle ; $$

$$ \text {i f} \langle y \neq 0 \rangle \text {t h e n} \langle b [ i ] := \text {f a l s e} \rangle ; $$

$$ \text {a w a i t} \langle y = 0 \rangle ; $$

$$ \text {g o t o s t a r t} f; $$

$$ \langle \boldsymbol {y} := i \rangle ; $$

$$ \text {i f} \langle x \neq i \rangle \text {t h e n} \langle b [ i ] := \text {f a l s e} \rangle ; $$

$$ f o r j := 1 t o N d o a w a i t (\neg b [ j ]) o d; $$

$$ \text {i f} \langle y \neq i \rangle \text {t h e n a w a i t} (y = 0); $$

$$ \begin{array}{l} \text {g o t o s t a r t f i f ;} \end{array} $$

$$ c r i t i c a l \quad s e c t i o n; $$

$$ \langle \mathbf {y} := 0 \rangle ; $$

$$ \langle b [ i ] := f a l s e \rangle $$

as quoted from "A Fast Mutual Exclusion Algorithm", Op.71 of Leslie Lamport. An ingenious solution!

One Tuesday afternoon I presented this extract - but still with the guard $x \neq i$ instead of true - to the ATAC, and we looked at it without much result; and privately I have done so.

At a next session Jayadev Misra presented to the ATAC the outline of the above assertional proof. He and K. Mani Chandy - who may have been involved in its design, I don't know- strongly felt that their experience in "desequentialization" of algorithms should provide the guidance for the introduction of the appropriate thought variables. And so it did! (The introduction of z , however, is food for further thought.)

At that session a (slightly weaker) simplification

It then took me another five hours of lying all loose ends together and smoothing the arguments to write down the above. (In the mean time I have learned to accept as quite normal that, after the core of the work has been done, the manuscript still requires somewhat over an hour per page: on the average no more than a few words or a formula per minute is a quite respectable output rate. People that have never actually observed their output rate usually have an entirely erroneous idea of the ergonomics of manuscript production and firmly believe that the mechanics of getting the characters on paper plays a major role. Quod non.)

Finally we note that the tests for $x = i$ and $y = i$ are used quite similarly. They share the property that their negations $x \neq i$ and $y \neq i$ are not falsified by program $k$ ; in both cases we find the appropriate negation as disjunct in the precondition of the test, and the condition itself as conjunct in the postcondition - be it that $x = i$ is replaced by $z = i$ .

Austn, 20 November 1985

prop. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 USA