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

1、隨著信息技術(shù)的高速發(fā)展，計(jì)算機(jī)系統(tǒng)已經(jīng)被廣泛的應(yīng)用于日常生活中的各個(gè)方面，比如電話通訊系統(tǒng)、銀行系統(tǒng)等。這些系統(tǒng)大部分都需要后臺(tái)運(yùn)行的分布式算法來(lái)完成一些基本目標(biāo)，比如分布式一致性和錯(cuò)誤避免。這些算法的正確性和有效性對(duì)系統(tǒng)而言是至關(guān)重要的。然而，由于分布式算法所運(yùn)行的環(huán)境復(fù)雜，算法的設(shè)計(jì)很容易出錯(cuò)。應(yīng)用恰當(dāng)?shù)臄?shù)學(xué)理論和分析方法可以增強(qiáng)系統(tǒng)的正確性和可靠性?；谀Ｐ蜋z測(cè)的形式化方法就是這樣一種技術(shù)，并已成功地在實(shí)踐中應(yīng)用于對(duì)復(fù)雜的時(shí)序線路

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

3、往往通過(guò)引入輪數(shù)來(lái)確保其能夠以一定的概率完成目標(biāo)，但這卻導(dǎo)致了輪數(shù)的無(wú)界性，從而導(dǎo)致在應(yīng)用模型檢測(cè)對(duì)算法進(jìn)行形式化驗(yàn)證時(shí)的空間爆炸問(wèn)題。本文的目標(biāo)就是針對(duì)這一類基于輪數(shù)的分布式算法，通過(guò)處理這類算法的狀態(tài)空間爆炸問(wèn)題來(lái)使用模型檢測(cè)來(lái)對(duì)這類算法進(jìn)行形式化驗(yàn)證。
　　 本文通過(guò)分析輪數(shù)之間的相互關(guān)系，發(fā)現(xiàn)雖然算法的輪數(shù)可以無(wú)限增加，然而輪數(shù)之間的距離卻是有界的?；谶@一發(fā)現(xiàn)本文提出了一種對(duì)這類算法進(jìn)行模型檢測(cè)的方法，通過(guò)維護(hù)輪數(shù)之間

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

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