Automated reasoning about parallel algorithms using powerlists

Misra [8] recently introduced a regular data structure, called powerlists, using which he showed how many data parallel algorithms, including Batcher's merge sort, bitonic sort, fast Fourier transform, prefix sum, can be described concisely using recursion. The elegance of these recursive descriptions is further reflected in deducing properties of these algorithms. It is shown in this paper how such proofs can be easily automated in a theorem prover RRL (Rewrite Rule Laboratory) based on equational and rewriting techniques. In particular, the cover set method for automating proofs by induction in RRL generates proofs which preserve the clarity and succinctness, to a large extant, of hand proofs given in [8]. This is illustrated using a correctness proof of Batcher's merge sort algorithm. Mechanically generated proofs from specifications ofpowerlists and parallel algorithms using different apl~roaches are contrasted. It is shown that one gets longer, complex proofs with many cases if powerlists are modeled as a subtype of lists. However, if powerlists are specified using a proposal by Kapur [2] in which the algebraic specification method is extended to associate applicability conditions with functions of a data type thus allowing constructors of a data structure to be partial, then one gets compact and elegant proofs, similar to the ones reported in [8]. Applicability conditions can be used to provide con. tezts for axioms and proofs just like type information. The effectiveness of the proposed axiomatic method becomes all the more evident while reasoning about nested powerlists for modeling n-dimensional arrays, for example, in specifying and reasoning about a transformation for embedding a multi-dimensional array into a hypercube such that adjacency of nodes is preserved by the transformation. A mechanically generated proof of this property of the embedding transformation, which was not proved in Misra's paper, is discussed in detail. This suggests that the proposed approach for automating reasoning about data parallel algorithms described recursively using powerlists should scale up, especially if structural properties of nested powerlists are built into RRL.