[[431416]]

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

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

這里我們按照本質、結構、作用 的順序簡明地描述Jepsen。

一、本質——只看Jepsen的特色

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

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

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

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

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

1.線性一致性

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

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

順序一致性和線性一致性最本質區別，在于不同Client間的操作，有沒有一個確定的happen-before關系。

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

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

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

2.線性一致性與Jepsen驗證

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

Jepsen內置了register/cas-register/multi-register/set/unordered-queue/fifo-queue這些Model。

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

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

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

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

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

二、結構——拆開Jepsen來使用

• 構建一個分布式系統環境
• 對分布式系統進行一系列操作
• 搜集操作的歷史記錄，驗證操作結果是符合預期的

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

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

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

圖4. Jepsen模塊示意

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

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

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

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

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

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

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

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

我們如果直接使用Jepsen來進行自定義測試的話，有兩部分工作。

1)包裝接口

2) 自定義Model和Checker

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

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

1.封裝接口

實現的操作如下，每一個操作中包括的接口和函數會被依次調用：

表2. restful鎖測試接口封裝

我們將這對四個操作的處理封裝進Client——LinearizableLockClient, 在Client里面加入處理每個操作返回值，根據成功、失敗、超時三種情況，生成History中各個操作Response的Log，這樣封裝接口的操作便完成了。后繼運行時，Jepsen會按照既定規則(比如隨機、定時···)對各個操作進行調用。如果只調用aquire release，Checker使用默認mutex的checker，可以驗證互斥性，全部都調用時使用自定義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"))) 
 
"初始化時鎖為釋放狀態" 
(defn mutex 
  "A single mutex responding to :acquire and :release messages" 
  [] 
  (Mutex. false)) 

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

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

圖5. 鎖可用性測試的History轉換

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

四、總結

最后我們對如何使用Jepsen做個總結：

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

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

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

參考文章：

Jepsen測試

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

當 Messaging 遇上 Jepsen

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

線性一致性理論 

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