PaxosStore中共识协议TPaxos的推导、规约与精化

发布时间：2021-04-08 10:30

　　PaxosStore是腾讯开发的高可用分布式存储系统,现已用于全面支持微信核心业务.PaxosStore实现了分布式共识协议Paxos的一种变体,称为TPaxos.TPaxos的新颖之处在于其"统一性":为每个参与者维护统一的状态类型,并采用统一格式的消息进行通信.然而,这种设计方案也带来了TPaxos与Paxos之间的诸多差异,给理解TPaxos造成了障碍.其次,虽然腾讯开源了TPaxos协议的核心代码（包括伪代码与C++代码）,但TPaxos仍缺少抽象而精确的形式化规约.最后,根据文献检索,TPaxos的正确性尚未经过必要的数学论证或者形式化工具的检验.针对这些情况,有3个主要贡献:首先,从经典的Paxos协议出发,论证如何逐步推导出TPaxos协议.基于这种推导,可以将TPaxos看作Paxos的一种自然变体,更易于理解.其次,给出了TPaxos协议的TLA+形式化规约.在开发规约的时候发现,TPaxos协议描述中存在至关重要但并未充分阐明的微妙之处:在消息处理阶段,参与者（作为接受者角色）是先作出"不再接受具有更小编号的提议"的承诺（promise）,还是先接受（accept）... 

【文章来源】：软件学报. 2020,31(08)北大核心EICSCD

【文章页数】：26 页

【参考文献】：
期刊论文
[1]类Paxos共识算法研究进展[J]. 王江,章明星,武永卫,陈康,郑纬民.  计算机研究与发展. 2019(04)



本文编号：3125383