[SERVER-47430] Update TLA+ to only vote for candidate with same config version and term as self Created: 09/Apr/20  Updated: 29/Oct/23  Resolved: 09/Apr/20

Status: Closed
Project: Core Server
Component/s: Replication
Affects Version/s: None
Fix Version/s: 4.4.0-rc2, 4.7.0

Type: Task Priority: Major - P3
Reporter: Siyuan Zhou Assignee: Siyuan Zhou
Resolution: Fixed Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Issue Links:
Backports
Related
is related to SERVER-46387 Only vote for candidate with same con... Closed
Backwards Compatibility: Fully Compatible
Backport Requested:
v4.4
Sprint: Execution Team 2020-04-20
Participants:

 Description   

Update the TLA+ spec to reflect the change in SERVER-46387.



 Comments   
Comment by Githook User [ 17/Apr/20 ]

Author:

{'name': 'Siyuan Zhou', 'email': 'siyuan.zhou@mongodb.com', 'username': 'visualzhou'}

Message: SERVER-47430 Update TLA+ to only vote for candidate with same config version and term as self

(cherry picked from commit 6e182b5c907f2965516b852311c9be6da05932d8)
Branch: v4.4
https://github.com/mongodb/mongo/commit/dd278880390a0dda81ef7e9866be4c16b7571b4a

Comment by Githook User [ 09/Apr/20 ]

Author:

{'name': 'Siyuan Zhou', 'email': 'siyuan.zhou@mongodb.com', 'username': 'visualzhou'}

Message: SERVER-47430 Update TLA+ to only vote for candidate with same config version and term as self
Branch: master
https://github.com/mongodb/mongo/commit/6e182b5c907f2965516b852311c9be6da05932d8

Comment by Siyuan Zhou [ 09/Apr/20 ]

Safety check of "NeverRollbackCommitted" with 4 nodes passed.

Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = .26
  based on the actual fingerprints:  val = .026
12326471047 states generated, 403328028 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 53.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 17 and the 95th percentile is 4).
Finished in 11h 49min at (2020-04-06 07:16:05)

But liveness checks with ConfigEventuallyPropagates and {{ElectableNodeEventuallyExists }} run for days and could not finish.

Comment by Siyuan Zhou [ 09/Apr/20 ]

Spinning this ticket off SERVER-46387 as it has been closed in earlier iterations.

Generated at Thu Feb 08 05:14:10 UTC 2024 using Jira 9.7.1#970001-sha1:2222b88b221c4928ef0de3161136cc90c8356a66.