paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Hydra: Generalizing Peephole Optimizations with Program Synthesis

Hydra:用程序合成泛化窥孔优化
OOPSLA 8(OOPSLA1)2024匹配度 3/10 · 论文属于程序合成与编译器窥孔优化,不含 LLM/Agent,也未涉及静态分析在 ML/Agentic 程序、浮点程序分析或贝叶斯程序分析中的应用;与用户核心交叉方向仅有 PL/形式验证的边缘联系。引用 10 inbox
Manasij Mukherjee, John Regehr
crossref: 2026-09-10

AI 速览

一句话:提出 Hydra,用程序合成自动将具体窥孔优化泛化为与位宽无关的通用重写规则,并生成可验证的 LLVM C++ 代码。

优化编译器依赖窥孔优化来化简指令组合、删除冗余指令。传统上,编译器开发者发现某个具体优化机会后,需要手工推导更通用的重写规则,以覆盖原代码及相似的指令集合,这一过程费时且易遗漏。本文提出 Hydra,一个以程序合成为核心的工具,自动完成窥孔优化的泛化。其关键挑战是:在存在位宽无关版本时,为每个优化找到该版本,使其不依赖输入位宽。作者用 LLVM 项目问题跟踪器中开发者提交的未泛化 missed peephole optimizations 进行评估,Hydra 能泛化其中 75%。所有生成的泛化窥孔优化均经过形式化验证,并可自动转换为适合加入 LLVM pass 的 C++ 代码。

问题
编译器窥孔优化通常由开发者从具体优化机会手工推导通用重写规则,难以系统覆盖相似指令组合,且容易遗漏可泛化的情况。
方法
Hydra 以程序合成为中心,自动为具体优化寻找更通用的重写规则,并重点求解与输入位宽无关的版本;生成的优化还会被形式化验证并转为 LLVM 可用的 C++ 代码。
评估
在 LLVM 问题跟踪器中未泛化的 missed peephole optimizations 上,Hydra 成功泛化了 75%;所有泛化结果均通过形式化验证,并可自动生成适合 LLVM pass 的 C++ 代码。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}