基于Coq的Paxos的形式化建模與驗(yàn)證
發(fā)布時(shí)間:2021-09-05 03:02
隨著互聯(lián)網(wǎng)的迅速發(fā)展和普及,網(wǎng)絡(luò)數(shù)據(jù)流量越來愈龐大。企業(yè)信息化程度的不斷加強(qiáng),導(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é)點(diǎn)宕機(jī),嚴(yán)重影響了系統(tǒng)的可用性。在單機(jī)服務(wù)逐漸不能滿足企業(yè)數(shù)據(jù)處理的需求情況下,人們開始搭建服務(wù)器集群的分布式系統(tǒng)。副本復(fù)制技術(shù)提高分布式系統(tǒng)的可靠性,在網(wǎng)絡(luò)負(fù)載較大的情況下實(shí)現(xiàn)負(fù)載均衡,緩解服務(wù)器的壓力。但是副本復(fù)制技術(shù)的引入,也帶來了副本數(shù)據(jù)一致性等問題。為了保證系統(tǒng)的高可用性和一致性,就需要使用分布式一致性算法,Paxos算法便是其中非常重要的一類。共識(shí)問題是指分布式系統(tǒng)中一組參與者就一個(gè)結(jié)果達(dá)成一致的過程。Paxos能夠很好的解決共識(shí)問題,越來越多的研究者將重點(diǎn)放在對(duì)算法本身的優(yōu)化或者具體工程實(shí)現(xiàn),Paxos在大型分布式系統(tǒng)得到了廣泛的運(yùn)用,比如區(qū)塊鏈系統(tǒng)以及谷歌文件系統(tǒng)等。雖然Paxos的工程實(shí)現(xiàn)越來越多,但是關(guān)于算法安全性的形式化工作卻很少,為了增強(qiáng)研究者和企業(yè)對(duì)Paxos的應(yīng)用信息,其安全性證明越來越重要。所以,本文在定理證明工具Coq中形式化描述和定義了Lam...
【文章來源】:華東師范大學(xué)上海市 211工程院校 985工程院校 教育部直屬院校
【文章頁(yè)數(shù)】:82 頁(yè)
【學(xué)位級(jí)別】:碩士
【部分圖文】:
副本復(fù)制技術(shù)原理
第二章分布式共識(shí)與PAXOS華東師范大學(xué)碩士學(xué)位論文(1)A:表示可用性(Availability),即系統(tǒng)中每個(gè)成功或失敗的請(qǐng)求保證都會(huì)有對(duì)應(yīng)的響應(yīng)。(2)P:表示分區(qū)容忍性(ToleranceofNetworkPartition),即系統(tǒng)中的信息可以在傳遞時(shí)可以發(fā)送丟失或者發(fā)送不成功,這種情況不會(huì)對(duì)系統(tǒng)的運(yùn)行產(chǎn)生影響。(3)C:表示一致性(Consistency),即在同一時(shí)間系統(tǒng)全部的服務(wù)器節(jié)點(diǎn)數(shù)據(jù)是相同的。圖2.2:CAP定理由上可知,在一個(gè)分布式系統(tǒng)中可用性、分區(qū)容忍性、一致性不可能同時(shí)滿足規(guī)定需求,而且分布式系統(tǒng)的各個(gè)服務(wù)組件必然會(huì)被部署到不同的數(shù)據(jù)節(jié)點(diǎn),導(dǎo)致必然會(huì)出現(xiàn)各種集群以及子網(wǎng)絡(luò),因此P是所有分布式系統(tǒng)的最基本的需求。所以在實(shí)際應(yīng)用中分布式系統(tǒng)都只能根據(jù)自身的特定需求和應(yīng)用場(chǎng)景在一致性和可用性之間取舍。13
第二章分布式共識(shí)與PAXOS華東師范大學(xué)碩士學(xué)位論文案內(nèi)容value。此階段消息被稱作是Accept請(qǐng)求消息。Phase2.2.Accepted響應(yīng)階段。如果Acceptor接收到了提案編號(hào)為行的Accept消息,且在此之前其沒有響應(yīng)過具有比提案編號(hào)更大的消息,那么Acceptor接受這個(gè)Accept請(qǐng)求消息,即接受這個(gè)提案編號(hào)N對(duì)應(yīng)的提案。此階段消息被稱作是Accepted響應(yīng)消息。圖2.3:BasicPaxos兩階段消息流在Proposer收到多數(shù)派Acceptor的Accepted響應(yīng)消息之后,此次提案就通過了,分布式系統(tǒng)中的Learner就可以學(xué)習(xí)該提案的提案內(nèi)容。Paxos實(shí)例在達(dá)成共識(shí)過程中,每個(gè)階段的消息傳遞情況如圖2.3所示。上述兩階段是理想情況下的BasicPasic算法的消息傳遞流程,但是在實(shí)際分布式系統(tǒng)中會(huì)比較復(fù)雜。在提案表決的過程中,由于多個(gè)Proposer可能并發(fā)運(yùn)行發(fā)起不同的提案決議,或者由于其他物理原因(消息傳遞超時(shí)、物理機(jī)宕機(jī)等),導(dǎo)致沒有任何一個(gè)Ppoposer收到多數(shù)派Acceptor的應(yīng)答消息,那么就需要選取一個(gè)更大的提案編號(hào)進(jìn)行下一輪的提案決議,所以BasicPaxos是一個(gè)多輪次的基于消息傳遞的共識(shí)算法。2.2.5BasicPaxos總結(jié)綜上所述,BasicPaxos是基于消息傳遞機(jī)制的多輪次選舉共識(shí)算法,其主要應(yīng)用在異步通信網(wǎng)絡(luò)和非拜占庭模型的分布式系統(tǒng)中。假設(shè)在分布式系統(tǒng)中有2F+1個(gè)節(jié)點(diǎn),盡管會(huì)有部分服務(wù)器發(fā)生故障或者網(wǎng)絡(luò)消息的延遲等通信問題,都不會(huì)影響整個(gè)系統(tǒng)的正常運(yùn)行,只要保證分布式系統(tǒng)中F+1個(gè)節(jié)點(diǎn)能夠正常地互相通信,18
本文編號(hào):3384543
【文章來源】:華東師范大學(xué)上海市 211工程院校 985工程院校 教育部直屬院校
【文章頁(yè)數(shù)】:82 頁(yè)
【學(xué)位級(jí)別】:碩士
【部分圖文】:
副本復(fù)制技術(shù)原理
第二章分布式共識(shí)與PAXOS華東師范大學(xué)碩士學(xué)位論文(1)A:表示可用性(Availability),即系統(tǒng)中每個(gè)成功或失敗的請(qǐng)求保證都會(huì)有對(duì)應(yīng)的響應(yīng)。(2)P:表示分區(qū)容忍性(ToleranceofNetworkPartition),即系統(tǒng)中的信息可以在傳遞時(shí)可以發(fā)送丟失或者發(fā)送不成功,這種情況不會(huì)對(duì)系統(tǒng)的運(yùn)行產(chǎn)生影響。(3)C:表示一致性(Consistency),即在同一時(shí)間系統(tǒng)全部的服務(wù)器節(jié)點(diǎn)數(shù)據(jù)是相同的。圖2.2:CAP定理由上可知,在一個(gè)分布式系統(tǒng)中可用性、分區(qū)容忍性、一致性不可能同時(shí)滿足規(guī)定需求,而且分布式系統(tǒng)的各個(gè)服務(wù)組件必然會(huì)被部署到不同的數(shù)據(jù)節(jié)點(diǎn),導(dǎo)致必然會(huì)出現(xiàn)各種集群以及子網(wǎng)絡(luò),因此P是所有分布式系統(tǒng)的最基本的需求。所以在實(shí)際應(yīng)用中分布式系統(tǒng)都只能根據(jù)自身的特定需求和應(yīng)用場(chǎng)景在一致性和可用性之間取舍。13
第二章分布式共識(shí)與PAXOS華東師范大學(xué)碩士學(xué)位論文案內(nèi)容value。此階段消息被稱作是Accept請(qǐng)求消息。Phase2.2.Accepted響應(yīng)階段。如果Acceptor接收到了提案編號(hào)為行的Accept消息,且在此之前其沒有響應(yīng)過具有比提案編號(hào)更大的消息,那么Acceptor接受這個(gè)Accept請(qǐng)求消息,即接受這個(gè)提案編號(hào)N對(duì)應(yīng)的提案。此階段消息被稱作是Accepted響應(yīng)消息。圖2.3:BasicPaxos兩階段消息流在Proposer收到多數(shù)派Acceptor的Accepted響應(yīng)消息之后,此次提案就通過了,分布式系統(tǒng)中的Learner就可以學(xué)習(xí)該提案的提案內(nèi)容。Paxos實(shí)例在達(dá)成共識(shí)過程中,每個(gè)階段的消息傳遞情況如圖2.3所示。上述兩階段是理想情況下的BasicPasic算法的消息傳遞流程,但是在實(shí)際分布式系統(tǒng)中會(huì)比較復(fù)雜。在提案表決的過程中,由于多個(gè)Proposer可能并發(fā)運(yùn)行發(fā)起不同的提案決議,或者由于其他物理原因(消息傳遞超時(shí)、物理機(jī)宕機(jī)等),導(dǎo)致沒有任何一個(gè)Ppoposer收到多數(shù)派Acceptor的應(yīng)答消息,那么就需要選取一個(gè)更大的提案編號(hào)進(jìn)行下一輪的提案決議,所以BasicPaxos是一個(gè)多輪次的基于消息傳遞的共識(shí)算法。2.2.5BasicPaxos總結(jié)綜上所述,BasicPaxos是基于消息傳遞機(jī)制的多輪次選舉共識(shí)算法,其主要應(yīng)用在異步通信網(wǎng)絡(luò)和非拜占庭模型的分布式系統(tǒng)中。假設(shè)在分布式系統(tǒng)中有2F+1個(gè)節(jié)點(diǎn),盡管會(huì)有部分服務(wù)器發(fā)生故障或者網(wǎng)絡(luò)消息的延遲等通信問題,都不會(huì)影響整個(gè)系統(tǒng)的正常運(yùn)行,只要保證分布式系統(tǒng)中F+1個(gè)節(jié)點(diǎn)能夠正常地互相通信,18
本文編號(hào):3384543
本文鏈接:http://sikaile.net/guanlilunwen/ydhl/3384543.html
最近更新
教材專著