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,...
Main Authors: | , , , |
---|---|
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 |