[
https://issues.apache.org/jira/browse/ZOOKEEPER-4903?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Wenhan Feng updated ZOOKEEPER-4903:
-----------------------------------
Attachment: tlc-state-path.txt
> An Inconsistency of `lastProcessed` variable in Spec and Impl
> -------------------------------------------------------------
>
> Key: ZOOKEEPER-4903
> URL: https://issues.apache.org/jira/browse/ZOOKEEPER-4903
> Project: ZooKeeper
> Issue Type: Bug
> Components: other
> Affects Versions: 3.10.0
> Reporter: Wenhan Feng
> Priority: Major
> Attachments: runtime-log, tlc-state-path.txt
>
>
> I have noticed that in the specification of ZKV3_7_0, it appears that the
> `SyncFollower` action uses an incorrect `lastProcessed`.
> In `SyncFollower`, the following code is used to determine which sync mode
> should be employed:
> {code:java}
> lastProcessedZxid == lastProcessed[i].zxid
> minCommittedIdx == lastSnapshot[i].index + 1
> maxCommittedIdx == IF zabState[i] = BROADCAST THEN lastCommitted[i].index
> ELSE Len(history[i])
> committedLogEmpty == minCommittedIdx > maxCommittedIdx
> minCommittedLog == IF committedLogEmpty THEN lastProcessedZxid
> ELSE history[i][minCommittedIdx].zxid
> maxCommittedLog == IF committedLogEmpty THEN lastProcessedZxid
> ELSE IF maxCommittedIdx = 0 THEN << 0,
> 0>>
> ELSE
> history[i][maxCommittedIdx].zxid
> {code}
> We can observe that `lastProcessedZxid` is assigned the value of
> `lastProcessed[i].zxid`, where `i` is the leader node ID and `lastProcessed`
> is a global variable in this specification.
> According to the comment in the specification, the `lastProcessed` variable
> means "The index and zxid of the last processed transaction in history". And
> we can see that it will be updated in the `StartZkServer\(i\)` Action with
> the following code:
> {code:java}
> LastProposed(i) == IF Len(history[i]) = 0 THEN [ index |-> 0, zxid |-> <<0,
> 0>> ]
> ELSE LET lastIndex == Len(history[i])
> entry == history[i][lastIndex]
> IN [ index |-> lastIndex,
> zxid |-> entry.zxid ]
> StartZkServer(i) ==
> LET latest == LastProposed(i)
> IN /\ lastCommitted' = [lastCommitted EXCEPT ![i] = latest]
> /\ lastProcessed' = [lastProcessed EXCEPT ![i] = latest]
> /\ lastSnapshot' = [lastSnapshot EXCEPT ![i] = latest]
> /\ UpdateElectionVote(i, acceptedEpoch[i])
> {code}
> We know that when a cluster finishes an election but before receiving any
> user requests, according to the specification, it will contain no history.
> And in `StartZKServer\(i\)`, `lastSnapshot[i]` will be assigned `[ index
> \|\-> 0, zxid \|\-> <<0, 0>> ]`.
> However, in the implementation code, I found that the `lastProcessed` used in
> the `LearnHanler.syncFollower()` function is actually the
> `dataTree.lastProcessedZxid` variable. And this variable is updated with the
> following code when `ZkServer` is starting:
> {code:java}
> Leader.java : Line 657: zk.setZxid(ZxidUtils.makeZxid(epoch, 0));
> Leader.java : Line 1609:
> zk.getZKDatabase().setlastProcessedZxid(zk.getZxid());
> {code}
> Therefore, when a cluster finishes an election but before receiving any user
> requests, its value is indeed `<<1, 0>>`. This causes the following
> `LeaderSyncFollower` action to choose an incorrect sync mode in the
> specification.
> I found that the specification already seems to use a variable, namely
> `tempMaxEpoch`, to record `zk.hzxid` (which `zk.getZxid()` actually
> retrieves). It seems that we should use `tempMaxEpoch[i]` in the
> `StartZkServer` action. And the correct code should be:
> {code:java}
> LastProposed(i) == IF Len(history[i]) = 0 THEN [ index |-> 0, zxid |->
> <<Maximum({tempMaxEpoch[i], 0}), 0>> ]
> ......
> StartZkServer(i) ==
> LET latest == LastProposed(i)
> IN ...... /\ lastProcessed' = [lastProcessed EXCEPT ![i] = latest]
> ......
> {code}
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
