Collaborative Research: FMitF: Track I: Automatic Discovery and Verification of Database Query Transformations

合作研究：FMitF：第一轨：数据库查询转换的自动发现和验证

• 批准号: 2220407
• 负责人: Jinyang Li
• 金额: $ 40万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2220407&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; Automatic

Society depends on web applications for many important tasks, ranging from banking, online shopping to social media. Most web applications rely on a database to store and query user or application data. As a result, query-processing time is critical for users’ experience. Existing databases can transform a query into one that executes faster using a set of manually specified strategies. The project team has conducted a study of popular web applications and found that existing databases fail to transform many queries, with dire performance consequences. The project’s novelties are to develop a system that can automatically discover new transformation strategies to improve query performance. The project's broader significance and importance are to greatly improve the database query processing time, thereby accelerating the end-to-end performance of web applications.Databases accelerate queries via query rewriting. Traditional query rewriting relies on pre-specified rules to transform a source query into an equivalent but more efficient destination query. Existing rules are crafted by human experts. Unfortunately, the rich features and subtle semantics of queries make it challenging to manually discover rules while guaranteeing their correctness. As a result, the set of hand-written rules grows very slowly and misses many rewrite opportunities. This project automates the process of discovering query rewrite rules and proving their correctness. The main insight is to model a rewrite rule as a pair of generic logical-query plans together with a set of constraints that ensure equivalent transformation. Doing so allows one to enumerate all generic logical-query plans up to some threshold size and to search for the set of necessary conditions that make a pair of enumerated plans equivalent. The project also develops a rule verifier that proves correctness using an SMT solver by converting a rule into first-order logic formulas.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.

社会依赖 Web 应用程序来完成许多重要任务，从银行、在线购物到社交媒体，大多数 Web 应用程序都依赖数据库来存储和查询用户或应用程序数据。因此，查询处理时间对于用户体验至关重要。现有数据库可以使用一组手动指定的策略将查询转换为执行速度更快的查询，该项目团队对流行的 Web 应用程序进行了研究，发现现有数据库无法转换许多查询，从而导致了可怕的性能后果。是要开发一个系统，可以自动发现新的转换策略来提高查询性能 该项目更广泛的意义和重要性是大大提高数据库查询处理时间，从而加速Web应用程序的端到端性能。数据库通过查询重写来加速查询。不幸的是，查询的丰富功能和微妙语义使得手动发现规则同时保证其正确性变得具有挑战性。结果，手写规则集增长非常缓慢，并且错过了许多重写机会，该项目自动执行发现查询重写规则并证明其正确性的过程，其主要见解是将重写规则建模为一对通用逻辑查询计划。一组确保等效转换的约束允许枚举达到某个阈值大小的所有通用逻辑查询计划，并搜索使一对枚举计划等效的必要条件集。该项目还开发了一条规则。验证者通过将规则转换为一阶逻辑公式，使用 SMT 求解器证明了正确性。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。