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

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