基于概率模型檢測的分布式算法驗(yàn)證和分析.pdf

1、分布式算法在實(shí)際應(yīng)用中具有重要的價值意義,本文采用一種基于概率模型檢測技術(shù)驗(yàn)證和分析了兩類分布式算法的性質(zhì),并這些性質(zhì)給出了相應(yīng)的證明。由于概率模型檢測可以窮舉狀態(tài)空間,相比于傳統(tǒng)方法,使得它更接近真實(shí)應(yīng)用環(huán)境,更利于我們研究算法的安全性和有效性;同時概率模型檢測器中的馬爾科夫技術(shù)可以分析出模型中那些不確定因素。
　　隨機(jī)分布式算法中有一種自動恢復(fù)狀態(tài)的算法—自穩(wěn)定算法, Mitchell Flatebo提出的自穩(wěn)定算法是通過一個

2、簡單隨機(jī)的解決方案解決n個進(jìn)程令牌環(huán)中的故障,使故障自動恢復(fù)正常。他證明出最壞的情況有n-1個令牌,所需要的時間的上界是0.5N2-0.5N-2。從實(shí)驗(yàn)中,發(fā)現(xiàn)這個上限出現(xiàn)的可能很小。而在實(shí)際應(yīng)用中,我們更注重系統(tǒng)預(yù)期恢復(fù)穩(wěn)定狀態(tài)的時間—預(yù)期最差時間。實(shí)驗(yàn)中,主要采用PRISM工具驗(yàn)證了Flatebo算法的性質(zhì),并且把它與同類型Herman自穩(wěn)定算法做了比較,當(dāng)系統(tǒng)中的結(jié)點(diǎn)數(shù)目增加時,它的性能會逐漸提高,優(yōu)于Herman算法;另外,還用

3、線性回歸從實(shí)驗(yàn)結(jié)果中擬合出預(yù)期最差時間在O(N1.45)和O(N1.47)之間;最后還給出一個驗(yàn)證和分析自穩(wěn)定算法的簡單方法。
　　本文研究的另一個分布式算法是隨機(jī)互斥算法,提出了一個基于概率模型檢測工具PRISM方法,用于驗(yàn)證和分析Kerry Raymond提出的分布式K互斥算法,首先驗(yàn)證了互斥算法無死鎖和無饑餓兩種基本性質(zhì);然后通過PRISM驗(yàn)證某一進(jìn)程進(jìn)入臨界區(qū)平均及時時間;接著分析我們的實(shí)驗(yàn)結(jié)果,當(dāng)各個進(jìn)程的相對訪問臨界區(qū)