一句话：提出语言参数化的程序等价性检查器 Keq，基于割双模拟，并用于 LLVM 指令选择翻译验证。
现代优化编译器如 LLVM 的翻译验证面临挑战：现有系统往往针对特定变换序列和统一输入输出语言定制。本文提出语言参数化的翻译验证设计，将变换相关部分与通用部分解耦，并给出 Keq——首个对输入/输出语言语义参数化、且不依赖具体变换的程序等价性检查器。Keq 基于割双模拟（cut-bisimulation）形式化，并证明其正确性。作者为 LLVM 指令选择 pass 原型化验证系统，可自动证明从 LLVM IR 到 x86-64 MachineIR 的翻译等价，该变换涉及不同语言，此前方法难以处理。实验在 SPEC 2006 的 GCC 程序上评估，Keq 成功证明 4732 个受支持函数中超过 90% 的翻译正确。
We propose a new design for a Translation Validation (TV) system geared towards practical use with modern optimizing compilers, such as LLVM. Unlike existing TV systems, which are custom-tailored for a particular sequence of transformations and a specific, common language for input and output programs, our design clearly separates the transformation-specific components from the rest of the system, and generalizes the transformation-independent components. Specifically, we present Keq, the first program equivalence checker that is parametric to the input and output language semantics and has no dependence on the transformation between the input and output programs. The Keq algorithm is based on a rigorous formalization, namely cut-bisimulation, and is proven correct. We have prototyped a TV system for the Instruction Selection pass of LLVM, being able to automatically prove equivalence for translations from LLVM IR to the MachineIR used in compiling to x86-64. This transformation uses different input and output languages, and as such has not been previously addressed by the state of the art. An experimental evaluation shows that Keq successfully proves correct the translation of over 90% of 4732 supported functions in GCC from SPEC 2006.
DOI 原文 ·
@inproceedings{paperbot6123,
title = {Language-parametric compiler validation with application to LLVM},
author = {Theodoros Kasampalis and Daejun Park and Zhengyao Lin and Vikram S. Adve and Grigore Roşu},
booktitle = {ASPLOS},
year = {2021},
doi = {10.1145/3445814.3446751}
}