Wenhan Feng created ZOOKEEPER-4892:
--------------------------------------
Summary: Inconsistency of the quorum rule of the leader election
process between the Zookeeper implmentation and specification.
Key: ZOOKEEPER-4892
URL: https://issues.apache.org/jira/browse/ZOOKEEPER-4892
Project: ZooKeeper
Issue Type: Bug
Components: quorum
Affects Versions: 3.9.3
Environment: Run Zookeeper specification with TLA+ Toolbox 1.8.0 in
Win11.
Run Zookeeper implementation in ubuntu 220.4
Reporter: Wenhan Feng
Attachments: Inconsistency in quorom rule.png
It seems the quorum rule of the leader election process between the Zookeeper
implmentation and specification is inconsistent.
In {*}implementation{*}, according to the code in the _FastLeaderElection_
class, a node maintains the votes of all nodes in the cluster it considers
through a `recvset` (which are modeled into _receiveVotes_ variable in the
specification). At the same time, it maintains its own vote through the
variables {_}proposedLeader{_}, {_}proposedZxid{_}, and _proposedEpoch_ (which
are modeled into _currentVote_ variable in the specification). The quorum rule
is that when there are votes from a majority of the nodes in the _recvset_ that
match its own vote ({_}proposedLeader{_}, {_}proposedZxid{_}, and
_proposedEpoch_) , the node considers the quorum rule is satisfied and moves to
the next stage of the election.
Related codes:
{code:java}
// Line 761-780 in FastLeaderElection.java
protected SyncedLearnerTracker getVoteTracker(Map<Long, Vote> votes, Vote vote)
{
....
for (Map.Entry<Long, Vote> entry : votes.entrySet()) {
if (vote.equals(entry.getValue())) {
voteSet.addAck(entry.getKey());
}
}
return voteSet;
}
// Line 1045 in FastLeaderElection.java
voteSet = getVoteTracker(recvset, new Vote(proposedLeader, proposedZxid,
logicalclock.get(), proposedEpoch));
{code}
In {*}specification{*}, according to the action _FLEHandleNotmsg_ and
_HandleNotmsg_, the node itself is initially included in the set of nodes that
have reached consensus. Then, the specification checks whether the votes from
other nodes in the _rreceiveVotes_ match the node's _currentVote_. If the
number of nodes whose votes match the node's _currentVote_ reaches a majority
with the node itself, the quorum is considered reached.
Related codes:
{code:java}
\* Line 216-222 in FastLeaderElection.tla.
VoteSet(i, msource, rcvset, thisvote, thisround) == \{msource} \union \{s \in
(Server \ {msource}): VoteEqual(rcvset[s].vote,
rcvset[s].round,
thisvote,
thisround)}
HasQuorums(i, msource, rcvset, thisvote, thisround) == LET Q == VoteSet(i,
msource, rcvset, thisvote, thisround)
IN IF Q \in Quorums THEN
TRUE ELSE FALSE
\* Line 433 in HandleNotmsg action of FastLeaderElection.tla.
/\ LET hasQuorums == HasQuorums(i, i, receiveVotes'[i], currentVote'[i],
n.mround)
{code}
```
```
We can see that these two mechanisms are not entirely consistent. Consider the
following three-node scenario:
1. The cluster starts, and at this point, node 1's _recvset_ contains votes
from nodes 1, 2, and 3, all of which are initial votes (denoted as
`InitialVote`).
2. Node 3 sends a _Notification-1_ (leader=N3, zxid=1, electionEpoch=1) to
nodes 1, 2, and 3.
3. Node 1 receives _Notification-1_ from node 3.
4. Node 1 updates its vote to _Notification-1_ and sends _Notification-1_ to
nodes 1, 2, and 3 again.
5. Node 1 updates its _recvset_. At this point, node 1's `recvset` is \{N1:
_InitialVote_, N2: _InitialVote_, N3: _Notification-1_}.
6. According to the specification, node 1 now believes that quorom nodes have
reached consensus. However, according to the implementation, node 1 needs to
receive the _Notification-1_ sent by itself in step 4 and update its _recvset_
(i.e., node 1's vote in the `recvset` must also be set to _Notification-1_)
before it can consider the quorum reached.
This figure "Inconsistency in quorom rule.png" in attachment shows the system
state after step 5 more detailedly.
I noticed that in the current version of the TLA+ specification, developers are
attempting to avoid modeling the process of a node sending a message to itself
and processing its own message. However, this simplification seems to lead to:
1. Inconsistencies between key algorithms in the specification and the
implementation. In the example above, the inconsistent quorum rule caused me
some confusion when I read the code.
2. Omission of some test scenarios. In the example above, There are some
possible concurrent behaviors in the cluster after step 5 but before node 1
receives its own `Notification` and updates its `recvset` in step 6. These
concurrent behaviors cannot be verified with the current version of the
specification.
I believe this issue can be fixed with the following two possible solutions:
1. *Simpler solution*: In the _HandleNotmsg\(i\)_ action of the specification,
update _receiveVotes[i]_ after performing `UpdateProposal\(i\)`. Then, modify
the _HasQuorums_ action to match the implementation's quorum rule.
2. *Complete solution*: Modify the _BroadcastNotmsg_ action in the
specification to include _Notification_ messages sent to itself in the
_recvqueue_, as is actually in the implementation (currently, the specification
directly ignores such messages). Also, improve the handling logic for these
types of messages in _FLEReceiveNotmsg_ and _FLEHandleNotmsg_ actions. Finally,
modify the _HasQuorums_ action to match the implementation's quorum rule.
If this issue is confirmed, I would be happy to provide a PR.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
