Automated reasoning about parallel algorithms using powerlists

Deepak Kapur, M. Subramaniam

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

4 Citations (Scopus)

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

Fingerprint

Automated Reasoning
Parallel algorithms
Parallel Algorithms
Data structures
Specifications
Sort
Fast Fourier transforms
Reasoning
Structural properties
Data Structures
Multidimensional Arrays
Algebraic Specification
Proof of correctness
Set Cover
Scale-up
Adjacency
Prefix
Rewriting
Fast Fourier transform
Hypercube

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

Automated reasoning about parallel algorithms using powerlists. / Kapur, Deepak; Subramaniam, M.

Algebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings. ed. / V.S. Alagar; Maurice Nivat. Springer Verlag, 1995. p. 416-430 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 936).

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

Kapur, D & Subramaniam, M 1995, Automated reasoning about parallel algorithms using powerlists. in VS Alagar & M Nivat (eds), Algebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 936, Springer Verlag, pp. 416-430, 4th International Conference on Algebraic Methodology and Software Technology, AMAST 1995, Montreal, Canada, 7/3/95. https://doi.org/10.1007/3-540-60043-4_68
Kapur D, Subramaniam M. Automated reasoning about parallel algorithms using powerlists. In Alagar VS, Nivat M, editors, Algebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings. Springer Verlag. 1995. p. 416-430. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-60043-4_68
Kapur, Deepak ; Subramaniam, M. / Automated reasoning about parallel algorithms using powerlists. Algebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings. editor / V.S. Alagar ; Maurice Nivat. Springer Verlag, 1995. pp. 416-430 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{7c15181234e0441da76733ddc19a0903,
title = "Automated reasoning about parallel algorithms using powerlists",
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.",
author = "Deepak Kapur and M. Subramaniam",
year = "1995",
month = "1",
day = "1",
doi = "10.1007/3-540-60043-4_68",
language = "English (US)",
isbn = "3540600434",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "416--430",
editor = "V.S. Alagar and Maurice Nivat",
booktitle = "Algebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings",

}

TY - GEN

T1 - Automated reasoning about parallel algorithms using powerlists

AU - Kapur, Deepak

AU - Subramaniam, M.

PY - 1995/1/1

Y1 - 1995/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84957804802&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84957804802&partnerID=8YFLogxK

U2 - 10.1007/3-540-60043-4_68

DO - 10.1007/3-540-60043-4_68

M3 - Conference contribution

AN - SCOPUS:84957804802

SN - 3540600434

SN - 9783540600435

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 416

EP - 430

BT - Algebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings

A2 - Alagar, V.S.

A2 - Nivat, Maurice

PB - Springer Verlag

ER -