On an argument by J.A. Carruth & J. Misra

On an argument by J.A. Carruth & J. Misra

In [0], Carruth & Misra start the analysis of the last case with

"● Executing $\gamma$ ,i≠k: We show that ${\neg }{{d}{k}}$ is a precondition for the execution of $\gamma$ . Since the effective execution of $\gamma$ preserves ${\neg }{{d}{k}}$ , we have then ${\neg }{{d}{k}}v$ as a postcondition.

We prove that $\neg {d}{k}$ is a precondition by assuming ${d}{k}$ as a precondition and deriving a contradiction.

The first purpose of this note is to show that, had the authors stuck to the standard proof format for the proof obligations, they would never have come up with (so many rabbits and) a reductio ad absurdum.

Its second purpose is to polish - if not to correct - their use of the Axiom of As- signment.

The purpose of the proof part under consideration is to show that the preconditions of $\gamma$ for $i \neq k$ is at least as strong

as

To this end we may use

• the properties of "now", in particular

(0) $\overline{p} \leq {now}$ (for all variables $\overline{p}$ of the appropriate type).

the "timing constraints"

(1) ${c}{i} \Rightarrow {\bar{c}}{i} \leq 1 + {\bar{b}}_{i}$

for all i in the range concerned

(2) ${d}{i} \Rightarrow \overline{{c}{i}} \leq 1 + \bar{b}_{i}$

(3) $d_{i} \Rightarrow 1 + \bar{c}{i} < \bar{d}{i}$

the "invariants"

$x = k \Rightarrow \overline{{b}{i}} \leq {\bar{c}}{k}$

for all $i,k$ in the

(5) ${d}_{k} \Rightarrow x = k$

range concerned

the definition of $\gamma :$

(6) $\left{ {{\gamma }{i}}\right} {s}{i},x,{c}_{i} \mathrel{\text{:=}} c,i,{now}$

${if}{s}_{i} = b$

As we shall see shortly, x quickly disappears from our proof obligation; in anticipation we "eliminate" x from our givens by using (4) and (s) to conclude

(7) ${d}{k} \Rightarrow {\bar{b}}{i} \leq {\bar{c}}_{k}$

We now proceed by observing for $i \neq k :$

$$ \begin{array}{l} w p: r _ {i} \cdot (\neg d _ {k} v x = k) \ = {0 (6) } \ w p. (s _ {i}, x, \overline {{c}} _ {i} := c, i, n o w). (\neg d _ {k} \vee x = k) \ = {\mathrm {A x i o m o f A s s i g n e m e n t} } \ \end{array} $$

$$ \begin{array}{l} \begin{array}{l l l} \neg d _ {k} & v & c = k \end{array} \ = {\quad i \neq k } \ \lnot d _ {k} \ \Leftrightarrow { \begin{array}{l} (7); \ 3 \end{array} \mathrm {w i t h} i := k } \ \overline {{b}} _ {i} > \overline {{c}} _ {k} \quad \vee \quad 1 + \overline {{c}} _ {k} \geq \overline {{d}} _ {k} \ \Leftrightarrow {\mathrm {a r i t h m e t i c}; (0) ^ {n} \mathrm {w i t h} \overline {{p}} := \overline {{d}} _ {k} } \ 1 + b _ {i} > 1 + \overline {{c}} _ {k} \vee 1 + \overline {{c}} _ {k} \geq n o w \ \Leftrightarrow \quad {\text {t r a n s i t i v i t y} ^ {\prime} \geqslant , > } \ 1 + \overline {{b}} _ {i} \geq n o w \ \end{array} $$

In order to establish that the precondition of $\gamma_ {i}$ implies the latter inequality, the authors argue - here one should know

that ${c}{i}$ is short for ${s}{i} = c -$

"Following the execution of $\gamma_{i}$ , timing constraint (Ti) holds, i.e.,

$$ (T _ {i}) \quad (c _ {i} \vee d _ {i}) \Rightarrow \overline {{c}} _ {i} \leq 1 + \overline {{b}} _ {i} $$

The effective execution of $\gamma_{i}$ sets $c_{i}$ to true and $\overline{c}i$ to now. Applying the axiom of assignment (to replace $c{i}$ by true and $\overline{c}_i$ by now)

$$ [ \dots ] \qquad n o w \leqslant 1 + \bar {b} _ {i} $$

holds prior to the effective execution of $\gamma_{i}$ (Note that their $(T_{1})$ is the conjunction of our (1) and (2).)

I would like to point out that from the

fact that $P$ holds after the execution of $S$ we are not allowed to conclude that

$\omega_{P}$ S.P

holds prior to the execution of S! From the fact that P holds after the execution of S, we are only allowed to conclude that the execution of S is guaranteed not to establish $\neg P$ ; we are allowed to conclude that

1. ${wp}.S.\left( {vP}\right)$

holds prior to the execution of S. Failing to distinguish between wp.s and its con- jugate (wp.S)* is a common source of flaws in mixed postulated/operational arguments; A.D. 1992, both authors should have known better than to mix these two types of arguments. Timing constraint (2) is superfluous.

[0] Proof of a Real-Time Mutual-Exclusion Algorithm, Notes on UNI TY: 32-92, by John Allen Carruth & Jayadev Misra, Sep10.1992

Austin, 28 April 1994

p r o f. d r. Eds g er W. Dg kstra D epart ment of C o mputer S cience The University of Texas at Austin Austin, TX 78712-1188 USA