[SERVER-44851] Update TLA+ model of heartbeat safe reconfig Created: 26/Nov/19  Updated: 29/Oct/23  Resolved: 07/Feb/20

Status: Closed
Project: Core Server
Component/s: Replication
Affects Version/s: None
Fix Version/s: 4.3.4

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:
Depends
is depended on by SERVER-45415 Factor RaftMongo.tla with MongoReplRe... Backlog
Backwards Compatibility: Fully Compatible
Sprint: Repl 2019-12-16, Repl 2019-12-30, Repl 2020-01-13, Repl 2020-01-27, Repl 2020-02-10
Participants:

 Description   

We need to update the model to check the final design.

  • Checking all entries in the previous config is also committed in the current config.
  • Model arbiters.

"force" reconfig may also be included in the model, but the correctness is tricky, so it's a stretch goal.



 Comments   
Comment by Githook User [ 06/Feb/20 ]

Author:

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

Message: SERVER-44851 Constrain commit points for model-checking.
Branch: master
https://github.com/mongodb/mongo/commit/dfccd546055fdbfa0401e67e4f0e5bc9e89ef358

Comment by Siyuan Zhou [ 27/Jan/20 ]

We didn't model arbiters as it's of low risk and low priority.

Comment by Githook User [ 23/Jan/20 ]

Author:

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

Message: SERVER-44851 Add the TLA+ spec of replication safe reconfig.
Branch: master
https://github.com/mongodb/mongo/commit/09cafd88ac1d7d84c0904a452d1629048f657522

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