Efficient Extraction for Effectful E-graphs
This program is tentative and subject to change.
E-Graphs 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 e-graph-based compiler for imperative Bril programs, and demonstrate that effect-aware extraction is no longer a bottleneck.
This program is tentative and subject to change.
Mon 5 OctDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 17:00 | |||
15:30 18mTalk | Spatial and Temporal Decomposition for Faster Translation Validation OOPSLA Benjamin Mikek Georgia Institute of Technology, Chathur Bommineni Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology, Thomas Reps University of Wisconsin-Madison DOI | ||
15:48 18mTalk | Efficient Extraction for Effectful E-graphs OOPSLA Oliver Flatt University of Washington, Anjali Pal University of Washington, Yihong Zhang University of Washington, Ryan Tjoa Jane Street, Kirsten Graham University of Washington, Alex Fischman University of Washington, Chandrakana Nandi Certora; University of Washington, Eli Rosenthal Google, Zachary Tatlock University of Washington, Haobin Ni University of Washington DOI | ||
16:06 18mTalk | Phaedrus: Predicting Dynamic Application Behavior with Lightweight Generative Models and LLMs OOPSLA Bodhisatwa Chatterjee NVIDIA, Georgia Institute of Technology, Neeraj Jadhav Georgia Institute of Technology, Santosh Pande Georgia Institute of Technology DOI | ||
16:24 18mTalk | Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution OOPSLA Charitha Saumya Intel, Muhammad Hassan Virginia Tech, Rohan Gangaraju University of Texas at Austin, Milind Kulkarni Purdue University, Kirshanthan Sundararajah Virginia Tech DOI Authorizer link Pre-print | ||