From dd7415544925304e509a19cf64add7ef4d9bdb4b Mon Sep 17 00:00:00 2001 From: Federico Ponzi Date: Wed, 12 Jun 2024 09:15:25 +0100 Subject: [PATCH] Diameter is nondeterministic with multiple workers Persist the learning from issue #883. Diameter is non-deterministic when the BFS is run with multiple workers. Signed-off-by: Federico Ponzi --- general/docs/current-tools.md | 4 ++++ tlatools/org.lamport.tlatools/src/tlc2/TLC.java | 2 ++ .../html/model/tlc-options-page.html | 17 ++++++++++++----- 3 files changed, 18 insertions(+), 5 deletions(-) diff --git a/general/docs/current-tools.md b/general/docs/current-tools.md index 0347684408..75172742b9 100644 --- a/general/docs/current-tools.md +++ b/general/docs/current-tools.md @@ -30,6 +30,10 @@ ISpec == IM!Spec TLC cannot handle natural numbers greater than 231 - 1. +When running the model checking in BFS mode with multiple workers on a medium-small model, the reported diameter might differ across runs. +This is a limitation we accept to avoid putting additional synchronization that would limit the scalability. +For small models, use a single worker. For large models, the diameter will almost always appear deterministic. + ### Additional Features #### Enhanced Replacement diff --git a/tlatools/org.lamport.tlatools/src/tlc2/TLC.java b/tlatools/org.lamport.tlatools/src/tlc2/TLC.java index cab68b805d..8b977607cc 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/TLC.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/TLC.java @@ -1687,6 +1687,8 @@ private void printUsage() + "duplicate operator definitions, this is likely due to the 'monolith' specification\n" + "creation. Try re-running TLC adding the 'nomonolith' option to the '-generateSpecTE'\n" + "parameter."); + tips.add("When using more than one worker, the reported depth might differ across runs. For small models, " + + "use a single worker. For large models, the diameter will almost always appear deterministic."); UsageGenerator.displayUsage(ToolIO.out, "TLC", TLCGlobals.versionOfTLC, "provides model checking and simulation of TLA+ specifications", diff --git a/toolbox/org.lamport.tla.toolbox.doc/html/model/tlc-options-page.html b/toolbox/org.lamport.tla.toolbox.doc/html/model/tlc-options-page.html index 7db4dc7f0c..1a6f1e9033 100644 --- a/toolbox/org.lamport.tla.toolbox.doc/html/model/tlc-options-page.html +++ b/toolbox/org.lamport.tla.toolbox.doc/html/model/tlc-options-page.html @@ -38,6 +38,11 @@

Number of worker threads

This parameter specifies the number of separate threads that TLC will spawn to perform that computation.  You should not set it to be greater than the number of separate processors (cores) on your computer; the Toolbox will warn you if you do. +When using multiple workers on a medium-small model, the reported Diameter might +differ across runs. +This is a limitation we accept to avoid putting additional synchronization that would limit +the scalability. For small models, use a single worker. For large models, +the diameter will almost always appear deterministic.

Fraction of physical memory allocated to TLC

@@ -85,17 +90,19 @@

Model-checking mode

breadth-first search.  This has the advantage that if TLC finds a violation of a safety property, then it will produce a shortest possible behavior that exhibits the -error.  You can direct TLC to use a depth-first search -by choosing the Depth-first option and specifying -the depth of its search.  (Limiting the depth ensures +error.  You can direct TLC to use a depth-first iterative +deeping (DFID) search by choosing the Depth-first option +and specifying the depth of its search.  (Limiting the depth ensures that only a finite set of states is explored, even if the complete set of reachable states is infinite.)  -With depth-first search, TLC will usually not produce -a shortest-length error trace.  When running in depth-first +With DFID search, TLC will usually not produce +a shortest-length error trace.  When running in DFID mode, TLC does not compute the entire state graph and does not use a state queue, so it does not produce any Diameter or Queue size statistics. +Additionally, the DFID option doesn't currently support +running with multiple workers.

Warning: Depth-first search is an experimental TLC