Skip to content

Specifying and Verifying the consensus algorithm in PaxosStore using TLA+

License

Notifications You must be signed in to change notification settings

Starydark/PaxosStore-tla

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

38 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Paxosstore-tla

A project of using TLA+ to model check and prove the correctness of the consensus algorithm in the PaxosStore@VLDB2017 paper and the open-source Tencent/paxosstore.

Specification

While constructing specification of the consensus algorithm TPaxos in PaxosStore, we uncover a crucial but sutble detail in TPaxos which is not fully clarified, called TPaxosAP. We verify the correctness of both TPaxos and TPaxosAP, and establish the refinement mappings from TPaxos to Voting and from TPaxosAP to EagerVoting(equivalent to Voting).

Module

  • TPaxos.tla: the specification of the 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.

Refinement relation

RefinementRelation

We prove the correctness of TPaxos using TLAPS(a internal proof system of TLA+). While writing the proof of TPaxos, we make some small changes on the specification which won't introduce additional rules but only made our proof not too complicated.

Experiment

We prove the refinement relation using the method of model checking. The details refers to experiment.

Others

PS. here is a similar work that provides a framework to specify and verify CRDT Protocols using TLA+.

About

Specifying and Verifying the consensus algorithm in PaxosStore using TLA+

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published