線性一致性（Linearizability）是分布式系統中常見的一致性保證。那么如何驗證系統是否正確地提供了線性一致性服務呢？本文希望從‘什么是線性一致性’，‘如何驗證線性一致性’，問題復雜度，常見的通用算法，以及工程實現五個部分，直觀、易懂地回答這個問題。
什么是線性一致性
MAURICE P. HERLIHY 和 JEANNETTE M. WING曾在“ Linearizability: A Correctness Condition for Concurrent Objects ” 中對線性一致性給出了形式化的定義和證明，對分布式系統來說，簡單的講就是即使發生網絡分區或機器節點異常，整個集群依然能夠像單點一樣提供一致的服務，即依次原子地執行每一條操作。假如我們可以站在最終操作執行的視角，將整個系統看做一個整體，一個保證線性一致性的服務應該如下圖所示進行服務：
由于每條操作是依次、原子的執行，相互之間沒有重疊，為了方便理解，可以把一個操作在圖上簡化為一個點。如下圖所示：
然而，實際情況中，分布式系統通常是很多節點作為一個整體對外提供服務，并在內部處理網絡或節點異常，我們無法站在上帝視角看到其執行序列。同時，我們真正關心的也是其作為一個整體對外的表現，而不是其中的每個單獨節點。我們所能做的是站在客戶端的角度，通過讀寫事件的發起和結束來感知整個系統。正如站在地球上仰望星空，通過光來感知天體，看到的每一次閃爍，可能真正發生在上萬年之前。因此，下圖才是真正可以看到的情況：
上圖，展示了在每個客戶端看來，其請求從發起到結束的時間點。因此，我們希望通過一系列客戶端的執行和返回序列來判斷系統是否正確提供了線性一致性服務。
如何驗證線性一致性
為了判斷系統是否正確提供了線性一致性，首先在運行過程中獲得一系列不同的執行歷史，接著驗證每組歷史是否滿足線性一致性，只要有一個不滿足，便可以說系統不滿足線性一致性。但如果沒有發現不滿足的歷史，也不證明系統一定正確。然而，在工程中通過對大量的執行歷史的驗證，使得我們對自己的系統更充滿信心，這就足夠了。那么現在的問題轉變為：如何驗證一組執行歷史是否滿足線性一致性。
通過客戶端可以看到一個讀寫請求的發起和結束時間，而其真正在服務端的執行可能發生在開始和結束中間的任意一點。因此，驗證線性一致性的關鍵就是找到一組依次執行的序列，如果這組執行序列存在，則可以說這組執行歷史是滿足線性一致的，如下圖所示：
明顯的，存在這么一組序列，因此我們說這組執行歷史是符合線性一致性的。再來看一個不符合線性一致性的例子，如下圖，可以看出，由于Client 3已經讀到1，說明在Client 3請求結束前Client 2已經寫成功，而又沒有其他請求再次修改x的值，因此Client 4不應該在之后讀到0。
實踐中，通常會通過在頻繁注入異常的情況下，隨機生成請求序列，收集執行的發起和結束歷史，并尋找合理的線性執行序列，如Jespen。
問題復雜度
直觀來看，這個問題是一個排序問題，極端情況下的時間復雜度為O(N!)。事實上，Phillip B. Gibbons和Ephraim Korach在Testing Shared Memories中已經證明其是一個NP-Complete問題。雖然Gavin Lowe在Testing for Linearizability中給出了一些特殊限制下的多項式甚至是線性復雜度的算法，但在通用場景下，判定線性一致性并不是一個容易解決的問題，其搜索空間會隨著執行歷史的規模急速膨脹。
通用算法
雖然判定線性一致性的復雜度極高，但我們還是能夠通過一些技巧，在大多數場景下，在工程可接受的時間內給出結果，這里介紹三個常見的，且一脈相承的通用算法。在此之前，先對算法面臨的問題進行抽象，以下圖執行歷史為例，給出算法的輸入和期待的輸出：
Input: 調用歷史
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: 執行序列
Client1 Put x=0 Client4 Get 0 Client2 Put x=1 Client3 Get 1
1，WG算法
請求的調用歷史中，存在著一種偏序關系：Prev，如果一個請求的Return發生時間早于另一請求的Invoke，我們便稱其Prev另一個請求。顯而易見，這種偏序關系是一致性驗證算法必須要保留的。禍兮福所倚，也正是這種對偏序關系的保留，給了算法加速的可能。WG算法的思路非常簡單：從調用歷史中找出沒有Prev的項，將其對應的請求執行并取出，之后對剩下的調用歷史重復該算法，直到沒有更多的調用歷史或執行結果不滿足。
如上述例子中，“Client1 Put x=0” 和 “Client2 Put x=1” 由于其Invoke前沒有任何請求Return，可以首先被取出。假如選擇“Client1 Put x=0”，將其對應的Invoke和Return從調用歷史中取出，得到新的歷史：
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
和一條已經序列化的請求：
Client1 Put x=0
此時可以看到剩余的歷史中，每一個請求的Invoke前都沒有其他請求的Return，因此都可以作為下一個取出的選擇。假設這次選擇Client3 Get 1，然而，明顯這個時候執行Get得到應該是0，與該請求的實際執行結果返回1不同，此時，需要回退并嘗試其他取出策略。可以看出WG算法其實是樹的深度優先搜索，其搜索樹如下圖，其中每個節點標識的是本次嘗試序列化的請求對應的調用歷史中的Invoke序號：
由于找到一個線性序列便可以停止，因此其中虛線部分是不會被實際執行的。
2，WGL算法
WGL算法由Gavin Lowe在WG算法的基礎上進行改進，其改進的方式主要是對搜索樹的剪枝：通過緩存已經見過的配置，來減少重復的搜索。緩存配置有兩部分組成：
- 當前已經序列化的請求
- 當前x值
由上面的搜索過程可知，如果當前序列化的請求和當前的x值完全相同，則后續的搜索過程一定一致，因此可以略過。
3，P-compositionality算法
P-compositionality算法利用了線性一致性的Locality原理，即如果一個調用歷史的所有子歷史都滿足線性一致性，那么這個歷史本身也滿足線性一致性。因此，可以將一些不相關的歷史劃分開來，形成多個規模更小的子歷史，轉而驗證這些子歷史的線性一致性，例如kv數據結構中對不同key的操作。上面提到了算法的計算時間隨著歷史規模的增加急速膨脹，P-compositionality相當于用分治的辦法來降低歷史規模，這種方法在可以劃分子問題的場景下會非常有用。
為什么Solitaire
工程實踐中，不只分布式系統，還包括需要并行訪問的系統，都可能需要驗證系統對外暴露的線性一致性功能。當然也有不少驗證線性一致性的工具，比如大名鼎鼎的Jespen使用的Knossos，是一個Clojure版本的WGL的算法實現；Porcupine是一個Go版本的P-compositionality實現；linearizability-checker是P-compositionality算法作者自己實現的一個樣例。但使用中還有幾個問題沒有解決：
- 計算速度慢：由于上面提到的復雜度，一致性算法驗證時間通常是相關測試中的瓶頸。盡可能的加快其計算速度，可以在相同時間內驗證更多的歷史，對發現系統中的潛在問題至關重要。
- 數據模型單一：大多數的驗證工具面向的都是KV接口，這就要求使用者將千差萬別的系統實際接口轉化為KV接口使用，而這層轉換會掩蓋系統中的眾多復雜性，比如將Device接口轉化為KV后會丟失對相互覆蓋操作的驗證。
- 具體問題具體分析：對一些數據模型來說，可能存在多項式甚至是線性復雜度的算法，那么針對這些數據模型使用通用的WGL算法就舍近求遠了。
Solitaire(https://github.com/CatKang/Solitaire)是一個C++實現，更快速，支持多數據模型的線性一致性檢測工具，致力于解決上述問題。其命名來源于上世紀著名的windows桌面紙牌游戲，要求玩家在保證大小先序關系的限制下，將打亂的撲克牌整理為有序。可以說與我們的線性一致性驗證工作非常契合了。
