TY - GEN
T1 - Caviar
T2 - 31st ACM SIGPLAN International Conference on Compiler Construction, CC 2022
AU - Kourta, Smail
AU - Namani, Adel Abderahmane
AU - Benbouzid-Si Tayeb, Fatima
AU - Hazelwood, Kim
AU - Cummins, Chris
AU - Leather, Hugh
AU - Baghdadi, Riyadh
N1 - Publisher Copyright:
© 2022 ACM.
PY - 2022/9/19
Y1 - 2022/9/19
N2 - Term Rewriting Systems (TRSs) are used in compilers to simplify and prove expressions. State-of-The-Art TRSs in compilers use a greedy algorithm that applies a set of rewriting rules in a predefined order (where some of the rules are not axiomatic). This leads to a loss of the ability to simplify certain expressions. E-graphs and equality saturation sidestep this issue by representing the different equivalent expressions in a compact manner from which the optimal expression can be extracted. While an e-graph-based TRS can be more powerful than a TRS that uses a greedy algorithm, it is slower because expressions may have a large or sometimes infinite number of equivalent expressions. Accelerating e-graph construction is crucial for making the use of e-graphs practical in compilers. In this paper, we present Caviar, an e-graph-based TRS for proving expressions within compilers. The main advantage of Caviar is its speed. It can prove expressions much faster than base e-graph TRSs. It relies on three techniques: 1) a technique that stops e-graphs from growing when the goal is reached, called Iteration Level Check; 2) a mechanism that balances exploration and exploitation in the equality saturation algorithm, called Pulsing Caviar; 3) a technique to stop e-graph construction before reaching saturation when a non-provable pattern is detected, called Non-Provable Patterns Detection (NPPD). We evaluate caviar on Halide, an optimizing compiler that relies on a greedy-Algorithm-based TRS to simplify and prove its expressions. The proposed techniques allow Caviar to accelerate e-graph expansion for the task of proving expressions. They also allow Caviar to prove expressions that Halide's TRS cannot prove while being only 0.68x slower. Caviar is publicly available at: https://github.com/caviar-Trs/caviar.
AB - Term Rewriting Systems (TRSs) are used in compilers to simplify and prove expressions. State-of-The-Art TRSs in compilers use a greedy algorithm that applies a set of rewriting rules in a predefined order (where some of the rules are not axiomatic). This leads to a loss of the ability to simplify certain expressions. E-graphs and equality saturation sidestep this issue by representing the different equivalent expressions in a compact manner from which the optimal expression can be extracted. While an e-graph-based TRS can be more powerful than a TRS that uses a greedy algorithm, it is slower because expressions may have a large or sometimes infinite number of equivalent expressions. Accelerating e-graph construction is crucial for making the use of e-graphs practical in compilers. In this paper, we present Caviar, an e-graph-based TRS for proving expressions within compilers. The main advantage of Caviar is its speed. It can prove expressions much faster than base e-graph TRSs. It relies on three techniques: 1) a technique that stops e-graphs from growing when the goal is reached, called Iteration Level Check; 2) a mechanism that balances exploration and exploitation in the equality saturation algorithm, called Pulsing Caviar; 3) a technique to stop e-graph construction before reaching saturation when a non-provable pattern is detected, called Non-Provable Patterns Detection (NPPD). We evaluate caviar on Halide, an optimizing compiler that relies on a greedy-Algorithm-based TRS to simplify and prove its expressions. The proposed techniques allow Caviar to accelerate e-graph expansion for the task of proving expressions. They also allow Caviar to prove expressions that Halide's TRS cannot prove while being only 0.68x slower. Caviar is publicly available at: https://github.com/caviar-Trs/caviar.
KW - Algebraic expressions simplification
KW - Equality Graphs
KW - Equality Saturation
KW - Term Rewriting Systems
UR - http://www.scopus.com/inward/record.url?scp=85127883482&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85127883482&partnerID=8YFLogxK
U2 - 10.1145/3497776.3517781
DO - 10.1145/3497776.3517781
M3 - Conference contribution
AN - SCOPUS:85127883482
T3 - CC 2022 - Proceedings of the 31st ACM SIGPLAN International Conference on Compiler Construction
SP - 54
EP - 64
BT - CC 2022 - Proceedings of the 31st ACM SIGPLAN International Conference on Compiler Construction
A2 - Egger, Bernhard
A2 - Smith, Aaron
PB - Association for Computing Machinery, Inc
Y2 - 2 April 2022 through 3 April 2022
ER -