標籤：

Linearizability 一致性驗證

02-04

作者：徐鵬

> 上篇文章介紹了 TiDB 如何使用 Jepsen 來進行一致性驗證，並且介紹了具體的測試案例，但是並沒有對 Jepsen 背後的一致性驗證演算法做過多介紹。這篇文章將會深入 Jepsen 的核心庫 knossos ，介紹 knossos 庫所涉及的 Linearizability（線性化）一致性驗證演算法。

Linearizability 一致性模型

什麼是一致性模型？

一致性模型確定了編寫系統的程序員與系統之間的某種協議，如果程序員遵守了這種協議，那麼這個系統就能提供某種一致性。常見的一致性模型有：

  • Strict Consistency
  • Linearizability (Atomic Consistency)
  • Sequential Consistency
  • Casual Consistency
  • Serializability
  • ……

需要注意的是這裡的系統指並發系統，分散式系統只是其中的一類。

什麼是 Linearizability ？

首先我們需要引入歷史（history）的概念，歷史是並發系統中由 invocation 事件和 response 事件組成的有限序列。

  • invocation: <x op(args*) A>，x 表示被執行對象的名稱；op 表示操作名稱，如讀和寫；args* 表示一系列參數值；A 表示進程的名稱
  • response：<x term(res*) A>，term 表示結束（termination）狀態；res* 表示一系列結果值
  • 如果 invocation 和 response 的 x（對象）和 A（進程）相同，那麼我們認為它們是對應操作，並且 complete（H）表示歷史中的最多成對操作

當我們的歷史 H 滿足以下條件時我們把它稱為順序化（sequential）歷史：

  1. H 中的第一個事件是 invocation
  2. 除了可能的最後一個事件外，每個 invocation 事件都緊跟著對應對應意味著對象和進程相同的 response 事件；每個 response 事件都緊跟著對應的 invocation 事件
  • H|A 代表只含有進程 A 操作的子歷史，H|x 代表只含有對象 x 操作的子歷史
  • 定義 well-formed：如果每個進程子歷史都是順序化的，那麼這個歷史 H 就是 well-formed。

如果一個歷史不是循序化的話那麼就是並發的。

歷史 H 在操作上引出非自反的偏序關係 <H

e0 <H e1 if res(e0) precedes inv(e1) in H

這裡的 res 和 inv 分別對應 response 和 invocation。

當歷史 H 可以通過增加 >=0 個 response 事件被延長時成為 H 並且滿足以下兩個條件時，則這個歷史是線性化（linearizable）的。

  • L1: complete(H) 與某個合法的順序化歷史 S 相等
  • L2: <H ? <S

complete(H) 表示進程以完整的操作進行交互，L2 表示如果 op1 在 H 中先於 op2 存在（注意這裡的先於強調實時發生的順序 real-time order），那麼在 S 中也是這樣。我們把 S 稱為 H 的線性化點（linearization）。

下面我們通過 3 個小例子來解釋一下以上 2 個條件。

Linearizability 的性質

  • 局部性（Locality），當且僅當 H 中每個對象 x 都是線性化的，才能保證 H 是線性化的
  • 非阻塞（Nonblocking），invocation 事件不用等待對應的 response 事件

驗證 Linearizability

正確（correctness）的定義

一段歷史 H 由兩種對象組成，representation(REP) 和 abstract(ABS) 。abstract 是被實現的類型，而 representation 類型則是用於實現 ABS 的類型。這兩種對象在以下條件下進行交互：

  1. 子歷史 H|REP 和 H|ABS 是 well-formed
  2. 對於每個進程 P，在子歷史 H|P 中，每一個 rep 操作都被 abs 操作所包含

對於某個實現中的所有歷史 H 來說，如果 H|ABS 是線性化的，那麼這個實現就是正確的。

REP 值的子集中的合法表現由表達不變性（representation invariant）所表示：I:REP->BOOL，一個合法表現的含義由抽象函數（abstract function）所表示：A:REP->ABS。對於一個正確的實現 p 來說，存在一個表達不變性 I，以及一個抽象函數 A，並且無論何時從一個合法的表達值 r 到達另一個表達值 r』，抽象操作 a 把抽象值 A(r) 變成 A(r』)。

我們從最簡單的隊列（FIFO queue）入手。

Enq 和 Deq 可以看做是 abstract operation，而 Enq 和 Deq 中的每條語句可以看做是 representation operation。

對線性化的歷史的驗證可以被轉換為對順序化歷史的驗證，對於給定的線性化歷史，我們把最終線性化點的對象的值稱為線性值。因為給定的歷史可能有超過一個線性化點，所以這個對象可能會有多個線性值。我們用表示所有線性值的集合，可以把它們看作是系統外部的觀察者所看到的值。

對於以下幾個隊列操作，對應的線性值分別有以下幾種。

為了證明正確性，我們需要保證：

For all r in Lin(H|REP), I(r) holds and A(r) ? Lin(H|ABS)

其中 H|REP 和 H|ABS 都是線性化的，r 代表 H|REP 的線性值，並且 I(r) = (r.back ≥ 1)& (? i. i ≥ r.back -> r.elements[i] = null) & (lbound(r.elements) = 1)

其中 lbound 是最小的數組索引（隊列從 1 開始）

A(r) = {q | elements(r) = elements(q) & <r ? <q}

其中偏序關係 < r 表示如果被插入元素 x 的賦值操作先於 y 的自增操作，則 x <r y，<q 代表隊列 q 的全序關係。

換句話說，隊列的表現值（representation value）就是隊列中的元素，這些元素的排列順序與 Enq 操作的順序一致。

下面這張圖可以幫助你很好地理解上述公式的意思。第二列是線性化的表現值（linearized representation values），第三列是線性化的抽象值（linearized abstract values），可以看到每一行中第二列都是第三列的子集。

Wing & Gong 線性化演算法

介紹完了如何證明 linearizability，下面我們可以繼續深入到 knossos 使用的兩個核心演算法之一——Wing & Gong Linearibility 演算法（WGL）。

WGL 演算法：對於給定的某個數據類型 T，它的並發實現為 ConcObj，而它的順序化要求為 SeqObj。對於給定的歷史 H，我們在保證 H 的實時順序 <H 的情況下嘗試 H 的每一系列可能的順序化操作，然後檢查每個順序化歷史 HS 在 SeqObj 上執行時是否是線性化的。如果 H 的每一種可能都失敗了，那麼這個歷史就不是線性化的。

我們定義歷史是由一系列事件組成的：

其中 iterm 是操作 op 的參數，name 是進行操作的進程的名字，prev 和 next 分別表示上一個和下一個事件，match 指向其對應的返回（res）事件。

另外我們還需要區域以及 lift(unlift) 這個概念。

區域（Section）：由觸發（inv）事件，對應的返回事件，以及它們中間包含的所有事件。

虛線同時可以看作是也是指針。

lift：將某對操作從歷史中移出

unlift：將移出的某對操作放回

這個演算法的核心是一個搜索（Search）函數，如果歷史是線性化的，那麼那麼他返回一個線性化點（即順序化歷史）。搜索使用一個棧來保存歷史中已經線性化的部分，這個棧及棧中的元素是這樣定義的：

其中 pi 和 pr 分別表示子歷史中第一個沒有被檢查的區域；inv 和 resp 表示子歷史中第一對操作；item、op 和 result 記錄這對操作的信息。

一個完整的搜索函數是這樣的：

  1. 初始化棧
  2. 通過操作的和定位當前的區域，否則返回線性化點
  3. 從當前區域開始，選擇一個操作並且將它的信息存儲在中
  4. 對選擇的操作進行順序化模擬，調用 op
  5. A：如果 op 返回真，意味著目前被檢查的所有操作能夠組成線性化的子歷史，所以把這個操作推入棧中，並將這個操作從歷史中移出，然後回到 2

B：1. 如果當前區域內還有一些未被選擇的觸發（inv）事件沒有排在任何返回（res）事件之後，那麼選擇一個然後回到 4 ; 2. 當前區域的所有操作已經被嘗試但是失敗了，所以我們需要將操作出棧然後嘗試其他的順序，如果棧是空的，那麼意味著歷史不是線性化的，函數返回；否則，將頂層元素出棧，這個元素包含了之前區域的所有信息，以及被選擇的操作，然後 undo 之前的，unlift 這個操作，最後，設置 current 為之前區域的指針，然後回到 5.B.1

註：4 中操作取決於具體模型，如果被測試的是一個寄存器的話，那可以是 read、write 和 cas，如果和時讀到的值和預期值不一致，則操作無法進行。

這就是整個 WGL 演算法。這個演算法很簡單也很好理解，但是有兩個明顯的缺點：

  1. 一旦操作數量上升，整個演算法會運行地很緩慢，因為可能會出現涉及大量回溯的操作
  2. 這個演算法只能驗證是否線性化，一旦線性化不成立，並不能給出具體違反線性化的出錯點

對此 knossos 庫的第二個演算法使用了 WGL 演算法的改進版本，與 WGL 中的棧存放操作信息不同的是它使用了樹遍歷和圖搜索兩種方法來使演算法更高效，同時存在 「記憶」 機制來避免對相同的操作進行重複驗證，並且如果所驗證的歷史不滿足一致性，會給出具體出錯的點。篇幅有限，如果你對這個演算法感興趣的話，文末有鏈接。

最後的思考

這篇文章介紹了什麼是 Linearizability、Linearizability 正確性的驗證及其演算法。這些演算法在分散式系統中的應用只是一個很小的方面，演算法本身是獨立的，它只需要一個歷史 H ，至於這個歷史是隨機生成的還是某個應用在實際中產生的並不重要。你可以使用這些演算法對任何並發系統進行驗證，小到一個無鎖隊列、Set，大到某個分散式系統。TiDB 作為一個分散式資料庫卻能被抽象化為一個隊列、寄存器來被用作測試這本身就是一個很有意思的地方，同時也很好地展現了這些演算法自身的魅力。

參考

Consistency Model

en.wikipedia.org/wiki/C

Knossos

github.com/jepsen-io/kn

Sequential Consistency

lamport.azurewebsites.net

Linearizability

cs.brown.edu/~mph/Herli

Linearizability versus Serializability

bailis.org/blog/lineari

WGL 演算法

cs.cmu.edu/~wing/public

Testing for Linearizability

cs.ox.ac.uk/people/gavi

推薦閱讀：

※怎樣理解王爾德的【談論天氣是無趣人類最後的避難所】這句話？

TAG:TiDB | 一致性 |