Equality Saturation is a new compiler optimization technique that
mitigates the phase ordering problem. Roughly, the problem is that there
is no single best order for a compiler to apply transformations to a
program. Equality saturation alleviates this limitation by exploring many
possible sequences of transformations. Unfortunately, the number of
possible sequences combinatorially explodes. To effectively explore part
of the exponentially many sequences, we developed a new compiler called
Peggy. Peggy uses a new program representation and an efficient engine
that infers equivalence between program fragments. We also extended these
components to check the correctness of other compilers (ie. translation
validation).
Perhaps the most interesting part of this work is emergent
optimiztions; Peggy can perform many sophisticated traditional
optimizations (like loop induction variable strength reduction), yet we
never had to directly implement any of them! Instead, Peggy uses very
simple, local axioms about equivalence between program fragments.
By inferring many equalities among program fragments and then selecting
the "best" program from among equivalent versions, Peggy is able to
derive many traditional optimizations and even some new ones.
Publications
-
Equality Saturation: A New Approach to Optimization
POPL 09: paper, slides, talk (by Ross)
with Ross Tate, Mike Stepp, and Sorin Lerner
Technical Reports