主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第5期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
易星辰,魏恒峰,黄宇,乔磊,吕建.PaxosStore中共识算法TPaxos的推导、规约与精化.软件学报,2020,31(8):0
PaxosStore中共识算法TPaxos的推导、规约与精化
TPaxos in PaxosStore: Derivation, Specification, and Refinement
投稿时间:2019-09-09  修订日期:2019-11-02
DOI:10.13328/j.cnki.jos.005964
中文关键词:  Paxos  PaxosStore  共识算法  TLA+  精化关系  模型检验
英文关键词:Paxos  PaxosStore  consensus protocols  TLA+  refinement mapping  model checking
基金项目:国家自然科学基金(61690204,61702253,61772258)
作者单位E-mail
易星辰 计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023  
魏恒峰 计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023 hfwei@nju.edu.cn 
黄宇 计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023  
乔磊 北京控制工程研究所, 北京 100190  
吕建 计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023  
摘要点击次数: 270
全文下载次数: 330
中文摘要:
      PaxosStore是腾讯开发的高可用分布式存储系统,现已用于全面支持微信核心业务.PaxosStore实现了分布式共识协议Paxos的一种变体,我们称之为TPaxos.TPaxos的新颖之处在于它的"统一性":它为每个参与者维护统一的状态类型,并采用统一格式的消息进行通信.然而,这种设计方案也带来了TPaxos与Paxos之间的诸多差异,给理解TPaxos造成了障碍.其次,虽然腾讯开源了TPaxos协议的核心代码(包括伪代码与C++代码),TPaxos仍缺少抽象而精确的形式化规约.最后,就我们所知,TPaxos的正确性尚未经过必要的数学论证或者形式化工具的检验.针对这些情况,本文有三个主要贡献.首先,我们从经典的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. We call it TPaxos in this paper. The originality of TPaxos lies in its "uniformity":it maintains for each participant a unified state type 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 we know, TPaxos has not yet been manually proven or formally checked. To address these issues, we make three main contributions in this paper. First, we demonstrate 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, we describe TPaxos in TLA+, a formal specification language. In the course of developing the TLA+ specification for TPaxos, we uncover a crucial but subtle detail in TPaxos which is not fully clarified: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 us to propose a variant of TPaxos, called TPaxosAP. In TPaxosAP, the participants accept proposals first and then make promise. Third, we verify the correctness of both TPaxos and TPaxosAP by refinement. Particularly, since the known voting mechanism called Voting cannot capture all the behaviors of TPaxosAP, we first propose EagerVoting for TPaxosAP and then establish the refinement mappings from TPaxosAP to EagerVoting and from EagerVoting to Consensus. We also verify them using the TLC model checker.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利