A compiler applies individual optimizations sequentially to transform a program. The order of the application affects the result of the program transformation. Some optimizations can undo the improvement done by other optimizations or even render some of them inapplicable. It is impossible to find one perfect order of application which ensures the best possible transformation for any program. Equality saturation solves this problem by non-destructive application of all possible optimizations until the representation of the optimized program is saturated. A Pseudo-Boolean solver is then applied to generate the best program according to some global optimization heuristic. Besides the optimization, equality saturation can also perform translation validation of compilers.

Supplementary materials:

Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. Equality saturation: a new approach to optimization. SIGPLAN Not. 44, 1 (January 2009) (https://dl.acm.org/citation.cfm?id=1480915)

Grechanik S.A. Proving Properties of Functional Programs via Equality Saturation. PhD Dissertation, Keldysh Institute for Applied Mathematics RAS (http://www.keldysh.ru/council/1/2017-grechanik/diss.pdf)

Presenter: Ekaterina Verbitskaya

Date: March 25, 2019

Time: 17:15

Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28