面向一類基于輪數的分布式算法的狀態(tài)空間分析與模型檢測.pdf

1、隨著信息技術的高速發(fā)展，計算機系統(tǒng)已經被廣泛的應用于日常生活中的各個方面，比如電話通訊系統(tǒng)、銀行系統(tǒng)等。這些系統(tǒng)大部分都需要后臺運行的分布式算法來完成一些基本目標，比如分布式一致性和錯誤避免。這些算法的正確性和有效性對系統(tǒng)而言是至關重要的。然而，由于分布式算法所運行的環(huán)境復雜，算法的設計很容易出錯。應用恰當的數學理論和分析方法可以增強系統(tǒng)的正確性和可靠性。基于模型檢測的形式化方法就是這樣一種技術，并已成功地在實踐中應用于對復雜的時序線路

2、設計和通信協(xié)議的正確性驗證。
　　 模型檢測通過遍歷系統(tǒng)所有可達的狀態(tài)空間來驗證系統(tǒng)是否滿足特定的安全屬性。當被驗證的系統(tǒng)的狀態(tài)空間非常大，甚至是無限的時候，就會導致模型檢測中的狀態(tài)空間爆炸問題：即在有限的時間和存儲空間條件下，無法遍歷系統(tǒng)的整個狀態(tài)空間，進而無法對系統(tǒng)的正確性進行驗證。在分布式計算領域中，存在著許多分布式算法用來解決分布式計算中的基本問題，比如領袖選舉問題和一致性問題。由于這些問題沒有確定性的解決方案，這些算法

3、往往通過引入輪數來確保其能夠以一定的概率完成目標，但這卻導致了輪數的無界性，從而導致在應用模型檢測對算法進行形式化驗證時的空間爆炸問題。本文的目標就是針對這一類基于輪數的分布式算法，通過處理這類算法的狀態(tài)空間爆炸問題來使用模型檢測來對這類算法進行形式化驗證。
　　 本文通過分析輪數之間的相互關系，發(fā)現雖然算法的輪數可以無限增加，然而輪數之間的距離卻是有界的。基于這一發(fā)現本文提出了一種對這類算法進行模型檢測的方法，通過維護輪數之間

4、的相對關系來對輪數進行表示，從而采用一種有限的表示方法來等價的對無界輪數進行表示，而不是對算法中的輪數直接進行表示。這樣就可以把算法的狀態(tài)空間表示為有限的，從而使這類算法的自動化驗證成為可能。同時文中也對這一方法的可行性進行了形式化的證明。
　　 本文將這一方法應用到了兩個領袖選舉算法(包括文中新提出的一個領袖選舉算法)和兩個分布式一致性算法中。以下是本文所專注的四個算法以及主要的理論結果：1)Itai-Rodeh領袖選舉算法：

5、在該算法的運行過程中，活動進程的輪數之間的距離最多為1；2)一個本文新提出的領袖選舉算法：在該算法中，活動進程之間的輪數之間的距離最多為n-1;3)由Bracha和Toueg提出的一個概率一致性算法：當只有一個進程可以崩潰時，在某個進程決定之前，所有正確進程的輪數之間的距離最多為3：4)一個包含故障檢測器的輪轉協(xié)調者算法：當只有一個進程可以崩潰時，在某個進程決定之前，所有正確進程的輪數之間的距離最多為2n。
　　 對于上述算法，