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

社会依赖于Web应用程序来完成许多重要任务，从银行业务，在线购物到社交媒体。大多数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.