CCRI: New: Incubating egg: Developing a Scalable, Cohesive Equality Saturation Ecosystem and Community

点击翻译按钮获取中文摘要

Many programming tools need to analyze and transform programs in order to make them faster and to guarantee their correctness. One of the most common approaches to achieve such goals is via simple "find and replace" rules, also known as rewrite rules. Essentially, engineers specify a large set of rules which are then repeatedly applied one-after-another to simplify a better version of the original program. While this approach is simple, it requires substantial effort from experts to make it effective because the quality of the results depends heavily on the order in which the rules are run and there is no single best order for all programs. The investigators recently developed a new approach called Equality Saturation which enables repeatedly applying all the rules simultaneously, thus generating all versions of the program for all different orders of rewrites. Their framework called EGG has been used to build state-of-the-art compilers for Machine Learning applications, Computer-Aided Design tools for 3D printing, and to automatically repair rounding errors in scientific computations. However, the successes also highlighted some limitations that make it difficult for new users to adopt EGG and to scale applications built on EGG. The project seeks to address these challenges by establishing an open-source ecosystem around EGG to unify several recent advances in Equality Saturation and fostering a robust and sustainable community to support its use. The project's novelties are providing improved algorithms for EGG to find opportunities to apply rewrites more efficiently and supporting flexible mechanisms for selecting the "best" version of a program discovered during EGG's search. The project's impacts are scaling EGG to domains with larger programs and lowering the barrier to entry for new users who want to quickly and easily build state-of-the-art program analysis and transformation tools.The technical approach of the project includes the implementation of novel relational e-matching algorithms for complex patterns, the adaptation of sketch-based extraction, and new techniques to support destructive rewriting. Destructive rewriting is very promising, essential in domains where associative and commutative rewrites lead to blow ups in the underlying equality graph (e-graph) data structure used to encode a set of terms modulo equivalence. In such domains, canonicalizing rewrites have proven promising, but encoding them in EGG previously required ad hoc manipulation of the e-graph. The investigators expect these advances to improve the performance and scalability of the existing EGG system. Additionally, new infrastructure to support debugging and visualization tools, reusable analyses and rulesets, educational and training resources, benchmark suites and datasets will be developed, to improve the usability of the system. Together, the investigators believe these innovations will establish the infrastructure necessary to enable a broad class of users to quickly and easily build program analyzers, optimizers, and synthesizers across diverse domains.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.