You are viewing a plain text version of this content. The canonical link for it is here.
Posted to notifications@zookeeper.apache.org by GitBox <gi...@apache.org> on 2021/08/31 15:51:21 UTC
[GitHub] [zookeeper] Vanlightly commented on a change in pull request #1690: ZOOKEEPER-3615: Provide formal specification and verification using TLA+ for Zab
Vanlightly commented on a change in pull request #1690:
URL: https://github.com/apache/zookeeper/pull/1690#discussion_r699459102
##########
File path: zookeeper-specifications/zab-1.0/FastLeaderElection.tla
##########
@@ -0,0 +1,518 @@
+(*
+ * Licensed to the Apache Software Foundation (ASF) under one
+ * or more contributor license agreements. See the NOTICE file
+ * distributed with this work for additional information
+ * regarding copyright ownership. The ASF licenses this file
+ * to you under the Apache License, Version 2.0 (the
+ * "License"); you may not use this file except in compliance
+ * with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ *)
+------------------------- MODULE FastLeaderElection -------------------------
+\* This is the formal specification for Fast Leader Election in Zab protocol.
+(* Reference:
+ FastLeaderElection.java, Vote.java, QuorumPeer.java in https://github.com/apache/zookeeper.
+ Medeiros A. ZooKeeper��s atomic broadcast protocol: Theory and practice[J]. Aalto University School of Science, 2012.
+*)
+EXTENDS Integers, FiniteSets, Sequences, Naturals, TLC
+
+-----------------------------------------------------------------------------
+\* The set of server identifiers
+CONSTANT Server
+
+\* Server states
+CONSTANTS LOOKING, FOLLOWING, LEADING
+
+\* Message types
+CONSTANTS NOTIFICATION
+
+\* Timeout signal
+CONSTANT NONE
+-----------------------------------------------------------------------------
+Quorums == {Q \in SUBSET Server: Cardinality(Q)*2 > Cardinality(Server)}
+
+NullPoint == CHOOSE p: p \notin Server
+
+-----------------------------------------------------------------------------
+\* Server's state(LOOKING, FOLLOWING, LEADING).
+VARIABLE state
+
+\* The epoch number of the last NEWLEADER packet accepted, used for comparing.
+VARIABLE currentEpoch
+
+\* The zxid of the last transaction in history.
+VARIABLE lastZxid
+
+\* currentVote[i]: The server who i thinks is the current leader(id,zxid,peerEpoch,...).
+VARIABLE currentVote
+
+\* Election instance.(logicalClock in code)
+VARIABLE logicalClock
+
+\* The votes from the current leader election are stored in ReceiveVotes.
+VARIABLE receiveVotes
+
+(* The votes from previous leader elections, as well as the votes from the current leader election are
+ stored in outofelection. Note that notifications in a LOOKING state are not stored in outofelection.
+ Only FOLLOWING or LEADING notifications are stored in outofelection. *)
+VARIABLE outOfElection
+
+\* recvQueue[i]: The queue of received notifications or timeout signals in server i.
+VARIABLE recvQueue
+
+\* A veriable to wait for new notifications, corresponding to line 1050 in FastLeaderElection.java.
+VARIABLE waitNotmsg
+
+\* leadingVoteSet[i]: The set of voters that follow i.
+VARIABLE leadingVoteSet
+
+(* The messages about election sent from one server to another.
+ electionMsgs[i][j] means the input buffer of server j from server i. *)
+VARIABLE electionMsgs
+
+\* Set used for mapping Server to Integers, to compare ids from different servers.
+VARIABLE idTable
+
+serverVars == <<state, currentEpoch, lastZxid>>
+
+electionVars == <<currentVote, logicalClock, receiveVotes, outOfElection, recvQueue, waitNotmsg>>
+
+leaderVars == <<leadingVoteSet>>
+
+varsL == <<serverVars, electionVars, leaderVars, electionMsgs, idTable>>
+-----------------------------------------------------------------------------
+\* Processing of electionMsgs
+BroadcastNotmsg(i, m) == electionMsgs' = [electionMsgs EXCEPT ![i] = [v \in Server |-> IF v /= i
+ THEN Append(electionMsgs[i][v], m)
+ ELSE electionMsgs[i][v]]]
+
+DiscardNotmsg(i, j) == electionMsgs' = [electionMsgs EXCEPT ![i][j] = IF electionMsgs[i][j] /= << >>
+ THEN Tail(electionMsgs[i][j])
+ ELSE << >>]
+
+ReplyNotmsg(i, j, m) == electionMsgs' = [electionMsgs EXCEPT ![i][j] = Append(electionMsgs[i][j], m),
+ ![j][i] = Tail(electionMsgs[j][i])]
+
+-----------------------------------------------------------------------------
+\* Processing of recvQueue
+RECURSIVE RemoveNone(_)
+RemoveNone(seq) == CASE seq = << >> -> << >>
+ [] seq /= << >> -> IF Head(seq).mtype = NONE THEN RemoveNone(Tail(seq))
+ ELSE <<Head(seq)>> \o RemoveNone(Tail(seq))
+
+\* Processing of idTable and order comparing
+RECURSIVE InitializeIdTable(_)
+InitializeIdTable(Remaining) == IF Remaining = {} THEN {}
+ ELSE LET chosen == CHOOSE i \in Remaining: TRUE
+ re == Remaining \ {chosen}
+ IN {<<chosen, Cardinality(Remaining)>>} \union InitializeIdTable(re)
+
+\* FALSE: id1 < id2; TRUE: id1 > id2
+IdCompare(id1,id2) == LET item1 == CHOOSE item \in idTable: item[1] = id1
+ item2 == CHOOSE item \in idTable: item[1] = id2
+ IN item1[2] > item2[2]
+
+\* FALSE: zxid1 <= zxid2; TRUE: zxid1 > zxid2
+ZxidCompare(zxid1, zxid2) == \/ zxid1[1] > zxid2[1]
+ \/ /\ zxid1[1] = zxid2[1]
+ /\ zxid1[2] > zxid2[2]
+
+ZxidEqual(zxid1, zxid2) == zxid1[1] = zxid2[1] /\ zxid1[2] = zxid2[2]
+
+\* FALSE: vote1 <= vote2; TRUE: vote1 > vote2
+TotalOrderPredicate(vote1, vote2) == \/ vote1.proposedEpoch > vote2.proposedEpoch
+ \/ /\ vote1.proposedEpoch = vote2.proposedEpoch
+ /\ \/ ZxidCompare(vote1.proposedZxid, vote2.proposedZxid)
+ \/ /\ ZxidEqual(vote1.proposedZxid, vote2.proposedZxid)
+ /\ IdCompare(vote1.proposedLeader, vote2.proposedLeader)
+
+VoteEqual(vote1, round1, vote2, round2) == /\ vote1.proposedLeader = vote2.proposedLeader
+ /\ ZxidEqual(vote1.proposedZxid, vote2.proposedZxid)
+ /\ vote1.proposedEpoch = vote2.proposedEpoch
+ /\ round1 = round2
+
+-----------------------------------------------------------------------------
+\* Processing of currentVote
+InitialVote == [proposedLeader |-> NullPoint,
+ proposedZxid |-> <<0, 0>>,
+ proposedEpoch |-> 0]
+
+SelfVote(i) == [proposedLeader |-> i,
+ proposedZxid |-> lastZxid[i],
+ proposedEpoch |-> currentEpoch[i]]
+
+UpdateProposal(i, nid, nzxid, nepoch) == currentVote' = [currentVote EXCEPT ![i].proposedLeader = nid, \* no need to record state in LOOKING
+ ![i].proposedZxid = nzxid,
+ ![i].proposedEpoch = nepoch]
+
+-----------------------------------------------------------------------------
+\* Processing of receiveVotes and outOfElection
+RvClear(i) == receiveVotes' = [receiveVotes EXCEPT ![i] = [v \in Server |-> [vote |-> InitialVote,
+ round |-> 0,
+ state |-> LOOKING,
+ version |-> 0]]]
+
+RvPut(i, id, mvote, mround, mstate) == receiveVotes' = CASE receiveVotes[i][id].round < mround -> [receiveVotes EXCEPT ![i][id].vote = mvote,
+ ![i][id].round = mround,
+ ![i][id].state = mstate,
+ ![i][id].version = 1]
+ [] receiveVotes[i][id].round = mround -> [receiveVotes EXCEPT ![i][id].vote = mvote,
+ ![i][id].state = mstate,
+ ![i][id].version = @ + 1]
+ [] receiveVotes[i][id].round > mround -> receiveVotes
+
+Put(i, id, rcvset, mvote, mround, mstate) == CASE rcvset[id].round < mround -> [rcvset EXCEPT ![id].vote = mvote,
+ ![id].round = mround,
+ ![id].state = mstate,
+ ![id].version = 1]
+ [] rcvset[id].round = mround -> [rcvset EXCEPT ![id].vote = mvote,
+ ![id].state = mstate,
+ ![id].version = @ + 1]
+ [] rcvset[id].round > mround -> rcvset
+
+RvClearAndPut(i, id, vote, round) == receiveVotes' = LET oneVote == [vote |-> vote,
+ round |-> round,
+ state |-> LOOKING,
+ version |-> 1]
+ IN [receiveVotes EXCEPT ![i] = [v \in Server |-> IF v = id THEN oneVote
+ ELSE [vote |-> InitialVote,
+ round |-> 0,
+ state |-> LOOKING,
+ version |-> 0]]]
+
+VoteSet(i, msource, rcvset, thisvote, thisround) == {msource} \union {s \in (Server \ {msource}): VoteEqual(rcvset[s].vote,
Review comment:
The argument i is not used in VoteSet body.
--
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