[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Measuring re-verification cost on MongoDB's TLA+ history: feedback welcome
Hi all,
I am an engineer studying how verification cost changes when a TLA+ specification
evolves. I measured TLC on two real commits from MongoDB's public specs and wrote a
short pilot report : https://github.com/amayene567/FormalSpecToolkit/blob/main/report/reverification_pilot_v3.pdf
Scripts, logs and a script that regenerates the specs from git:
https://github.com/amayene567/FormalSpecToolkit
Two observations:
- Adding two invariants to RaftMongo (SERVER-45853) raised checking time by about 57%
on an identical state space.
- SERVER-47430 strengthens the vote guard in MongoReplReconfig. A TLC refinement check
confirms that every child step is a parent step, yet a full re-check revisits
2.4 million already explored states. The same strengthening was later relaxed in the server (SERVER-57262) because it caused a liveness problem; the spec update (SERVER-58788) is still open.
I would value feedback on three points :
- To check refinement I instantiate the parent module in the child's model and check PROPERTY [][Parent!Next]_vars, with the model's SYMMETRY and state CONSTRAINT. Is that sound in this setting, or should it be run without SYMMETRY?
- Is there any way in TLC to reuse a previous run's state space or fingerprints after
a spec change?
- I am building a small benchmark of versioned specs with measured verification cost. Do you know other public repositories with long TLA+ commit histories?
Thanks,
AMAYENE SEKE Louis Quentin
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/362d7fc1-3576-4646-86ac-4915cf99dc7fn%40googlegroups.com.