[tlaplus] Possible TLC soundness bug when checking temporal properties

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

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