Halide语言的形式语义
摘要：用户可调度语言的语言健全性的首次形式化及元理论，以及广泛使用的数组处理语言Halide。用户可调度语言在高性能计算中平衡了抽象和控制的关系，通过将程序的计算内容和计算方式的规划分开。在此过程中，它们提出了一个新颖的语言健全性声明：程序的结果应该始终相同，无论如何调度。然而，这个健全性保证较为复杂，因为调度可能导致冗余计算和对未初始化数据的计算。此外，Halide通过一个编译时的边界推断引擎确保内存安全，该引擎确定生成代码中每个缓冲区和循环的安全大小，从而提出了一个新的挑战：形式化和分析依赖于不可靠程序合成算法结果的语言规范。我们的形式化工作揭示了Halide系统中的缺陷并带来了改进，我们相信它为设计新语言和工具提供了基础，将程序员可控的调度应用于其他领域。
作者：Alex Reinking, Gilbert Louis Bernstein, Jonathan Ragan-Kelley
论文ID：2210.15740
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-10-31