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

  • Dump the whole state graph and check the trace with Python (Jesse's Skunkworks script) or follow Pressler's "Verifying Software Traces Against a Formal Specification with TLA+ and TLC"?
  • Use/disable TLC's "symmetry set" optimization?
  • In addition to checking that we go from one permitted state to another, also check that we get there only by executing actions enabled in the spec?


 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.

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