作者：謝其駿

北京航空航天大學在讀碩士知态， Databend 研發(fā)工程師實習生

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

本文的貢獻：

• 本文借鑒了編譯器超優(yōu)化的思想捷兰，通過列舉所有有效的邏輯查詢計劃來嘗試發(fā)現(xiàn)潛在的等效計劃，從而自動發(fā)現(xiàn)新的更有效的重寫規(guī)則负敏。

• 本文還提出了一個新的基于 SMT 的驗證器贡茅，以驗證不同枚舉下兩個查詢的等價性。

Abstract

查詢重寫將一個關(guān)系型數(shù)據(jù)庫的查詢轉(zhuǎn)換為一個等價的更高效的查詢其做，這對數(shù)據(jù)庫應用的性能至關(guān)重要顶考。這些重寫依賴于預先指定的重寫規(guī)則，在現(xiàn)有的系統(tǒng)中妖泄，這些重寫規(guī)則是通過人工洞察發(fā)現(xiàn)的驹沿，并在多年中慢慢積累。

image.png

圖一：Query Rewrite in Apache Calcite

本文介紹了 WeTune蹈胡，一個自動發(fā)現(xiàn)新的重寫規(guī)則的規(guī)則生成器渊季，受到編譯器超優(yōu)化的啟發(fā)，WeTune 枚舉了一定閾值下的所有有效的邏輯查詢計劃罚渐，并試圖發(fā)現(xiàn)可能導致更有效重寫的等效計劃却汉。核?挑戰(zhàn)是確定哪?組條件（約束）可以來證明這?對查詢計劃之間的等價性。通過枚舉每對查詢之間的表及其屬性相關(guān)的約束的組合情況荷并，來解決這?挑戰(zhàn)病涨。

本文還提出了?種新的基于 SMT 的驗證器來驗證查詢對在不同枚舉約束下的等價性。為了評估 WeTune 發(fā)現(xiàn)的重寫規(guī)則的有效性璧坟，我們將它們應?于從 GitHub 上 20個最流?的開源 Web 應?程序收集的 SQL 查詢既穆。WeTune 成功優(yōu)化了現(xiàn)有數(shù)據(jù)庫?法優(yōu)化的 247 個查詢，從?實現(xiàn)了顯著的性能提升雀鹃。

Introduce

查詢重寫幻工，將原始查詢轉(zhuǎn)換為語義等價的替代查詢，是查詢優(yōu)化的重要步驟黎茎。有效的重寫可以將輸?查詢的執(zhí)?時間加快?個數(shù)量級囊颅。重寫依賴于指定查詢之間等價關(guān)系的規(guī)則。現(xiàn)有的規(guī)則通常由?類專家制定，可能需要數(shù)?年才能積累踢代。

然?盲憎，僅僅依靠??來發(fā)現(xiàn)重寫規(guī)則是不夠的。查詢語?豐富的特性和微妙的語義使得證明等價性和編寫規(guī)則具有挑戰(zhàn)性胳挎。但是由于?寫的重寫規(guī)則集增??常緩慢饼疙，錯過了許多重寫機會。在 Web 應?程序開發(fā)中普遍使?對象關(guān)系映射 (ORM) 框架使情況變得更糟慕爬。ORM 使程序員?需顯式構(gòu)建 SQL 查詢窑眯，但也會產(chǎn)??直觀的查詢，其模式會避開?類制定的規(guī)則医窿。

為了了解遺漏重寫的影響磅甩，我們研究了 Github 上?個流?的開源 Web 應?程序中的 50 個真實查詢。所有這些查詢都已被開發(fā)?員重寫以修復它們的性能問題姥卢。即使是最新版本的 SQL Server 也未能將其中 27 個查詢 (54%) 重寫為開發(fā)?員?動修復的更?效的形式卷要。?個這樣的查詢會導致延遲?達 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ī)則被認為是有希望的德频。

盡管大體的方法比較簡單苍息，但是也存在著以下一些挑戰(zhàn)：

如何有效的枚舉查詢規(guī)則

a. 一方面需要在有效的搜索空間當中發(fā)現(xiàn)具有代表性的查詢計劃。

b. 另一方面為了產(chǎn)生一般性的規(guī)則壹置， 我們需要避免過度嚴苛的約束條件竞思。

怎么驗證這些產(chǎn)生規(guī)則的正確性

a. 對一般的 query plan，現(xiàn)存的校驗器無法驗證正確性钞护。

b. 需要一個新的校驗器盖喷。

為了應對上述挑戰(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 應?程序桑腮，WeTune 輸出 1106 條有希望的重寫規(guī)則泉哈，其中 35 條?于優(yōu)化這些應?程序的查詢。此外破讨，我們的結(jié)果表明丛晦，WeTune 可以成功優(yōu)化現(xiàn)有系統(tǒng)遺漏的 247 個查詢，從?將延遲減少?達 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ī)則進行正確性的校驗。當我們得到一組經(jīng)過校驗的正確的規(guī)則之后铅忿，會把它輸入到有效規(guī)則選擇器中剪决，然后有效規(guī)則選擇器會過濾出一系列的真正能夠提高數(shù)據(jù)庫性能的有用的規(guī)則。

image.png

圖二：WeTune 主要框架

?????? 規(guī)則枚舉器

規(guī)則枚舉器中總共分為三步檀训，第一步是對所有可能的查詢計劃模版的一個枚舉柑潦，第二步是對每一對查詢計劃模版枚舉所有可能的約束條件，第三步是利用規(guī)則校驗器來找到所有正確的規(guī)則峻凫。

image.png

圖三：規(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 表示一個謂詞邏輯析孽。

image.png

圖四：支持的六種關(guān)系算子

2?? 規(guī)則

規(guī)則是一個三元組 (q src ,q dest ,C ) ,分別表示源查詢計劃模版搭伤、目標查詢計劃模版和約束條件，約束條件是指參數(shù)化的約束條件一個集合袜瞬，用符號來表示一些具體的名字怜俐。如果是一個正確的規(guī)則，意味著如果約束條件成立邓尤，那么源查詢計劃模版和目標查詢計劃模版語義等價恒成立拍鲤。

圖五：WeTune 發(fā)現(xiàn)的一個規(guī)則

3?? 枚舉查詢計劃模版

介紹完需要的概念之后，下面介紹規(guī)則枚舉器的第一步汞扎，枚舉查詢計劃模版季稳。我們先從結(jié)點數(shù)量為一的模版進行枚舉，然后當結(jié)點數(shù)目超過一定數(shù)量的時候澈魄，就會停止枚舉景鼠。

下面以最大結(jié)點數(shù)為 2 進行舉例：

image.png

圖六：枚舉查詢計劃舉例

第一步先列出所有可能的 6 種算子，然后把算子的葉子結(jié)點接著填充痹扇，當達到最大數(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 是非空的莉钙。

把一對查詢計劃模版中所有可能的約束條件都列出來，這些所有可能的約束條件的集合就形成了初始的約束條件集筛谚。找到初始約束條件集合后還要找到最松弛的約束條件子集磁玉，最松弛的含義是如果減少當前約束條件集的任何一個條件，那么這個規(guī)則都不會恒成立驾讲。

image.png

圖七：規(guī)則枚舉器算法

在第 11 行中 ProveEq( q src ,q dest ,C * ) 會用到規(guī)則校驗器蚊伞。

?????? 規(guī)則校驗器

本文提供了兩個規(guī)則校驗器，一個是內(nèi)置的基于 FOL（一階邏輯表達式）的規(guī)則校驗器吮铭，另一個是現(xiàn)有的 SQL 等價性校驗器 SPES时迫。

1?? 內(nèi)置規(guī)則校驗器

內(nèi)置的規(guī)則校驗器主要有兩個步驟，第一步是把從規(guī)則枚舉器中傳來的規(guī)則轉(zhuǎn)換成一階邏輯表達式谓晌，第二步是把一階邏輯表達式 SMT Solver 中掠拳，判斷每一個規(guī)則是否正確。

image.png

圖八：內(nèi)置規(guī)則校驗器流程

1.1 規(guī)則形式化

給定一個規(guī)則扎谎，對于 q src 和 q dest 碳想，我們先用 U 表達式來表示烧董，然后再把 U 表達式轉(zhuǎn)換成一階邏輯表達式毁靶。對于 C 約束條件，我們直接轉(zhuǎn)換成一階邏輯表達式逊移。

U 表達式是在包的語義下對 SQL 查詢建模的一種方式预吆，主要描述的是元組在一個關(guān)系表里面的出現(xiàn)的次數(shù)。

下面是 U 表達式建模的式子：

• ?R?(??) 返回在關(guān)系R中元組x出現(xiàn)的次數(shù)胳泉。
• [??] ? 如果??存在則為1拐叉，否則為0。這個表達式可以將布爾值轉(zhuǎn)換成整數(shù)扇商，因此可用于將謂詞轉(zhuǎn)換成U表達式凤瘦。
• ||?? || ? 如果?? > 0則為1，否則為0案铺。這里e是一個U表達式蔬芥，它用來模擬數(shù)據(jù)去重。
• not(??) ? 如果?? > 0則為0控汉，否則為1笔诵。這里e是一個U表達式，它用來模擬謂詞的否定姑子。
• 對于所有的乎婿，D是求和域的元組集合，f是函數(shù)D到整數(shù)N的映射街佑，默認情況下谢翎，D是包含所有元組的無限集合捍靠。用來模擬映射。

可以用來表示SELECT DISTINCT x.k FROM R AS x WHERE x.a>12
為了把查詢計劃模版轉(zhuǎn)換成 U 表達式森逮，分成了兩個步驟：

• 翻譯查詢計劃模版中的符號

1. 關(guān)系表符號 rel 轉(zhuǎn)換成 ?r?(t)：Tuple->N 剂公，表示元組到自然數(shù)的映射。

2. 屬性符號 attrs 轉(zhuǎn)換成 ?a?(t)：Tuple->Tuple吊宋，表示元組到元組的映射纲辽。

3. 謂詞符號 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)

image.png

圖九：SQL 運算符轉(zhuǎn)換成 U 表達式的規(guī)則

將查詢計劃模版轉(zhuǎn)換成 U 表達式之后拖吼，再根據(jù)圖十轉(zhuǎn)換成一階邏輯表達式。

image.png

圖十：U 表達式轉(zhuǎn)換成一階邏輯表達式的規(guī)則

接著再根據(jù)圖十一把約束條件轉(zhuǎn)換成一階邏輯表達式这吻。

image.png

圖十一：約束條件轉(zhuǎn)換成一階邏輯表達式的規(guī)則

1.2 驗證規(guī)則

把查詢計劃模版和約束條件轉(zhuǎn)換成一階邏輯表達式之后吊档，接著使用 SMT 求解器來進行檢查正確性。

規(guī)則的正確性定義為：

其中 q I和 C I 分別表示具體情況下的查詢計劃和約束條件唾糯。

為了證明一階邏輯表達式的重言性怠硼，SMT 檢查所有的情況可能會超時。相反移怯，來證明不可滿足（UNSAT）要容易得多香璃，當 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 具體化学少，具體有如下三個步驟：

1. 把每一個符號具體命名，放到一個集合里秧骑，隨機生成一些名字版确。

2. 對于每個屬性，找到通過 SubAttrs 約束找到對應的關(guān)系表腿堤，然后把名字 c 改成 t.c ( t是這個屬性 c 所屬于的關(guān)系表)阀坏。

3. 通過關(guān)系的屬性來構(gòu)建 schema 定義。

image.png

圖十二：SPES 和內(nèi)置校驗器能力對比

我們可以發(fā)現(xiàn)兩者的能力是相互補充的笆檀。

?????? 有效規(guī)則選擇器

在生成被校驗正確的規(guī)則后忌堂，WeTune 搜集一些真實世界的查詢 sql，然后迭代的以貪心的方式（重寫后具有最少的算子）來不斷利用已有的規(guī)則進行優(yōu)化酗洒，會利用已有的 SQL server 的成本估算器（如 MySQL 的 EXPLAIN EXTENDED 和 MS SQL 的 SHOW_PLAN_ALL ）來對比重寫前后的查詢花費士修。

評估

評估的目的是為了回答以下三個問題：

1. WeTune 可以發(fā)現(xiàn)多少新的有用的規(guī)則枷遂？

2. WeTune 對于已有的系統(tǒng)中可以優(yōu)化多少新的查詢？

3. WeTune 內(nèi)置的校驗器和 SPES 相比如何棋嘲？

WeTune 在查詢計劃模版最大節(jié)點為 4 的情況下酒唉，一共發(fā)現(xiàn)了 1106 個正確的規(guī)則。

本文在 Github 上選了 20 個 star 最多的開源 web 應用沸移，搜集了一些查詢優(yōu)化的 issue 和一些不同的真實查詢痪伦，一共收集了 50 個 issue 和 8518 個不同的查詢。

在上述的查詢中雹锣，WeTune 一共有 35 條可以應用的規(guī)則网沾，MS SQL Server 缺失了 9 條，Calcite 缺失了 22 條蕊爵，兩個系統(tǒng)中有 5 條規(guī)則都缺失了辉哥。

image.png

圖十三：發(fā)現(xiàn)可以應用的規(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 可以支持復雜謂詞的規(guī)則今缚。

限制

1. 內(nèi)置校驗器的不完整性：

只有上述提到的 U 表達式才可以轉(zhuǎn)換成 FOL 并有 STM 求解器驗證参淹，同時 SMT 求解器可能會超時，從而錯過有用的規(guī)則围小。

3. SQL 運算符的有限性：

內(nèi)置的校驗器只能支持上述提到的一些運算符宪迟，同時 WeTune 也不支持遞歸查詢酣衷。

參考

1. https://ipads.se.sjtu.edu.cn/_media/publications/wetune_final.pdf

2. https://dl.acm.org/doi/10.1145/3514221.3526125

關(guān)于 Databend

Databend 是一款開源、彈性次泽、低成本穿仪，基于對象存儲也可以做實時分析的新式數(shù)倉席爽。期待您的關(guān)注，一起探索云原生數(shù)倉解決方案啊片，打造新一代開源 Data Cloud只锻。

???? Databend Cloud：https://databend.cn

?? Databend 文檔：https://databend.rs/

?? Wechat：Databend

? GitHub：https://github.com/datafuselabs/databend