Speeding up symbolic reasoning for relational queries

Speeding up symbolic reasoning for relational queries
复制标题

加速关系查询的符号推理

DOI:
--
复制
发表时间:
2018
期刊:
Proc. ACM Program. Lang.
影响因子:
--
通讯作者:
Rastislav Bodík
Rastislav Bodík
中科院分区:
--
文献类型:
--
作者:
Chenglong Wang;Alvin Cheung;Rastislav Bodík

文献摘要

被引文献

相似文献

对关系查询进行推理的能力在许多类型的数据库应用程序中扮演着重要的角色,例如测试数据生成、查询等价性检查和计算机辅助查询创作。不幸的是,关系查询的符号推理可能具有挑战性,因为关系表是元组的多个集(包),而底层语言(如SQL)可能会在元组之间引入复杂的计算。我们提出了一种空间求精算法,合理地减少了这类应用程序需要考虑的表空间。精化过程独立于特定的数据集应用,使用查询语言的抽象语义来利用查询输出中的元组的起源来修剪搜索空间。我们实现了精化算法,并使用三个推理任务在SQL上对其进行了评估:有界查询等价检查、操作关系数据的应用程序的测试生成和数据库应用程序的并列测试。使用真实世界的基准测试,我们的精化算法在对一大类具有挑战性的SQL查询进行推理时,显著加快了SQL求解器的速度(高达100倍),例如那些具有聚合的查询。
The ability to reason about relational queries plays an important role across many types of database applications, such as test data generation, query equivalence checking, and computer-assisted query authoring. Unfortunately, symbolic reasoning about relational queries can be challenging because relational tables are multisets (bags) of tuples, and the underlying languages, such as SQL, can introduce complex computation among tuples. We propose a space refinement algorithm that soundly reduces the space of tables such applications need to consider. The refinement procedure, independent of the specific dataset application, uses the abstract semantics of the query language to exploit the provenance of tuples in the query output to prune the search space. We implemented the refinement algorithm and evaluated it on SQL using three reasoning tasks: bounded query equivalence checking, test generation for applications that manipulate relational data, and concolic testing of database applications. Using real world benchmarks, we show that our refinement algorithm significantly speeds up (up to 100×) the SQL solver when reasoning about a large class of challenging SQL queries, such as those with aggregations.