[SERVER-43593] Deploy TLA+ trace checker to Evergreen Created: 24/Sep/19  Updated: 06/Dec/22  Resolved: 13/Jan/20

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

Type: New Feature Priority: Major - P3
Reporter: A. Jesse Jiryu Davis Assignee: Backlog - Replication Team
Resolution: Won't Fix Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Issue Links:
Depends
depends on SERVER-44481 resmoke.py cannot enable failpoints f... Closed
Assigned Teams:
Replication
Participants:

 Description   

Select some/all replication fuzz tests for checking. At the beginning of these fuzz tests, disable oplog truncation and enable the logging component that is introduced for the sake of trace checking. At the end of these tests, run the scripts that extract an execution trace and compare it to our selected TLA+ specs. Output a useful report and fail the test if the actual trace is not permitted by one of the specs.



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

We've decided to stop implementation and write the paper describing how far we got.

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