FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Verification of Rewriting-based Query Optimizers

Authors: Aalok Thakkar, Balaji Krishnamurthy and Piyush Gupta

Paper Information

Title:Verification of Rewriting-based Query Optimizers
Authors:Aalok Thakkar, Balaji Krishnamurthy and Piyush Gupta
Proceedings:WST WST2018proceedings
Editor: Salvador Lucas
Keywords:Rewriting, Verification, Query Optimization
Abstract:

ABSTRACT. We report on our ongoing work on automated verification of rewriting-based query optimizers. Rewriting-based query optimizers are a widely adapted in relational database architecture however, designing these rewrite systems remains a challenge. In this paper, we discuss automated termination analysis of optimizers where rewrite-rules are expressed in a SQL-like programming language called HoTTSQL, for which semantic equivalence is decidable and a rich theory and some tools have been developed. We discuss how it is not sufficient to reason about rule specific (local) properties such as semantic equivalence, and it is necessary to work with set-of-rules specific (global) properties such as termination and loop-freeness to prove correctness of the optimizer. We put forward a way to translate the rules in HoTTSQL and reason termination using Tyrolean Termination Tool 2.

Pages:1
Talk:Jul 19 14:30 (Session 134I: Complexity / Applications)
Paper: