[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: |
|
||||||||
| 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. |