作者：Jeffrey F. Lukman, Huan Ke, Cesar A. Stuardo等

日期：2019年3月25日

原文鏈接：

https://ucare.cs.uchicago.edu/pdf/eurosys19-flyMC.pdf

摘要

我們為數據中心/云系統提供了一種快速且可擴展的測試方法，例如Cassandra，Hadoop，Spark和ZooKeeper。這個方法的獨特之處在于它有能力可以通過復雜的消息交錯來測試工作負載，以克服路徑/狀態空間爆炸問題故障。我們介紹了三種強大的算法：狀態對稱性，事件獨立性和并行翻轉。相對于其他最新解決方案，這些算法都使我們的方法比平均速度快16倍(最高78倍)。我們將技術與8種廣泛使用的數據中心系統集成在一起，成功重現了12個舊缺陷，并發現10個新缺陷。這些均在沒有隨機游走或手動檢查點的情況下完成。

CCS概念?計算機系統組織→云計算；分布式體系結構?;?可靠且容錯的系統和網絡?;?可靠性。

關鍵字：可靠性，可用性，分布式系統，軟件模型檢查，分布式并發錯誤

引言

數據中心系統，例如分布式Key-Value Store，可擴展的文件系統，數據并行計算框架以及分布式同步服務，是現代云的骨干引擎。但它們是復雜的。這個復雜性使它們很難正確使用。在此類系統中的所有類型的問題中，復雜的消息交錯，崩潰，重新啟動是最麻煩的問題[39， 50，61，62，79]。跨多個節點的事件的這種不確定性順序會導致“分布式并發”錯誤出現(或簡稱為“ DC錯誤”)。開發人員每月處理DC問題[45，48]，或更糟糕的是每周處理新開發的協議[6]。它們難以復現和診斷(要花費數周到數月的時間才能修復大多數問題)，并導致有害后果，例如整個集群不可用，數據丟失/不一致以及操作失敗[59]。

理想情況下，應該在測試中發現錯誤，而不是在部署中發現錯誤[35]。一種符合要求的系統測試技術是無狀態/軟件模型檢查。該檢查直接在實施級別的分布式系統上運行[46，49，55，58，73、80、81]。這些軟件模型檢查器1嘗試對不確定性事件進行許多可能的交錯，例如消息和故障時機，從而將目標系統推向未探測狀態，并可能揭示難以發現的錯誤。

檢查器1在本文中，“檢查器”專門代表了分布式系統的軟件模型檢查器，不包括“本地”線程調度檢查器[22、66]或經典模型檢查器[37、42]。

圖1. 檢查器1可擴展性

x軸代表經過測試的協議(Raft或Paxos)，并具有1到3個并發更新。對數比例的y軸表示耗盡搜索空間的路徑數(即路徑爆炸)。與我們的檢查器FlyMC相比，當前的檢查器在更復雜的工作負載下無法很好地擴展。“↑”表示路徑探索不完整

檢查器的克星之一是路徑爆炸問題。舉例說明，假設有10個并發消息(事件){a，b，..，j}，那么諸如深度優先搜索(DFS)之類的簡單檢查器必須執行10！個(階乘)特定執行路徑(ab..ij，ab..ji等)。圖1進一步說明了爆炸問題。灰色的“ DFS”欄顯示了在簡單工作負載下(例如Raft更新協議(“ Raft-1”)的實例化)[67] 幾乎有100條路徑(沿y軸)探索。

為了解決這個問題，檢查器采用了路徑縮減算法。例如，MODIST [81]和其他一些人[73,80]修改了流行的動態局部降階(DPOR)概念[38，41]，“由給定節點處理的消息獨立于發往其他節點的其他并發消息(因此，不需要交錯)。” SAMC [58]也進一步擴展了DPOR。結果相較原始DFS方法的路徑減少效果顯著，如圖1中的Raft-1的“ mDPOR”和“ SAMC”欄所示。

盡管取得了這些早期的成功，但我們發現在更復雜的工作負載下，路徑爆炸問題仍然沒有得到解決。例如，在兩個或三個并發的Raft更新(圖1中的Raft-2和-3工作負載)下，在MODIST和SAMC中探索路徑的數量仍然顯著增加。更不用說更復雜的工作負載，例如Paxos [57]，路徑爆炸更大(例如，圖1中的Paxos-1到-3工作負載)。

圖2. Cassandra Paxos(CASS-1)中的復雜DC錯誤

我們將此錯誤標記為“ CASS-1” [4]，該漏洞需要進行三個Paxos更新，并且僅需要兩次翻轉就可以暴露(在提議以投票1提交之前必須啟用帶投票2的prepare消息，在提議投票2之前必須啟用帶投票3的prepare消息)發生在54個事件的所有可能翻轉中，導致數據不一致

綜上所述，現有檢查器無法在更復雜的分布式工作負載下擴展。但是實際上，一些現實世界中的錯誤仍然隱藏在復雜的交錯之后(第7節)。例如，圖2中Cassandra中的Paxos錯誤只能在具有三個并發更新和總共54個事件的工作負載下出現。使用現有的檢查器這些類型的錯誤將需要數周的時間出現，浪費了測試計算資源，延遲了錯誤的發現和修復。由于上述所有原因，為了找到DC錯誤，一些檢查器將其算法與隨機游走[81]或手動檢查點[49]混合在一起，希望更快地達到導致DC錯誤的“有趣的”的交錯。但是，這種方法變得不系統。與系統地覆蓋和可觀察事件有關的所有狀態覆蓋率相比，隨機和手動方法導致的覆蓋范圍較差。

我們介紹FLYMC，這是一種快速，可擴展且系統的軟件/無狀態模型檢查器。它涵蓋了與可觀察事件有關的所有狀態，以測試分布式系統的實現。FLYMC通過利用分布式系統的內部屬性來實現可擴展性。

我們在下面用三種FLYMC的算法進行說明。

(1)通信與狀態對稱：在云系統中很常見，許多節點具有相同的角色(例如，跟隨者節點，數據節點)。這種對稱節點的狀態轉換通常僅取決于消息的順序和內容，而與節點ID /地址無關。因此，FLYMC減少了代表相同對稱通信或狀態轉換的不同路徑為單條路徑。

(2)事件獨立性：盡管狀態對稱性大大省略了對稱路徑，但許多事件仍必須在非對稱路徑中進行排列。FLYMC能夠識別大量事件獨立性，可以利用這些事件獨立性來減輕浪費的重新排序。例如，FLYMC自動將更新不相交變量集的并發消息標記為獨立。FLYMC還可以在與系統崩潰相關的事件之間找到獨立性。

(3)平行翻轉：盡管先前的方法減少了對每個節點的消息交錯，但是總的來說，仍然必須在所有節點之間完成許多翻轉(事件的重新排序)。問題在于，在現有的檢查器中，一次僅翻轉(重新排序)一對事件。為了加快速度，并行翻轉在不同節點上同時執行并發消息的重新排序，以快速達到難以到達的極端情況。

最后，不僅路徑減少而且wall-clock(現實時間)速度也很重要。為了某些正確性和功能目的，現有的檢查程序必須在每對啟用的事件之間等待不可忽略的時間。在簡單的工作負載下，等待時間是合理的，但會嚴重影響復雜工作負載的總測試時間。FLYMC通過執行本地順序和狀態轉換緩存來優化此設計，這將在后面進行介紹(第5節)。

總的來說，這些算法使FLYMC平均比其他先進的基于系統和隨機的方法快16倍(最高78倍)，并且設計優化將其提高到28倍(最高158倍)。FLYMC與8個廣泛使用的系統集成在一起，這是我們所知道的最大數量的集成。我們對10個協議實現(Paxos，Raft等)進行了模型檢查，成功重現了12個舊錯誤，并發現了10個新的DC錯誤，這些錯誤均已被開發人員確認，并且均以系統的方式進行，沒有隨機游走或手動檢查點。這些錯誤中的某些錯誤是在合理的時間內無法由先前的檢查器解決的。我們有公開發布了FLYMC [20]。

以下各節詳細介紹了我們的四個貢獻：

1. ??高度可擴展的檢查器算法，可為給定的工作負載提供系統的狀態覆蓋。(第3節)。

2. ??支持靜態分析的檢查器設計可幫助開發人員從目標系統中提取信息，并使用其編寫算法的特定部分(第4節)。

3. ??其他改進功能可改善檢查程序的探索路徑中的wall-clock速度(第5節)。

4. ??與具有挑戰性的應用程序進行了全面的集成，并通過詳細的評估證明了檢查程序的有效性。(第6-7節)。

對于有興趣的讀者，我們提供了深入的技術報告[21]。

背景

Checker架構：檢驗器的概念及其詳細工作原理可以在現有檢驗器文獻中找到[58，第2.1節] [81，第2節] [73，第3節] [21，第2節]。本節簡要討論了重要的組件和術語。

圖3.檢查器架構

如圖3所示，檢查器運行目標工作負載(例如，在節點A和B中)并攔截所有運行中的消息(例如，被灰色“鉤子”攔截的并發消息a1，a2，b1和b2)以控制其時間。然后，檢查程序的服務器一次啟用一個消息事件(例如，啟用b1)。檢查程序的鉤子等待目標系統停止運行(在處理b1之后)，節點等待將新的結果全局狀態(例如S1)傳遞給檢查程序的服務器，該服務器將其記錄為狀態事件歷史記錄(例如S0 + b1) →S1)。開發人員決定要檢查的全局狀態變量(例如，角色，領導者，投票編號)。然后，服務器運行斷言以查找新狀態下的任何安全沖突。

每個啟用事件生成的新事件將被檢查器再次攔截(例如，響應b1生成的a3，圖中未顯示)。整個過程重復執行(S0 + b1→S1，S1 + b2→S2，... + a3→...)，直到到達終止點——違反規范或工作負載無任何違反地終止(例如，沒有觀察到更多消息)。這形成了一條探索路徑(例如b1b2 ... a3)。路徑表示事件的唯一總順序；它也被稱為“跟蹤”或“執行序列” [44、54、81]。

給定先前使用的路徑，檢查器將置換可能的交錯(以探索路徑)并重新啟動工作負載。例如，在下一次運行中，它將在b1之前翻轉b2，因此在相同的工作量內使用新的路徑b2b1...。路徑也可以包含崩潰/重啟事件；例如，路徑b1BB↑b2 ...表示在處理b1之后，但在b2到達之前注入了崩潰B和節點B上的重新啟動B↑。如果存在，則整個測試完成(耗盡狀態空間) 沒有更多的探索途徑。

FLYMC算法

通過考慮分布式系統的屬性，我們使FLYMC具有兩種簡化算法：通信和狀態對稱(第3.1節)和事件獨立性(第3.2節)；一種優化算法：并行翻轉(第3.3節)。這兩種簡化算法減少了不必要的交錯(冗余路徑)，這些交錯會導致探索之前相同的狀態。優化算法對交錯進行優先級排序，從而可以更快地處理極端情況。

在本節中，我們以以下格式描述每種算法：

(a)要解決的特定路徑爆炸問題；

(b)減少或確定優先級的直覺；

(c)高層描述中的算法；

(d)與現有解決方案的比較。

在第4節的后面，我們將討論正確實現這些算法的復雜性，以及我們的靜態分析支持如何在這方面幫助開發人員。

通信與狀態對稱

圖4.通信對稱性

解釋圖在第3.1節的部分問題

難題：讓我們想象一下圖4a中的簡單通信，其中消息k triggersl，x觸發器y，k和x是相同類型的消息(例如，寫請求)。圖4b和4c示出了兩個可能的重新排序的路徑klxy和xykl。盡管這些路徑似乎不同，但它們在圖4b-c中的通信結構暗示了不對稱減小的可能性。

在本地并發文獻中實現對稱約簡的一種方法是抽象系統屬性[32，33，75]。將其應用于分布式系統時，我們最初嘗試僅抽象通信結構，特別是通過將發送方和目標節點ID(例如IP地址)抽象為規范的接收順序；例如，在圖4b中，由于節點B是第一個接收到的節點，因此其節點ID被抽象為節點“ 1”(例如，kA→B變為k2→1)。類似地，在圖4c中，由于節點A是第一個接收到的節點，因此它的節點ID被抽象為節點“ 1”(例如，xB→A變為x2→1)，因此，由于k和x是消息，因此這兩個圖表現出通信對稱性。從節點“ 2”到“ 1”具有相同類型。

不幸的是，這種方法并不總是有效的，因為大多數消息都帶有唯一的內容。例如，在Paxos中，消息k和x帶有不同的投票號，因此不能被相同地對待。因此，盡管圖4b和4c中的通信結構(箭頭)看起來是對稱的，但僅對消息進行抽象并不會導致大量減少。

簡介：幸運的是，在許多云系統中，許多節點具有相同的角色(例如，跟隨者節點，數據節點)，盡管它們的節點ID不同。此外，這種對稱節點的狀態轉換通常僅取決于消息的順序和內容，而與發送/接收節點ID無關。

圖5.狀態對稱

該圖在第3.1節的“直覺”部分中進行了說明

為了說明這一點，讓我們考慮圖5a-b中的兩個通信結構，它們代表了具有兩個并發更新(實線和虛線)的(大大簡化了)Paxos實現的第一階段。節點A廣播其準備消息(實線)，a1向其自身廣播，b1向節點B廣播，“ 1”表示投票號1。類似，節點B向其自身廣播b2，廣播給投票號2的節點a2(虛線) 行。

如果我們比較圖5a-b中的兩個通信結構，則它們不是對稱的，這與圖4中的先前示例不同。但是，讓我們分析每個節點的狀態轉換，例如該節點已收到的最高投票數，如圖3所示。圖5的中間表。在此Paxos示例中，每個節點僅接受較高的選票，而放棄新的較低的選票，因此節點的準備狀態單調增加。按照圖5a中的b1a2b2a1的左順序，節點A的狀態轉換為00222，而節點B的狀態轉換為01122。右邊的順序a1b2a2b1，狀態轉換是對稱的(鏡像)，A中為01122，B中為00222。

綜上所述，盡管兩條路徑沒有顯示出通信對稱性(圖5a-b)，但它們的狀態轉換卻是對稱的(中間表)。因此，狀態對稱對于路徑修剪可能是有效的(例如，如果已經探索過b1a2b2a1，則a1b2a2b1就是多余的)。

算法：為實現對稱性，首先，我們保留過去執行過的狀態-事件轉換(第2節)的歷史記錄，格式如下：Si + ej→Sj其中“ S”表示全局狀態(即， 每個節點狀態的集合)和ej是下一個啟用的事件。因此，啟用ej時，全局狀態將從狀態Si轉換為Sj。

此外，我們保留了{absState + absEv}過渡的歷史記錄，其中absState表示抽象的全局狀態(按字母順序)，不包括對稱節點(如數據節點)的節點ID(以及類似的absEv forevents)。使用圖5a中的示例，第一個事件將生成{00 + 1}，其中00表示數據節點A和B的抽象狀態(僅具有最高的投票號，不包括節點ID)，而1表示抽象的a1消息。隨后，我們將{01 + 2}，{12 + 2}和{22 + 1}記錄到歷史記錄中。重要的是要注意狀態12來自字母順序的狀態21；也就是說，對稱實現需要按字母/數字排序。

根據這個歷史記錄，圖5b中的第二階a1b2a2b1將被標記為對稱；當系統處于狀態00時啟用a1(抽象為+1)時，將找到歷史匹配項{00 + 1}。同樣，對于b2(抽象為+2)，當系統處于狀態01時，將找到匹配項{01 + 2}。一個警告是，由于仍在建立歷史記錄，因此狀態對稱在較早的路徑中效果較差，但是在經過一些初始路徑后，“緩存命中率”顯著增加(第5節中有更多說明)。

比較：在經典(狀態)模型檢查中，對稱性通常用于對稱處理器[32，75]。在分布式檢查器中，除了SAMC[58]，沒有發現使用對稱性的方法[46，49，55，58，73，80，81]。但是，SAMC僅使用對稱性來減少不必要的崩潰時間，而沒有用于并發消息。FLYMC的對稱性更為強大，因為它還可以概括碰撞時間。更具體地說，崩潰是作為針對特定節點的崩潰事件而抽象的。例如{12 +2}意味著在節點上注入了編號為2的崩潰(與數據節點ID無關)。

事件獨立性

難題：盡管狀態對稱性省略了對稱路徑，但在非對稱路徑中，還有許多其他事件需要重新排序。例如，如果四個不同類型的消息a1 ... a4與節點A并發，則排列將導致4！倍多的路徑。由于仍然必須對發送給每個節點的一些并發消息進行重新排序，因此需要進行更多的減少。

圖6.具有多個崩潰的復雜計時的ZooKeeper錯誤(ZOOK-1)

該錯誤在第3.2節和第7.1節中被引用。標記為ZOOK-1 [13]的錯誤需要46個事件，包括3個崩潰事件和3個重新啟動事件，以及兩個傳入事務，ZooKeeper原子廣播(ZAB)和領導者選舉(LE)協議之間的復雜并發

直覺：在這種情況下，FLYMC適應了引言中提到的DPOR的“獨立”(又稱可交換性)概念。在DPOR中，如果Si + e1 + e2→Sj和Si + e2+ e1→Sj，則兩個事件e1和e2是獨立的。也就是說，如果e1e2或e2e1導致了從Si到Sj的相同全局狀態轉換，則當系統位于Si時，事件對e1和e2不必翻轉，從而減少了探索路徑的數量。分布式系統中獨立性的一個示例是，當許多并發消息(到達目標節點)更新不同的變量時。例如，在某些分布式系統(例如ZooKeeper)中，原子廣播協議可能與領導者選舉協議同時運行(由于節點崩潰)，但是這兩個協議中的某些消息不會更新相同的變量(當系統處于特定狀態Si)，因此沒有必要翻轉它們。

算法：盡管有狀態模型檢查器(具有已知的狀態轉換)[29，38，41，69]提出了DPOR /獨立性的概念，但使其適應無狀態分布式檢查器并不是一件容易的事–檢查器如何事先知道Si + e1e2和+e2e1在執行事件之前會導致相同的未來狀態Sj嗎？為此，FLYMC通過靜態分析幫助開發人員提前識別不相干的更新(第4.1節中的更多詳細信息)。

本質上，對于發送給節點N的每條消息ni，我們的靜態分析都會在n當前狀態下處理ni的流程中，構建實時readSet和updateSet，這是一組待讀取和已更新的變量。也就是說，我們的方法結合了以下事實：ni的讀取和更新集會隨著節點N在不同狀態之間的轉換而改變。因此，如果ni的readSet和updateSet在當前狀態Si下不與nj的updateSet重疊，則發給節點N的兩條消息ni和nj被標記為獨立，反之亦然。此外，如果兩個消息的updateSets完全相交，并且集合中的所有變量都增加/減少了一個(例如，分布式系統中的通用確認增量“ ack ++”)，然后將這兩個消息標記為獨立/可交換。

除了減少不必要的消息交錯之外，可伸縮檢查器還必須減少在不同時間的不必要的崩潰注入。50％的DC bug只能在至少一個碰撞注入后浮出水面，而12％的DC bug在特定時間至少需要兩次碰撞事件[59](例如，圖6中復雜的ZooKeeperbug)，這進一步加劇了路徑爆炸問題(設想不同) 故障定時，例如..a1a2A..，..a1A..，..a2A..，其中“A”表示節點A崩潰)。因此，FLYMC的獨立性適應性的另一個獨特之處是為碰撞事件構建了以上場景。例如，如果跟隨者節點崩潰(B)，而領導者節點A通過減少活動節點數(例如liveNodes–)作出反應，則B的updateSet將包含A的liveNodes變量。

比較：先前的檢查程序采用了DPOR的獨立性，但程度有限，因此在復雜的交錯下無法擴展。例如，MODIST [81，第3.6節]，CrystalBall [80，第2.2節]和dBug [73，第2節]僅采用DPOR，其規則如下：“給定節點要處理的消息獨立于其他并發消息 運往其他節點”。但是，因為它們是不分析目標源代碼的黑匣子檢查器，所以他們找不到更多的獨立性。另一方面，FLYMC是白盒檢查程序，它在當今基于DevOps的云開發中利用對源代碼的訪問，開發人員是測試人員，反之亦然[60]。

SAMC是白盒檢查器的另一個示例，但是開發人員需要手動分析其目標系統代碼并遵循SAMC簡單原則。因此，SAMC僅引入了謹慎而嚴格的歸約算法，這些算法的功能不如FLYMC強大(請注意，在FLYMC中，上述集合的內容將通過靜態分析支持自動構建)。

例如，FLYMC將丟棄的消息([58，第3.3.1節])概括為空的updateSet，這樣的消息將自動與任何其他消息不沖突，因此不需要重新排序。再舉一個例子，不會導致新消息的崩潰(例如，跟隨節點B崩潰后仍保持仲裁)將不會與所有未完成的消息交錯[58，第3.3.2節]，因為FLYMC自動識別崩潰事件B的updateSet(例如，領導節點中的liveNodes)與運行中消息的updateSet不沖突。

平行翻轉

難題：雖然我們以前的方法減少了對每個節點的消息重新排序，但總的來說，仍然必須在所有節點之間進行許多翻轉。問題在于，在現有的檢查器中，要創建新的重新排序路徑，一次只能翻轉一對事件。例如，在圖7a中，兩個并發消息a1和a2正在傳輸到節點A，四個消息b1 ... b4則傳輸到節點B。圖7b說明了現有方法如何一次僅翻轉一對非獨立事件；例如，在路徑＃1 a1a2b1b2b3b4之后，通過在b3之前滑動b4，然后在b2之前滑動b4的后繼路徑＃3，創建下一個路徑＃2，依此類推。現在，讓我們假設一個錯誤是由a2a1排序引起的(即，必須在a1之前啟用a2)。在上面的標準方法中，將花費4！重新排序(到B的四個消息中)，然后才有機會在a1之前翻轉a2。

直覺：在分析BUG基準時，我們觀察到了這樣的規律。例如，要中了圖2中的Paxos bug，nodeC必須在Commit#1之前接收到Prepare#2消息，但有8個更早的in-flight消息到其他節點，必須重新排序。更糟糕的是，在這之后，Prepare#3消息必須在Propose#2之前到達，但有5個更早的消息需要翻轉。因此，誘發BUG的翻轉沒有提前行使。

這個問題促使我們引入平行翻轉。也就是說，我們允許對事件的平行翻轉，而不是一次翻轉一次，而是允許對事件的并行翻轉。并行翻轉也符合一個典型的開發者的觀點，即成熟的云系統一般在 "一階"(常見交錯下)都是穩健的，但同時在所有節點上進行 "不常見 "的交錯，可能會更快地發現bug[27]。

算法：對于下一個要探索的路徑，我們在每個節點中翻轉兩個消息對，因此在所有N個節點中同時翻轉N次(但我們不在一個節點內進行多次翻轉)。例如，在圖7c中，在執行路徑#1 a1a2b1...b4后，在路徑#2中，我們同時進行了a2a1和b4b3的翻轉。這是允許的，因為在飛行過程中向節點A發送的信息與向節點B發送的信息是獨立的(根據我們的DPOR 在§3.2中采用)。如果無法進行平行翻轉，則返回到單次翻轉(例如，在路徑#3中只進行b4b2翻轉)。

我們強調，并行翻轉是一種優先級算法，而不是簡化算法。也就是說，這種算法可以幫助開發者更快地挖掘出bug，但不會減少狀態空間。因此，在實現中，FLYMC保留了并行翻轉之前的單次翻轉路徑，并將并行翻轉之前的單次翻轉路徑轉化為一組低優先級的探索路徑，這樣FLYMC就可以保持系統性。

比較：我們沒有發現有任何分布式檢查器采用并行翻轉這樣的算法。然而，在軟件測試文獻[31，44]中，我們發現，我們的方法在精神上類似于 "分支翻轉"，即同時翻轉多個分支約束，以更快地覆蓋更多的極端案例。

智聯聯盟秘書處翻譯，如有需調整、需提高等，歡迎反饋！

推 薦 閱 讀

TiD系列線上沙龍 | 測試架構師思維養成

TiD系列線上沙龍 | 構建全面敏捷思想的測試團隊

TiD系列線上沙龍 | 從DevOps與中臺戰略的落地挑戰談“業務IT協同化”

TiD系列線上沙龍 | 如何查找性能瓶頸的證據鏈

點擊“

總結

以上是生活随笔為你收集整理的编写程序计算交错序列_外文翻译 | FlyMC：高度可扩展地测试分布式系统中的复杂交错...的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。