PaxosStore中共识协议TPaxos的推导、规约与精化
作者:
作者单位:

作者简介:

易星辰(1996-),男,硕士生,主要研究领域为分布数据一致性,形式化方法;乔磊(1982-),男,博士,研究员,CCF专业会员,主要研究领域为航天器嵌入式操作系统设计及验证;魏恒峰(1986-),男,博士,CCF专业会员,主要研究领域为分布数据一致性,形式化方法;吕建(1960-),男,博士,教授,博士生导师,CCF会士,主要研究领域为软件方法学;黄宇(1982-),男,博士,教授,博士生导师,CCF专业会员,主要研究领域为分布式算法,分布式系统,网络化软件系统.

通讯作者:

魏恒峰,E-mail:hfwei@nju.edu.cn

中图分类号:

基金项目:

国家自然科学基金(61690204,61702253,61772258)


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

Fund Project:

National Natural Science Foundation of China (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模型检验工具验证了它们的正确性.

    Abstract:

    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 checker.

    参考文献
    相似文献
    引证文献
引用本文

易星辰,魏恒峰,黄宇,乔磊,吕建. PaxosStore中共识协议TPaxos的推导、规约与精化.软件学报,2020,31(8):2336-2361

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2019-08-31
  • 最后修改日期:2019-11-02
  • 录用日期:
  • 在线发布日期: 2020-04-20
  • 出版日期: 2020-08-06
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号