Optimism in Equality Saturation
summary
Shows that a naive optimistic e-class analysis on e-graphs becomes unsound because rewrites create ill‑formed cycles that look like loops but aren’t, and proposes an algorithm that treats real loop cycles and rewrite‑created cycles differently by computing successive pessimistic analyses that ignore back edges then reintroduce previous-iteration results until a post‑fixpoint; implements a prototype for SSA programs that yields measurable precision improvements over pure abstract interpretation and pessimistic e-class analysis while keeping performance comparable to existing tools.
AI-written summary · about
chapters (10)
- 0:00Optimism in equality saturation
- 1:55Optimistic analysis in compilers
- 2:36Loop invariants and e-class limits
- 4:02Equality saturation and egraphs
- 8:13E-class analysis in equality saturation
- 9:57Problem with optimistic e-class analysis
- 11:43Well-formed vs ill-formed cycles
- 13:10Optimistic e-class algorithm
- 15:59Final results and paper
- 16:20Q&A
related talks
30megg: Fast and Extensible Equality Saturation
19meqsat: An Equality Saturation Dialect for Non-destructive Rewriting
26mEquality Saturation Guided by Large Language Models
24mIncremental Equality Saturation
20mEquality Saturation and Joins
22mFrom Rewriting to Fixpoints: Solving Recursive Equations with E-Graphs
17mBetter Together: Unifying Datalog and Equality Saturation
13mMind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers