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

TPaxos Consensus Protocol in PaxosStore:Derivation,Specification,and Refinement

作　　者：易星辰 魏恒峰 黄宇[1] 乔磊[2] 吕建[1] YI Xing-Chen;WEI Heng-Feng;HUANG Yu;QIAO Lei;LÜ Jian(State Key Laboratory for Novel Software Technology(Nanjing University),Nanjing 210023,China;Beijing Institute of Control Engineering,Beijing 100190,China)

机构地区：[1]计算机软件新技术国家重点实验室(南京大学),江苏南京210023 [2]北京控制工程研究所,北京100190

出　　处：《软件学报》2020年第8期2336-2361,共26页Journal of Software

基　　金：国家自然科学基金(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模型检验工具验证了它们的正确性.PaxosStore is a highly available distributed storage system developed by Tencent Inc.to support the comprehensive business of WeChat.PaxosStore employs a variant of Paxos which is a classic protocol for solving distributed consensus.It is called as TPaxos in this study.The originality of TPaxos lies in its“uniformity”:it maintains a unified state type for each participant and adopts a universal message format for communication.However,this design choice brings various differences between TPaxos and Paxos,rendering TPaxos hard to understand.Moreover,although the core code(including both pseudocode and source code in C++)for TPaxos is publicly available,there still lacks a formal specification of TPaxos.Finally,as far as literature demonstrates,TPaxos has not yet been manually proven or formally checked.To address these issues,three main contributions are expounded in this paper.First,it is demonstrated that how to derive TPaxos from classic Paxos step by step.Based on this derivation,TPaxos can be regarded as a natural variant of Paxos and is much easier to understand.Second,TPaxos in TLA+,a formal specification language,is described.In the course of developing the TLA+specification for TPaxos,a crucial but subtle detail is uncovered in TPaxos which is not fully clarified.That is,upon messages,do the participants(as acceptors)make promise that no proposals with smaller proposal numbers will be accepted before accepting proposals or vice versa?This leads to two different interpretations of TPaxos and motivates authors to propose a variant of TPaxos,called TPaxosAP.In TPaxosAP,the participants accept proposals first,and then make promise.Third,the correctness of both TPaxos and TPaxosAP is verified by refinement.Particularly,since the known voting mechanism called Voting cannot capture all the behaviors of TPaxosAP,EagerVoting for TPaxosAP is first proposed and then the refinement mappings are established from TPaxosAP to EagerVoting and from EagerVoting to consensus.They are also verified using the TLC model ch

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

分 类 号：TP316[自动化与计算机技术—计算机软件与理论]