Optimizing compilers have become a cornerstone for high-performance program generation in research and industry. Optimizations, including those implemented manually by a user and those target-specific and non-target-specific, are used to transform programs to achieve good performance. Although these optimizations are necessary for performance, assessing their correctness has remained a major challenge; the risk of incorrect code being deployed increases with unproven optimization flows. In this work, we target the formal verification of correctness of a transformed program by computing whether a pair of programs are semantically equivalent, one being a transformed version of the other. We restrict the class of programs supported to enable a hybrid concrete-symbolic interpretation approach to equivalence, which in turn is mostly agnostic to how the programs are implemented (syntax, schedule, storage, etc.). This approach can show equivalence in linear time with respect to the operations executed by the programs. We develop a verifier for a meaningful subset of MLIR, and report on the verification of the AMD MLIR-AIR and MLIR-AIE toolchains, as well as the standard mlir-opt on hundreds of benchmarks variants.

翻译：优化编译器已成为研究界与工业界实现高性能程序生成的基石。无论是用户手动实现的优化，还是面向特定目标与非特定目标的优化，都被用于转换程序以达成优异性能。尽管这些优化对性能至关重要，但其正确性评估始终是一项重大挑战——未经证明的优化流程会增加部署错误代码的风险。本研究针对转换后程序的正确性形式化验证问题，通过判定一对程序是否语义等价（其中一个为另一个的转换版本）来实现验证。我们限定所支持的程序类别，采用混合具体-符号解释方法进行等价性判定，该方法基本上与程序的具体实现方式（语法、调度、存储等）无关。该方案能以与程序执行操作数成线性时间复杂度来证明等价性。我们为MLIR的有意义子集开发了验证器，并报告了对AMD MLIR-AIR与MLIR-AIE工具链的验证结果，以及在数百个基准测试变体上对标准mlir-opt工具的验证情况。