PolyCheck: dynamic verification of iteration space transformations on affine programs
PolyCheck: dynamic verification of iteration space transformations on affine programs
复制标题
PolyCheck：仿射程序迭代空间变换的动态验证
DOI：
10.1145/2837614.2837656
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
P. Sadayappan
中科院分区：
文献类型：
--
作者：
Wenlei Bao;S. Krishnamoorthy;L. Pouchet;F. Rastello;P. Sadayappan
高级编译器转换，尤其是循环转换，被广泛认为是重组程序以改善数据区域并暴露并行性的关键优化。确保程序转换的正确性至关重要，至今已开发出三种主要方法：仿射程序等效的证明，匹配程序的执行痕迹，并检查程序输出的逐个位置。每种技术都有所支持的转换，空间复杂性或对测试数据集的敏感性的局限性。在本文中，我们采用了一种新的方法来解决所有三个限制，以提供自动错误检查器，以验证对仿期程序的任何迭代重新排序转换，包括非携带转换，与原始程序数据成比例的空间消耗，并与任意数据集成正比给定尺寸。我们通过利用仿射程序控制和数据流的结构来实现这一目标，以在转换后的程序中以编译时间轻量级检查器代码生成。实验结果评估了我们方法的正确性和有效性及其对先前方法的覆盖率增加。
High-level compiler transformations, especially loop transformations, are widely recognized as critical optimizations to restructure programs to improve data locality and expose parallelism. Guaranteeing the correctness of program transformations is essential, and to date three main approaches have been developed: proof of equivalence of affine programs, matching the execution traces of programs, and checking bit-by-bit equivalence of program outputs. Each technique suffers from limitations in the kind of transformations supported, space complexity, or the sensitivity to the testing dataset. In this paper, we take a novel approach that addresses all three limitations to provide an automatic bug checker to verify any iteration reordering transformations on affine programs, including non-affine transformations, with space consumption proportional to the original program data and robust to arbitrary datasets of a given size. We achieve this by exploiting the structure of affine program control- and data-flow to generate at compile-time lightweight checker code to be executed within the transformed program. Experimental results assess the correctness and effectiveness of our method and its increased coverage over previous approaches.
使用时序逻辑辅助条件进行程序转换
影响因子：
1.3
作者：
Kalvala S
通讯作者：
Kalvala S
从测试到证明
DOI：
10.1007/s10009-012-0267-5
发表时间：
2013
影响因子：
1.5
作者：
Ashutosh Gupta;Rupak Majumdar;Andrey Rybalchenko
通讯作者：
Andrey Rybalchenko