如何驗(yàn)證線性一致性

線性一致性（Linearizability）是分布式系統(tǒng)中常見(jiàn)的一致性保證。那么如何驗(yàn)證系統(tǒng)是否正確地提供了線性一致性服務(wù)呢？本文希望從‘什么是線性一致性’，‘如何驗(yàn)證線性一致性’，問(wèn)題復(fù)雜度，常見(jiàn)的通用算法，以及工程實(shí)現(xiàn)五個(gè)部分，直觀、易懂地回答這個(gè)問(wèn)題。

什么是線性一致性

MAURICE P. HERLIHY 和 JEANNETTE M. WING曾在“ Linearizability: A Correctness Condition for Concurrent Objects ” 中對(duì)線性一致性給出了形式化的定義和證明，對(duì)分布式系統(tǒng)來(lái)說(shuō)，簡(jiǎn)單的講就是即使發(fā)生網(wǎng)絡(luò)分區(qū)或機(jī)器節(jié)點(diǎn)異常，整個(gè)集群依然能夠像單點(diǎn)一樣提供一致的服務(wù)，即依次原子地執(zhí)行每一條操作。假如我們可以站在最終操作執(zhí)行的視角，將整個(gè)系統(tǒng)看做一個(gè)整體，一個(gè)保證線性一致性的服務(wù)應(yīng)該如下圖所示進(jìn)行服務(wù)：

由于每條操作是依次、原子的執(zhí)行，相互之間沒(méi)有重疊，為了方便理解，可以把一個(gè)操作在圖上簡(jiǎn)化為一個(gè)點(diǎn)。如下圖所示：

然而，實(shí)際情況中，分布式系統(tǒng)通常是很多節(jié)點(diǎn)作為一個(gè)整體對(duì)外提供服務(wù)，并在內(nèi)部處理網(wǎng)絡(luò)或節(jié)點(diǎn)異常，我們無(wú)法站在上帝視角看到其執(zhí)行序列。同時(shí)，我們真正關(guān)心的也是其作為一個(gè)整體對(duì)外的表現(xiàn)，而不是其中的每個(gè)單獨(dú)節(jié)點(diǎn)。我們所能做的是站在客戶端的角度，通過(guò)讀寫事件的發(fā)起和結(jié)束來(lái)感知整個(gè)系統(tǒng)。正如站在地球上仰望星空，通過(guò)光來(lái)感知天體，看到的每一次閃爍，可能真正發(fā)生在上萬(wàn)年之前。因此，下圖才是真正可以看到的情況：

上圖，展示了在每個(gè)客戶端看來(lái)，其請(qǐng)求從發(fā)起到結(jié)束的時(shí)間點(diǎn)。因此，我們希望通過(guò)一系列客戶端的執(zhí)行和返回序列來(lái)判斷系統(tǒng)是否正確提供了線性一致性服務(wù)。

如何驗(yàn)證線性一致性

為了判斷系統(tǒng)是否正確提供了線性一致性，首先在運(yùn)行過(guò)程中獲得一系列不同的執(zhí)行歷史，接著驗(yàn)證每組歷史是否滿足線性一致性，只要有一個(gè)不滿足，便可以說(shuō)系統(tǒng)不滿足線性一致性。但如果沒(méi)有發(fā)現(xiàn)不滿足的歷史，也不證明系統(tǒng)一定正確。然而，在工程中通過(guò)對(duì)大量的執(zhí)行歷史的驗(yàn)證，使得我們對(duì)自己的系統(tǒng)更充滿信心，這就足夠了。那么現(xiàn)在的問(wèn)題轉(zhuǎn)變?yōu)椋?strong>如何驗(yàn)證一組執(zhí)行歷史是否滿足線性一致性。

通過(guò)客戶端可以看到一個(gè)讀寫請(qǐng)求的發(fā)起和結(jié)束時(shí)間，而其真正在服務(wù)端的執(zhí)行可能發(fā)生在開(kāi)始和結(jié)束中間的任意一點(diǎn)。因此，驗(yàn)證線性一致性的關(guān)鍵就是找到一組依次執(zhí)行的序列，如果這組執(zhí)行序列存在，則可以說(shuō)這組執(zhí)行歷史是滿足線性一致的，如下圖所示：

明顯的，存在這么一組序列，因此我們說(shuō)這組執(zhí)行歷史是符合線性一致性的。再來(lái)看一個(gè)不符合線性一致性的例子，如下圖，可以看出，由于Client 3已經(jīng)讀到1，說(shuō)明在Client 3請(qǐng)求結(jié)束前Client 2已經(jīng)寫成功，而又沒(méi)有其他請(qǐng)求再次修改x的值，因此Client 4不應(yīng)該在之后讀到0。

實(shí)踐中，通常會(huì)通過(guò)在頻繁注入異常的情況下，隨機(jī)生成請(qǐng)求序列，收集執(zhí)行的發(fā)起和結(jié)束歷史，并尋找合理的線性執(zhí)行序列，如Jespen。

問(wèn)題復(fù)雜度

直觀來(lái)看，這個(gè)問(wèn)題是一個(gè)排序問(wèn)題，極端情況下的時(shí)間復(fù)雜度為O(N!)。事實(shí)上，Phillip B. Gibbons和Ephraim Korach在Testing Shared Memories中已經(jīng)證明其是一個(gè)NP-Complete問(wèn)題。雖然Gavin Lowe在Testing for Linearizability中給出了一些特殊限制下的多項(xiàng)式甚至是線性復(fù)雜度的算法，但在通用場(chǎng)景下，判定線性一致性并不是一個(gè)容易解決的問(wèn)題，其搜索空間會(huì)隨著執(zhí)行歷史的規(guī)模急速膨脹。

通用算法

雖然判定線性一致性的復(fù)雜度極高，但我們還是能夠通過(guò)一些技巧，在大多數(shù)場(chǎng)景下，在工程可接受的時(shí)間內(nèi)給出結(jié)果，這里介紹三個(gè)常見(jiàn)的，且一脈相承的通用算法。在此之前，先對(duì)算法面臨的問(wèn)題進(jìn)行抽象，以下圖執(zhí)行歷史為例，給出算法的輸入和期待的輸出：

Input: 調(diào)用歷史

1，Client1: Invoke Put x=0
2，Client2: Invoke Put x=1
3，Client1: Return Put x=0
4，Client3: Invoke Get x
5，CLient4: Invoke Get x
6，Client3: Return Get 1
7，Client4: Return Get 0
8，Client2: Return Put x=1

Output: 執(zhí)行序列

Client1 Put x=0
Client4 Get 0
Client2 Put x=1
Client3 Get 1

1，WG算法

請(qǐng)求的調(diào)用歷史中，存在著一種偏序關(guān)系：Prev，如果一個(gè)請(qǐng)求的Return發(fā)生時(shí)間早于另一請(qǐng)求的Invoke，我們便稱其Prev另一個(gè)請(qǐng)求。顯而易見(jiàn)，這種偏序關(guān)系是一致性驗(yàn)證算法必須要保留的。禍兮福所倚，也正是這種對(duì)偏序關(guān)系的保留，給了算法加速的可能。WG算法的思路非常簡(jiǎn)單：從調(diào)用歷史中找出沒(méi)有Prev的項(xiàng)，將其對(duì)應(yīng)的請(qǐng)求執(zhí)行并取出，之后對(duì)剩下的調(diào)用歷史重復(fù)該算法，直到?jīng)]有更多的調(diào)用歷史或執(zhí)行結(jié)果不滿足。

如上述例子中，“Client1 Put x=0” 和 “Client2 Put x=1” 由于其Invoke前沒(méi)有任何請(qǐng)求Return，可以首先被取出。假如選擇“Client1 Put x=0”，將其對(duì)應(yīng)的Invoke和Return從調(diào)用歷史中取出，得到新的歷史：

2，Client2: Invoke Put x=1
4，Client3: Invoke Get x
5，CLient4: Invoke Get x
6，Client3: Return Get 1
7，Client4: Return Get 0
8，Client2: Return Put x=1

和一條已經(jīng)序列化的請(qǐng)求：

Client1 Put x=0

此時(shí)可以看到剩余的歷史中，每一個(gè)請(qǐng)求的Invoke前都沒(méi)有其他請(qǐng)求的Return，因此都可以作為下一個(gè)取出的選擇。假設(shè)這次選擇Client3 Get 1，然而，明顯這個(gè)時(shí)候執(zhí)行Get得到應(yīng)該是0，與該請(qǐng)求的實(shí)際執(zhí)行結(jié)果返回1不同，此時(shí)，需要回退并嘗試其他取出策略。可以看出WG算法其實(shí)是樹(shù)的深度優(yōu)先搜索，其搜索樹(shù)如下圖，其中每個(gè)節(jié)點(diǎn)標(biāo)識(shí)的是本次嘗試序列化的請(qǐng)求對(duì)應(yīng)的調(diào)用歷史中的Invoke序號(hào)：

由于找到一個(gè)線性序列便可以停止，因此其中虛線部分是不會(huì)被實(shí)際執(zhí)行的。

2，WGL算法

WGL算法由Gavin Lowe在WG算法的基礎(chǔ)上進(jìn)行改進(jìn)，其改進(jìn)的方式主要是對(duì)搜索樹(shù)的剪枝：通過(guò)緩存已經(jīng)見(jiàn)過(guò)的配置，來(lái)減少重復(fù)的搜索。緩存配置有兩部分組成：

• 當(dāng)前已經(jīng)序列化的請(qǐng)求

• 當(dāng)前x值

由上面的搜索過(guò)程可知，如果當(dāng)前序列化的請(qǐng)求和當(dāng)前的x值完全相同，則后續(xù)的搜索過(guò)程一定一致，因此可以略過(guò)。

3，P-compositionality算法

P-compositionality算法利用了線性一致性的Locality原理，即如果一個(gè)調(diào)用歷史的所有子歷史都滿足線性一致性，那么這個(gè)歷史本身也滿足線性一致性。因此，可以將一些不相關(guān)的歷史劃分開(kāi)來(lái)，形成多個(gè)規(guī)模更小的子歷史，轉(zhuǎn)而驗(yàn)證這些子歷史的線性一致性，例如kv數(shù)據(jù)結(jié)構(gòu)中對(duì)不同key的操作。上面提到了算法的計(jì)算時(shí)間隨著歷史規(guī)模的增加急速膨脹，P-compositionality相當(dāng)于用分治的辦法來(lái)降低歷史規(guī)模，這種方法在可以劃分子問(wèn)題的場(chǎng)景下會(huì)非常有用。

為什么Solitaire

工程實(shí)踐中，不只分布式系統(tǒng)，還包括需要并行訪問(wèn)的系統(tǒng)，都可能需要驗(yàn)證系統(tǒng)對(duì)外暴露的線性一致性功能。當(dāng)然也有不少驗(yàn)證線性一致性的工具，比如大名鼎鼎的Jespen使用的Knossos，是一個(gè)Clojure版本的WGL的算法實(shí)現(xiàn)；Porcupine是一個(gè)Go版本的P-compositionality實(shí)現(xiàn)；linearizability-checker是P-compositionality算法作者自己實(shí)現(xiàn)的一個(gè)樣例。但使用中還有幾個(gè)問(wèn)題沒(méi)有解決：

• 計(jì)算速度慢：由于上面提到的復(fù)雜度，一致性算法驗(yàn)證時(shí)間通常是相關(guān)測(cè)試中的瓶頸。盡可能的加快其計(jì)算速度，可以在相同時(shí)間內(nèi)驗(yàn)證更多的歷史，對(duì)發(fā)現(xiàn)系統(tǒng)中的潛在問(wèn)題至關(guān)重要。

• 數(shù)據(jù)模型單一：大多數(shù)的驗(yàn)證工具面向的都是KV接口，這就要求使用者將千差萬(wàn)別的系統(tǒng)實(shí)際接口轉(zhuǎn)化為KV接口使用，而這層轉(zhuǎn)換會(huì)掩蓋系統(tǒng)中的眾多復(fù)雜性，比如將Device接口轉(zhuǎn)化為KV后會(huì)丟失對(duì)相互覆蓋操作的驗(yàn)證。

• 具體問(wèn)題具體分析：對(duì)一些數(shù)據(jù)模型來(lái)說(shuō)，可能存在多項(xiàng)式甚至是線性復(fù)雜度的算法，那么針對(duì)這些數(shù)據(jù)模型使用通用的WGL算法就舍近求遠(yuǎn)了。

Solitaire(https://github.com/CatKang/Solitaire)是一個(gè)C++實(shí)現(xiàn)，更快速，支持多數(shù)據(jù)模型的線性一致性檢測(cè)工具，致力于解決上述問(wèn)題。其命名來(lái)源于上世紀(jì)著名的Windows桌面紙牌游戲，要求玩家在保證大小先序關(guān)系的限制下，將打亂的撲克牌整理為有序?？梢哉f(shuō)與我們的線性一致性驗(yàn)證工作非常契合了。

參考

• Linearizability: A Correctness Condition for Concurrent Objects

• Testing for Linearizability

• Faster linearizability checking via P -compositionality

• Testing Distributed Systems for Linearizability

• Testing Shared Memories

• 線性一致性理論

• Solitaire: 一個(gè)更快的，適配更多數(shù)據(jù)模型的一致性驗(yàn)證工具

• knossos: Jespen所使用的一致性驗(yàn)證工具，WGL算法實(shí)現(xiàn)

• porcupine: go版本P-compositionality算法實(shí)現(xiàn)

• linearizability-checker: P-compositionality算法實(shí)現(xiàn)

• Jespen

原文鏈接：https://mp.weixin.qq.com/s/calyZj0-ZfiYuDlJWQoHaA