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

日期：2019年3月25日

原文鏈接：

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

摘要

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

CCS概念?計算機系統(tǒng)組織→云計算；分布式體系結(jié)構(gòu)?;?可靠且容錯的系統(tǒng)和網(wǎng)絡(luò)?;?可靠性。

關(guān)鍵字：可靠性，可用性，分布式系統(tǒng)，軟件模型檢查，分布式并發(fā)錯誤

引言

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

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

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

圖1. 檢查器1可擴展性

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

背景

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

圖3.檢查器架構(gòu)

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

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

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

FLYMC算法

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

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

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

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

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

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

在第4節(jié)的后面，我們將討論正確實現(xiàn)這些算法的復(fù)雜性，以及我們的靜態(tài)分析支持如何在這方面幫助開發(fā)人員。

通信與狀態(tài)對稱

圖4.通信對稱性

解釋圖在第3.1節(jié)的部分問題

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

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

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

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

圖5.狀態(tài)對稱

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

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

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

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

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

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

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

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

事件獨立性

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

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

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

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

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

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

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

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

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

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

平行翻轉(zhuǎn)

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

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

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

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

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

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

智聯(lián)聯(lián)盟秘書處翻譯，如有需調(diào)整、需提高等，歡迎反饋！

推 薦 閱 讀

TiD系列線上沙龍 | 測試架構(gòu)師思維養(yǎng)成

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

TiD系列線上沙龍 | 從DevOps與中臺戰(zhàn)略的落地挑戰(zhàn)談“業(yè)務(wù)IT協(xié)同化”

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

點擊“

總結(jié)

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

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。