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

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

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.