[SERVER-45853] Check CommitPointEventuallyPropagates, NeverRollbackCommitted and NeverRollbackBeforeCommitPoint Created: 29/Jan/20  Updated: 29/Oct/23  Resolved: 30/Jan/20

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

Type: New Feature Priority: Major - P3
Reporter: A. Jesse Jiryu Davis Assignee: A. Jesse Jiryu Davis
Resolution: Fixed Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Backwards Compatibility: Fully Compatible
Sprint: Repl 2020-02-10
Participants:

 Description   

NeverRollbackCommitted and NeverRollbackBeforeCommitPoint hold for small replica sets in RaftMongo.tla, and CommitPointEventuallyPropagates should hold for all model configurations. Enable them in MCRaftMongo.cfg, and move commentary about them to that file.



 Comments   
Comment by Githook User [ 30/Jan/20 ]

Author:

{'username': 'ajdavis', 'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@mongodb.com'}

Message: SERVER-45853 Enable RaftMongo.tla invariants

Also speed up model-checking for all Replication models, and remove an
obsolete comment in RaftMongo.tla.
Branch: master
https://github.com/mongodb/mongo/commit/348880238de3229826053491b1163c88dc3a0575

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