[GitHub] [zookeeper] Vanlightly commented on pull request #1690: ZOOKEEPER-3615: Provide formal specification and verification using TLA+ for Zab

[GitBox <gi...@apache.org>]

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: notifications-unsubscribe@zookeeper.apache.org

For queries about this service, please contact Infrastructure at:
users@infra.apache.org