Automated reasoning about parallel algorithms using powerlists

Deepak Kapur, M. Subramaniam

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationAlgebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings
EditorsV.S. Alagar, Maurice Nivat
PublisherSpringer Verlag
Pages416-430
Number of pages15
ISBN (Print)3540600434, 9783540600435
DOIs
StatePublished - Jan 1 1995
Event4th International Conference on Algebraic Methodology and Software Technology, AMAST 1995 - Montreal, Canada
Duration: Jul 3 1995Jul 7 1995

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume936
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th International Conference on Algebraic Methodology and Software Technology, AMAST 1995
CountryCanada
CityMontreal
Period7/3/957/7/95

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Automated reasoning about parallel algorithms using powerlists'. Together they form a unique fingerprint.

  • Cite this

    Kapur, D., & Subramaniam, M. (1995). Automated reasoning about parallel algorithms using powerlists. In V. S. Alagar, & M. Nivat (Eds.), Algebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings (pp. 416-430). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 936). Springer Verlag. https://doi.org/10.1007/3-540-60043-4_68