TPaxos In PaxosStore:Specification,Refinement,and Theorem Proving

To achieve high system availability and fault tolerance,distributed data storage systems usually adopt the data replication technology,replicating multiple copies of the same data at multiple replicas.However,data replication introduces the data consistency problem.The distributed consensus protocols can address this problem by providing strong data consistency between multiple replicas.Paxos is a classic distributed consensus protocol,and it has been widely used in distributed systems that require strong consistency,including Google's distributed lock service system(Chubby),Microsoft's automated data center management system(Autopilot),Alibaba's enterprise database(OceanBase),etc.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 construct the TPaxos protocol and not only describe its relationship with Paxos,but also prove its correctness rigorously,including the following four main contributions.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 establish refinement mappings between the Paxos variants.For TPaxos,we still use the Voting mechanism used by Paxos to establish a refinement mapping from TPaxos to Voting.Particularly,since Voting cannot capture all the behaviors of TPaxosAP,we propose a new voting mechanism,called EagerVoting.We also demonstrate the equivalence between EagerVoting and Voting by refinement.The Voting and EagerVoting mechanisms precisely characterize the differences and similarities among Paxos,TPaxos,and TPaxosAP.Finally,we use TLAPS(TLA+Proof System)to rigorously prove the correctness of TPaxos and TPaxosAP,based on the existing proof framework for Paxos.