Fri 17 Jun 2016 11:30 - 12:00 at Grand Ballroom San Rafael - Parallelism II Chair(s): Albert Cohen

This paper demonstrates a novel combination of program synthesis and verification to lift stencil computations from low-level Fortran code to a high-level summary expressed using a predicate language. The technique is sound and mostly automated, and leverages counter-example guided inductive synthesis (CEGIS) to find provably correct translations. Lifting existing code to a high-performance description language has a number of benefits, such as maintainability and performance portability. For example, our experiments show that the lifted summaries can enable domain specific compilers to do a better job of parallelization as compared to an off-the-shelf compiler working on the original code, and can even support fully automatic migration to hardware accelerators such as GPUs. We have implemented verified lifting in a system called STNG and have evaluated it using microbenchmarks, mini-apps, and real-world applications. We demonstrate the benefits of verified lifting by first automatically summarizing Fortran source code into a high-level predicate language, and subsequently translating the lifted summaries into Halide, with the translated code achieving median performance speedups of 4.1X and up to 24X for non-trivial stencils as compared to the original implementation.

Fri 17 Jun

pldi-2016-papers
10:30 - 12:00: Research Papers - Parallelism II at Grand Ballroom San Rafael
Chair(s): Albert CohenINRIA
pldi-2016-papers146615220000010:30 - 11:00
Talk
Alexander SpiegelmanTechnion - Israel institute of technology, Guy Golan-GuetaYahoo Labs, Idit KeidarTechnion - Israel institute of technology
Media Attached
pldi-2016-papers146615400000011:00 - 11:30
Talk
Sara BaghsorkhiIntel Labs, Nalini VasudevanGoogle, Youfeng WuIntel Corporation
Media Attached
pldi-2016-papers146615580000011:30 - 12:00
Talk
Shoaib KamilMIT CSAIL, USA, Alvin CheungUniversity of Washington, Shachar ItzhakyMIT CSAIL, Armando Solar-LezamaMIT
Media Attached