标题： 在纯函数式数据并行语言中验证索引数组的性质 显示英文标题

标题： Verifying Properties of Index Arrays in a Purely-Functional Data-Parallel Language

摘要： 本文提出了一种新颖的方法，用于自动验证具有非线性索引的纯数据并行程序的性质——这些性质以函数的前后条件形式表达。 程序由二阶数组组合器（例如，map、scan 和 scatter）和循环的嵌套组成。 关键思想是将数组表示为索引函数：程序是在这些索引函数上的变换，性质在这些变换上进行传播和推断。 我们的框架通过将索引函数提炼为代数（不）等式，并将其传递给基于 Fourier-Motzkin 的求解器来证明索引函数上的性质。 该框架具有实用性和可访问性：性质不限于可判定逻辑，而是精心选择以表达可以自动推理和推断的实际有用保证。 这些保证不仅限于程序正确性，还可以在整个编译器流水线中用于优化。 我们在纯数据并行语言 Futhark 中实现了我们的系统，并在七个应用上展示了其实用性，报告了平均验证时间为 1 秒。 两个案例研究展示了在 GPU 程序中消除动态验证如何带来显著的加速。 显示英文摘要

摘要： This paper presents a novel approach to automatically verify properties of pure data-parallel programs with non-linear indexing -- expressed as pre- and post-conditions on functions. Programs consist of nests of second-order array combinators (e.g., map, scan, and scatter) and loops. The key idea is to represent arrays as index functions: programs are index function transformations over which properties are propagated and inferred. Our framework proves properties on index functions by distilling them into algebraic (in)equalities and discharging them to a Fourier-Motzkin-based solver. The framework is practical and accessible: properties are not restricted to a decidable logic, but instead are carefully selected to express practically useful guarantees that can be automatically reasoned about and inferred. These guarantees extend beyond program correctness and can be exploited by the entire compiler pipeline for optimization. We implement our system in the pure data-parallel language Futhark and demonstrate its practicality on seven applications, reporting an average verification time of 1 second. Two case studies show how eliminating dynamic verification in GPU programs results in significant speedups.