Skip to Main content Skip to Navigation
Conference papers

On the Verification of Polyhedral Program Transformations

Christophe Alias 1 Guillaume Iooss 2 Sanjay Rajopadhye 3
1 CASH - CASH - Compilation and Analysis, Software and Hardware
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
2 CORSE - Compiler Optimization and Run-time Systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : This paper presents a pragma language to specify a polyhedral program transformation directly in the code and a verification algorithm able to check the correctness of the specified transformation. Our language is general enough to specify a loop tiling by an arbitrary polyhedral tile shape (e.g., hexagons, diamonds, trapezoids), and whose size may depend on a scaling parameter (monoparametric tiling). Our verification algorithm checks the legality of the proposed transformation, and provides counterexamples of unsatisfied dependences when it is incorrect. In addition, out tool infers the domain of scaling parameters where the tiling is not legal. We developed a tool suite implementing these concepts with a verification tool (MPPCHECK) and a code generation tool (MPPCODEGEN), that are available and may be downloaded together with a rich set of examples. We evaluate the performance of the verification and the code generation on kernels from the PolyBench suite.
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03106070
Contributor : Christophe Alias <>
Submitted on : Monday, January 11, 2021 - 3:25:37 PM
Last modification on : Wednesday, January 13, 2021 - 10:02:07 AM
Long-term archiving on: : Monday, April 12, 2021 - 7:05:11 PM

File

alias-perso.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03106070, version 1

Citation

Christophe Alias, Guillaume Iooss, Sanjay Rajopadhye. On the Verification of Polyhedral Program Transformations. 18th International Conference on High Performance Computing & Simulation (HPCS 2020), 3rd Special Session on Compiler Architecture, Design and Optimization (CADO 2020), Jan 2020, Barcelona, Spain. ⟨hal-03106070⟩

Share

Metrics

Record views

53

Files downloads

33