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

CCRI：新：孵化蛋：开发可扩展、有凝聚力的平等饱和生态系统和社区

• 批准号: 2232339
• 负责人: Zachary Tatlock
• 金额: $ 199.91万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-06-15 至 2026-05-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2232339&HistoricalAwards=false
• 关键词: CCRI; New; Incubating; egg; Developing

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.

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