Papers for

program synthesis teams

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Egraph extraction speeds up effectful program compilation by ten times

Efficient Extraction for Effectful E-Graphs

Abstract: 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 eqcc, a prototype egraph-based compiler for imperative Bril programs and demonstrate that effect-aware extraction is no longer a bottleneck.

Fri 25 SeptProgramming Languages
The gist
Finding the best way to simplify programs that involve memory and input/output actions is hard because the order of these actions matters. The authors found that the problem is generally very complex but created a new method called Statewalk DP that can handle typical cases quickly. This method does not need complicated external tools to work and makes extracting optimized programs much faster. They tested their approach on a small-language compiler and saw big speed improvements without losing quality.
Open → 2609.31887v1