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

New York University, New York NY

Investigators

Abstract

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.