A heuristic explanation of Batcher’s Baffler

Copyright Notice

The manuscript

EWD 953a: A heuristic explanation of Bachers's Baffler was published as

Science of Computer Programming 9: 213-220, copyright © 1986. It is reproduced here by permission of the publisher, Elsevier Science. Single copies of the manuscript may be downloaded and printed for the reader's personal research and study.

A heuristic explanation of Batcher's Baffler

by Edsger W. Dijkstra *

Abstract Batcher's Baffler - so named by David Gries- is a sorting algorithm that is of interest because many of its "comparison swaps" can be executed concurrently. It is also of interest because it used to be hard to explain.

This note explains Batcher's Baffler by designing it. Besides including all heuristics, it has two distinguishing features, both contributing to its clarity and brevity:

(o) the (little) theory the algorithm relies upon is dealt with in isolation; (1) by suitable abstractions, all case analyses have been removed from the argument.

*) Author's address:

Department of Computer Sciences The University of Texas at Austin. Austin, TX 78712 - 1188 United States of America

Batcher's Baffler - so named by David Gries [1] after K.E. Batcher [0], who published his design in 1968-- is a sorting algorithm. Its building block treats a set of disjoint pairs of elements, swapping each pair of values that is out of order; the pairs of the set being disjoint, they will be treated as if dealt with concurrently. Since eventually all pairs have to be in order, we are interested in theorems about sets of "comparison swaps" that maintain for some other pairs the fact that they are already in order.

We shall present the relevant lemmata graphically. A dotted arrow $x \rightarrow y$ stands for the comparison swap

$$ x, y := x \min y, x \max y $$

a solid arrow $x \rightarrow y$ stands for the relation

$$ x \leq y $$

The graphs representing our lemmata should be read as follows: if the inequalities corresponding to the solid arrows initially hold, they are maintained by the execution of the comparison swaps corresponding to the dotted arrows (whose inequalities eventually hold as well).

Lemma 0

Proof According to the axiom of assignment, the postcondition $a \leq b \land A \leq B$ is guaranteed by the precondition

a min A < b min B a max A < b max B , which is implied by the initial asb A s B (End of Proof.)

Lemma 1

Proof The four solid arrows are together equivalent to $a\max A \leq b\min B\;;$

this relation is maintained by (each of) the operations corresponding to the dotted arrows, since the values of both its sides remain unaffected. (End of Proof.)

So much for the little theory we need.

*

*

*

Our purpose is to sort array $f(i: 0 \leq i < N)$ in increasing order. For simplicity's sake, this finite array is mentally extended in both directions to infinity:

$$ i < 0 \Rightarrow f _ {i} = - c ^ {\prime \prime} \quad a n d \quad i \geq N \Rightarrow f _ {i} = + c ^ {\prime \prime} $$

For brevity's sake, we introduce the transitive predicate OK given by ${OK} \cdot i.j \equiv {p}{i} \leq {p}{j}\;$ ;

note that, thanks to the array extension, we have

$$ i < 0 \vee j \geqslant N \Rightarrow O K. i. j $$

Our purpose is to establish relation $R$ given by

$$ R \equiv (\underline {{A}} i: O K. i. (i + 1)) $$

by rearranging the values in $f(i:0 \leq i < N)$ . (The advantage of the array extension is that the above universal quantification is over all integers, i.e. that we don't need to bother anymore about subscript bounds.)

The algorithm will manipulate array $f$ only by means of the operation $\operatorname{Ord}$ given by

$$ \begin{array}{l} O r d. i j = i f O K. i j \rightarrow s k i p \ \mathrm {I} \neg \mathrm {O K}. i. j \rightarrow p _ {i}, p _ {j} := p _ {j}, p _ {i} \ \frac {p _ {i}}{L} \ \end{array} $$

Operation Ord. i. j establishes OK. i. j ; note that, thanks to the array extension, we have

$$ i < 0 \vee j \geqslant N \Rightarrow \operatorname {O r d .} i, j = s k i p $$

independently of the values in $f\left( {i : 0 \leq i < N}\right)$ . The algorithm will invoke Ord. i. j only with $i < j$ , thus ensuring that the sequence $f\left( {i : 0 \leq i < N}\right)$ remains a permutation of its initial value.

After these preliminaries we can begin with the design of the algorithm. In view of $\mathcal{R}$ we choose as invariant $\widetilde{\mathcal{P}}_0$ , given by

$$ P O \equiv (\mathrm {A i}: O K, i. (i + 1)) $$

which is easily established since $t \geq N \Rightarrow {P}{0}$ . Since -by construction!- ${P}{0} \land t = 1 \Rightarrow R$ ,our choice of invariant suggests for Batcher's Baffler the form

$$ \begin{array}{l} " e s t a b l i s h \quad t \geq N ^ {\prime} {P o } \ ; \underline {{d o}} + \neq 1 \rightarrow " r e d u c e + u n d e r \ i n v a r i a n c e o f P o ^ {\prime \prime} \ \operatorname {o d} {R }. \ \end{array} $$

The guiding principle of our development is that, once an OK relation has been established, it will be maintained. This means that, if "reduce $t$ under invariance of $P_0$ " involves the transition from $t = t'$ to $t = t''$ , we require $t'$ and $t''$ to satisfy

$$ (\neg i: O K. i. (i + t ^ {\prime})) \Rightarrow (\neg i: O K. i. (i + t ^ {\prime})) $$

an implication whose validity requires (in view of

OK's transitivity) t" to be a divisor of t'. Under that constraint the most modest decrease of t -i.e. the one that strengthens Po as little as possible- is halving it. We propose to reduce t by halving it (and, hence, to restrict t to powers of 2). (Note that, at this stage of our analysis, this proposal is tentative; its wisdom, however, will transpire shortly.)

Explicit incorporation of the manipulation of t yields for Batcher's Baffler a program of the form

$$ t := 1; \underline {{d o}} t < N \rightarrow t := t \cdot 2 \underline {{o d}} {P 0 \wedge (t \text {i s a p o w e r o f} 2) } $$

$$ ; \underline {{d o}} f \neq 1 \rightarrow t := t / 2 {P _ {1} } $$

$$ ; " r e s t o r e P o" {P o } $$

$$ \operatorname {o d} {R } $$

with ${P}_{1}$ given by

$$ P _ {i} \equiv (\underline {{A}} i: O K. i. (i + 2 \cdot t)) $$

The rest of this note is concerned with the development of the subalgorithm for "restore $\mathsf{P}0$ " as specified by pre- and postcondition:

$$ {P _ {1} } " r e s t o r e P _ {0}" {P _ {0} } $$

(For this subalgorithm it is no longer relevant that $t$ is a power of 2.)

The design of Batcher's Baffler is driven by the desire to find sets of Ord operations with disjoint arguments because such Ord operations can be executed concurrently. Since each Ord operation establishes the corresponding OK relation, we are invited to consider - as our sweetly reasonable "units of establishment", so to speak - conjunctions of OK relations with disjoint arguments. Is it, for instance, possible to write postcondition $P_0$ as $P_2 \land P_3$ such that in each of $P_2$ and $P_3$ the OK relations have disjoint arguments?

We can ensure ${P}{0} \equiv {P}{2} \land {P}_{3}$ with

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

${P}_{3} \equiv \;\left( {A;{7e}.j : {Ok}.i.\left( {i + t}\right) }\right)$

with any boolean function $e$ . Requiring the OK relations in ${P}_{2}$ to have disjoint arguments boils down to requiring

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

For $P_{3}$ the analogous requirement is

${ae}.i \Rightarrow e.\left( {i + t}\right)$

Combining the two requirements, we conclude that with e satisfying

(0) $e.i \equiv \neg e.\left( {i + t}\right)$

$P_{2}$ and $P_{3}$ can each be established by a set of concurrent Ord operations. From now on, e denotes a predicate satisfying (o). Note that there are many such predicates, all variations on the same theme; the simplest one is

(1) $e.i \equiv \left( {i{\;\operatorname{mod}\;2} \cdot + }\right) < t$

Remark It is the factor 2 in the above formula that will justify our earlier choice of reducing $t$ by halving it. (End of Remark.)

Using II to denote the potentially concurrent combination of statements, we define S2 and S3 by

S2: (1i: e.i: Ord.i.(i+ t)) and

S3: (11i: 7 e.i.: Ord. i. (i+1))

Remark In these quantifications, i ranges over infinitely many values, but this presents no unsurmountable implementation problems since Ord. i. (i+1) differs from skip for only a finite number of values of i . (End of Remark.)

Statement S2 establishes P2 and statement S3 establishes P3, but we cannot establish P2 $\wedge$ P3 - i.e. PO- by performing S2 and S3 (in some order) consecutively,

for in general the second one will destroy what the first one has established. So after the execution of the first one, we have to proceed more carefully.

Let "restore $P_0$ " start with $S_{2}$ establishing $P_{2}$ . This choice of $S_{2}$ is irrelevant since - see (o)- we are free to call either polarity of the partitioning predicate e. Proceeding from thereon "more carefully" means establishing $P_{3}$ while maintaining $P_{2}$ . The alternative to establishing $P_{3}$ directly (i.e. by $S_{3}$ ) is establishing $P_{3}$ by means of a repetition with some invariant $P_{4}$ , where $P_{4}$ is a suitable generalization of $P_{3}$ ; our purpose is to construct that repetition such that it has the stronger $P_{2} \wedge P_{4}$ as invariant.

Before proceeding we rewrite $p_3$ for simplicity's sake in such a way that its dummy is controlled by the same range as the dummy in $p_2$ . In view of (0), we can do so by renaming (with $i + t$ replacing $i$ ):

$$ P _ {3} \equiv (\underline {{A}} i: e. i: O K. (i + t). (i + 2 \cdot t)) $$

We generalize $P_{3}$ by replacing the constant 2 by the variable $u$ , i.e. we propose

$$ P _ {4} \equiv (\underline {{A}} i: e. i: O K. (i + t). (i + u \cdot t)) \quad \mathrm {w i t h e v e n} u. $$

The latter constraint on u ensures that the OK relations in $P_4$ are disjoint so that $P_4$ can be established by S4 , given by

S4: (11i: e.i: Ora, (i+1). (i+u. t))

In view of our aim that the stronger $P_{2} \wedge P_{4}$ be an invariant, it now stands to reason to investigate under which conditions S4 main-tains $P_{2}$ . That is, for i satisfying e.i we have to investigate the fate of OK.i.(i+ t); on account of (o) and because u is even, this is the same as investigating the fate of OK. (i+ u+ t). (i+ u+ t + t) for any i satisfying e.i. With its incident Ord operations from S4 it yields the picture -nodes now being labelled by subscripts

which is certainly not a lemma, but we can recognize the sequence $\rightarrow \rightarrow \rightarrow \rightarrow$ in Lemma1, redrawn for the purpose:

Of the three solid arrows added, the two horizontal ones are implied by $P_{1}$ because $u$ is even and the OK relation is transitive. The third one is implied by $P_{4}(2 \cdot u / u)$ . (Here we have used the notation "R(E/x)" for the expression R in which E has been substituted for x.) In other words, for statement S4 we have established the theorem

$\left{ {{P}{1} \land {P}{2} \land {P}{4}\left( {2 \cdot u/u}\right) }\right} \sim \left{ {{P}{2} \land {P}_{4}}\right}$

Remembering that for the design of "restore $P_0$ " we could rely on the precondition $P_1$ and taking the invariance of $P_1$ for the time being for granted, we see from our last theorem, since - by construction -

[{P}{4}\; \land u = 2 \Rightarrow {P}{3}]

that we can establish $P_{3}$ under invariance of $P_{2}$ by first establishing $P_{4}$ with $u$ equal to a sufficiently high power of 2 , and then repeatedly halving $u$ while each time main-. taining $P_{2} \land P_{4}$ by an execution of S4 .

Thus the fully annotated version of "restore

$$ \begin{array}{l} {P _ {1} } S _ {2} {P _ {1} \wedge P _ {2} } \ ; u := \mathrm {s u i t a b l e p o w e r o f 2} ^ {\prime \prime} {P _ {1} \wedge P _ {2} \wedge P _ {4} } \ ; \underline {{\underline {{d o}}}} u \neq 2 \rightarrow u := u / 2 {P _ {1} \wedge P _ {2} \wedge P _ {4} (2 \cdot u / u) } \ ; S 4 {P _ {1} \wedge P _ {2} \wedge P _ {4} } \ \mathrm {o d} \left{P _ {2} \wedge P _ {4} \wedge u = 2, \mathrm {h e n c e} P _ {0} \right}. \ \end{array} $$

We are left with two obligations: determining a "suitable power of 2" and showing the invariance of $P_{1}$ .

Since

$$ u + - t \geq N \Rightarrow (\underline {{A}} i: O K. (i + t). (i + u +)) $$

and the consequent implies $P\& a$ u satisfying the antecedent would do the job. With for e the specific choice (1), the weaker u.t ≥ N will do because

$$ \begin{array}{l} u + \geq N \ \Rightarrow \quad {\mathrm {c o n s i d e r} i < - t, - t \leq i < 0, 0 \leq i } \ (A i: i + t < 0 v \neq e. i v i + u \cdot t \geqslant N) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (A i: e. i: i + t < 0 v i + u o + \geq N) \ \Rightarrow {\mathrm {b y t h e e x p e n s i o n t o a n i n f i n i t e a r r a y} } \ (A i: e. i: O K. (i + t). (i + u \cdot t)) \ = {\mathrm {d e f i n i t i o n} o p P _ {4} } \ p _ {4} \ \end{array} $$

Finally we have to show that $P_{1}$ , i.e.

$$ (\mathrm {A i}: \mathrm {O K}, \mathrm {i}. (i + 2 \cdot t)) $$

is maintained by S2 and by S4 . The latter two are both of the form

$$ (1 1 i: p. i: O r d. i. (i + m \cdot t)) $$

with odd $m$ and $p,i \equiv e.i$ or $p,i \equiv 7$ e.i.,i.e. with

$$ p. i \equiv - p. (i + m \cdot t) $$

Hence, each OK relation of ${P}_{1}$ occurs once as a solid arrow in the following diagrams with i satisfying p.i :

In this diagram, we recognize Lemma 0; hence neither S2 nor S4 falsifies $P_{1}$ . This concludes our heuristic explanation of Batcher's Baffler.

Concluding Remarks

Several aspects of the above are worth noting.

For the expression $\beta_{i} < f_{j}$ we introduced the transitive predicate OK.i.j "for brevity's sake. More important than the physical abbreviation is that in the notation OK.i.j we only retained what matters in the sequel, viz. the two index values; not only the re-ferences to $f$ , but -more importantly- the subexpressions $\beta_{i}$ and $f_{j}$ have disappeared; so has the relational operator $\leq$ , and rightly so, for we could have wished to sort in descending order.

The way in which the invariants have been derived from the postconditions -P0 from R and P4 from P3 - is absolutely standard; it is known as "replacing a constant by a variable". The choice of which constant is to be replaced by a variable is usually severely constrained by the requirement that we can think of an initial value for that vari- able with which to establish the invariant.

We have introduced two variables, $t$ and $u$ , constrained to be a power of 2. We could have been more explicit by representing in our analysis their values by $2^{h}$ and $2^{k + 1}$ respectively,

i.e. we could have introduced the natural variables $h$ and $k$ instead. It seems a minor notational variation, but I would like to point out that if makes all the difference. The difference is not so much that the identifiers $t$ and $u$ are shorter than the alternatives ${2}^{h}$ and ${2}^{k + 1}$ .

The difference is that with the latter notation their being a power of 2 would have permeated all through our formalism, even where their being a power of 2 had not yet been decided or did no longer matter. The nomenclature provided by t and u enables us to do justice to the latter disentanglement of the argument.

The extension of the finite array to an infinite one was presented as a way of simplifying the postcondition and the intermediate assertions, but note that it has bought us much more. Without it, our two lemmata would not have sufficed and our invariance proofs would have been burdened by case analyses to take care of all sorts of boundary effects due to "missing elements".

The extension to an infinite array has also protected us from the introduction of expressions like

and from the suggestion $\overrightarrow{that}$ the algorithm is really de- signed for $N$ of the form ${2}^{n}$ .

Acknowledgements

I am first and foremost indebted to four persons:

I am indebted to K.E. Batcher for having designed this ingenious algorithm. I am indebted to D. Gries for drawing my attention to this algorithm by sending me a manuscript in which this algorithm was explained and proved to be correct. In the above I have followed his way of breaking down the invariant. - I am indebted to C.S. Scholten for simplifying my original derivation by extending the finite array to an infinite one. I am indebted to A.J.M. van Gasteren for raising my standards of disentanglement, for making me more aware of the issues involved, and for teaching me the relevant techniques.

Without these four persons, the above heuristic explanation would not have been written.

Finally I mention in gratitude my opportunity of presenting (in successive stages) my explanation to about half a dozen audiences, for each time my audience did not act as sponge but as whetstone. I also thank the referees.

[0] K.E. Batcher, "Sorting networks and their applications", Proc. Spring Joint Computer Conference, 1968 [1] D. Gries, Private Communication