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

III：媒介：协作研究：数据密集型系统优化器的推理

• 批准号: 1954222
• 负责人: Dan Suciu
• 金额: $ 50万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-09-01 至 2023-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1954222&HistoricalAwards=false
• 关键词: III; Medium; Collaborative; Research; Reasoning

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.

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

项目成果

Convergence of Datalog over (Pre-) Semirings

• DOI: 10.1145/3517804.3524140
• 发表时间: 2021-05
• 期刊: Proceedings of the 41st ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems
• 作者: Mahmoud Abo Khamis;H. Ngo;R. Pichler;Dan Suciu;Y. Wang

Free Join: Unifying Worst-Case Optimal and Traditional Joins

自由连接：统一最坏情况的最优连接和传统连接

• DOI: 10.1145/3589295
• 发表时间: 2023
• 期刊: Proceedings of the ACM on Management of Data
• 作者: Wang, Yisu Remy;Willsey, Max;Suciu, Dan
• 通讯作者: Suciu, Dan

A Near-Optimal Parallel Algorithm for Joining Binary Relations

一种二元关系连接的近最优并行算法

• DOI: 10.46298/lmcs-18(2:6)2022
• 发表时间: 2022
• 期刊: Logical Methods in Computer Science
• 影响因子: 0.6
• 作者: Ketsman, Bas;Suciu, Dan;Tao, Yufei
• 通讯作者: Tao, Yufei

Optimizing Recursive Queries with Progam Synthesis

• DOI: 10.1145/3514221.3517827
• 发表时间: 2022-02
• 期刊: Proceedings of the 2022 International Conference on Management of Data
• 作者: Y. Wang;Mahmoud Abo Khamis;H. Ngo;R. Pichler;Dan Suciu

Optimizing Tensor Programs on Flexible Storage

在灵活存储上优化张量程序

• DOI: 10.1145/3588717
• 发表时间: 2023
• 期刊: Proceedings of the ACM on Management of Data
• 作者: Schleich, Maximilian;Shaikhha, Amir;Suciu, Dan
• 通讯作者: Suciu, Dan