Equality saturation: a new approach to optimization

By Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner. 2009

337 citations recorded by the source corpus.

Optimizations in a traditional compiler are applied sequentially, with each optimization destructively modifying the program to produce a transformed program that is then passed to the next optimization. We present a new approach for structuring the optimization phase of a compiler. In our approach, optimizations take the form of equality analyses that add equality information to a common intermediate representation. The optimizer works by repeatedly applying these analyses to infer equivalences between program fragments, thus saturating the intermediate representation with equalities. Once saturated, the intermediate representation encodes multiple optimized versions of the input program. At this point, a profitability heuristic picks the final optimized program from the various programs represented in the saturated representation. Our proposed way of structuring optimizers has a variety of benefits over previous approaches: our approach obviates the need to worry about optimization ordering, enables the use of a global optimization heuristic that selects among fully optimized programs, and can be used to perform translation validation, even on compilers other than our own. We present our approach, formalize it, and describe our choice of intermediate representation. We also present experimental results showing that our approach is practical in terms of time and space overhead, is effective at discovering intricate optimization opportunities, and is effective at performing translation validation for a realistic optimizer.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software, Optimization & Training

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

In Optimization & Training

Citations in the corpus

SPoC: Search-based Pseudocode to Code (2019, methodology): “The most focused and effective method is to formulate synthesis as a constraint satisfaction problem [32, 33], which requires that the synthesis problem can be translated to a theory with effective constraint solvers.”
egg: Fast and extensible equality saturation (2020, methodology): “The “purely syntactic” restriction has forced existing equality saturation applications [Panchekha et al. 2015; Stepp et al. 2011; Tate et al. 2009] to resort to ad hoc passes over the e-graph to implement analyses like constant folding.”
DreamCoder: growing generalizable, interpretable knowledge with wake–sleep Bayesian program learning (2020, methodology): “resolve this exponential growth we introduce a new data structure for representing and manipulating the set of refactorings, combining ideas from version space algebras (18–20) and equivalence graphs (21), and we derive a dynamic program for its construction (supplementary S4.5). This data structure”
Stochastic superoptimization (2012, background): “Denali [11], and the more recent Equality Saturation technique [18], attempt to gain scalability by only considering programs that are known to be equal to the input program.”
A large-scale benchmark for few-shot program induction and synthesis (2021, methodology): “Program Expression Graphs (PEGs) (Tate et al., 2009) are a new representation of programs that allows equational reasoning and build e-graphs on arbitrary imperative programs.”
Compiler validation via equivalence modulo inputs (2014, methodology): “introduce the Peggy optimization and translation validation framework for JVM based on equality saturation [25].”
Semantic code search via equational reasoning (2020, methodology): “Its marriage to Ross Tate’s E-PEGs, together with additional reasoning capabilities and careful design of a language of more abstract nodes, produced Yogo .”
DreamCoder: bootstrapping inductive program synthesis with wake-sleep library learning (2021, methodology): “Inspired by the E-graph equality saturation approachwithin program analysis [53], we build a graph tracking the equivalences exposed by I βn , and finally return a single structure for each program compiling all of these equivalences.”