JetStream: Generating Verified Query Accelerators for Existing Database Systems
Akhilesh Balasingam, Amadou Ngom, Geoffrey X. Yu, Tim Kraska
Recent work has shown that LLMs can synthesize highly instance-optimized database systems for fixed workloads, but to date these systems only replace the DBMS's native storage and assume static data: users must migrate their data, often give up ad-hoc queries, lose acceleration once the data changes, and lack formal correctness guarantees. We present JetStream, which instead generates query-specific accelerators that extend an existing DBMS. Given a set of parameterized query templates, a staged agentic workflow synthesizes accelerators that run directly over the DBMS's native tables and may maintain custom auxiliary state, while the host DBMS remains responsible for storage, transactions, recovery, and all the other queries. A fixed, engine-neutral substrate keeps auxiliary state transactionally consistent under writes, while generated backend adapters handle engine-specific hooks. JetStream generates two kinds of accelerators: tested accelerators, which may use any optimization and are validated by differential testing, and verified accelerators, which trade some performance for a machine-checked proof that every answer satisfies a trusted specification derived from the SQL. On TPC-H at SF=20, JetStream achieves a $584\times$ geomean read speedup over DuckDB ($89\times$ verified) and retains $139\times$ ($46\times$ verified) under a continuous update stream of 10,000 modified rows per second.
尚无 AI 解读,展示原文摘要