An assertional proof of a program by G.L.Peterson

An assertional proof of a program by G.L.Peterson.

Consider

program $p : { {Lp} = 0 ∧ 7\operatorname{inp}}$

[{L}{p}\text{,in}p \mathrel{\text{:=}} 1,\text{true};{ {P}{1} : {L}_{p} = 1 ∧ \text{in}p} ]

\begin{array}{l} L p, h o l d := 2, p; {P _ {2}: L p = 2 ∧ H p } \ i f ¬ i n q \rightarrow L p := 3 \ [ ] h o l d ≠ p \rightarrow L p := 3 \ f _ {i}; {P _ {B}: L _ {P} = 3 ∧ H _ {P} } \ \mathrm {C r i t i c a l S e c t i o n}; \ L p, i n p := 0, f a s e \ \end{array}

cd

with ${H}_{p} = \left( {\text{hold} = p \vee \text{hold} = q ∧ \text{Lq} = 2}\right) ∧ \operatorname{inp}$

and the "mirror" of the above with $\left( {p,p}\right)$ and $\left( {q,q}\right)$ in-

We observe that the above program $p$ cannot falsify ${Hq} : \left( {\text{hold} = q\vee \text{hold} = p ∧ \mathrm{{Lp}} = 2}\right) ∧$ ing for the following reasons

1) if cannot falsify ing 2) when it $\operatorname{falsi}\left( {p - q}\right)$ hold $= q$ ,if "verifies" hold $= p ∧ {Lp} = 2$ 3) it cannot falsify hold $= p ∧ {Lp} = 2 ∧$ ing ,since its truth implies that both guards of ${Lp} : = 3$ are false.

For reasons of symmetry, program $q$ cannot falsify Hp , which program p establishes at hold:=p . This establishes the validity of the local assertions. Since

\begin{array}{l} P _ {3} \wedge Q _ {3} = (L _ {q} = 3 \wedge H _ {p}) \wedge (L _ {p} = 3 \wedge H _ {q}) ⇒ \ (h o l d = p) \wedge (h o l d = q) = F \ \end{array}

mutual exclusion is guaranteed; (hold≠p) v (hold≠q) furthermore guarantees the absence of the danger of deadlock.

The above solution appears in "Myths about the mutual exclusion problem" (submitted to IPL) by G.L. Peterson (Department of Computer Science, The University of Rochester, Rochester, N.Y. 14627). I think it a very nice solution, much nicer than his justification for it. I quote from Peterson's paper

"The protocols of $P_{1}$ and $P_{2}$ are given in Figure 1. $Q_{1}$ and $Q_{2}$ are initially false and turn may start as either 1 or 2.

\begin{array}{l} 1 ^ {} \mathrm {t r i y i n g p r o t o c o l} \mathrm {f o r} P _ {1} ^ {} \ Q 1 := t r u e \ \end{array}

T U R N := 1

wait until not Q2 or $\operatorname{TURN} = 2$

Critical Section

$\left| \begin{array}{l} * \text{exit protocol for } P_{1}^{*} \end{array}\right|$

Q _ {1} := \mathrm {f a l s e}

\begin{array}{l} / ^ {} t r y i n g p r o t o c o l f o r P _ {2} ^ {} / \ Q 2 := \mathrm {f r u e} \ \mathrm {T U R N} := 2 \ w a i t u n t i l n o f Q 1 o r T U R N = 1 \ C r i t i c a l S e c t i o n \ / ^ {} e x i t p r o t o c o l f o r P _ {2} ^ {} / \ Q _ {2} := \mathrm {f a l s e} \ \end{array}

As can be seen, the algorithm has a very simple structure. This results in an easy proof of correctness. First, neither process can be locked out. Consider $P_{1}$ , it has only one wait loop, and assume it can be forced to remain there forever. After a finite amount of time, $P_{2}$ will be doing one of three general things: not trying to enter, waiting in its protocol, or repeatedly cycling through its protocols. In the first case, $P_{1}$ notes that $Q_{2}$ is false and proceeds. The second case is impossible due to turn being either 1 or 2. In the third case $P_{2}$ will quickly set TURN to 2 and never change it back to 1, allowing $P_{1}$ to proceed. For mutual exclusion, assume that both processes are in their critical sections at some point. They both could not have succeeded in their wait loops at the same time so one process had to be second. But the value of some variable must change between the tests, and the second process's last step before testing sets TURN to a value which causes it to wait. (End of quotation)

I did not demonstrate the absence of the danger of infinite overhaking. I should have added to that purpose "Since program $p$ cannot falsify $Hq$ , it cannot overtake program $q$ in $Q2$ , since $(Hq ∧ \mathrm{hold} = p) ⇒ L_p = 2$ .

Peterson continues his text with "Since the more complex algorithms naturally require more complex

proofs, one wonders whether the prevalent attitude on "formal" correctness arguments is based on poorly structured algorithms. Perhaps good parallel algorithms are not really all that hard to understand.

I am very much tempted to rephrase the last sentence as "Perhaps good parallel algorithms are not really all that hard to prove to be correct." (and then it could be observed that that statement could be interpreted as my definition of "good"). I must assume to be -like everyone else - biased by my past experience. On account of my past experience with operational arguments a la Peterson, I was most unhappy with his "justification" (which, even if I could reproduce it, I would not dream of presenting to my students). I liked Peterson's solution so much that I felt that it deserved an equally nice correctness proof a la Gries-Owicki, and I was very pleased when I found it. (I was badly out of training: it took me disgracefully long to design it!) It makes two things abundantly clear: firstly why the order of setting "in" and "hold" is relevant, and, secondly, why the order of testing "in" and "hold" - individually! - is irrelevant. Note that the one program "wails until" a condition which, when found true by the one program, may immediately be falsified by the other!

Pbalaansraa 5

5671 AL NUENEN

The Netherlands

26 February 1981

p r o f. d r. Eds g er W. Dg ksha

Burroughs Research Fellow.