[specs][doc] FizzBee spec for the Venice's LeaderFollower protocol #958
Conversation
This is a literal transilation of TLA+ syntax to FizzBee syntax.
|
Looks great! Could I also trouble you to include a readme file with the PR for how to run the spec/install fizz? |
|
Sure. Added the README file pointing to the instructions at. https://github.com/fizzbee-io/fizzbee At present, there is no precompiled binary, I have the full instructions to compile from source that I have tested in MacBook and Ubuntu on EC2. |
There was a problem hiding this comment.
Thanks for sharing this! It is my first time reading FizzBee (and I am not that familiar with TLA+ either, so please bear with me...). I left a few comments, some of which may be for Zac, others which may be about how to model a given situation in FizzBee itself... I'd be interested to hear your thoughts on these. Thanks again!
1. Maintain a bool variable newly_promoted to indicate a new leader who has not caught up on previous version topics. 2. Continue to update vtOffset and rtOffset for each node irrespective of whether the node is a leader or follower. 3. Make the leader and follower consumption serial instead of atomic - The leader will first post to version_topic, then, update the local datastore, then update the offsets - Similarly, the follower will first update its local datastore and then update the offsets. The system can crash at either of these points, and the design is verified to work even if the system crashes in between
|
@FelixGV @ZacAttack I have made the changes you asked for in this commit: c721c5e Please take a look and let me know. |
Summary, imperative, start upper case, don't end with a period
FizzBee spec for the Venice's LeaderFollower protocol, a one-to-one translation from the TLA+ syntax to the FizzBee syntax.
How was this PR tested?
Manually run it with the fizz model checker.
Does this PR introduce any user-facing changes?