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