On the Optimization of Equivalent Concurrent Computations
Henrich Lauko, Luk\'a\v{s} Koren\v{c}ik, Peter Goodman

TL;DR
This paper introduces a novel approach using extended e-graphs to optimize concurrent computations by identifying and merging equivalent subcomputations, a capability not present in existing equality saturation frameworks.
Contribution
It extends equality saturation techniques to handle concurrent environments, enabling optimization of equivalent concurrent computations through non-local reasoning.
Findings
First framework to optimize concurrent computations via equality saturation.
Successfully merges equivalent concurrent subcomputations.
Provides a new method for optimizing parallel code.
Abstract
In this submission, we explore the use of equality saturation to optimize concurrent computations. A concurrent environment gives rise to new optimization opportunities, like extracting a common concurrent subcomputation. To our knowledge, no existing equality saturation framework allows such an optimization. The challenge with concurrent environments is that they require non-local reasoning since parallel computations are inherently unrelated and disjoint. This submission presents a new approach to optimizing equivalent concurrent computations: extending e-graphs to capture equal concurrent computations in order to replace them with a single computation.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsConstraint Satisfaction and Optimization · Formal Methods in Verification · Logic, Reasoning, and Knowledge
