WIP: TLA+ specification of consensus protocol #1
Conversation
| \* Arrays are 1-indexed, while the % operator returns a number between 0 and NumParticipants. | ||
| \* This explains the following slightly complicated expression | ||
| mover(turnNumber) == 1 + ((turnNumber-1) % NumParticipants) | ||
| safeToSend(state) == |
There was a problem hiding this comment.
can we add some spacing here to it's clear that mover and safeToSend are different chunks of logic (methods?functions? not sure what they're called in TLA+)
ConsensusUpdate.tla
Outdated
| msg := NULL; | ||
| end macro; | ||
|
|
||
| macro voteOrreturnFailure(turnNumber, votesRequired) |
There was a problem hiding this comment.
| macro voteOrreturnFailure(turnNumber, votesRequired) | |
| macro voteOrReturnFailure(turnNumber, votesRequired) |
| either returnFailure(state.turnNumber) | ||
| or if msg.turnNumber > state.turnNumber then | ||
| \* First, update our state based on the incoming message | ||
| if msg.votesRequired = 0 then returnSuccess() |
There was a problem hiding this comment.
It might be clearer if returnSuccess was renamed to indicate it also "sends" a success message.
ConsensusUpdate.tla
Outdated
| mover(turnNumber) == 1 + ((turnNumber-1) % NumParticipants) | ||
| safeToSend(state) == | ||
| /\ state.type = Types.WAITING | ||
| /\ \/ state.ourIndex = state.turnNumber % NumParticipants |
There was a problem hiding this comment.
Should mover definition be used here?
| \* work this way | ||
| either returnFailure(state.turnNumber) | ||
| or if msg.turnNumber > state.turnNumber then | ||
| \* First, update our state based on the incoming message |
There was a problem hiding this comment.
A thought: should we strive to eliminate comments that explain code?
| (***************************************************************************) | ||
| fair process consensusUpdate \in DOMAIN Participants | ||
| variables | ||
| state = [ |
There was a problem hiding this comment.
why is msg defined at the start of the file as opposed to here?
There was a problem hiding this comment.
Good question! state is a variable that belongs to a process, while msg is a global variable that all processes have access to.
When translated, TLA+ does this by having state be a function whose domain is the set of labels used to label the processes. In this case, DOMAIN Participants are the labels of the processes, so the variable state referred to in the Pluscal specification corresponds to the variable state[p] in the TLA+ translation, where p is the index of the participant.
I'll add to the TLA+ primer
ConsensusUpdate.tla
Outdated
| ReachConsensus: | ||
| while Running(state) do | ||
| if safeToSend(state) /\ msg = NULL then | ||
| either returnFailure(state.turnNumber) \* If the commitment is not valid |
There was a problem hiding this comment.
If voteOrReturnFailure is used on line 143 below, is this line needed?
|
|
||
| \* Safety properties | ||
|
|
||
| TypeOK == |
There was a problem hiding this comment.
The "safety" and "liveness" properties can be checked in a "model" of the specification (a particular set of values for the constants). The TypeOK property, for instance, specifies what values the msg and state variables can be. (IE. it's a sort of type safety.)
No description provided.