paxosstore-tla

TLA+ model checking and TLAPS theorem proving for the Paxos implementation in PaxosStore by WeChat

See the PaxosStore@VLDB2017 paper and the open-source Tencent/paxosstore.

Name		Name	Last commit message	Last commit date
Latest commit History 10 Commits
EagerVoting.tlaps		EagerVoting.tlaps
EagerVoting.toolbox		EagerVoting.toolbox
EagerVotingL.toolbox		EagerVotingL.toolbox
OneVaulePerBallotPaxosStore.toolbox		OneVaulePerBallotPaxosStore.toolbox
OneVotePaxosStore.toolbox		OneVotePaxosStore.toolbox
PaxosStore.toolbox		PaxosStore.toolbox
UniversalPaxosStore.toolbox		UniversalPaxosStore.toolbox
UniversalPaxosStoreWithVotes.tlaps		UniversalPaxosStoreWithVotes.tlaps
UniversalPaxosStoreWithVotes.toolbox		UniversalPaxosStoreWithVotes.toolbox
paxosstore-tencent		paxosstore-tencent
.gitignore		.gitignore
Consensus.pdf		Consensus.pdf
Consensus.tla		Consensus.tla
EagerVoting.pdf		EagerVoting.pdf
EagerVoting.tla		EagerVoting.tla
EagerVotingL.pdf		EagerVotingL.pdf
EagerVotingL.tla		EagerVotingL.tla
LICENSE		LICENSE
OneVaulePerBallotPaxosStore.pdf		OneVaulePerBallotPaxosStore.pdf
OneVaulePerBallotPaxosStore.tla		OneVaulePerBallotPaxosStore.tla
OneVotePaxosStore-Accept-ErrorTrace.md		OneVotePaxosStore-Accept-ErrorTrace.md
OneVotePaxosStore.pdf		OneVotePaxosStore.pdf
OneVotePaxosStore.tla		OneVotePaxosStore.tla
PaxosStore.pdf		PaxosStore.pdf
PaxosStore.tla		PaxosStore.tla
README.md		README.md
RefineEV-3P3B3V-Quorum-vs-All-ErrorTrace.md		RefineEV-3P3B3V-Quorum-vs-All-ErrorTrace.md
Sets.tla		Sets.tla
UniversalPaxosStore.pdf		UniversalPaxosStore.pdf
UniversalPaxosStore.tla		UniversalPaxosStore.tla
UniversalPaxosStoreWithVotes.pdf		UniversalPaxosStoreWithVotes.pdf
UniversalPaxosStoreWithVotes.tla		UniversalPaxosStoreWithVotes.tla
Voting.pdf		Voting.pdf
Voting.tla		Voting.tla

License

hengxin/paxosstore-tla

Folders and files

Latest commit

History

Repository files navigation

paxosstore-tla

About

Topics

Resources

License

Stars

Watchers

Forks

Languages