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 - 11:00|
Alexander SpiegelmanTechnion - Israel institute of technology, Guy Golan-GuetaYahoo Labs, Idit KeidarTechnion - Israel institute of technologyMedia Attached
|11:00 - 11:30|
|11:30 - 12:00|
Shoaib KamilMIT CSAIL, USA, Alvin CheungUniversity of Washington, Shachar ItzhakyMIT CSAIL, Armando Solar-LezamaMITMedia Attached