An approach for proving the correctness of inspector/executor transformations

Michael Norrish, Michelle Mills Strout

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

Abstract

To take advantage of multicore parallelism, programmers and compilers rewrite, or transform, programs to expose loop-level parallelism. Showing the correctness, or legality, of such program transformations enables their incorporation into compilers. However, the correctness of inspector/executor strategies, which develop parallel schedules at runtime for computations with nonaffine array accesses, rests on the correctness of the inspector code itself. Since inspector code is often provided in a run-time library, showing the correctness of an inspector/ executor transformation in a compiler requires proving the correctness of any hand-written or compiler-generated inspector code as well. In this paper, we present a formally defined language (called PseudoC) for representing loops with indirect array accesses. We describe how using this language, where the reads and writes in array assignments are distinguished, it is possible to formally prove the correctness of a wavefront parallelism inspector in HOL4. The key idea is to reason about the equivalence of the original code and the inspector/executor code based on operational semantics for the PseudoC grammar and properties of an executable action graph representation of the original and executor loops.

Original languageEnglish (US)
Title of host publicationLanguages and Compilers for Parallel Computing - 27th International Workshop, LCPC 2014, Revised Selected Papers
EditorsJames Brodman, Peng Tu
PublisherSpringer-Verlag
Pages131-145
Number of pages15
ISBN (Electronic)9783319174723
DOIs
StatePublished - 2015
Externally publishedYes
Event27th International Workshop on Languages and Compilers for Parallel Computing, LCPC 2014 - Hillsboro, United States
Duration: Sep 15 2014Sep 17 2014

Publication series

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

Conference

Conference27th International Workshop on Languages and Compilers for Parallel Computing, LCPC 2014
Country/TerritoryUnited States
CityHillsboro
Period9/15/149/17/14

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'An approach for proving the correctness of inspector/executor transformations'. Together they form a unique fingerprint.

Cite this