Proving Correctness for Balancing Networks

Balancing networks have recently been proposed by Aspnes, Herlihy and Shavit (Proc. of the 23rd Annual ACM Symp. on Theory of Computing, pp. 348--358, May 1991) as a new class of distributed, lowcontention data structures suitable for solving a variety of multi-processor coordination problems that can be expressed as balancing problems. In a recent work (Proc. of the 13th Annual ACM Symp. on Principles of Distributed Computing, pp. 206--215, August 1994), Busch and Mavronicolas develop a mathematical theory of the combinatorial structure of balancing networks. In this work, a paradigmatic methodology for showing correctness of balancing networks is developed as a direct consequence of this combinatorial theory. This methodology is applied to yield a transparent correctness proof for the bitonic counting network introduced by Aspnes et al., whose layout is isomorphic to that of the classical, bitonic sorting network of Batcher; our proof provides an interesting complement to the one ..