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 Times are displayed in time zone: Tijuana, Baja California change
10:30 - 12:00: Parallelism IIResearch Papers at Grand Ballroom San Rafael Chair(s): Albert CohenINRIA | |||
10:30 - 11:00 Talk | Transactional Data Structure Libraries Research Papers Alexander SpiegelmanTechnion - Israel institute of technology, Guy Golan-GuetaYahoo Labs, Idit KeidarTechnion - Israel institute of technology Media Attached | ||
11:00 - 11:30 Talk | FlexVec: Auto-Vectorization for Irregular Loops Research Papers Media Attached | ||
11:30 - 12:00 Talk | Verified Lifting of Stencil Computations Research Papers Shoaib KamilMIT CSAIL, USA, Alvin CheungUniversity of Washington, Shachar ItzhakyMIT CSAIL, Armando Solar-LezamaMIT Media Attached |