Knuth-Bendix completion boosts program optimization speed and quality
Augmenting Rewrite Rule Sets via Knuth-Bendix Completion
Programming Languages
Summary
Optimizing computer programs is tricky because the order of changes can affect the outcome. The authors studied a way to automatically generate rules that help explore many possible program changes without missing good ones. They showed that their method speeds up finding better program versions by adding new rules that were not manually created before. This means program optimization can become more efficient and catch improvements previously overlooked.
What this means in practice
- •For compiler developers: Enhance compilers by automatically generating rewrite rules that find better program optimizations faster.
- •For software performance engineers: Improve software performance tuning by using expanded rule sets to explore more optimization opportunities.
Authors
Michael Schifferer, Marcel Ullrich, Sebastian Hack
Abstract
Equality Saturation (EqSat) is a powerful technique for program optimization, systematically exploring the search space of candidate programs to overcome the phase ordering problem. However, the feasibility and performance of EqSat rely heavily on the specific rewrite rules used to derive equivalent programs. These rule sets are typically handcrafted, requiring extensive domain expertise and carrying the risk of missing valuable transformations. In this work, we evaluate Knuth-Bendix Completion (KBC) as a method for automatically generating and augmenting rewrite rules for EqSat. Our experiments show faster optimization as well as reaching better terms with previously missed optimizations.