Verification and Performance Evaluation of Specialized Polyhedral Parallel Code

  • 2015-05-22
  • Research

It is critical to develop methods and tools to automatically assert the correctness of programs generated by modern optimizing compilers


It is critical to develop methods and tools to automatically assert the correctness of programs generated by modern optimizing compilers that involve parallelization and loop transformations. In particular in the presence of parallelization it is necessary to verify for all possible program executions that the generated program implements the same semantics as the original program. In the presence of floating point operations reordering of instructions and parallelization requires to also consider precision aspects of floating point computations.

We focus on the polyhedral model and present a technique to verify whether the original program and the optimized program are equivalent and also determine whether the generated parallel code has data races. Our technique uses program specialization and verifies these properties for a given program and selected fixed parameters. The specialized programs are transformed until they can be exactly matched - which proves the equivalence. The data race check is performed on the specialized programs.

A number of performance evaluations of polyhedral transformations for various benchmarks with different compilers and polyhedral variants are presented. The measurements show how important such transformations are to achieve high performance with improved cache locality and/or loops that have been parallelized.

The goal of this work is to automatically detect errors in code generated by polyhedral compilers. We check the correctness of a set of parallel polyhedral transformations and demonstrate our approach on a collection of benchmarks from the PolyBench/C 3.2 suite.


Markus Schordan is a computer scientist at Lawrence Livermore National Laboratory (Center for Applied Scientific Computing (CASC)). His research interests include program analysis and verification, compiler construction, reverse code generation, and programming languages for high-performance computing. The software systems of interest are specific HPC applications and large-scale software systems in general. Reverse code generation is of interest for optimistic parallel discrete event simulation.

In 2009 he received an R&D 100 AWARD (ROSE), in 2011 a Best Paper Award at the 11th IEEE Source-Code and Manipulation Conference (SCAM 2011), in 2012 and 2013 the Method Combination Award in the RERS Challenge (participation team Markus Schordan and Adrian Prantl), and in 2014 he won the RERS Challenge 2014 (1st in 5 of 7 categories, including category overall; participation team Markus Schordan and Marc Jasper).

He received a Diploma Degree in computer science from TU Vienna in 1997, and a PhD degree from University Klagenfurt in 2001 (with distinction). He is author or co-author of 35+ refereed and invited papers of conferences and journals. He is a member of the IFIP Working group 2.4 Software Implementation Technology, the ACM, and IEEE.

He has served as co-organizer of the ISoLA 2014 Track “Evaluation and Reproducibility of Program Analysis”, GPUScA 2011, GPUScA 2010, Dagstuhl Seminar No. 08161 “Scalable Program Analysis”. He served as program committee member of several conferences, most recently Euro-Par 2015, SOFSEM 2015, ISoLA 2014, SYNASC 2014, SYNASC 2013, ARW 2013, SYNASC 2012, GPGPU-5 2012, GPUScA 2011, CC 2011, PPPJ 2011, GPUScA 2010, SYNASC 2010.


This talk is organized by the Compilers and Languages Group at the Institute of Computer Languages. Tea at the library of E185/1, Argentinierstr. 8, 4th floor (central) at 14:30.


Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!