软件学报

作者：易星辰，魏恒峰，黄宇，乔磊，吕建

单位：易星辰，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002311,魏恒峰，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002302,黄宇，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002303,乔磊，北京控制工程研究所, 北京 10019004,吕建，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002305

关键词：Paxos;PaxosStore;共识协议;TLA+;精化关系;模型检验

基金：国家自然科学基金（61690204，61702253，61772258）

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

来源：2020年第8期

《软件学报》期刊编辑部

查看软件学报杂志2020年第8期