一句话:提出 Hydra,用程序合成自动将具体窥孔优化泛化为与位宽无关的通用重写规则,并生成可验证的 LLVM C++ 代码。
优化编译器依赖窥孔优化来化简指令组合、删除冗余指令。传统上,编译器开发者发现某个具体优化机会后,需要手工推导更通用的重写规则,以覆盖原代码及相似的指令集合,这一过程费时且易遗漏。本文提出 Hydra,一个以程序合成为核心的工具,自动完成窥孔优化的泛化。其关键挑战是:在存在位宽无关版本时,为每个优化找到该版本,使其不依赖输入位宽。作者用 LLVM 项目问题跟踪器中开发者提交的未泛化 missed peephole optimizations 进行评估,Hydra 能泛化其中 75%。所有生成的泛化窥孔优化均经过形式化验证,并可自动转换为适合加入 LLVM pass 的 C++ 代码。
Optimizing compilers rely on peephole optimizations to simplify combinations of instructions and remove redundant instructions. Typically, a new peephole optimization is added when a compiler developer notices an optimization opportunity---a collection of dependent instructions that can be improved---and manually derives a more general rewrite rule that optimizes not only the original code, but also other, similar collections of instructions. In this paper, we present Hydra, a tool that automates the process of generalizing peephole optimizations using a collection of techniques centered on program synthesis. One of the most important problems we have solved is finding a version of each optimization that is independent of the bitwidths of the optimization's inputs (when this version exists). We show that Hydra can generalize 75% of the ungeneralized missed peephole optimizations that LLVM developers have posted to the LLVM project's issue tracker. All of Hydra's generalized peephole optimizations have been formally verified, and furthermore we can automatically turn them into C++ code that is suitable for inclusion in an LLVM pass.
@article{paperbot2547,
title = {Hydra: Generalizing Peephole Optimizations with Program Synthesis},
author = {Manasij Mukherjee and John Regehr},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649837}
}