Vanlightly commented on pull request #1690:
URL: https://github.com/apache/zookeeper/pull/1690#issuecomment-909366826
I have started looking at the new version. One thing I have done is add a
TypeOK invariant checking that the types of all variables are correct in all
states. This helps me understand the spec better as it acts as a reference for
what the different variables hold but can also be useful for catching type
errors. I have it running with simulation for a few hours so far with no
violations.
Here's the TypeOK:
```
ServersIncNullPoint == Server \union {NullPoint}
Zxid ==
Seq(Nat)
HistoryItem ==
[epoch: Nat,
counter: Nat,
value: Value]
Proposal ==
[msource: Server, mtype: {"RECOVERYSYNC"}, mepoch: Nat, mproposals:
Seq(HistoryItem)] \union
[msource: Server, mtype: {PROPOSAL}, mepoch: Nat, mproposal:
HistoryItem]
Message ==
[mtype: {FOLLOWERINFO}, mepoch: Nat] \union
[mtype: {NEWLEADER}, mepoch: Nat, mlastZxid: Zxid] \union
[mtype: {ACKLD}, mepoch: Nat] \union
[mtype: {LEADERINFO}, mepoch: Nat] \union
[mtype: {ACKEPOCH}, mepoch: Nat, mlastEpoch: Nat, mlastZxid: Zxid] \union
[mtype: {UPTODATE}, mepoch: Nat, mcommit: Nat] \union
[mtype: {PROPOSAL}, mepoch: Nat, mproposal: HistoryItem] \union
[mtype: {ACK}, mepoch: Nat, mzxid: Zxid] \union
[mtype: {COMMIT}, mepoch: Nat, mzxid: Zxid]
ElectionState == {LOOKING, FOLLOWING, LEADING}
Vote ==
[proposedLeader: ServersIncNullPoint,
proposedZxid: Zxid,
proposedEpoch: Nat]
ElectionVote ==
[vote: Vote, round: Nat, state: ElectionState, version: Nat]
ElectionMsg ==
[mtype: {NOTIFICATION}, msource: Server, mstate: ElectionState, mround:
Nat, mvote: Vote] \union
[mtype: {NONE}]
TypeOK ==
/\ zabState \in [Server -> {ELECTION, DISCOVERY, SYNCHRONIZATION,
BROADCAST}]
/\ acceptedEpoch \in [Server -> Nat]
/\ history \in [Server -> Seq(HistoryItem)]
/\ commitIndex \in [Server -> Nat]
/\ learners \in [Server -> SUBSET ServersIncNullPoint]
/\ cepochRecv \in [Server -> SUBSET ServersIncNullPoint]
/\ ackeRecv \in [Server -> SUBSET ServersIncNullPoint]
/\ ackldRecv \in [Server -> SUBSET ServersIncNullPoint]
/\ ackIndex \in [Server -> [Server -> Nat]]
/\ currentCounter \in [Server -> Nat]
/\ sendCounter \in [Server -> Nat]
/\ committedIndex \in [Server -> Nat]
/\ committedCounter \in [Server -> [Server -> Nat]]
/\ forwarding \in [Server -> SUBSET ServersIncNullPoint]
/\ initialHistory \in [Server -> Seq(HistoryItem)]
/\ tempMaxEpoch \in [Server -> Nat]
/\ cepochSent \in [Server -> BOOLEAN]
/\ leaderAddr \in [Server -> ServersIncNullPoint]
/\ synced \in [Server -> BOOLEAN]
/\ proposalMsgsLog \in SUBSET Proposal
/\ epochLeader \in [1..MAXEPOCH -> SUBSET ServersIncNullPoint]
/\ inherentViolated \in BOOLEAN
/\ forwarding \in [Server -> SUBSET Server]
/\ msgs \in [Server -> [Server -> Seq(Message)]]
\* Fast Leader Election
/\ electionMsgs \in [Server -> [Server -> Seq(ElectionMsg)]]
/\ recvQueue \in [Server -> Seq(ElectionMsg)]
/\ leadingVoteSet \in [Server -> SUBSET Server]
/\ receiveVotes \in [Server -> [Server -> ElectionVote]]
/\ currentVote \in [Server -> Vote]
/\ outOfElection \in [Server -> [Server -> ElectionVote]]
/\ lastZxid \in [Server -> Zxid]
/\ state \in [Server -> ElectionState]
/\ waitNotmsg \in [Server -> BOOLEAN]
/\ currentEpoch \in [Server -> Nat]
/\ logicalClock \in [Server -> Nat]
```
I still need to dig into the logic further so I understand it and check it
against ZK code.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: [email protected]
For queries about this service, please contact Infrastructure at:
[email protected]
