使用模型检测方法对Paxos算法进行验证与改进

Verification and Improvement of Paxos Algorithm Based on Model Checking

因通信的同步问题、网络分区的可靠性问题等,分布式系统难以在通信、分区等环节失效的情况下对特定的状态达成共识.Paxos是近年分布式系统中常见且有效的共识算法,本文通过使用模型检测的方法对Paxos算法进行形式化建模,分析和验证了Paxos作为共识算法所应当满足的性质,结果表明,Paxos算法满足安全性、活性,但执行过程中有发生活锁的可能,并通过模型检测器重现了算法发生活锁时的运行轨迹.最后通过对算法进行改进,以应对现有算法执行过程中可能出现的活锁问题,并通过了模型检测器的验证.

Due to the synchronization of communication and the reliability of network partition,it is difficult for distributed systems to reach a consensus on a specific state when the communication,partition,or others fail.Paxos is a common and effective consensus algorithm in distributed systems in recent years.This paper uses the method of model checking to formally model the Paxos algorithm,analyzes and verifies the properties that Paxos should satisfy as a consensus algorithm.The results show that Paxos algorithm meets the safetyand liveness,but it is possible to generate livelocks,the trace of livelock is reproduced by model checker.Finally,the algorithm is improved to deal with the livelock problem that may occur during the execution of thealgorithm,and it has passed the verification of the model checker.