Analytical and Empirical Tools for Advanced Query Optimizer Engineering

数据库查询优化器是容易出现错误的复杂系统。其目的是通过开发一个设计过程来对抗这种现象，该设计过程将可以形式化和推理的区域与需要制作和实验的区域分开。形式化技术应用于优化器模块（或规则块）的规范，可以通过表示可证明的规则和规则触发策略来构造优化器模块。规则是声明式地表达的（即，没有代码），以允许定理证明者验证。规则块对相关规则进行分组，并提出解雇它们的命令和决定何时解雇合适的策略。相关的工具可以自动执行规则验证，并允许可视化规则和规则块对查询的影响。将经过验证的模块组装成一个可行的整体需要进行实验和评估。在此过程中提供帮助的工具允许可视化组合优化器对给定查询集的控制流，并测量查询转换的结果所带来的性能改进。该项目的目的是开发一种方法和相关的工具套件，用于开发有效、正确和可扩展的查询优化器。这项工作有助于查询优化器的规范、设计、验证和经验评估。

Database query optimizers are complex systems prone to bugs. The intention is to counter this phenomenon by developing a design process that separates the areas that can be formalized and reasoned about from those that require crafting and experimentation. Formal techniques are applied to the specification of optimizer modules (or rule blocks), which can be constructed by expressing provable rules and rule firing strategies. Rules are expressed declaratively (i.e., without code) to permit theorem prover verification. Rule blocks group related rules and propose an order for firing them and a strategy for deciding when firing is appropriate. Associated tools automate rule verification, and permit the effects of rules and rule blocks on queries to be visualized. Assembly of proven modules into a workable whole requires experimentation and evaluation. Tools to assist in this process permit visualization of the assembled optimizer's flow of control on given query sets, and measurement of the performance improvements as a result of transformations of queries. The aim of the project is to develop a methodology and associated suite of tools for the development of effective, correct and extensible query optimizers. This work contributes to the specification, design, verification and empirical evaluation of query optimizers.