English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

Term Rewriting Systems (TRSs) are used in compilers to simplify and proveexpressions. State-of-the-art TRSs in compilers use a greedy algorithm thatapplies a set of rewriting rules in a predefined order (where some of the rulesare not axiomatic). This leads to a loss of the ability to simplify certainexpressions. E-graphs and equality saturation sidestep this issue byrepresenting the different equivalent expressions in a compact manner fromwhich the optimal expression can be extracted. While an e-graph-based TRS canbe more powerful than a TRS that uses a greedy algorithm, it is slower becauseexpressions may have a large or sometimes infinite number of equivalentexpressions. Accelerating e-graph construction is crucial for making the use ofe-graphs practical in compilers. In this paper, we present Caviar, ane-graph-based TRS for proving expressions within compilers. The main advantageof Caviar is its speed. It can prove expressions much faster than base e-graphTRSs. It relies on three techniques: 1) a technique that stops e-graphs fromgrowing when the goal is reached, called Iteration Level Check; 2) a mechanismthat balances exploration and exploitation in the equality saturationalgorithm, called Pulsing Caviar; 3) a technique to stop e-graph constructionbefore reaching saturation when a non-provable pattern is detected, calledNon-Provable Patterns Detection (NPPD). We evaluate caviar on Halide, anoptimizing compiler that relies on a greedy-algorithm-based TRS to simplify andprove its expressions. The proposed techniques allow Caviar to acceleratee-graph expansion for the task of proving expressions. They also allow Caviarto prove expressions that Halide's TRS cannot prove while being only 0.68xslower.

Caviar: An E-graph Based TRS for Automatic Code Optimization