【論文分享｜SIGMOD'22】WeTune 自動(dòng)發(fā)現(xiàn)和驗(yàn)證重寫規(guī)則
作者：謝其駿
北京航空航天大學(xué)在讀碩士，?Databend 研發(fā)工程師實(shí)習(xí)生
https://github.com/jun0315
論文原文：
Zhaoguo Wang, Zhou Zhou, Yicun Yang, Haoran Ding, Gansen Hu, Ding Ding, Chuzhe Tang, Haibo Chen, Jinyang Li. WeTune: Automatic Discovery and Verification of Query Rewrite Rules. 2022 ACM SIGMOD International Conference on Management of Data (SIGMOD'22)
源碼地址：
https://ipads.se.sjtu.edu.cn:1312/opensource/wetune
本文的貢獻(xiàn)：
本文借鑒了編譯器超優(yōu)化的思想，通過列舉所有有效的邏輯查詢計(jì)劃來嘗試發(fā)現(xiàn)潛在的等效計(jì)劃，從而自動(dòng)發(fā)現(xiàn)新的更有效的重寫規(guī)則。
本文還提出了一個(gè)新的基于 SMT 的驗(yàn)證器，以驗(yàn)證不同枚舉下兩個(gè)查詢的等價(jià)性。
Abstract
查詢重寫將一個(gè)關(guān)系型數(shù)據(jù)庫的查詢轉(zhuǎn)換為一個(gè)等價(jià)的更高效的查詢，這對(duì)數(shù)據(jù)庫應(yīng)用的性能至關(guān)重要。這些重寫依賴于預(yù)先指定的重寫規(guī)則，在現(xiàn)有的系統(tǒng)中，這些重寫規(guī)則是通過人工洞察發(fā)現(xiàn)的，并在多年中慢慢積累。
圖一：Query Rewrite in Apache Calcite
本文介紹了 WeTune，一個(gè)自動(dòng)發(fā)現(xiàn)新的重寫規(guī)則的規(guī)則生成器，受到編譯器超優(yōu)化的啟發(fā)，WeTune 枚舉了一定閾值下的所有有效的邏輯查詢計(jì)劃，并試圖發(fā)現(xiàn)可能導(dǎo)致更有效重寫的等效計(jì)劃。核?挑戰(zhàn)是確定哪?組條件（約束）可以來證明這?對(duì)查詢計(jì)劃之間的等價(jià)性。通過枚舉每對(duì)查詢之間的表及其屬性相關(guān)的約束的組合情況，來解決這?挑戰(zhàn)。
本文還提出了?種新的基于 SMT 的驗(yàn)證器來驗(yàn)證查詢對(duì)在不同枚舉約束下的等價(jià)性。為了評(píng)估 WeTune 發(fā)現(xiàn)的重寫規(guī)則的有效性，我們將它們應(yīng)?于從 GitHub 上 20個(gè)最流?的開源 Web 應(yīng)?程序收集的 SQL 查詢。WeTune 成功優(yōu)化了現(xiàn)有數(shù)據(jù)庫?法優(yōu)化的 247 個(gè)查詢，從?實(shí)現(xiàn)了顯著的性能提升。
Introduce
查詢重寫，將原始查詢轉(zhuǎn)換為語義等價(jià)的替代查詢，是查詢優(yōu)化的重要步驟。有效的重寫可以將輸?查詢的執(zhí)?時(shí)間加快?個(gè)數(shù)量級(jí)。重寫依賴于指定查詢之間等價(jià)關(guān)系的規(guī)則?，F(xiàn)有的規(guī)則通常由?類專家制定，可能需要數(shù)?年才能積累。
然?，僅僅依靠??來發(fā)現(xiàn)重寫規(guī)則是不夠的。查詢語?豐富的特性和微妙的語義使得證明等價(jià)性和編寫規(guī)則具有挑戰(zhàn)性。但是由于?寫的重寫規(guī)則集增??常緩慢，錯(cuò)過了許多重寫機(jī)會(huì)。在 Web 應(yīng)?程序開發(fā)中普遍使?對(duì)象關(guān)系映射 (ORM) 框架使情況變得更糟。ORM 使程序員?需顯式構(gòu)建 SQL 查詢，但也會(huì)產(chǎn)??直觀的查詢，其模式會(huì)避開?類制定的規(guī)則。
為了了解遺漏重寫的影響，我們研究了 Github 上?個(gè)流?的開源 Web 應(yīng)?程序中的 50 個(gè)真實(shí)查詢。所有這些查詢都已被開發(fā)?員重寫以修復(fù)它們的性能問題。即使是最新版本的 SQL Server 也未能將其中 27 個(gè)查詢 (54%) 重寫為開發(fā)?員?動(dòng)修復(fù)的更?效的形式。?個(gè)這樣的查詢會(huì)導(dǎo)致延遲?達(dá) 37 秒，?其等效的重寫查詢只需要 0.3 秒。
在本?中，我們提出了 WeTune，這是?種規(guī)則?成器，?需任何??操作即可?動(dòng)發(fā)現(xiàn)新的重寫規(guī)則。從編譯器超優(yōu)化中汲取靈感，它通過窮舉搜索找到語義上等效的最佳代碼序列，WeTune 旨在通過對(duì)所有潛在規(guī)則的枚舉?動(dòng)發(fā)現(xiàn)重寫規(guī)則，然后對(duì)每個(gè)?成的規(guī)則進(jìn)?正確性檢查。在此發(fā)現(xiàn)過程中，WeTune 依靠啟發(fā)式?法過濾掉那些不太可能提?性能的規(guī)則，也就是?原始查詢運(yùn)算符更多的規(guī)則，其余的重寫規(guī)則被認(rèn)為是有希望的。
盡管大體的方法比較簡單，但是也存在著以下一些挑戰(zhàn)：
如何有效的枚舉查詢規(guī)則
a. 一方面需要在有效的搜索空間當(dāng)中發(fā)現(xiàn)具有代表性的查詢計(jì)劃。
b. 另一方面為了產(chǎn)生一般性的規(guī)則， 我們需要避免過度嚴(yán)苛的約束條件。
怎么驗(yàn)證這些產(chǎn)生規(guī)則的正確性
a. 對(duì)一般的 query plan，現(xiàn)存的校驗(yàn)器無法驗(yàn)證正確性。
b. 需要一個(gè)新的校驗(yàn)器。
為了應(yīng)對(duì)上述挑戰(zhàn)，WeTune 將重寫規(guī)則表示為查詢計(jì)劃模版和一組與查詢計(jì)劃模版相關(guān)的約束。先在運(yùn)算符閾值以內(nèi)枚舉所有可能的查詢計(jì)劃模版，查詢計(jì)劃模版是通用的，它使用符號(hào)而不是具體的表、列和謂詞。接著會(huì)進(jìn)一步枚舉所有的約束條件，這些條件使得一對(duì)查詢計(jì)劃模版在語義上是等價(jià)的。
WeTune 使? SQL 驗(yàn)證器驗(yàn)證每個(gè)重寫規(guī)則的正確性。它包括?個(gè)內(nèi)置的驗(yàn)證器，它提供了?種將重寫規(guī)則建模為 SMT 公式的方法。然后使? SMT 求解器?動(dòng)解決正確性問題。除了內(nèi)置的驗(yàn)證器，WeTune 還可以?持使?現(xiàn)有的 SQL 驗(yàn)證器，如 SPES 來證明正確性。
文中還對(duì) WeTune 在現(xiàn)實(shí)世界中的有效性進(jìn)行了評(píng)估，選取了 GitHub 上 20 個(gè)最流?的 Web 應(yīng)?程序，WeTune 輸出 1106 條有希望的重寫規(guī)則，其中 35 條?于優(yōu)化這些應(yīng)?程序的查詢。此外，我們的結(jié)果表明，WeTune 可以成功優(yōu)化現(xiàn)有系統(tǒng)遺漏的 247 個(gè)查詢，從?將延遲減少?達(dá) 99%。這種優(yōu)化是由于 WeTune 能夠發(fā)現(xiàn)任何現(xiàn)有系統(tǒng)都不知道的新重寫規(guī)則。WeTune 可以成功驗(yàn)證發(fā)現(xiàn)的重寫規(guī)則。
Wetune?Approach
WeTune 主要包括三個(gè)部分，分別是規(guī)則枚舉器、規(guī)則校驗(yàn)器和有效規(guī)則選擇器。在 WeTune 中，首先會(huì)用規(guī)則枚舉器通過暴力的算法列舉出一切可能的規(guī)則，然后再用規(guī)則校驗(yàn)器去對(duì)每一個(gè)規(guī)則進(jìn)行正確性的校驗(yàn)。當(dāng)我們得到一組經(jīng)過校驗(yàn)的正確的規(guī)則之后，會(huì)把它輸入到有效規(guī)則選擇器中，然后有效規(guī)則選擇器會(huì)過濾出一系列的真正能夠提高數(shù)據(jù)庫性能的有用的規(guī)則。
圖二：WeTune 主要框架
??????? 規(guī)則枚舉器
規(guī)則枚舉器中總共分為三步，第一步是對(duì)所有可能的查詢計(jì)劃模版的一個(gè)枚舉，第二步是對(duì)每一對(duì)查詢計(jì)劃模版枚舉所有可能的約束條件，第三步是利用規(guī)則校驗(yàn)器來找到所有正確的規(guī)則。
圖三：規(guī)則枚舉器流程圖
在具體介紹之前，先介紹上文中提到的一些概念：
1?? 查詢計(jì)劃模版
查詢計(jì)劃模版是一顆樹，這棵樹上的每一個(gè)節(jié)點(diǎn)是帶有符號(hào)化的輸入或者是參數(shù)的關(guān)系代數(shù)的算子。在這篇文章中主要支持 6 種關(guān)系算子，每一個(gè)關(guān)系算子里面，每個(gè)關(guān)系算子的輸出都是一個(gè)單獨(dú)的關(guān)系。除了 input 算子之外，其他的算子都會(huì)需要 1 到 2 個(gè)關(guān)系作為輸入。在查詢計(jì)劃模版中，需要將之前那種具體的參數(shù)符號(hào)化，用 r 去表示一個(gè)關(guān)系，用 a 去表示一系列的屬性，用 p 表示一個(gè)謂詞邏輯。
圖四：支持的六種關(guān)系算子
2?? 規(guī)則
規(guī)則是一個(gè)三元組 (q src ,q dest ,C?) ,分別表示源查詢計(jì)劃模版、目標(biāo)查詢計(jì)劃模版和約束條件，約束條件是指參數(shù)化的約束條件一個(gè)集合，用符號(hào)來表示一些具體的名字。如果是一個(gè)正確的規(guī)則，意味著如果約束條件成立，那么源查詢計(jì)劃模版和目標(biāo)查詢計(jì)劃模版語義等價(jià)恒成立。
圖五：WeTune 發(fā)現(xiàn)的一個(gè)規(guī)則
3?? 枚舉查詢計(jì)劃模版
介紹完需要的概念之后，下面介紹規(guī)則枚舉器的第一步，枚舉查詢計(jì)劃模版。我們先從結(jié)點(diǎn)數(shù)量為一的模版進(jìn)行枚舉，然后當(dāng)結(jié)點(diǎn)數(shù)目超過一定數(shù)量的時(shí)候，就會(huì)停止枚舉。
下面以最大結(jié)點(diǎn)數(shù)為 2 進(jìn)行舉例：
圖六：枚舉查詢計(jì)劃舉例
第一步先列出所有可能的 6 種算子，然后把算子的葉子結(jié)點(diǎn)接著填充，當(dāng)達(dá)到最大數(shù)量的時(shí)候，停止枚舉。
4?? 枚舉約束條件
找到所有的查詢計(jì)劃模版之后，接著對(duì)每一對(duì)查詢計(jì)劃模版窮舉所有的約束條件，采用的是啟發(fā)式搜索方法，第一步需要找到一個(gè)初始的約束條件集，使得這一對(duì)查詢計(jì)劃模版在語義上是等價(jià)的，然后再對(duì)這個(gè)初始約束條件集不斷松弛，松弛的目的是讓這個(gè)規(guī)則更具有普遍性，找到初始條件集的一些子集，然后使這些子集也可以讓這個(gè)等價(jià)條件成立。
初始約束條件集是要枚舉所有可能的約束條件，本文定義了兩類約束條件：
符號(hào)關(guān)系約束類型
a. RelEq(r1,r2),AttrsEq(a1,a2),PredEq(p1,p2)
b. SubAttrs(a1,a2)：每個(gè)在 a1 中的屬性在 a2 中也有。
完整性約束類型
a. RefAttrs(r1,a1,r2,a2)：如果 a1 在 r1 中的話，那么 a2 也在 r2 中。
b. Unique(r,a)：r.a 是獨(dú)一無二的。
c. NotNull(r,a)：r.a 是非空的。
把一對(duì)查詢計(jì)劃模版中所有可能的約束條件都列出來，這些所有可能的約束條件的集合就形成了初始的約束條件集。找到初始約束條件集合后還要找到最松弛的約束條件子集，最松弛的含義是如果減少當(dāng)前約束條件集的任何一個(gè)條件，那么這個(gè)規(guī)則都不會(huì)恒成立。
圖七：規(guī)則枚舉器算法
在第 11 行中 ProveEq( q src ,q dest ,C * ) 會(huì)用到規(guī)則校驗(yàn)器。
??????? 規(guī)則校驗(yàn)器
本文提供了兩個(gè)規(guī)則校驗(yàn)器，一個(gè)是內(nèi)置的基于 FOL（一階邏輯表達(dá)式）的規(guī)則校驗(yàn)器，另一個(gè)是現(xiàn)有的 SQL 等價(jià)性校驗(yàn)器 SPES。
1?? 內(nèi)置規(guī)則校驗(yàn)器
內(nèi)置的規(guī)則校驗(yàn)器主要有兩個(gè)步驟，第一步是把從規(guī)則枚舉器中傳來的規(guī)則轉(zhuǎn)換成一階邏輯表達(dá)式，第二步是把一階邏輯表達(dá)式 SMT Solver 中，判斷每一個(gè)規(guī)則是否正確。
圖八：內(nèi)置規(guī)則校驗(yàn)器流程
1.1 規(guī)則形式化
給定一個(gè)規(guī)則，對(duì)于 q src 和 q dest ，我們先用 U 表達(dá)式來表示，然后再把 U 表達(dá)式轉(zhuǎn)換成一階邏輯表達(dá)式。對(duì)于 C 約束條件，我們直接轉(zhuǎn)換成一階邏輯表達(dá)式。
U 表達(dá)式是在包的語義下對(duì) SQL 查詢建模的一種方式，主要描述的是元組在一個(gè)關(guān)系表里面的出現(xiàn)的次數(shù)。
為了把查詢計(jì)劃模版轉(zhuǎn)換成 U 表達(dá)式，分成了兩個(gè)步驟：
翻譯查詢計(jì)劃模版中的符號(hào)
關(guān)系表符號(hào) rel 轉(zhuǎn)換成 ?r?(t)：Tuple->N ，表示元組到自然數(shù)的映射。
屬性符號(hào) attrs 轉(zhuǎn)換成 ?a?(t)：Tuple->Tuple，表示元組到元組的映射。
謂詞符號(hào) predicate 轉(zhuǎn)換成 ?p?(t)：Tuple->Bool，表示元組到布爾值的映射。
在樹結(jié)構(gòu)上以遍歷的方式翻譯查詢計(jì)劃
ToUExpr(q):<fl,tl>:=ToUExpr(q.child[0])?//None?if?no?child
????<fr,tr>:=ToUExpr(q.child[1])?//None?if?single?child
????return?TranslateByFigure9(q,fl,tl,fr,tr)
圖九：SQL 運(yùn)算符轉(zhuǎn)換成 U 表達(dá)式的規(guī)則
將查詢計(jì)劃模版轉(zhuǎn)換成 U 表達(dá)式之后，再根據(jù)圖十轉(zhuǎn)換成一階邏輯表達(dá)式。
圖十：U 表達(dá)式轉(zhuǎn)換成一階邏輯表達(dá)式的規(guī)則
接著再根據(jù)圖十一把約束條件轉(zhuǎn)換成一階邏輯表達(dá)式。
圖十一：約束條件轉(zhuǎn)換成一階邏輯表達(dá)式的規(guī)則
1.2 驗(yàn)證規(guī)則
把查詢計(jì)劃模版和約束條件轉(zhuǎn)換成一階邏輯表達(dá)式之后，接著使用 SMT 求解器來進(jìn)行檢查正確性。
規(guī)則的正確性定義為：
為了證明一階邏輯表達(dá)式的重言性，SMT 檢查所有的情況可能會(huì)超時(shí)。相反，來證明不可滿足（UNSAT）要容易得多，當(dāng) STM 求解器發(fā)現(xiàn) ?(C ? ?t.q src (t)=q dest (t) 是不可滿足（UNSAT）的話，那么可以證明規(guī)則的正確性。
2?? SPES 校驗(yàn)器
相比于內(nèi)置的校驗(yàn)器，SPES 校驗(yàn)器還支持 UNION 和 Aggregation 運(yùn)算符。對(duì)于一個(gè)給定的規(guī)則 ?q src ,q dest , C ? ，還需要轉(zhuǎn)換成 SPES 的輸入格式。SPES 只接受具體的 SQL 查詢，不能識(shí)別約束條件集合 C。WeTune 利用 C 把 q src ,q dest 具體化，具體有如下三個(gè)步驟：
把每一個(gè)符號(hào)具體命名，放到一個(gè)集合里，隨機(jī)生成一些名字。
對(duì)于每個(gè)屬性，找到通過 SubAttrs 約束找到對(duì)應(yīng)的關(guān)系表，然后把名字 c 改成 t.c ( t是這個(gè)屬性 c 所屬于的關(guān)系表)。
通過關(guān)系的屬性來構(gòu)建 schema 定義。
圖十二：SPES 和內(nèi)置校驗(yàn)器能力對(duì)比
我們可以發(fā)現(xiàn)兩者的能力是相互補(bǔ)充的。
??????? 有效規(guī)則選擇器
在生成被校驗(yàn)正確的規(guī)則后，WeTune 搜集一些真實(shí)世界的查詢 sql，然后迭代的以貪心的方式（重寫后具有最少的算子）來不斷利用已有的規(guī)則進(jìn)行優(yōu)化，會(huì)利用已有的 SQL server 的成本估算器（如 MySQL 的 EXPLAIN EXTENDED 和 MS SQL 的 SHOW_PLAN_ALL ）來對(duì)比重寫前后的查詢花費(fèi)。
評(píng)估
評(píng)估的目的是為了回答以下三個(gè)問題：
WeTune 可以發(fā)現(xiàn)多少新的有用的規(guī)則？
WeTune 對(duì)于已有的系統(tǒng)中可以優(yōu)化多少新的查詢？
WeTune 內(nèi)置的校驗(yàn)器和 SPES 相比如何？
WeTune 在查詢計(jì)劃模版最大節(jié)點(diǎn)為?4 的情況下，一共發(fā)現(xiàn)了?1106 個(gè)正確的規(guī)則。
本文在 Github 上選了?20 個(gè) star 最多的開源 web 應(yīng)用，搜集了一些查詢優(yōu)化的 issue 和一些不同的真實(shí)查詢，一共收集了?50 個(gè) issue 和?8518 個(gè)不同的查詢。
在上述的查詢中，WeTune 一共有 35 條可以應(yīng)用的規(guī)則，MS SQL Server 缺失了 9 條，Calcite 缺失了?22 條，兩個(gè)系統(tǒng)中有?5 條規(guī)則都缺失了。
圖十三：發(fā)現(xiàn)可以應(yīng)用的規(guī)則 ?（W 表示內(nèi)置校驗(yàn)器，S 表示 SPES，B 表示兩者）
對(duì)于收集的?50 個(gè)重寫優(yōu)化 issue，WeTune 可以優(yōu)化?76%（38個(gè)），MS SQL Server 和 Calcite 只能優(yōu)化?46%（?23 個(gè)）和?8%（?4 個(gè)）。
對(duì)于?8518 個(gè)查詢，WeTune 可以重寫優(yōu)化?674 個(gè)，在這其中有?247 個(gè) MS SQL Server 不能重寫優(yōu)化。而這些有?4251 個(gè)查詢僅包含 SELECT 子句和 WHERE 子句，沒有 JOIN，Subquery，Aggregate 和其他的子句，這些往往實(shí)際需要在物理執(zhí)行層進(jìn)行優(yōu)化（例如索引選擇等），這些超出了 WeTune 的范圍，因此結(jié)果表明 WeTune 比起現(xiàn)有的數(shù)據(jù)庫可以優(yōu)化更多的查詢。
通過驗(yàn)證規(guī)則，內(nèi)置校驗(yàn)器可以支持完整性約束的規(guī)則，SPES 可以支持復(fù)雜謂詞的規(guī)則。
限制
內(nèi)置校驗(yàn)器的不完整性：
只有上述提到的 U 表達(dá)式才可以轉(zhuǎn)換成 FOL 并有 STM 求解器驗(yàn)證，同時(shí) SMT 求解器可能會(huì)超時(shí)，從而錯(cuò)過有用的規(guī)則。
SQL 運(yùn)算符的有限性：
內(nèi)置的校驗(yàn)器只能支持上述提到的一些運(yùn)算符，同時(shí) WeTune 也不支持遞歸查詢。
參考
https://ipads.se.sjtu.edu.cn/\_media/publications/wetune\_final.pdf
https://dl.acm.org/doi/10.1145/3514221.3526125
關(guān)于?Databend
Databend 是一款開源、彈性、低成本，基于對(duì)象存儲(chǔ)也可以做實(shí)時(shí)分析的新式數(shù)倉。期待您的關(guān)注，一起探索云原生數(shù)倉解決方案，打造新一代開源 Data Cloud。
?????? Databend Cloud：https://databend.cn
?? Databend 文檔：https://databend.rs/
?? Wechat：Databend
? GitHub：https://github.com/datafuselabs/databend
