arup-chauhan opened a new pull request, #2355:
URL: https://github.com/apache/zookeeper/pull/2355
### Description
This PR is the first incremental change for ZOOKEEPER-4892.
Scope is intentionally limited to FastLeaderElection TLA vote-state
synchronization.
When a server updates its proposal in LOOKING flow, its self entry in
`receiveVotes[i][i]` must reflect the same current vote. I have not changed the
Java runtime code and change is limited to TLA model consistency for self-vote
tracking.
This is PR-1 of a planned 2-PR sequence for ZOOKEEPER-4892. PR-2 will cover
quorum vote-set/counting alignment (`VoteSet`/`HasQuorums`).
### Changes
- Updated `RvPut(...)` in
`zookeeper-specifications/system-spec/zk-3.7/FastLeaderElection.tla`:
- synchronizes `receiveVotes[i][i]` with `currentVote'[i]`
- keeps self round/state/version aligned during receive-vote updates
- Updated `RvClearAndPut(...)`:
- explicitly sets self entry (`v = i`) to `currentVote'[i]`
- keeps existing behavior for source vote insertion and reset of other
entries
### Validation
- `mvn -q -DskipTests install`
- `mvn -q -pl zookeeper-server -DskipTests compile`
- TLC notes:
- Spec parses and semantically processes.
- Existing model currently has an unbounded `CHOOSE` at `NullPoint` in
base file, which blocks full BFS model checking.
- A temporary local bounded-`NullPoint` run was used to complete TLC
simulation sanity.
--
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: [email protected]
For queries about this service, please contact Infrastructure at:
[email protected]
