一句话：为函数式张量语言 ATL 的降级算法提供形式化正确性证明，并用新类型系统修复截断 reshape 的可靠性缺陷。
高性能图像处理和机器学习需要高效数组代码，常需通过改变计算阶段与粒度来控制计算强度和局部性，但纯函数式张量语言难以表达。本文针对前期提出的 ATL（用 reshape 算子解耦计算顺序与存储顺序）给出其编译算法的形式化正确性证明，这是首个从可独立控制计算/存储顺序的函数式源语言到命令式循环嵌套的 lowering 验证。证明难点是为存储索引重映射建立良构不变式；该工作还发现原算法在截断 reshape 上存在可靠性缺陷。作者提出新类型系统显式刻画安全条件，使良类型程序的编译器正确性可证，并在常见程序与优化上评估，性能与 Halide 等编译器相当。
Producing efficient array code is crucial in high-performance domains like image processing and machine learning. It requires the ability to control factors like compute intensity and locality by reordering computations into different stages and granularities with respect to where they are stored. However, traditional pure, functional tensor languages struggle to do so. In a previous publication, we introduced ATL as a pure, functional tensor language capable of systematically decoupling compute and storage order via a set of high-level combinators known as reshape operators. Reshape operators are a unique functional-programming construct since they manipulate storage location in the generated code by modifying the indices that appear on the left-hand sides of storage expressions. We present a formal correctness proof for an implementation of the compilation algorithm, marking the first verification of a lowering algorithm targeting imperative loop nests from a source functional language that enables separate control of compute and storage ordering. One of the core difficulties of this proof required properly formulating the complex invariants to ensure that these storage-index remappings were well-formed. Notably, this exercise revealed a soundness bug in the original published compilation algorithm regarding the truncation reshape operators. Our fix is a new type system that captures safety conditions that were previously implicit and enables us to prove compiler correctness for well-typed source programs. We evaluate this type system and compiler implementation on a range of common programs and optimizations, including but not limited to those previously studied to demonstrate performance comparable to established compilers like Halide.
@article{paperbot2515,
title = {A Verified Compiler for a Functional Tensor Language},
author = {Amanda Liu and Gilbert Bernstein and Adam Chlipala and Jonathan Ragan-Kelley},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656390}
}