eqsat: An Equality Saturation Dialect for Non-destructive Rewriting
This program is tentative and subject to change.
With recent algorithmic improvements and easy-to-use libraries, equality saturation is being picked up for hardware design, program synthesis, theorem proving, program optimization, and more. Existing work on using equality saturation for program optimization makes use of external equality saturation libraries such as egg, typically generating a single optimized expression. In the context of a compiler, such an approach uses equality saturation to replace a small number of passes. In this work, we propose an alternative approach that represents equality saturation natively in the compiler’s intermediate representation, facilitating the application of constructive compiler passes that maintain the e-graph state throughout the compilation flow. We take LLVM’s MLIR framework and propose a new MLIR dialect named eqsat that represents e-graphs in MLIR code. This not only provides opportunities to rethink e-matching and extraction techniques by orchestrating existing MLIR passes, such as common subexpression elimination, but also avoids translation overhead between the chosen e-graph library and MLIR. Our eqsat intermediate representation (IR) allows programmers to apply equality saturation on arbitrary domain-specific IRs using the same flow as other compiler transformations in MLIR.
This program is tentative and subject to change.
Tue 17 JunDisplayed time zone: Seoul change
10:30 - 12:00 | |||
10:30 20mTalk | eqsat: An Equality Saturation Dialect for Non-destructive Rewriting EGRAPHS Jules Merckx Ghent University, Alexandre Lopoukhine University of Cambridge, Samuel Coward Imperial College London, UK / Intel Corporation, Jianyi Cheng University of Edinburgh, UK, Bjorn De Sutter Ghent University, Belgium , Tobias Grosser University of Cambridge Pre-print | ||
10:50 20mTalk | Hatching Theory Instantiations with Yardbird EGRAPHS Cole Vick University of Texas at Austin, Samuel Thomas The University of Texas at Austin, Texas, USA | ||
11:10 20mTalk | Automated High-Level Synthesis Design Modularization via E-Graph Anti-Unification EGRAPHS Andy Wanna Georgia Institute of Technology, Cong "Callie" Hao Georgia Institute of Technology, Theo Drane AMD |