Wed 23 Oct 2024 14:40 - 15:00 at IBR West - Performance Analysis and Optimisation 1 Chair(s): Manu Sridharan

Equality graphs (e-graphs) are used to compactly represent equivalence classes of terms in symbolic reasoning systems. Beyond their original roots in automated theorem proving, e-graphs have been used in a variety of applications. They have become particularly important as the key ingredient in the popular technique of equality saturation, which has notable applications in compiler optimization, program synthesis, program verification, and symbolic execution, among others. In a typical equality saturation workflow, an e-graph is used to store a large number of equalities that are generated by local rewrites during a saturation phase, after which an optimal term is extracted from the e-graph as the output of the technique. However, despite its crucial role in equality saturation, e-graph extraction has received relatively little attention in the literature, which we seek to start addressing in this paper. Extraction is a challenging problem and is notably known to be NP-hard in general, so current equality saturation tools rely either on slow optimal extraction algorithms based on integer linear programming (ILP) or on heuristics that may not always produce the optimal result. In fact, in this paper, we show that e-graph extraction is hard to approximate within any constant ratio. Thus, any such heuristic will produce wildly suboptimal results in the worst case. Fortunately, we show that the problem becomes tractable when the e-graph is sparse, which is the case in many practical applications. We present a novel parameterized algorithm for extracting optimal terms from e-graphs with low treewidth, a measure of how “tree-like” a graph is, and prove its correctness. We also present an efficient Rust implementation of our algorithm and evaluate it against ILP on a number of benchmarks extracted from the Cranelift benchmark suite, a real-world compiler optimization library based on equality saturation. Our algorithm optimally extracts e-graphs with treewidths of up to 10 in a fraction of the time taken by ILP. These results suggest that our algorithm can be a valuable tool for equality saturation users who need to extract optimal terms from sparse e-graphs.

Wed 23 Oct

Displayed time zone: Pacific Time (US & Canada) change

13:40 - 15:20
Performance Analysis and Optimisation 1OOPSLA 2024 at IBR West
Chair(s): Manu Sridharan University of California at Riverside
13:40
20m
Talk
Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning
OOPSLA 2024
Gabriel Ryan Columbia University, Burcu Cetin Columbia University, Christian Yongwhan Lim Columbia University, Suman Jana Columbia University
DOI
14:00
20m
Talk
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations
OOPSLA 2024
Luke Geeson University College London, James Brotherston , Wilco Dijkstra Arm Ltd, Alastair F. Donaldson Imperial College London, Lee Smith Arm, Tyler Sorensen University of California at Santa Cruz, John Wickerson Imperial College London
DOI Media Attached
14:20
20m
Talk
Practical Verification Of Smart Contracts Using Memory Splitting
OOPSLA 2024
Shelly Grossman Tel Aviv University, Alexander Bakst Certora, Sameer Arora Certora Inc., John Toman Certora, inc., Chandrakana Nandi Certora, Mooly Sagiv Tel Aviv University
DOI
14:40
20m
Talk
Fast and Optimal Extraction for Sparse Equality GraphsOOPSLA 2024 Distinguished Paper Award
OOPSLA 2024
Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Chun Kit Lam Hong Kong University of Science and Technology, Lionel Parreaux HKUST (The Hong Kong University of Science and Technology)
DOI
15:00
20m
Talk
HybridSA: GPU Acceleration of Multi-Pattern Regex Matching using Bit Parallelism
OOPSLA 2024
Alexis Le Glaunec Rice University, Lingkun Kong Rice University, Konstantinos Mamouras Rice University
DOI