Home

Equality Saturation: A New Approach to Optimization

Equality Saturation: A New Approach to Optimization, Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner, POPL 2009.

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.

I thought this was one of the more interesting papers at POPL this year. The idea of tackling the phase ordering problem by splitting the problem into two steps --- first computing classes of equivalent programs, and second picking the best member of the equivalence class --- is very clever.

By neelk at 2009-03-03 15:20 | Implementation | other blogs | 19275 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Neutral GA

This reminds me of the research by Olsson on ADATE. He did genetic programming of a sort without any actual randomness -- just a series of transforms that explored a set of programs with neutral fitness. Once a program with higher fitness was found previous ones would be abandoned and the search would begin again.

By awwaiid at Tue, 2009-03-03 19:19 | login or register to post comments

Not many loop optimizations yet

They do not appear to address loop unrolling, splitting, etc. and rely on the transformation to/from CFG to handle fusion (?). It'd be interesting to see if their PEG's loop lifting could be extended to handle unrolling via nesting and un-nesting constant-sized loops. An optimizer trying to vectorize code could benefit from the lack of optimization ordering, at the cost of a potentially huge state explosion. For a small set of constant unrolling factors, though...

And as far as their claim that loop fusion is handled by the CFG transformation, well, I don't buy it. You don't necessarily want to fuse loops if there are heavy functions inside or you'll blow your instruction cache. So you need a bit of the inlining information. Again, the global nature of their system could help if the state doesn't explode too horribly.

Pretty cool.

By Jason Riedy at Tue, 2009-03-03 21:51 | login or register to post comments

Nice!

This seems like a really neat idea for exploring a large problem space. I'm not entirely clear on correctness though, is there anything preventing the equality from being read right-to-left as well? (My specific concern is running example used to motivate the improvement theory). Same with termination, what happens with your equalities are recursive functions?

By Peter A Jonsson at Wed, 2009-03-04 14:55 | login or register to post comments

LLVM

I wonder if LLVM could benefit from this. In LLVM, optimizations are done in passes and I've often found different pass sequences suit different kinds of code. For example, the one way to turn two mutually recursive functions in LLVM into a loops is to first inline code followed by recursion->loop transform. It won't work if you reverse the sequence. This scheme also has to change if there are, say, five mutually recursive (but still tail) functions.

By Srikumar Subramanian at Fri, 2009-03-06 09:50 | login or register to post comments

Source code link

An implementation of Program Expression Graphs from the paper "Equality Saturation: a new Approach to Optimization" by Ross Tate et al.

By Serguey Zefirov at Fri, 2009-10-30 17:01 | login or register to post comments

Code for peggy / Pueblo

Is the code for peggy publicly available?

They also refer to a solver called Pueblo, but the link I found is dead:

http://www.eecs.umich.edu/~hsheini/pueblo/

By johnleuner at Thu, 2010-03-18 11:39 | login or register to post comments

http://goto.ucsd.edu/~mstepp/peggy/

The source code of Peggy.

By Serguey Zefirov at Sun, 2012-11-25 11:12 | login or register to post comments

Yay! Impressive.

I'd been noticing this problem (destruction of information during compilation) and had some vague ideas in this direction, but this is great work! very rigorously developed.

The explosion of state is worrying. I can see why they're trying to minimize the number of different transformations their system works with. But I'm not entirely convinced of their claims that the transformations they're using subsume other conventional transformations.

This is an excellent problem domain for distributed computing, IMO; all that state information, all those alternatives - It's very parallelizable.

Ray Dillinger

By Ray Dillinger at Sun, 2012-11-25 13:27 | login or register to post comments

distributed, or quantum

mmm, quantum.

By raould at Wed, 2012-11-28 20:26 | login or register to post comments