[[431416]]

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

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

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

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

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

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

圖1. Jepsen提供的一致性驗(yàn)證能力

一句話總結(jié)：Jepsen ≈ 多進(jìn)程測(cè)試程序 + 線性一致性驗(yàn)證

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

1.線性一致性

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

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

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

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

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

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

2.線性一致性與Jepsen驗(yàn)證

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

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

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

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

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

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

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

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

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

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

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

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

圖4. Jepsen模塊示意

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

表1. Jepsen測(cè)試實(shí)踐上的選擇

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

測(cè)試有效性主要靠框架豐富的測(cè)試功能保證的，而編寫難度直接影響著項(xiàng)目效率和規(guī)?；Ｖ苯邮褂瞄_源框架Jepsen，則是看重它已有功能完備，認(rèn)可度高。搭建新框架，則測(cè)試上手簡(jiǎn)單、編寫case易規(guī)?；?，同時(shí)根據(jù)語(yǔ)言特性可以更適合某些測(cè)試場(chǎng)景(如解決OOM、直接復(fù)用已有測(cè)試框架的代碼)。

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

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

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

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

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

1)包裝接口

2) 自定義Model和Checker

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

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

1.封裝接口

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

表2. restful鎖測(cè)試接口封裝

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

2.自定義Model和Checker

我們驗(yàn)證鎖，Model部分仍然使用的是Jepsen提供的mutex。事實(shí)上Jepesen中涵蓋的model基本已涵蓋大部分場(chǎng)景，見knossos的model.clj,這里摘取我們驗(yàn)證鎖用到的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"))) 
 
"初始化時(shí)鎖為釋放狀態(tài)" 
(defn mutex 
  "A single mutex responding to :acquire and :release messages" 
  [] 
  (Mutex. false)) 

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

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

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

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

四、總結(jié)

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

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

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

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

參考文章：

Jepsen測(cè)試

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

當(dāng) Messaging 遇上 Jepsen

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

線性一致性理論 

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