[SERVER-43588] Select and update TLA+ specs for trace checking Created: 24/Sep/19  Updated: 29/Oct/23  Resolved: 13/Jan/20

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

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

Issue Links:
Issue split
split to SERVER-44458 Productionize RaftMongo TLA+ spec Closed
Backwards Compatibility: Fully Compatible
Participants:

 Description   

Among TLA+ specs that the Replication Team has already written, select some to test against our actual implementation. Selection criteria:

  • How finished the spec is
  • How disjoint its test coverage is from other specs (subjective measure)
  • How high is the risk of implementation bugs in the logic that the spec models
  • How high is the risk of spec bugs; i.e., mismatches between the model and the implementation

See a list of possible specs (not exhaustive) in the Scope doc for this project.



 Comments   
Comment by A. Jesse Jiryu Davis [ 13/Jan/20 ]

We selected RaftMongo only, see SERVER-44458.

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