Misra’s weakest fair buffer

Misra's weakest fair buffer

To begin with, we are interested in functions $f$ of type nat $\rightarrow$ nat that are involutions -i.e. are their own inverses - and have no fixpoints, i.e.

(0) $\left\langle {\forall n : \left( {{f}{0}f}\right) .n = n \land {f}{1}n \neq n}\right\rangle$

Because $f.p = q \Rightarrow f.q = p \land p \neq q$ , function $f$ partitions the natural numbers into pairs $\left( {p,q}\right)$ of distinct values: in English, the "meaning" of $f$ would be "the partner of" or "the other". Function $f$ de- ternines the partitioning into pairs; con- versely, the partitioning determines $f$ .

We say that a program generates $f$ if it generates all pairs $\left( {p,q}\right)$ satisfying

$M.p,q \equiv p = q \land p < q$

We shall consider separately generating

can generate any function $f$ satisfying (0).

The program that generates the $(p,q)$ pairs in the order of increasing $p$ is straightforward. The first conjunct of the invariant, which relates a local variable to the amount of output generated is of an absolutely standard structure

Po: $\langle \forall p,q : M.p.q \land p < n \equiv \left( {p,q}\right)$ has been generated $}$ ; it is initially,when nothing has been generated, established by $n = 0$ ,and the desired answer will be generated by increasing n under invariance of Po .

In order to control that the pairs generated form a partitioning of the natural numbers, the second conjunct links a local variable - of type: Set of naturals- to the irrevocable commitments made beyond n, more precisely

${P}_{1} : \langle {\forall q} : f \cdot q < n \land n \leq q \equiv q \in S\rangle$

it is initially established - with $n = 0$

The following program does the job

11 var n: nat = 0; var S: Set of nat = $\phi$

$\therefore$ do $n \in S \rightarrow S \mathrel{\text{:=}} S - { n} ;n \mathrel{\text{:=}} n + 1$

[ \cap n \notin S \rightarrow \left\lbrack {\operatorname{var}r : \text{nat}}\right\rbrack ]

$$ ; \text {s o l v e} r: n < r \land r \notin S $$

$$ ; g e n e r a t e (n, r) $$

$$ ; \tilde {S} := S + {r }; n := n + 1 $$

]

[\frac{cd}{d}]

The algorithm's nondeterminacy is concentrated in the instruction to solve

r: n<r ∧ r∉S

Since $S$ is finite, constructing a solution is no problem; for the same reason the instruction to solve it is a statement of unbounded nondeterminacy, and thanks to this unbounded nondeterminacy, the program can generate any function $f$ .

But this is not the solution Jayadev Misra was interested in. When we identify with the natural numbers a sequence of events, we can associate with the pair

$\left( {p,q}\right)$ a message,put into the buffer at event no. $p$ ,and taken out of the buffer at event no. q . In our program these events are guarded by the mutually exclusive guards n $\notin S$ and $n \in S$ respectively,whereas for an unbounded buffer one would like the guards to be true and $S \neq \varnothing$ respectively -i.e. the only constraint being that you cannot take a message out of an empty buffer-.

We are now heading for a program that generates the (p,q) pairs in the order of increasing q . Again the elements in S correspond to the messages in the buffer , but instead of a q -the precise event number at which to leave the buffer - each element contains an index with the weaker connotation that the element with the smaller index leaves the buffer before the element with the larger index

The new Po is

$P{0}^{\prime } : \langle \forall p,q : M.p.q \land q < n \equiv {\prime }^{\prime }\left( {p,q}\right)$ has been generated

$$ n := 0 $$

Besides the local variable $S_{1}$ which is now of type Set of (nat, nat), there is a variable and used to ensure that each element entering the buffer gets a larger index than ever left the buffer. The new Pi is

${P}_{1}$

$\left\langle {\forall p : p < n \land n \leq f.p} \Rightarrow \left\langle {3j : \operatorname{ind} < j \land \left( {p,j}\right) \in S}\right\rangle \rangle$

It is initially established by $S,{ind} = \phi ,0$ .

The following program - Misra's, that is

If var n,ind : nat = 0,0

; var $S$ : Set of (nat, nat) do

[\text{I}\left\lbrack {\operatorname{var}\mathrm{r},\mathrm{i} : \mathrm{{nat}}}\right\rbrack \text{;}\ \text{; solve }\mathrm{r},\mathrm{i} : \left( {\mathrm{r},\mathrm{i}}\right) \in \mathrm{S} \land ]

$\left{ \begin{array}{l} ;\text{ generate }\left( {r,n}\right) \ \end{array}\right.$

I true

11 var i: nat

; solve i: ind $<$ i

$$ \begin{array}{l l} & \vdots \ & \mathrm {I I} \ & \mathrm {I I} \end{array} \quad \begin{array}{l l} & S := S + {(n, i) }; n := n + 1 \ & \mathrm {o d} \ & \mathrm {I I} \end{array} $$

With the guards not excluding each other, a new -and desired, see above- nondeter minacy has been introduced; progress re quires that it be resolved fairly, and this requirement suffices. Fairness of the buffer is now shown by showing that with some element (p,j) in S, only a finite number of selections of the first guaraded command is possible before (p,j) itself is removed from S. A slight complication is caused by the fact that several elements in S may have the same index, but it is overcome in the standard fashion by the lexical order on the pair

$$ j - i n d, \langle \underline {{N}} r: (r, i n d) \in S \rangle $$

and observing

(i) that it is bounded from below by

(0,0) as long as $\left( {p,j}\right) \in S$

(ii) it is decreased by the first alternative

(iii) it is left unchanged by the second alternative

To show that also the second program can generate any $f$ ,we resolve its nondeterminacy by replacing in the second alternative

(i) the guard true $n < f$ . (ii) the equation $\vdots$ in $d < i$ for instance the replacements, we can add the conjunct ind $\leq n$ to the invariant.

Austin, 3 December 1995

prof. dr. Edsger W. Dykstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78750-1188 USA