高效提取有效 E-Graph
Efficient Extraction for Effectful E-Graphs
浏览论文内容
中文总结 AI 辅助
本文提出 Statewalk DP 算法，高效处理 E-Graph 中效果感知提取问题，证明其可处理性并实现比 ILP 数量级加速，在 eqcc 编译器中验证效果。
中文摘要 AI 辅助
E-Graph 已推动了程序优化、综合和验证领域的最新进展，但对于那些内存和 I/O 操作必须遵循执行顺序的有效程序，它们仍然难以应用。现有的效果感知提取算法依赖于整数线性规划（ILP），并主导了总运行时间。我们引入了 Statewalk DP，一种新的提取算法，它无需外部求解器即可高效地强制执行效果顺序。我们证明了找到任何效果安全的提取都是 NP 完全的，但表明 Statewalk DP 在状态行走宽度（一个衡量效果间数据流交互复杂性的参数）上是可处理的。在实践中，状态行走宽度通常保持较小，使得 Statewalk DP 能够在我们的基准测试中实现比 ILP 提取数量级的加速，同时生成与 LLVM 相当的程序。我们在 eqcc 中实现了该算法，这是一个基于 E-Graph 的原型编译器，用于命令式 Bril 程序，并证明了效果感知提取不再是瓶颈。
英文摘要
Egraphs have enabled recent advances in program optimization, synthesis, and verification, yet remain difficult to apply to effectful programs whose memory and I/O operations must respect execution order. Existing effect-aware extraction algorithms rely on integer linear programming (ILP) and dominate total runtime. We introduce Statewalk DP, a new extraction algorithm that enforces effect ordering efficiently without external solvers. We prove that finding any effect-safe extraction is NP-complete, but show that Statewalk DP is tractable in statewalk width, a parameter that measures the complexity of dataflow interactions among effects. In practice, statewalk width generally remains small, enabling Statewalk DP to achieve order-of-magnitude speedups over ILP extraction while producing programs comparable to LLVM across our benchmarks. We implement the algorithm in eggcc, a prototype egraph-based compiler for imperative Bril programs and demonstrate that effect-aware extraction is no longer a bottleneck.
发表机构
- University of Washington（华盛顿大学）
- Certora Inc.（Certora公司）
- Google（谷歌）
机构由 AI 辅助整理，请以论文原文为准。
