From notifications-return-9557-archive-asf-public=cust-asf.ponee.io@zookeeper.apache.org Wed Sep 1 09:43:35 2021 Return-Path: X-Original-To: archive-asf-public@cust-asf.ponee.io Delivered-To: archive-asf-public@cust-asf.ponee.io Received: from mxout1-ec2-va.apache.org (mxout1-ec2-va.apache.org [3.227.148.255]) by mx-eu-01.ponee.io (Postfix) with ESMTPS id C10CD18068A for ; Wed, 1 Sep 2021 11:43:35 +0200 (CEST) Received: from mail.apache.org (mailroute1-lw-us.apache.org [207.244.88.153]) by mxout1-ec2-va.apache.org (ASF Mail Server at mxout1-ec2-va.apache.org) with SMTP id 98428445E7 for ; Wed, 1 Sep 2021 09:42:30 +0000 (UTC) Received: (qmail 78633 invoked by uid 500); 1 Sep 2021 09:42:30 -0000 Mailing-List: contact notifications-help@zookeeper.apache.org; run by ezmlm Precedence: bulk List-Help: List-Unsubscribe: List-Post: List-Id: Reply-To: dev@zookeeper.apache.org Delivered-To: mailing list notifications@zookeeper.apache.org Received: (qmail 78571 invoked by uid 99); 1 Sep 2021 09:42:30 -0000 Received: from ec2-52-202-80-70.compute-1.amazonaws.com (HELO gitbox.apache.org) (52.202.80.70) by apache.org (qpsmtpd/0.29) with ESMTP; Wed, 01 Sep 2021 09:42:30 +0000 From: =?utf-8?q?GitBox?= To: notifications@zookeeper.apache.org Subject: =?utf-8?q?=5BGitHub=5D_=5Bzookeeper=5D_Vanlightly_commented_on_a_change_in_p?= =?utf-8?q?ull_request_=231690=3A_ZOOKEEPER-3615=3A_Provide_formal_specifica?= =?utf-8?q?tion_and_verification_using_TLA+_for_Zab?= Message-ID: <163048935033.16310.17368790914070424217.asfpy@gitbox.apache.org> Date: Wed, 01 Sep 2021 09:42:30 -0000 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit References: In-Reply-To: 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 == <> + +electionVars == <> + +leaderVars == <> + +varsL == <> +----------------------------------------------------------------------------- +\* 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 <> \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 {<>} \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