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
10:30 - 12:00: Research Papers - Parallelism II at Grand Ballroom San Rafael Chair(s): Albert CohenINRIA | ||||||||||||||||||||||||||||||||||||||||||
10:30 - 11:00 Talk | Alexander SpiegelmanTechnion - Israel institute of technology, Guy Golan-GuetaYahoo Labs, Idit KeidarTechnion - Israel institute of technology Media Attached | |||||||||||||||||||||||||||||||||||||||||
11:00 - 11:30 Talk | Media Attached | |||||||||||||||||||||||||||||||||||||||||
11:30 - 12:00 Talk | Shoaib KamilMIT CSAIL, USA, Alvin CheungUniversity of Washington, Shachar ItzhakyMIT CSAIL, Armando Solar-LezamaMIT Media Attached |