隨著互聯(lián)網(wǎng)的迅速發(fā)展和普及,網(wǎng)絡(luò)數(shù)據(jù)流量越來愈龐大。企業(yè)信息化程度的不斷加強,導(dǎo)致大量的數(shù)據(jù)亟待處理,數(shù)據(jù)已成為各類企業(yè)的命脈。傳統(tǒng)的應(yīng)用服務(wù)使用單一服務(wù)器模式,但是由于網(wǎng)絡(luò)環(huán)境的不穩(wěn)定,服務(wù)器容易發(fā)生數(shù)據(jù)丟失、節(jié)點宕機,嚴重影響了系統(tǒng)的可用性。在單機服務(wù)逐漸不能滿足企業(yè)數(shù)據(jù)處理的需求情況下,人們開始搭建服務(wù)器集群的分布式系統(tǒng)。副本復(fù)制技術(shù)提高分布式系統(tǒng)的可靠性,在網(wǎng)絡(luò)負載較大的情況下實現(xiàn)負載均衡,緩解服務(wù)器的壓力。但是副本復(fù)制技術(shù)的引入,也帶來了副本數(shù)據(jù)一致性等問題。為了保證系統(tǒng)的高可用性和一致性,就需要使用分布式一致性算法,Paxos算法便是其中非常重要的一類。共識問題是指分布式系統(tǒng)中一組參與者就一個結(jié)果達成一致的過程。Paxos能夠很好的解決共識問題,越來越多的研究者將重點放在對算法本身的優(yōu)化或者具體工程實現(xiàn),Paxos在大型分布式系統(tǒng)得到了廣泛的運用,比如區(qū)塊鏈系統(tǒng)以及谷歌文件系統(tǒng)等。雖然Paxos的工程實現(xiàn)越來越多,但是關(guān)于算法安全性的形式化工作卻很少,為了增強研究者和企業(yè)對Paxos的應(yīng)用信息,其安全性證明越來越重要。所以,本文在定理證明工具Coq中形式化描述和定義了Lam... 

【文章來源】：華東師范大學(xué)上海市 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：82 頁

【學(xué)位級別】：碩士

【部分圖文】：

副本復(fù)制技術(shù)原理

第二章分布式共識與PAXOS華東師范大學(xué)碩士學(xué)位論文（1）A：表示可用性（Availability），即系統(tǒng)中每個成功或失敗的請求保證都會有對應(yīng)的響應(yīng)。（2）P：表示分區(qū)容忍性（ToleranceofNetworkPartition），即系統(tǒng)中的信息可以在傳遞時可以發(fā)送丟失或者發(fā)送不成功，這種情況不會對系統(tǒng)的運行產(chǎn)生影響。（3）C：表示一致性（Consistency），即在同一時間系統(tǒng)全部的服務(wù)器節(jié)點數(shù)據(jù)是相同的。圖2.2:CAP定理由上可知，在一個分布式系統(tǒng)中可用性、分區(qū)容忍性、一致性不可能同時滿足規(guī)定需求，而且分布式系統(tǒng)的各個服務(wù)組件必然會被部署到不同的數(shù)據(jù)節(jié)點，導(dǎo)致必然會出現(xiàn)各種集群以及子網(wǎng)絡(luò)，因此P是所有分布式系統(tǒng)的最基本的需求。所以在實際應(yīng)用中分布式系統(tǒng)都只能根據(jù)自身的特定需求和應(yīng)用場景在一致性和可用性之間取舍。13

第二章分布式共識與PAXOS華東師范大學(xué)碩士學(xué)位論文案內(nèi)容value。此階段消息被稱作是Accept請求消息。Phase2.2．Accepted響應(yīng)階段。如果Acceptor接收到了提案編號為行的Accept消息，且在此之前其沒有響應(yīng)過具有比提案編號更大的消息，那么Acceptor接受這個Accept請求消息，即接受這個提案編號N對應(yīng)的提案。此階段消息被稱作是Accepted響應(yīng)消息。圖2.3:BasicPaxos兩階段消息流在Proposer收到多數(shù)派Acceptor的Accepted響應(yīng)消息之后，此次提案就通過了，分布式系統(tǒng)中的Learner就可以學(xué)習(xí)該提案的提案內(nèi)容。Paxos實例在達成共識過程中，每個階段的消息傳遞情況如圖2.3所示。上述兩階段是理想情況下的BasicPasic算法的消息傳遞流程，但是在實際分布式系統(tǒng)中會比較復(fù)雜。在提案表決的過程中，由于多個Proposer可能并發(fā)運行發(fā)起不同的提案決議，或者由于其他物理原因（消息傳遞超時、物理機宕機等），導(dǎo)致沒有任何一個Ppoposer收到多數(shù)派Acceptor的應(yīng)答消息，那么就需要選取一個更大的提案編號進行下一輪的提案決議，所以BasicPaxos是一個多輪次的基于消息傳遞的共識算法。2.2.5BasicPaxos總結(jié)綜上所述，BasicPaxos是基于消息傳遞機制的多輪次選舉共識算法，其主要應(yīng)用在異步通信網(wǎng)絡(luò)和非拜占庭模型的分布式系統(tǒng)中。假設(shè)在分布式系統(tǒng)中有2F+1個節(jié)點，盡管會有部分服務(wù)器發(fā)生故障或者網(wǎng)絡(luò)消息的延遲等通信問題，都不會影響整個系統(tǒng)的正常運行，只要保證分布式系統(tǒng)中F+1個節(jié)點能夠正常地互相通信，18


本文編號：3384543