可線性化檢查：與 NP 完全問題做鬥爭
作者 | 夏梓耀
杏仁後端工程師，勵志成為計算機藝術家
本文的英文標題是：Linearizability Checking: Fighting With The NP-Complete
測試分散式系統正確性
一個分散式程式由一組非同步程序組成，它們通過通訊網路進行訊息傳遞。
分散式系統很難被正確實現，因為它們必須處理好併發和故障（failure）， 網路訊息可能延遲、重複、重排和丟包，而且機器可能在任何時候宕機。
即使設計在論文中被證明是正確的，但在實現中也很難避免細微的錯誤，除非用形式化方法保證，否則我們必須去測試我們認為是“正確的“的系統。
而形式化驗證技術，目前還具有很高的 cost （高到你難以想象），所以現在主要還是以測試為主，（僅部分核心邏輯會使用形式化驗證方式）。
不過，測試一個分散式系統的難度也很高，不亞於編寫一個正確的分散式程式， 併發性和不確定性使得在測試中很難捕捉到 bug，尤其是在某些極端情況下，比如幾個節點同時宕機，或者特定的網路延遲時。
對分散式程式的測試，就是對一個併發系統的測試
《Java併發程式設計實戰》第 12 章中說到：
併發測試大致分為兩類，即安全性測試與活躍性測試。在第一章，我們將安全性定義為“不發生任何錯誤的行為”，而將活躍性定義為“某個良好的行為終究會發生”。
書中所說的安全性和活躍性，對應《多處理器程式設計的藝術》一書中所指的：正確性和演進性，這兩種特性可以有效描述併發物件的行為。
（本文只探討併發系統的正確性，不談演進性，死鎖檢查就是演進性方面的測試，本文全文假設併發系統是 deadlock-free 的）
在談如何測試併發系統的正確性前，我們先來給出一些基本概念，我們必須知道什麼是正確性，什麼又是併發物件。
併發物件（concurrent object）
A concurrent object is an abstract data type that permits concurrent operations that appear to be atomic. A concurrent object is shared concurrently among components.
併發物件是一種非常 OO 的稱呼，物件就是一個包含資料的容器（以某種方式組織資料），每個物件提供一系列方法，以介面形式暴露，它定義了物件的行為。
不OO的稱呼又叫：併發資料型別（concurrent data type），你可以和 抽象資料型別（Abstract Data Type）對應起來
在順序計算模型中，程式的執行過程是操作的有序序列，即：在單執行緒下，物件的方法都是順序執行的，方法執行在時間上不重疊，這種情況下的物件稱之為順序物件。
在併發計算模型中，併發程式的執行可以看做是多個併發執行緒對一組共享物件的操作序列，即：在多執行緒環境下，物件的方法併發執行，方法執行在時間上可以相互重疊，這種場景下的物件稱之為併發物件。
比如 Java 併發庫裡常見的一些併發集合型別就是併發資料型別。
所以併發和順序，僅和計算環境（模型）有關，將順序物件丟到併發執行場景下，它就是併發物件（只不過可能會出錯），反之亦然。
當然，這樣的併發物件是無意義的，我們不做討論，所以我們討論的併發物件是指：支援併發操作的物件；所謂支援併發是指：在併發執行中，依然可以保證其行為的正確性。
正確性
什麼是行為的正確性？行為符合預期就是正確。
預期是什麼？針對順序物件，其介面描述文件中描述了某個方法執行的副作用：該操作會對物件的狀態做出怎樣的改變，這就是行為的預期，是一種非形式化的描述（當然也可以用某種形式化語言來描述，甚至用程式碼來描述，這個我們以後再表），稱之為：規範（Specification），因為其針對的是順序執行，故稱之為：順序規範（sequential specification）
我們常常寫的UT就是基於程式的順序規範進行的。
那麼併發物件的正確性呢？還可以通過順序規範來約束嗎？顯然不行，它是針對順序執行的，那麼該用什麼來描述併發物件的行為正確性呢？
《多處理器程式設計的藝術》第三章指出：併發物件的行為能夠用它們的正確性和演進性有效的進行描述，併發物件的正確性是基於某種與順序行為等價的概念，即三種正確性條件：靜態一致性，順序一致性和可線性化性（Linearizability），其約束的強度依次增大，可線性化是最強的約束，適用於描述由可線性化元件構成的高層系統。
也就是說我們可以用可線性化性（或者叫：線性一致性）來說明併發物件的正確性，所以對併發物件的正確性測試就是，測試其線性一致性。
Linearizability is a well-established correctness criterion for concurrent data types and it corresponds to one of the three desirable propertiesof a distributed system, namely consistency
其次，線性一致性有個很重要的定理，即 Herlihy 和 Wing 的 locality principle：併發系統 Q 的每個併發物件是可線性化的，則 Q 是可線性化的。
也就是說我們對併發系統中每個併發物件的可線性化檢查，就是對整個併發系統的可線性化檢查；當系統行為複雜時，我們可以對系統內每個併發物件進行線性一致性檢查，從而保證整個併發系統的正確性。
這個定理的另一個意義是，線性一致是可複合的，我們可以基於符合線性一致的系統/元件，去構建其它系統。
可線性化性（Linearizability ）
那麼什麼是可線性化性（線性一致性）呢？其表現特點是：
每個方法呼叫都應該呈現出一種與它的呼叫和響應之間的某個時刻的行為相同的瞬時效果
嗯，不知道在說什麼，不著急，上面這句話是從約束條件的角度來說，也就是實現者若想系統具有線性一致性，必須要遵循該約束條件（對實現者來說必須要關注的概念是可線性化點，也就是保證方法在呼叫和響應之間能原子或瞬時執行），我們是從測試者的角度出發的，不過在此之前，必須再說一些基礎概念。
歷史（History）
歷史是用來描述併發系統的一次執行過程的，它是方法呼叫事件和響應事件的一個有限序列，形式化的來說其定義 如下：
令 E = { call,ret } × N， { call, ret } 為識別符號集合，其包含兩個元素call和ret，前者表示呼叫（事件），後者表示呼叫的返回/響應（事件），N為自然數集合，即E是一個形如 {<call, 1>, <call, 2>, <ret, 1>, <ret, 2>} 這樣的集合。
E 中某個元素 calln = <call, n> 稱之為呼叫（call），如： <call, 1> ，我們可以簡寫為call1，讀作'呼叫1'，retn= <ret, n> 稱之為響應（return），ret1讀為'響應1'。若call的n和ret的n相等，則稱為相匹配的，如：ret1是call1的匹配響應
操作（operation）：具有輸入和輸出引數的過程的執行稱為操作
一個物件（object）包含操作的有限集合（可以理解為前面討論的一組介面）
對所有E中的元素 e，有兩個函式，obj和op，obj(e) 返回物件，op(e) 返回操作
歷史（History）就是一個 <H, obj, op> 的三元組，其中H是呼叫和響應的有限序列，即是一個關於 call 和 return 的全序集合（這個全序關係就是事件發生的時間順序關係），我們可以將三元組簡寫成H。
我們可以將歷史理解為一段完整的操作日誌記錄，且日誌中記錄了所有操作相關的資訊
歷史可以用歷史圖進行視覺化。如下圖：
（圖1）
圖中描述的是一段對集合（set）併發操作的歷史，call和ret組成了一個完整的操作，如：insert(1)，後面跟的布林值是響應的結果（返回值），圖上可以看出insert操作和remove操作在時間上是有重疊的，這個歷史可以表示為：
H = <call1, call2, ret1, ret2, call3, ret3>
完整與順序歷史（Complete and sequential history）
在歷史H中，若一個呼叫沒有與之相匹配的響應，則該呼叫是 未決 的，H可以通過新增零個或若干個未決呼叫的響應，使之成為完整的歷史，則該歷史稱為 完整 的（Complete），即：一個歷史是完整的，當每一個 call 都有唯一一個匹配的 return。 如果一個完整歷史的每個操作都是互相不重疊的，這樣的歷史稱為：順序歷史（sequential history），即歷史是順序的（sequential）。
順序歷史其實就是我們前面說的順序物件順序執行所產生的歷史，順序歷史的例子 H2：
（圖2）
它是一維的，每個操作都不疊加，每個call都緊隨著匹配的return，下面是另一個例子 H3：
顯然 H3 的操作順序是不符合set的順序規範的，remove 操作不應該返回 false，但是 H3 是良定（符合定義）的順序歷史
happen-before
你可能在看 Java 記憶體模型時看到過 happen-before 原則，我們在這裡深入理解一下它，happen-before 是一種偏序關係（集合上反自反可傳遞的關係），它是歷史中 call 之間的關係，即呼叫上的偏序關係。
如果操作 op1 的 call1 匹配的響應 ret1 ，先與 op2 的 call2 發生，則稱：call1 happen-before call2，記為 call1 -> call2。若 call1 -> call2 則，call2 一定能看到 call1 的修改（操作結果），這就是 happen-before 原則。
既然是偏序關係，那麼就存在無關的 call-x 和 call-y 他們即不是 call-x -> call-y，也不是 call-y -> call-x，這種關係稱為：happen concurrently，即它們是並行的，不用互相保證什麼
可以看出圖1中 call1 和 call3 是 happen-before 關係，call2 和 call3 是 happen-before 關係，而 call1 和 call2 是 happen concurrently 關係。
如果H是順序歷史，那麼 -> 就是一個全序關係，如上面 H2，所有 call 都是 happen-before 關係
我們又不設計記憶體模型，為什麼要說 happen-before 呢？下面就引出核心概念，並且把前面的順序歷史，順序規範，happen-before 等概念全部聯絡到一起
可線性化性（Linearizability）
可線性化性的形式化定義如下：
如果歷史 H 可以被擴充套件為一個完整歷史 H' 且存在一個合法的順序歷史 S，並使得：
L1： H' 和 S 是兩個等價的關於 call 和 return 的集合
L2： 若在H中方法 call1 happen-before call2，那麼在 S 中也成立
則稱歷史H是可線性化的，S 稱作 H 的一個線性化（H 可以有多個線性化）
非形式化的來說，H到H'，表示操作是完整的，即 deadlock-free（你若都執行不下去了，勢必不會完整，更不要談正確性了），條件 L1 指無視順序下，H' 和 S 等價，條件 L2 指 S 保持 H 中的 happen-before 關係
所以所謂可線性化，就是將多維降成一維（符合順序規範），只要能降維成功，則就是可線性化的，就是正確的。
這個理解是不是易懂多了？
可線性化性所隱含的基本思想就是每個併發歷史都等價於某個順序歷史
知道可線性化的概念了，那麼測試可線性化性的方法也就有了，我們編寫這樣一個判定程式：它接收一段歷史H，並尋找其合法的順序歷史S，判定順序歷史S是否合法，只需要其符合物件的順序規範就行。
這樣的程式就是：Linearizability Checker，它以一段併發歷史 H 和順序規範 Space 為引數，去搜索其等價的符合順序規範 Space 的順序歷史 S，而且搜尋到的順序歷史 S 必須保持原有 happen-before 關係，找到則返回 true，找不到則返回 false。
聽上去好像不復雜啊，但是很遺憾，這樣一個程式是一個 NP 完全問題（證明過程：略），什麼是 NP 完全問題？簡單的說就是沒有多項式的時間的解決方法的問題，這樣的搜尋程式要處理一個巨大的搜尋空間下進行的，其最壞的時間複雜度可以達到 O(N!) ，N 是歷史的長度。
（等價的問題是子集求和問題，即：求出給定集合 S 的某個子集 S'，其元素的和剛好等於給定值 t，你能寫出一個多項式時間複雜度的解法嗎？如果可以，恭喜你證明了 P = NP 問題，你將獲得百萬美元大獎，併名留千史）
所以，開發 Linearizability Checker 就是人類與 NPC 問題的抗爭過程
Linearizability Checker
最早提出的 Linearizability Checker 是 WG 可線性化演算法（Wing & Gong linearizability algorithm），其具體實現是：將歷史表示成call和return的雙向連結串列，而順序規範則是在一個順序物件上重演（replay）操作，驗證其返回否和響應返回的資料一致去表示，即：順序規範是可執行的。具體演算法如下圖：
所謂 minimal operation op 是指：歷史中第一個前面沒有 return 的 call，如例子 H 中的 call1。
run op on S 表示在順序物件 S 上 執行操作 op 也就是發起 call，如果其返回和 call 匹配的 return 中的返回是一致的，則這個 call 是可線性化的，將其 op 也就是 call 和匹配的 return 從連結串列中去掉（連結串列節點如果為call，它的match欄位指向其匹配的return）：h - op，進行下一個操作的可線性化檢查（遞迴），如果按照這個連結串列的順序，每個操作都可以被線性化，那麼返回true，表示整個歷史都是可線性化的，如果 S 執行某個call的返回與return不一致，那麼就回溯操作，即：undo op on S，找下一個 minimal operation op。
從全域性過程上來看，這個搜尋過程保持了 happen-before 關係，即併發歷史中有 happen-before 關係的那部分 call 是不允許重排的，而 happen concurrently 是允許重排的，找下一個 minimal operation op 就是個重排過程
上圖中的演算法是簡寫形式，真正實現時，用 stack 取代遞迴，每次將以線性化的 call 儲存到棧中，用於回溯操作
不過WG演算法，本質上還是一種樹搜尋演算法，樹搜尋的缺點就是：沒有檢測重複出現的狀態，導致搜尋空間非常大。
Lowe 擴充套件了 WG 演算法，若想消減搜尋空間，就得把不檢測重複出現狀態的樹搜尋演算法改成圖搜尋演算法，因為兩個操作 op1 和 op2 它們的操作順序可能是可以交換的，或者稱為順序無關的，比如對一個 map 上的不同 key 的操作，那麼這兩個操作就是順序無關的，不管是先執行 op1 還是先執行 op2，其導致 S 的狀態都是一樣的，所以：如果之前出現過線性化順序 <op1 , op2> 對應狀態 S1 且進行了回溯時遇到 <op2 ， op1> 這樣的重排時，就可以跳過了，因為他們的狀態是一樣的，這在已經線性化的操作序列很長，最後又進行了回溯時，會極大的提高效率，這就是WGL演算法，或者稱為WG圖搜尋演算法，如下圖：
它使用快取去記住已經出現過的狀態，其背後的思想是：如果併發資料型別的操作導致相同的狀態，那麼只需要考慮併發資料型別的兩種操作組合中的一種
其具體實現是用一個hash map （就是上圖中的 cache）去記錄已經遇到過的狀態和已經線性化的記錄（上圖中用bitset去表示），因為要記錄狀態，那麼順序物件就必須使用不可變物件（immutable），也就是每次操作之後都返回呼叫結果，以及被改變狀態後的自己
我們來用圖1中的歷史H = <call1, call2, ret1, ret2, call3, ret3> 帶入到演算法中，來感受一下其過程：
首先 entry 為 call1，entry.match != null，因為 call1.match => ret1，故執行 apply(call1, s)，s 是 set 的初始狀態（空集合），call1對應的操作是 insert(1)，所以執行後，返回true，其ret1的值也是true，故 is_linearizable 是 true，然後拷貝一份 cache 到 cache'，此時拷到第5行，因為 is_linearizable 為true，所以貝線性化記錄 linearized 到 linearized ′，將索引1設定為1（entry_id(call1) => 1 ），然後更新 cache，到第9行，因為cache'不等於cache，所以將call1和狀態s入棧，並寫入記錄 linearized 中，更新狀態s，然後通過LIFT操作將call1和其匹配的ret1從歷史中刪除，接著將entry指向新歷史的第一個節點，即 call2，call2 執行的是 remove(1) 操作，此時返回 true，因為之前 call1 已經插入1了，所以 is_linearizable 為 false，進行回溯操作，將call1 從棧頂彈出（entry 變成 call1），通過 UNLIFT 操作從新插入連結串列，並且恢復狀態s，此時entry更新為call1的 next 即 call2，繼續迴圈，一直執行後，我們發現了 <call2, call1, call3> 這樣的線性化記錄，並且原歷史H已經沒有任何元素了，所以本次檢查結束，並且返回 true （第25行）
也就是說我們得到了 <call2, ret2, call1, ret1, call3, ret3> 這樣的一個順序歷史，並且它符合set的順序規範，也代表了我們的併發物件 set 實現是正確的
通過WGL演算法雖然可以減小搜尋空間，但是效率依然不高，最可怕的是引入快取後，記憶體空間佔用會比原來高很多，我們還需要繼續努力。
還記得前面的 locality principle 嗎？ locality principle 還可以被推廣泛化，得到更通用的結論那就是： P-compositionality
P-compositionality
P-compositionality 中的 P 是分割槽（partitioning），我想你可能已經猜到我要說什麼了，沒錯，就是將歷史按照某種規則進行分割槽，前面的 locality principle 只是一種按物件的分割槽方式，對同一個併發物件來說，還可以繼續分割槽，即：將一個歷史 H 按照某種分割槽規則分為 n 個子歷史，能這麼做的依據很簡單，就是操作的無關性，前面提到過對 map 上不同 key 的操作，op1 和 op2 ，它們是無關的，我們可以按 key 對map的併發歷史進行分割槽，每個 key 的併發子歷史是可線性化的，則整個歷史都是可線性化的，這樣我們就將一個巨大的搜尋空間，分解為一個個小的搜尋空間，我們可以順序的，或者批量併發的去執行可線性化檢查，縮短時間，減小記憶體消耗。
下面給出 P-compositionality 的定義：
令 P 是一個（分割槽）函式，將歷史 H 分解為 H 的非平凡分割槽（non-trivial partition），且 P 滿足 P(H) != { H } ，非平凡分割槽的意思是有意義的分割槽，即不可以是沒有用的分割槽
一個規範（specification） φ 是 P-compositional 指： 當一個歷史 H 是關於 φ 可線性化的，當且僅當它的每一個非平凡分割槽 H' ∈ P(H) 是關於 φ 可線性化的。當這個等式成立時，我們就叫P-compositionality
locality principle 就是 P-compositionality 的一個例項，它通過一個分割槽函式 Pobj 將歷史中的相同物件進行分割槽，並且每個物件的歷史是對 φ 可線性化的。
我們同樣可以對set的元素進行分割槽，set.insert(k) 和 set.insert(k')，可以分為對 k 和對 k' 的操作歷史，這樣我們就將 set 的順序規範 φset，分割槽為了 φset-k，我們稱之為Pset-compositionality 。
顯然對於有些操作就不能進行分割槽了，比如 set 的 size 操作
所以通過 P-compositionality，我們可以先對大歷史進行某種方式的分割槽，然後再執行驗證，不過尋找分割槽演算法又變成了新的挑戰。
Ending
當然除了以上介紹的演算法外，很多其它演算法以及優化方法，不過都是圍繞著如何裁剪搜尋空間上，畢竟這是針對NPC問題唯一有效的處理方向。
我們總結一下本文的內容，首先我們要測試併發系統的正確性，可以轉變為測試併發物件的線性一致性，測試併發物件的線性一致性的判定程式叫 Linearizability Checker，它的原理是將多維的併發歷史，轉變為不重疊的一維順序歷史，轉變時必須保證呼叫的happen-before關係，且滿足順序規範，若轉變成功則表示歷史可線性化。
基於WG系演算法以及 P-compositionality 的 Linearizability Checker 開源實現：porcupine
本文內容到此已全部結束，感謝閱讀，並向那些不斷探索，挑戰理論極限的科學家致敬。
參考資料
paper
-
Testing for Linearizability
-
Faster linearizability checking via P-compositionality
slide
-
狀態空間圖和搜尋樹
blog
-
testing-distributed-systems-for-linearizability
-
人工智慧——狀態空間搜尋及狀態空間表示法
-
什麼是P問題、NP問題和NPC問題
book
-
《多處理器程式設計的藝術》
-
《Java併發程式設計實戰》
-
《分散式計算——原理、演算法與系統》
全文完
以下文章您可能也會感興趣：
我們正在招聘 Java 工程師，歡迎有興趣的同學投遞簡歷到 [email protected] 。
杏仁技術站
長按左側二維碼關注我們，這裡有一群熱血青年期待著與您相會。