starydark / paxosstore-tla

Specifying and Verifying the consensus algorithm in PaxosStore using TLA+

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

Theorem Proving

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

paxosstore-tla's Issues

书写并检验TPaxos的Liveness性质

借鉴 Lamport 已有的 TLA+ Spec for Paxos, 书写并检验 TPaxos 的 Livensss 性质。

在此过程中，更深入理解 Safety, Liveness, Fairness。

Quorum vs. All in `Accept`

Using "All" vs. "Quorum" in Accept(p, b, v) in UniversalPaxosStore.

See the error-trace: RefineEV-3P3B3V-Quorum-vs-All-ErrorTrace

Check the theorem.

Accept has not ever been enabled with model "2P2B2V" in UniversalPaxosStore

Module: UniversalPaxosStore
Model: 2P2B2V
Result: 9 diameter, 218 states, 37 distinct states

Problem: Accept has not ever been enabled

TODO:

• Confirm the model checking result
• Is it normal for "2P2B2V"? Find bugs or Explain it.

更大规模的模型检验实验

继续开始更大规模的模型检验实验

• Participant 数目 >= 5

利用 TLC Profile 工具识别性能瓶颈并尝试改进