III: Medium: Collaborative Research: Reasoning about Optimizers for Data-Intensive Systems

今天，我们见证了新的数据密集型系统的爆炸式增长，无论是传统的数据处理还是机器学习，这些系统都迫切需要为其声明性语言提供强大的优化器。开发和验证这样的优化器是非常困难的：在过去，它们仅由少数具有专门团队的商业数据库供应商开发，而大多数现代系统是由没有此类专业知识的小团队开发的。为了应对这一挑战，该项目研究并实现了在数据密集型系统中验证查询优化规则的自动化方法。具体而言，本项目将有四个研究重点：(1)我们将开发基于半环代数恒等式的公理基础，将其作为框架实现，并将其应用于验证现有系统中的优化规则。(2)我们将扩展框架来推理结合线性代数和关系代数的语言，例如操作向量、矩阵和张量的语言，并扩展验证器来推理张量优化规则。(3)我们将对用于验证优化规则的基于半环的公理系统的完备性和可判定性进行理论研究，并专门针对各种查询语言片段进行研究。(4)我们将为声明性查询语言的自动推理构建一个新的基于云的基础设施，使研究人员能够轻松地为不同的数据密集型系统开发可执行语义，使形式化方法研究人员能够开发针对查询语言推理的新技术，并使应用程序开发人员能够利用我们的基础设施构建新的应用程序。在这个项目中开发的所有软件工件都将向公众发布，并计划在本科和研究生课程中使用它们。任何从开放源代码收集的基准都将被聚合到一个公开访问的存储库中，目的是使该领域的研究人员和实践者能够进行实验并重现结果。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Today, we witness an explosion of new data-intensive systems, both for traditional data processing and for machine learning, and these systems critically require powerful optimizers for their declarative languages. Developing and verifying such optimizers is very difficult: in the past, they were developed only by a small number of commercial database vendors with dedicated teams, while most modern systems are developed by small teams without such expertise. To address this challenge, this project studies and implements automated methods for verifying query optimization rules in data-intensive systems.Specifically, this project will have four research focuses: (1) We will develop an axiomatic foundation based on algebraic identities in a semiring, implement it as a framework, and apply it to verify optimization rules in existing systems. (2) We will extend the framework to reason about languages that combine linear algebra with relational algebra, for example languages that manipulate vectors, matrices, and tensors, and extend the verifier to reason about tensor optimization rules. (3) We will conduct a theoretical study of the completeness and decidability of the semiring-based axiomatic system used for verifying optimization rules, and specialize this study for various query language fragments. (4) We will build a new cloud-based infrastructure for automated reasoning of declarative query languages, to enable researchers to easily develop executable semantics for different data-intensive systems, formal methods researchers to develop new techniques targeted for query language reasoning, and application developers to build new applications that make use of our infrastructure.All software artifacts developed in this project will be released to the public, with plans to incorporate their usage in both the undergraduate and graduate curricula. Any collected benchmarks from open source will be aggregated into a repository that is publicly accessible, with the goal to enable researchers and practitioners in the field to experiment and reproduce the results.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.