Verified lifting of stencil computations
Verified lifting of stencil computations
复制标题
验证了模板计算的提升
DOI：
10.1145/2908080.2908117
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Armando Solar
中科院分区：
文献类型：
--
作者：
Shoaib Kamil;Alvin Cheung;Shachar Itzhaky;Armando Solar
本文展示了一种新颖的程序综合和验证的组合，将模板计算从低级Fortran代码提升到使用谓词语言表示的高级摘要。这项技术是合理的，大部分是自动化的，并利用反例指导的归纳合成(CEGIS)来找到可证明是正确的翻译。将现有代码提升到高性能描述语言有许多好处，包括可维护性和性能可移植性。例如，我们的实验表明，与处理原始代码的现成编译器相比，提升的摘要可以使特定于域的编译器更好地进行并行化，甚至可以支持完全自动迁移到GPU等硬件加速器。我们已经在一个名为STNG的系统中实现了经过验证的提升，并使用微基准、迷你应用程序和真实世界的应用程序对其进行了评估。我们演示了验证提升的好处，方法是首先自动将Fortran源代码汇总为高级谓词语言，然后将提升的摘要翻译成Halide，与原始实现相比，翻译后的代码实现了4.1X的中值性能加速，对于非普通模板，性能提升高达24X。
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, including 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.