Ross Tate ; Michael Stepp ; Zachary Tatlock ; Sorin Lerner - Equality Saturation: A New Approach to Optimization

lmcs:1016 - Logical Methods in Computer Science, March 28, 2011, Volume 7, Issue 1 - https://doi.org/10.2168/LMCS-7(1:10)2011
Equality Saturation: A New Approach to Optimization

Authors: Ross Tate ORCID-iD; Michael Stepp ; Zachary Tatlock ; Sorin Lerner

    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.


    Volume: Volume 7, Issue 1
    Published on: March 28, 2011
    Accepted on: June 25, 2015
    Submitted on: October 12, 2009
    Keywords: Computer Science - Programming Languages,D.3.4
    Fundings :
      Source : OpenAIRE Research Graph
    • CAREER: Automatically Generating and Processing Program Analyses and Optimizations; Funder: National Science Foundation; Code: 0644306

    Linked data

    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.ecoop.2022.13
    • 10.4230/lipics.ecoop.2022.13
    REST: Integrating Term Rewriting with Program Verification
    Grannan, Z. ; Vazou, N. ; Darulova, E. ; Summers, A. ;

    15 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 591 times.
    This article's PDF has been downloaded 340 times.