Skip to content

TLA+ specifications related to Viewstamped Replication

License

Notifications You must be signed in to change notification settings

Vanlightly/vsr-tlaplus

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

20 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

vsr-tlaplus

TLA+ specifications related to Viewstamped Replication.

The following specifications exist:

  • Viewstamped Replication Revisited paper.
    • VSR.tla is based solely on the paper and does not implement any fixes to protocol defects from this paper.

State transfer defect

To reproduce the state transfer defect of the revisited paper, set the following constant values:

    ReplicaCount = 3
    ClientCount = 1
    Values = {v1, v2, v3}
    StartViewOnTimerLimit = 3

When running with model checking, ensure you have at least 500GB of disk available and a large number of cores, else you'll ever run out of disk or have to wait multiple days.

Alternatively, use simulation mode, which has a good chance of hitting it sooner.

About

TLA+ specifications related to Viewstamped Replication

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages