-
Notifications
You must be signed in to change notification settings - Fork 25
Zen with terms #30
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Zen with terms #30
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I left a handful of thoughts about names, but the rest looks good.
ZenWithTerms/tla/ZenWithTerms.tla
Outdated
VARIABLE joinVotes | ||
VARIABLE allowElection | ||
VARIABLE electionWon | ||
VARIABLE publishVersion |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I wonder whether lastPublishedVersion
would be a better name, in parallel with lastPublishedConfiguration
?
ZenWithTerms/tla/ZenWithTerms.tla
Outdated
|
||
\* node state (map from node id to state) | ||
VARIABLE currentTerm | ||
VARIABLE currentConfiguration \* committed config |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How about lastCommittedConfiguration
, given the comment?
ZenWithTerms/tla/ZenWithTerms.tla
Outdated
VARIABLE lastAcceptedValue | ||
VARIABLE lastAcceptedConfiguration | ||
VARIABLE joinVotes | ||
VARIABLE allowElection |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Perhaps startedJoinSinceLastReboot
?
Makes sense. Thanks @DaveCTurner |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM Thanks @ywelsch
This is an alternative specification to https://github.com/elastic/elasticsearch-formal-models/blob/master/cluster/tla/consensus.tla that resembles existing Zen more closely in that it does not require force-publishing the last accepted value upon election, but limits this only to the configuration.