A project of using TLA+ to model the consensus algorithm in the paper PaxosStore@VLDB2017 and the open-source Tencent/paxosstore.
TPaxos(the consensus algorithm above) is a variant of basic Paxos, and we uncover a crucial but sutble detail in TPaxos which is not fully clarified, called TPaxosAP. We establish refinement mapping from TPaxos to Voting and from TPaxosAP to EagerVoting(equivalent to Voting) to verify the correctness of TPaxos and TPaxosAP, Voting is a high-level spec in paper Byzantizing Paxos by Refinement.
- TPaxos.tla: the specification of TPaxos.
- TPaxosAP.tla: the specification of the variant of TPaxos.
- TPaxosWithVotes.tla: the refinement mapping of TPaxos refining Voting.
- TPaxosAPWithVotes.tla: the refinement mapping of TPaxosAP refining EagerVoting.
- EagerVoting.tla: a specification that is equivalent to Voting.
- Voting.tla: a specification introduced by Lamport in paper Byzantizing Paxos by Refinement.
- Consensus.tla: a specification that implemented by Voting.
There are three experiments we have made:
- TPaxos and TPaxosAP satisfy Consistency.
- TPaxos refines Voting, TPaxosAP refines EagerVoting.
- EagerVoting refines Consensus.
- Participant(Symmetry set): the set of all servers. e.g. {p1, p2, p3}
- Value(Symmetry Set): the set of all value. e.g. {v1, v2}
- Ballot(Redefine Nat): the set of ballot numbers. e.g. 0..2 or other bigger set
- Consistency: Invariant in model checking TPaxos and TPaxosAP satisfying Consistency.
- SpecV => V!Spec: Properties in model checking refinement mapping.