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

许多编程工具需要分析和转换程序，以使它们更快，并保证它们的正确性。实现这些目标的最常见方法之一是通过简单的“查找和替换”规则，也称为重写规则。从本质上讲，工程师指定了一大堆规则，然后一个接一个地重复应用，以简化原始程序的更好版本。虽然这种方法很简单，但它需要专家付出大量的努力才能使其有效，因为结果的质量在很大程度上取决于规则运行的顺序，并且没有适用于所有程序的单一最佳顺序。研究人员最近开发了一种新的方法，称为相等饱和，可以同时重复应用所有规则，从而为所有不同的重写顺序生成程序的所有版本。他们的框架被称为EGG，已被用于为机器学习应用程序构建最先进的编译器，用于3D打印的计算机辅助设计工具，以及自动修复科学计算中的舍入误差。然而，这些成功也突出了一些限制，这些限制使得新用户很难采用EGG并扩展基于EGG的应用程序。该项目旨在通过围绕EGG建立一个开源生态系统来解决这些挑战，以统一平等饱和的几个最新进展，并培养一个强大和可持续的社区来支持其使用。该项目的新颖之处在于为EGG提供了改进的算法，以便更有效地找到应用重写的机会，并支持灵活的机制来选择EGG在搜索过程中发现的程序的“最佳”版本。该项目的影响是将EGG扩展到具有更大程序的领域，并为想要快速轻松地构建最先进的程序分析和转换工具的新用户降低进入门槛。该项目的技术方法包括为复杂模式实现新的关系电子匹配算法，适应基于草图的提取，以及支持破坏性重写的新技术。破坏性重写是非常有前途的，在结合和交换重写导致用于编码一组模等价项的底层相等图（e-graph）数据结构爆炸的领域是必不可少的。在这些领域，规范化重写已被证明是有前途的，但是在EGG中编码它们以前需要对电子图进行特别的操作。研究人员希望这些进展能够改善现有EGG系统的性能和可扩展性。此外，将开发新的基础设施来支持调试和可视化工具、可重用分析和规则集、教育和培训资源、基准套件和数据集，以提高系统的可用性。总之，研究人员相信这些创新将建立必要的基础设施，使广大用户能够快速轻松地构建跨不同领域的程序分析器、优化器和合成器。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.