diff --git a/safekeeper/spec/readme.md b/safekeeper/spec/readme.md index 3d0a04fefa..ec2649d87d 100644 --- a/safekeeper/spec/readme.md +++ b/safekeeper/spec/readme.md @@ -1,3 +1,8 @@ +The specifications, models and results of running of them of the compute <-> +safekeepers consensus algorithm for committing WAL on the fleet of safekeepers. +Following Paxos parlance, compute which writes WAL is called (WAL) proposer here +and safekeepers which persist it are called (WAL) acceptors. + Directory structure: - Use modelcheck.sh to run TLC. - MC*.tla contains bits of TLA+ needed for TLC like constraining the state space, and models/ actual models.