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.