一句话：提出 Halide 端到端翻译验证算法，用 prophetic 注解和 refinement 映射证明生成代码正确。
本文研究张量编程语言领域特定编译器的正确性，以 Halide 为代表性对象。论文提出一种独立于调度语言的翻译验证算法，面向仿射 Halide 规格说明。编译器在生成的数组赋值上添加“prophetic”注解，这些注解给出从生成代码中的赋值到规格中张量定义的 refinement 映射。验证实现结合仿射求解器与通用 SMT 求解器，能够处理完整的 Halide 基准测试。该工作为 DSL 编译器优化结果提供端到端正确性保障，而不依赖对调度变换逐一证明。
This paper considers the correctness of domain-specific compilers for tensor programming languages through the study of Halide, a popular representative. It describes a translation validation algorithm for affine Halide specifications, independently of the scheduling language. The algorithm relies on “prophetic” annotations added by the compiler to the generated array assignments. The annotations provide a refinement mapping from assignments in the generated code to the tensor definitions from the specification. Our implementation leverages an affine solver and a general SMT solver, and scales to complete Halide benchmarks.
@article{paperbot1527,
title = {End-to-end translation validation for the halide language},
author = {Basile Clément and Albert Cohen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527328}
}