Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Optimism in Equality Saturation

Russel Arbore, Alvin Cheung, Max Willsey

TL;DR

The paper tackles the difficulty of performing precise abstract interpretation on cyclic programs within equality saturation frameworks. It introduces a formal SSA-based representation that supports path-sensitive analysis and defines an optimistic, sound dataflow algorithm for SSA e-graphs, enabling precise reasoning even in the presence of cycles. By coupling abstract interpretation with equality saturation through a two-stage fixpoint approach and leveraging relational e-graph abstractions, the method yields more precise results than traditional GFP-based solutions and can outperform established compilers on targeted examples. The Rust prototype demonstrates practical feasibility, including cycle de-duplication and improved optimization potential, suggesting a path toward broader adoption of optimistic analyses in SSA-based optimization pipelines and potential extensions to contextual or colored e-graphs.

Abstract

Equality saturation is a technique for program optimization based on non-destructive rewriting and a form of program analysis called e-class analysis. The current form of e-class analysis is pessimistic and therefore ineffective at analyzing cyclic programs, such as those in SSA form. We propose an abstract interpretation algorithm that can precisely analyze cycles during equality saturation. This results in a unified algorithm for optimistic analysis and non-destructive rewriting. We instantiate this approach on a prototype abstract interpreter for SSA programs using a new semantics of SSA. Our prototype can analyze simple example programs more precisely than clang and gcc.

Optimism in Equality Saturation

TL;DR

The paper tackles the difficulty of performing precise abstract interpretation on cyclic programs within equality saturation frameworks. It introduces a formal SSA-based representation that supports path-sensitive analysis and defines an optimistic, sound dataflow algorithm for SSA e-graphs, enabling precise reasoning even in the presence of cycles. By coupling abstract interpretation with equality saturation through a two-stage fixpoint approach and leveraging relational e-graph abstractions, the method yields more precise results than traditional GFP-based solutions and can outperform established compilers on targeted examples. The Rust prototype demonstrates practical feasibility, including cycle de-duplication and improved optimization potential, suggesting a path toward broader adoption of optimistic analyses in SSA-based optimization pipelines and potential extensions to contextual or colored e-graphs.

Abstract

Equality saturation is a technique for program optimization based on non-destructive rewriting and a form of program analysis called e-class analysis. The current form of e-class analysis is pessimistic and therefore ineffective at analyzing cyclic programs, such as those in SSA form. We propose an abstract interpretation algorithm that can precisely analyze cycles during equality saturation. This results in a unified algorithm for optimistic analysis and non-destructive rewriting. We instantiate this approach on a prototype abstract interpreter for SSA programs using a new semantics of SSA. Our prototype can analyze simple example programs more precisely than clang and gcc.

Paper Structure

This paper contains 38 sections, 1 theorem, 3 equations, 7 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Equality Saturation
  3. Optimism
  4. Optimism in Equality Saturation
  5. Background
  6. Equality Saturation
  7. E-Graphs
  8. Batched Rewriting and Rebuilding
  9. E-Class Analysis
  10. Cycles in E-Graphs
  11. Abstract Interpretation
  12. Single Static Assignment Form
  13. Challenges in Abstract Interpretation over E-Graphs
  14. The Problem
  15. Addressing the Problem
  16. ...and 23 more sections

Key Result

proposition 1

$\sigma_{i+1}(c) \sqsubseteq \sigma_i(c)$ for all e-classes $c \in (N_i / \equiv_i)$.

Figures (7)

  • Figure 1: An example e-graph during equality saturation. Symbols are e-nodes, solid edges connect e-nodes to argument e-classes, and dashed red edges connect e-nodes in the same e-class. (Note that some e-graph literature connect e-nodes → argument e-classes. We go the other way, e-nodes ← argument e-classes, indicating the flow of the data, aligning with the convention of drawing SSA graphs.)
  • Figure 2: A program in pseudo-code and its compilation into a SSA program.
  • Figure 3: Flow insensitive dataflow analysis (with the $\mathcal{P}(\mathbb{Z})$ lattice) of the program from Figure \ref{['fig:ssa-graph-example']}.
  • Figure 4: A trace of the dataflow algorithm performing a flow insensitive interval analysis on the running example program (from Figure \ref{['fig:ssa-example-program']}).
  • Figure 5: The interval ($\mathcal{I}$) and offset ($\mathcal{O}$) abstractions. Both abstractions are fairly standard, except that the concretization functions return functions that take and ignore a control flow walk argument.
  • ...and 2 more figures

Theorems & Definitions (11)

  • definition 1: E-Graphs
  • definition 2: Cyclic Terms
  • definition 3: Represented Graphs
  • definition 4: $\rightarrow_{\text{\tiny WALK}}$
  • definition 5: Denotation of SSA Nodes
  • definition 6: Well-formed SSA Programs
  • definition 7: Abstract Interpretation of SSA Programs
  • definition 8: Equivalence Abstraction
  • definition 9: E-Lifted Abstract Interpretations
  • definition 10: Abstract Interpretation of SSA E-Graphs
  • ...and 1 more