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

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

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.