[SERVER-43592] Check that real execution traces are permitted by selected TLA+ specs 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 | ||
| Backwards Compatibility: | Fully Compatible |
| Participants: |
| Description |
|
Write a script that determines whether an actual execution trace (extracted from the logs after a replica set test) matches a trace permitted by a given TLA+ spec. The exact technique is TBD; it will involve some interaction between TLC and our custom checking code. Questions:
|
| Comments |
| Comment by A. Jesse Jiryu Davis [ 14/Jan/20 ] |
|
We chose to implement Ron Pressler's method of generating a temporary TLA+ spec that asserts a particular execution trace is a valid spec behavior, and then model-checking the temporary spec with TLC. I wrote a Python script that parses and merges logs from a real replica set, generates the temporary spec, and executes TLC. The final point, checking that we execute each state transition via the expected action, is future work. |