[[431416]]

女媧團隊在過去大半年時間里持續(xù)投入女媧2.0研發(fā)，將一致性引擎和業(yè)務狀態(tài)機解耦，一致性引擎可支持Paxos、Raft、EPaxos等多種一致性協(xié)議，根據(jù)業(yè)務需求支撐不同的業(yè)務狀態(tài)機。其中的一致性引擎模塊是關(guān)鍵，研發(fā)一致性引擎時，保證一致性引擎的正確性是一大挑戰(zhàn)，所以我們用了TLA+、Jepsen等工具保證一致性引擎的正確性。這里分享一些Jepsen應用方面的體會。

目前網(wǎng)上已經(jīng)有了對于Jepsen的介紹，比如《Jepsen測試》《當 Messaging 遇上 Jepsen》,從原理和用法都有詳盡的說明，做到了致廣大而盡細微。大家可以先閱讀這些文章，對Jepsen有一個全面的了解，也可以在某些細節(jié)沒搞懂時去看看文章中詳細的闡述。本文相當于是摘要、總結(jié)和補充，一方面給大家對Jepsen的一個直觀的認識，一方面通過介紹女媧在使用Jepsen時的例子，實際說明Jepsen的作用與特點，給大家實踐過程中使用Jepsen一些參考。

這里我們按照本質(zhì)、結(jié)構(gòu)、作用 的順序簡明地描述Jepsen。

一、本質(zhì)——只看Jepsen的特色

在分布式系統(tǒng)的測試領域，最耳熟能詳?shù)膬纱蠊ぞ撸褪荰LA+和Jepsen了，其關(guān)系類似于演繹與歸納，白盒與黑盒。TLA+要求編寫測試的人能夠真實地抽象出需要驗證的分布式系統(tǒng)，在每一個細微的邏輯部分做到對真實系統(tǒng)精煉而準確的還原，而后對這個抽象系統(tǒng)在各種狀態(tài)空間進行遍歷，如果驗證抽象系統(tǒng)始終滿足定義的規(guī)則，則可推斷并保證真實系統(tǒng)的正確性，就好比有了一份關(guān)鍵信息詳實的地圖，在地圖上畫通了路線圖，真實世界按路線走也可以走到終點。Jepsen則是從系統(tǒng)對外提供的接口入手，通過實際構(gòu)建系統(tǒng)、進行操作、注入錯誤、驗證結(jié)果這一系列在錯誤注入情況下對系統(tǒng)行為的演練和分析，真實地撞出不符合既定規(guī)則的情況，通過對歷史記錄的分析找到這些情況，好比造出了一大堆散亂的拼圖，各種嘗試，最后驗證能不能拼成一個合理而規(guī)則的圖形。

由此我們不難看出兩者的難點。TLA+的難點在演繹的正確性，用TLA+寫的模型，前提是抽象系統(tǒng)與真實系統(tǒng)關(guān)鍵部分實現(xiàn)都要完全符合，如果與工程實現(xiàn)不符，就會導致一些真實系統(tǒng)中可能會遇到的問題不能被驗證到。而Jepsen最大的難點，則是根據(jù)搜集測試用例中的歷史記錄，如何歸納出系統(tǒng)是否出現(xiàn)相應的錯誤，而且歸納本身特點也決定，Jepsen測試不能涵蓋所有異常情況。在這個歸納的過程中，線性一致性是最難歸納驗證的，系統(tǒng)線性一致性的驗證也是Jepsen最大特色。

圖1. Jepsen提供的一致性驗證能力

一句話總結(jié)：Jepsen ≈ 多進程測試程序 + 線性一致性驗證

• 多進程測試程序是為了生成系統(tǒng)在各種情況下的操作記錄，線性一致性驗證則是對操作記錄的檢查。Jepsen是黑盒測試，通過在一個節(jié)點上起多個Client線程，對待測試系統(tǒng)發(fā)送各種請求，然后搜集請求結(jié)果，以此構(gòu)建各個請求操作的記錄。我們一般對系統(tǒng)都會有類似測試，相比而言，Jepsen增加了把操作記錄組織為History供后繼分析這一部分。
• 線性一致性驗證是Jepsen同F(xiàn)ailover測試最大的差異。Jepsen中雖然可以進行其他非線性一致性的驗證，但這些測試相對線性一致性的驗證會比較簡單直觀，所以這里主要詳細闡述線性一致性驗證，其中相關(guān)的兩個關(guān)鍵問題：
  • 什么是線性一致性
  • 各種不同系統(tǒng)的驗證如何統(tǒng)一為線性一致性的驗證。

1.線性一致性

之前提到的文章已經(jīng)對線性一致性提供很詳盡的論文資料和直觀說明，大家可以研究一下。文章里給出了順序一致性和線性一致性直觀的例子：

圖2 順序一致性與線性一致性

順序一致性和線性一致性最本質(zhì)區(qū)別，在于不同Client間的操作，有沒有一個確定的happen-before關(guān)系。

由于Jepsen中的Client都在同一個節(jié)點上，所以可以用系統(tǒng)時間(不會回退)記錄一個請求從Client發(fā)出到Client收到響應的時間點(對應圖中一個矩形的最左邊和最右邊)，因此能知道兩個操作之間是不是直接有happen-before關(guān)系。如果一個操作的結(jié)束時間在另一個操作開始時間之前，則兩個操作有確定happen-before關(guān)系;如果兩個操作的矩形在時間軸上有重疊，則它們的happen-before關(guān)系則并行的，順序不確定，在線性一致性系統(tǒng)中可以任意調(diào)整先后順序。

如圖2中的Get2收到響應的時間明顯是在Set2發(fā)出請求之前的，已經(jīng)有了確定的happen-before關(guān)系，卻能夠Get到在自己之前Set的數(shù)據(jù)，所以違反線性一致性。Set3 和 Get2操作是并行的，但無論其先后順序如何，均不能排列出滿足線性一致性的序列了。

而左圖的順序一致性則不同，由于P1 P2可能是不同節(jié)點的Client，其操作在時間軸上并沒有一個相同的參考，故只能保證同一Client上的操作有嚴格happen-before關(guān)系即可，因此是可以通過排列得到一個滿足順序一致性的序列的。

2.線性一致性與Jepsen驗證

Jepsen中用Model來驗證線性一致性，Model就是一個狀態(tài)機，而Jepsen測試產(chǎn)生的History是一條條輸入的Log。Log之間會有happen-before關(guān)系，也會有并行關(guān)系，Checker所要做到，便是找到一個正確的Log順序，可以在不違背happen-before的約束下，讓狀態(tài)機在每個時間應用Log后保持行為正確，而一旦違反，則找到了系統(tǒng)不符合線性一致性的證據(jù)。

Jepsen內(nèi)置了register/cas-register/multi-register/set/unordered-queue/fifo-queue這些Model。

比如我們想測試自己實現(xiàn)的分布式鎖，我們有Lock和Unlock兩種操作，便可以直接套用cas-register(這里用作說明，實際使用的是mutex)，每次搶鎖成功將register 0置1，釋放成功將register 1置0，那么在滿足happen-before的情況下，一旦出現(xiàn)無論如何排列Log，都無法得到一個正確的狀態(tài)機輸出(如下圖左邊)的情況，就說明實現(xiàn)的分布式鎖不滿足線性一致性。

圖3 History符合線性一致性的例子

我們假設上述P1 P2的操作都返回成功，則對于左圖中可能的順序，我們將其輸入Model:

而對于右圖則由于P2 Lock操作與P1的Unlock操作是并行的，所以History可以有Seq3這一排序。

對于想要測試的其他系統(tǒng)和功能也是如此，在滿足線性一致性的條件下，History會有各種可能的Log排列。若History在任何順序下輸入Model，都因為不能滿足Model自身的約束，則可以反證系統(tǒng)不滿足線性一致性。實際在Jepsen的線性一致性求解用的knossos，不會這樣全部排列遍歷的，具體用的可線性化驗證算法——WGL，可參考《線性一致性理論》。

二、結(jié)構(gòu)——拆開Jepsen來使用

• 構(gòu)建一個分布式系統(tǒng)環(huán)境
• 對分布式系統(tǒng)進行一系列操作
• 搜集操作的歷史記錄，驗證操作結(jié)果是符合預期的

根據(jù)需要可以可視化，生成反映系統(tǒng)性能和可用性的圖，以便直觀描述系統(tǒng)對于注入錯誤有哪些響應。

引文中Jepsen測試的這3個步驟，分別對應Jepsen結(jié)構(gòu)中的DB、Generator、Checker模塊。有了1.1我們對Jepsen本質(zhì)的認識，實際實踐過程中可能還有所困惑，像是應不應該使用Jepsen、如何使用Jepsen等問題，則要從Jepsen的結(jié)構(gòu)說起。按照之前的定義Jepsen = 多進程測試程序 + 線性一致性驗證，我們可以根據(jù)需要將Jepsen拆解開來使用。我們可以

• 全部使用用Jepsen來編寫測試用例
• 也可以用自己的測試框架，生成類似Jepsen格式的History，最后代入到Jepsen驗證器或自己的驗證器中。

圖4. Jepsen模塊示意

像TIDB的chaos，用Go重新實現(xiàn)了Jepsen功能的測試框架，使用了porcupine這個Go和線性一致性驗證器，也能完成和Jepsen一樣的測試效果。對于實踐而言，這兩種方案都可以完成我們的功能，而在技術(shù)選型時，則還需要考慮以下幾點:

表1. Jepsen測試實踐上的選擇

從實踐的角度來看，我們一方面關(guān)心驗證有效性，一方面在意編寫測試的難度。

測試有效性主要靠框架豐富的測試功能保證的，而編寫難度直接影響著項目效率和規(guī)模化。直接使用開源框架Jepsen，則是看重它已有功能完備，認可度高。搭建新框架，則測試上手簡單、編寫case易規(guī)模化，同時根據(jù)語言特性可以更適合某些測試場景(如解決OOM、直接復用已有測試框架的代碼)。

所以當我們只需要測試系統(tǒng)線性一致性等Jepsen已提供的驗證model(包括register/cas-register/multi-register/mutex/set/unordered-queue/fifo-queue等)時，為了簡便起見，可以直接套用Jepsen中的model，通過將自身系統(tǒng)提供的接口封裝為和已有驗證model的操作等價的語義，便可以直接運用Jepsen進行驗證。比較適合系統(tǒng)功能與已有Jepsen測試相符的情況，此時可以迅速測試系統(tǒng)的各項功能。

如果我們有很多想要新定義測試的場景，或者已經(jīng)積累了功能豐富的測試框架，或者希望有一個團隊都能很好很快上手的工具，則搭建新框架是更有效率的選擇。相比于給所有人普及Clojure或者給出一個易用的模板，還是讓大家用老錘子砸新釘子更加順手。

三、作用——女媧使用Jepsen的例子

從本質(zhì)和結(jié)構(gòu)分析下來，我們不難看出，Jepsen不限于測試并驗證一致性，但其最大特點就是線性一致性。所以一切需要有線性一致性保證的系統(tǒng)，都可以使用Jepsen的這種線性一致性驗證能力。無論是依托一致性協(xié)議的分布式鎖、分布式隊列，還是像MySQL這種主從復制的數(shù)據(jù)庫。

我們?nèi)绻苯邮褂肑epsen來進行自定義測試的話，有兩部分工作。

1)包裝接口

2) 自定義Model和Checker

由于系統(tǒng)的接口都是固定的，在Jepsen中包裝出來即可。包裝接口時，主要注意讓接口能夠快速收到響應，減少操作的耗時，因為一旦耗時時間過長，會導致大量本有確定happen-before關(guān)系的操作變成并行，極大加重了不必要的計算，也容易產(chǎn)生OOM問題。比如restful接口使用curl和使用Clojure的http庫兩種方式調(diào)用，驗證的效率截然不同。

最大的工作量是在Model和Checker處做改造，來適配我們系統(tǒng)特有的狀態(tài)機。下面我來介紹一下女媧的restful分布式鎖的互斥性和可用性驗證，大家可以參考etcd的restful鎖接口理解。鎖的互斥性驗證，在Jepsen中已有實現(xiàn)的例子，比如etcd的分布式鎖測試，只需要我們按照女媧的接口調(diào)用做出類似實現(xiàn)acqure和release即可。而如果想測試鎖的可用性，比如停止心跳后是否在timeout時間內(nèi)一定有其他client可以搶到鎖這種邏輯，則需要我們對Model部分和Checker部分進行相應的改造。

1.封裝接口

實現(xiàn)的操作如下，每一個操作中包括的接口和函數(shù)會被依次調(diào)用：

表2. restful鎖測試接口封裝

我們將這對四個操作的處理封裝進Client——LinearizableLockClient, 在Client里面加入處理每個操作返回值，根據(jù)成功、失敗、超時三種情況，生成History中各個操作Response的Log，這樣封裝接口的操作便完成了。后繼運行時，Jepsen會按照既定規(guī)則(比如隨機、定時···)對各個操作進行調(diào)用。如果只調(diào)用aquire release，Checker使用默認mutex的checker，可以驗證互斥性，全部都調(diào)用時使用自定義Checker來驗證可用性。

2.自定義Model和Checker

我們驗證鎖，Model部分仍然使用的是Jepsen提供的mutex。事實上Jepesen中涵蓋的model基本已涵蓋大部分場景，見knossos的model.clj,這里摘取我們驗證鎖用到的mutex:

(defrecord Mutex [locked?] 
  Model 
  (step [r op] 
    (condp = (:f op) 
      :acquire (if locked? 
                  "ERROR:已加鎖仍可以搶到" 
                 (inconsistent "already held")  
                 (Mutex. true)) 
      :release (if locked? 
                 (Mutex. false) 
                  "ERROR:未持有鎖卻可以釋放" 
                 (inconsistent "not held"))))   
 
  Object 
  (toString [this] (if locked? "locked" "free"))) 
 
"初始化時鎖為釋放狀態(tài)" 
(defn mutex 
  "A single mutex responding to :acquire and :release messages" 
  [] 
  (Mutex. false)) 

可以看到Mutex繼承了Model，會根據(jù)每一個op更新自身狀態(tài)，即正常的加鎖和釋放，當已加鎖仍可以搶到或者未持有鎖卻可以釋放，則說明有不一致，Model執(zhí)行出錯。

Checker部分則是驗證鎖可用性的關(guān)鍵，我們想驗證的是當lease過期之前，即touch-lease的間隔時間內(nèi)，鎖不會被搶到，在timeout時間——lease-ttl后則可以被搶到。于是我們根據(jù)已有的History，虛擬出一個Client，它的開始時間會在一個release-lease操作的lease-ttl時間后，進行一個release操作，如果過程中鎖又被搶到或者被另一個Client自己釋放，則在History中取消這個虛擬Client的操作。由此我們可以繼續(xù)使用線性一致性Checker對Mutex Model的驗證，來證明鎖的可用性——在鎖心跳過期之前不會被其他Client搶到，鎖lease-ttl結(jié)束之后可以被搶到。由于我們鎖的釋放時間是一個動態(tài)范圍，所以將Release的起始和結(jié)束時間間隔加上這個動態(tài)范圍，實際的轉(zhuǎn)換效果如下圖。

圖5. 鎖可用性測試的History轉(zhuǎn)換

由此我們可以看出，通過對Model和Checker的改造是可以很靈活多樣的，我們得到一個History之后，可以根據(jù)業(yè)務狀態(tài)機調(diào)整Model執(zhí)行Log的結(jié)果，也可以對History本身進行處理應對一些延伸的場景，如果不驗證線性一致性而是其他功能(比如最終一致性、watch等)，還可以直接分析History——最終一致性要求最后操作全部完成后讀某個寄存器結(jié)果相同，watch要求各個Client自己watch結(jié)果拼接成的序列一致，都是比較容易實現(xiàn)的操作。

四、總結(jié)

最后我們對如何使用Jepsen做個總結(jié)：

相對TLA+,Jepsen是更容易應用在測試自己的分布式系統(tǒng)中的。我們在需要驗證線性一致性的時候，只需要根據(jù)自身業(yè)務狀態(tài)機抽象出Model，處理History，就可以直接使用線性一致性驗證器進行驗證;需要驗證其它一致性時，則通過History，可以很簡單地寫出相應的測試case。

如果希望實際使用中，在生成History和驗證時有自己的需要，可以按結(jié)構(gòu)拆分，只使用Jepsen的一部分或者自己搭建框架。比如使用自有錯誤注入框架，自己生成History，給到Jepsen的一致性Checker;或是使用Jepsen生成History，自己寫簡單的腳本讀取后進行分析;或是直接搭建類似框架，更高效地應對豐富的功能、場景，快速編寫更易上手、更具有可讀性的測試代碼。

對于各種分布式系統(tǒng)，Jepsen絕對是必要的且易于編寫測試驗證的，最低成本幫助我們發(fā)現(xiàn)工程實現(xiàn)中各種各樣的問題。

參考文章：

Jepsen測試

https://ata.alibaba-inc.com/articles/109813

當 Messaging 遇上 Jepsen

https://developer.aliyun.com/article/727886

線性一致性理論 

https://zhuanlan.zhihu.com/p/338057286