基于Coq的Paxos的形式化建模与验证

发布时间：2021-09-05 03:02

　　随着互联网的迅速发展和普及,网络数据流量越来愈庞大。企业信息化程度的不断加强,导致大量的数据亟待处理,数据已成为各类企业的命脉。传统的应用服务使用单一服务器模式,但是由于网络环境的不稳定,服务器容易发生数据丢失、节点宕机,严重影响了系统的可用性。在单机服务逐渐不能满足企业数据处理的需求情况下,人们开始搭建服务器集群的分布式系统。副本复制技术提高分布式系统的可靠性,在网络负载较大的情况下实现负载均衡,缓解服务器的压力。但是副本复制技术的引入,也带来了副本数据一致性等问题。为了保证系统的高可用性和一致性,就需要使用分布式一致性算法,Paxos算法便是其中非常重要的一类。共识问题是指分布式系统中一组参与者就一个结果达成一致的过程。Paxos能够很好的解决共识问题,越来越多的研究者将重点放在对算法本身的优化或者具体工程实现,Paxos在大型分布式系统得到了广泛的运用,比如区块链系统以及谷歌文件系统等。虽然Paxos的工程实现越来越多,但是关于算法安全性的形式化工作却很少,为了增强研究者和企业对Paxos的应用信息,其安全性证明越来越重要。所以,本文在定理证明工具Coq中形式化描述和定义了Lam... 

【文章来源】：华东师范大学上海市 211工程院校 985工程院校 教育部直属院校

【文章页数】：82 页

【学位级别】：硕士

【部分图文】：

副本复制技术原理

第二章分布式共识与PAXOS华东师范大学硕士学位论文（1）A：表示可用性（Availability），即系统中每个成功或失败的请求保证都会有对应的响应。（2）P：表示分区容忍性（ToleranceofNetworkPartition），即系统中的信息可以在传递时可以发送丢失或者发送不成功，这种情况不会对系统的运行产生影响。（3）C：表示一致性（Consistency），即在同一时间系统全部的服务器节点数据是相同的。图2.2:CAP定理由上可知，在一个分布式系统中可用性、分区容忍性、一致性不可能同时满足规定需求，而且分布式系统的各个服务组件必然会被部署到不同的数据节点，导致必然会出现各种集群以及子网络，因此P是所有分布式系统的最基本的需求。所以在实际应用中分布式系统都只能根据自身的特定需求和应用场景在一致性和可用性之间取舍。13

第二章分布式共识与PAXOS华东师范大学硕士学位论文案内容value。此阶段消息被称作是Accept请求消息。Phase2.2．Accepted响应阶段。如果Acceptor接收到了提案编号为行的Accept消息，且在此之前其没有响应过具有比提案编号更大的消息，那么Acceptor接受这个Accept请求消息，即接受这个提案编号N对应的提案。此阶段消息被称作是Accepted响应消息。图2.3:BasicPaxos两阶段消息流在Proposer收到多数派Acceptor的Accepted响应消息之后，此次提案就通过了，分布式系统中的Learner就可以学习该提案的提案内容。Paxos实例在达成共识过程中，每个阶段的消息传递情况如图2.3所示。上述两阶段是理想情况下的BasicPasic算法的消息传递流程，但是在实际分布式系统中会比较复杂。在提案表决的过程中，由于多个Proposer可能并发运行发起不同的提案决议，或者由于其他物理原因（消息传递超时、物理机宕机等），导致没有任何一个Ppoposer收到多数派Acceptor的应答消息，那么就需要选取一个更大的提案编号进行下一轮的提案决议，所以BasicPaxos是一个多轮次的基于消息传递的共识算法。2.2.5BasicPaxos总结综上所述，BasicPaxos是基于消息传递机制的多轮次选举共识算法，其主要应用在异步通信网络和非拜占庭模型的分布式系统中。假设在分布式系统中有2F+1个节点，尽管会有部分服务器发生故障或者网络消息的延迟等通信问题，都不会影响整个系统的正常运行，只要保证分布式系统中F+1个节点能够正常地互相通信，18


本文编号：3384543