Equality Saturation: A New Approach to Optimization

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,...

Full description

Bibliographic Details
Main Authors: Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2011-03-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/1016/pdf
_version_ 1797268802493218816
author Ross Tate
Michael Stepp
Zachary Tatlock
Sorin Lerner
author_facet Ross Tate
Michael Stepp
Zachary Tatlock
Sorin Lerner
author_sort Ross Tate
collection DOAJ
description 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.
first_indexed 2024-04-25T01:38:16Z
format Article
id doaj.art-e225e6f7f8d744ae91336ae2478ea0f7
institution Directory Open Access Journal
issn 1860-5974
language English
last_indexed 2024-04-25T01:38:16Z
publishDate 2011-03-01
publisher Logical Methods in Computer Science e.V.
record_format Article
series Logical Methods in Computer Science
spelling doaj.art-e225e6f7f8d744ae91336ae2478ea0f72024-03-08T09:14:52ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742011-03-01Volume 7, Issue 110.2168/LMCS-7(1:10)20111016Equality Saturation: A New Approach to OptimizationRoss Tatehttps://orcid.org/0000-0002-7608-4605Michael SteppZachary Tatlockhttps://orcid.org/0000-0002-4731-0124Sorin LernerOptimizations 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.https://lmcs.episciences.org/1016/pdfcomputer science - programming languagesd.3.4
spellingShingle Ross Tate
Michael Stepp
Zachary Tatlock
Sorin Lerner
Equality Saturation: A New Approach to Optimization
Logical Methods in Computer Science
computer science - programming languages
d.3.4
title Equality Saturation: A New Approach to Optimization
title_full Equality Saturation: A New Approach to Optimization
title_fullStr Equality Saturation: A New Approach to Optimization
title_full_unstemmed Equality Saturation: A New Approach to Optimization
title_short Equality Saturation: A New Approach to Optimization
title_sort equality saturation a new approach to optimization
topic computer science - programming languages
d.3.4
url https://lmcs.episciences.org/1016/pdf
work_keys_str_mv AT rosstate equalitysaturationanewapproachtooptimization
AT michaelstepp equalitysaturationanewapproachtooptimization
AT zacharytatlock equalitysaturationanewapproachtooptimization
AT sorinlerner equalitysaturationanewapproachtooptimization