For the record: Batcher’s Baffler

For the record: Batchers Baffler

In this note we consider a special sorting routine for array $f(i:0\leq i < N)$ . Predicate OK is given by

$$ O K. i j \equiv f _ {i} < f _ {j}; $$

quantificatons over OK.i.j are implicitly constrained

$$ \begin{array}{l} b y \ 0 \leq i < j < N \ \end{array} $$

The functional specification of Batcher's Baffler is

[\left\lbrack {N : \operatorname{int}{ N \geq 0}\right\rbrack ]

$\therefore \operatorname{I}\left\lbrack {f\left( {i : 0 \leq i < N}\right) : \text{array of}\operatorname{int}\left{ {{bag}.f = B}\right} }\right\rbrack$

; Batcher's Baffler

$$ {b a g. f = B \wedge (A i: O K. i. (i + 1)) } $$

1

1

From now on we no longer mention the invariance of $\operatorname{bag}f = B$ ; it is trivially maintained as the algorithm only manipulates array $f$ by means of the operation Ord given by

$$ O r d. i j = \mathrm {i f} O K. i j \rightarrow s k i p ] \rightarrow O K. i j \rightarrow s w a p. P. i j $$

• the swap interchanges the values of ${P}{i}$ and ${f}{j} -$ . The ord operation satisfies ${$ true $}$ Ord.i.j. ${ 0\left( {i,j}\right)$ ; quantifications over it are again implicitly constrained

There are many ways of expressing our postcondition that $f$ is ascending, but this one is a nice starting point for the invariant

${P}{0} : \;\left( {{A}{i} : {OK}.i\left( {i + t}\right) }\right)$

which suggests for Batcher's Baffier the form

"establish $t \geq N$ " (Po)

Let the decrease of t under invariance of Po involve the transition from $t = t^{\prime}$ to $t = t^{\prime \prime}$ with $t'' < t'$ . It would be nice if we could exploit the precondition $(\bar{A} i: O K. i.(i + t'))$ by keeping it invariant; we can only hope to do so provided it is implied by the postcondition $(\bar{A} i: O K. i.(i + t'))$ , i.e. provided $t^{\prime \prime}$ is a factor of $t'$ . Under that constraint, the most modest decrease of t -i.e. the one that strengthens Po as little as possibl - is halving t , and therefore we suggest to restrict t to powers of 2 . (The confirmation of the wisdom of this choice will come later.)

Our next approximation of Batcher's Baffler gives explicitly the manipulations on $t$ :

$$ \begin{array}{l} t := 1; \mathrm {d o} t < N \rightarrow t := 2 \cdot t \mathrm {o d} {P _ {0} \wedge t \mathrm {i s a p o w e r o f} 2 } \ \frac {d o}{d t} \neq 1 \rightarrow t := t / 2 \ ; {P _ {1}: (\underline {{A}} i: O K, i. (i + 2 \cdot t)) } \ " r e s t o r e P o " \ {P _ {0}: (\underline {{A}} i: O K, i. (i + t)) } \ \end{array} $$

ad

The rest of this note is concerned with the algorithm for "restore $P_0$ " as specified by its pre- and postconditions in the last approximation. (For this subalgorithm it is no longer relevant that it is a power of 2).

The design of Bather's Baffler is driven by the desire of finding groups of Ord operations with disjoint argument pairs, because such Ord operations could be executed concurrently. As each Ord operation establishes the corresponding OK relation, we are in- vited to try to partition the OK relations in the postcondition Po such that the argument pairs in each group are disjoint. This is achieved by writing Po as P2 P3 with

${P}{2} : \;\left( {{A}{i} : e.i : {OK}.i.\left( {i + k}\right) }\right)$ and

${P}_{3} : \;\left( {\underline{A}i;\gamma e.i;\;{OK}.i.\left( {i + k}\right) }\right)$

provided we can find a predicate such that

$$ e. i \equiv \neg e. (i + t) $$

There are many such predicates, all variations on the same theme. The simplest is

$$ e. i \equiv (i \mod 2. t) < t $$

Remark. It is the factor of 2 in the above formula that will justify our earlier choice to restrict t to powers of 2 . (End of Remark.)

Using II to denote the potentially concurrent combination, we have indeed

$$ {\mathrm {t r u e} } (1 1 i: e. i: O r d. i. (i + b)) {P _ {2} } \quad (0) $$

$$ {\mathrm {t r u e} } (\parallel i: \mathrm {r e . i : O r d . i . (i + t)}) {\mathcal {P} _ {3} } \tag {1} $$

But we cannot achieve $P_{2} \wedge P_{3}$ - i.e. $P_{0}$ by performing (0) and (1) consecutively (in some order), for in general the second one will destroy what the first one has accomplished. So we have to proceed more carefully, e.g. first establishing $P_{2}$ by means of (0) and then establishing $P_{3}$ with a repetition for which $P_{2}$ is an invariant, i.e. we may expect that repetition to establish $P_{2} \wedge P_{3}$ under invariance of $P_{2} \wedge P_{4}$ where $P_{4}$ is some generalization of $P_{3}$ .

Remark I did not fully check it, but my impression is that the choice just made is irrelevant, and that we could equally well have established P3 first. (End of Remark.)

For our analysis we rewrite - because it is slightly

${P}{3} : \;\left( {{A}{i} : e.i : {OK}.({i + 1}.}\right) .\left( {i + 2 \cdot i}\right) )$

and (1) as

$$ (\parallel i: e. i: O r d. (i + t). (i + 2 \cdot t)) \tag {1} $$

and ask ourselves under what further conditions the generalized operation

$$ \left(\left| i: e. i: \mathrm {o r d .} (i + t). (i + v \cdot t)\right) \quad \mathrm {w i t h e v e n} v\right) \tag {2} $$

maintains ${P}_{2}$ . (Parameter $v$ is constrained to even values so as to ensure that the argument pairs are disjoint.) In our analysis we shall use the lemmata and -grudgingly- The notation of EWD932 b.

(i) The OK relations of $\mathcal{P}2$ with no argument involved in an Ord operation of (2) are maintained on account of Lemma 0. (ii) Of the OK relations of $P2$ with one argument in-

neither of which, however, is a lemma. But

represent Lemma 3. Note that, $v$ being even, the two OK relations added are implied by $P_1$ . (Here we are getting our first glimpse of how to exploit precondition $P_1$ .)

(iii) Finally we investigate the OK relations of $P2$ with both arguments involved in an Ord operation of (2): with e.i

This, again, is not a lemma, but we can recognize

Two of the added OK relations are again implied by

$$ (A _ {i}: e. i: O K. (i + t). (i + 2 \cdot v \cdot t)) $$

tells us that (2), which eo ipso establishes

${P}{4} : \;\left( {{A}{i} : e.i : {OK}.({i}^{2} + t).({i}^{2} + v \cdot t)}\right)$

when preceded by $v \coloneqq v / 2$ mainfains -besides $P_2$ - $P_4$ as well. As $P_4 \wedge v = 2 \Rightarrow P_3$ ,

$$ P _ {4} \wedge v \geq 2 \wedge v i s a p o w e r o f 2 $$

is the proper invariant under which repeated execu-tion of (2) can establish P3 without falsi- lying P2 ; it can be initialized by establishing v.t. N. Under the as yet unverified assumption of Pi's validity in the precondition of (2) we would get the following text for Batcher's Bafier:

$$ [ t, v _ {0}: \mathrm {i n t}; \underline {{d o}} t < N \rightarrow t := 2 \cdot t \underline {{o d}}; v _ {0} := 1 {P _ {0} \wedge t \cdot v _ {0} \geq N } $$

$$ ; \underline {{d o}} t \neq 1 \rightarrow t, v 0 := t / 2, 2 * v 0 \left{P _ {1} \wedge t \cdot v 0 \geqslant N \right} $$

$$ j (1 1 i: e. i: O r d. i (i + t)) {P _ {1} \wedge P _ {2} \wedge t \cdot v o \geq N } $$

$$ ; \llbracket v: i n t; v := v 0 {P _ {1} \wedge P _ {2} \wedge P _ {4} } $$

$$ ; \underline {{d o}} v \neq 2 \rightarrow v := v / 2 \left{\rho_ {1} \wedge \rho_ {2} \wedge \rho_ {4} ^ {v} _ {2 \cdot v} \right} $$

$$ ; (1 1 i: e. i: O r d. (i + t). (i + v. t)) {P _ {1} \wedge P _ {2} \wedge P _ {4} } $$

$$ \mathrm {o d} {P _ {2} \wedge P _ {4} \wedge v = 2 } $$

$$ ] \left{P _ {0} \wedge + v _ {0} \geqslant N \right} $$

$$ \mathrm {o d} {P _ {0} \wedge t = 1 } $$

$$ ] 1) \left{(\underline {{A}} i: O K. i. (i + 1)) \right} $$

EWD935a-6

We are left with the obligation of verifying that neither (0) nor (2) falsifies

${P}_{1} : \left( {\underline{A}i : {Ok}.i.\left( {i + 2 \cdot t}\right) }\right)$

Operations (0) and (2) are of the form

(II: p.i.: Ord. i. (i + m. t)) (3)

with $p.i \equiv e.i\;$ or $p.i \equiv 7.e.i\;$ and ${odd}m\;$ . We shall verify the invariance of ${P}_{1}$ under (3).

(i) The OK relations of $P_{1}$ with no argument involved in an Ord operation of (3) are maintained on account of Lemma 0. (ii) Of the OK relations of $P$ with one argument involved in an Ord operation of (3) we have two types:

$\left( {i + \left( {2 + m}\right) \cdot t > N}\right)$

(i-m.t<0)

Fortunately they represent Lemma 1b and i a respectively.

(iii) OK relations of $P$ with both arguments involved in an Ord-relation of (3) are of the types:

This, fortunately, is Lemma 2, and thus Pi's invariance under (3) has been demonstrated.

And this completes my treatment of Batcher's

This algorithm was invented by K.E. Batcher in 1968 and brought to my attention by David Gries, who invented its name and proved its correctness, in essence along the same lines but in a very different presentation. Besides considerable notational differences the main distinctions of this presentation are

(i) the isolation of the Lemmata as in EwD932 b, (ii) the amount of heuristics included.

It is worth noting that Lemmata O through 4 of EWD932 b have all been used. Lemma 5 - which is more or less an extra - is followed in EWD932 b by precisely the sorting process that Batcher's Baffler would generate for $N = 4$ .

Finally I would like to draw attention to the considerable benefit we derived from the convention introduced right at the beginning of implicitly constraining the arguments of OK and similarly of Ord.

I am endebt to David Gries and to the Tuesday Afternoon Clubs of Eindhoven and of Austin.

Austin 18 September 1985

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