Possible TLC soundness bug when checking temporal properties

[Markus Kuppe]

Federico Ponzi has identified a soundness bug in TLC that affects the verification of temporal properties, when TLC is configured with more than the default number of worker threads. This bug has existed since at least 2009 and possibly since support for the verification of temporal properties was first introduced.

The bug is caused by a concurrency issue in TLC, and we consider the likelihood of encountering this bug to be very low. However, it remains a critical issue that needs to be addressed.

For immediate mitigation, please check temporal properties using only a single worker (command line flag: `-workers 1`). Again, TLC runs with a single worker by default.

We are working on a fix and will release a new version of TLC once the bug is resolved. Announcements regarding the new release will be made here. For technical details or to offer help, please refer to the GitHub issue at https://github.com/tlaplus/tlaplus/issues/971.

Markus

[Leslie Lamport]

Should TLC be able to check such a property? I suspect that the error is that TLC should report that it can't check the property. For example, vio1 does not show a counterexample to the property. The behavior that it reports satisfies the property [](~x) , and [](~x) => [](x => y) is a tautology for any formula y.

Is there a spec somewhere of what temporal properties TLC can check? I seem to recall that it doesn't check properties of the form [](F => []G). (Such properties, with F and G state predicates, have to be proved in proofs of liveness properties.)

Leslie

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0DCE5FB8-B2B0-4DBE-A77A-6EA26C5A527D%40lemmster.de.