Fix deadlock detection in the parallel checker #110
Comments
|
I seem to have run into broken deadlock checking when checking |
|
The parallel checker is not in the unstable yet. What kind of problem do you have? |
|
For any markus@avocado:~/src/TLA/_specs/models/tutorials/ewd840(main)$ apalache check EWD840
# Tool home: /home/markus/src/TLA/_community/apalache
# Package: /home/markus/src/TLA/_community/apalache/mod-distribution/target/apalache-pkg-0.15.1-SNAPSHOT-full.jar
# JVM args: -Xmx4096m -DTLA-Library=/home/markus/src/TLA/_community/apalache/src/tla
#
# APALACHE version 0.15.1-SNAPSHOT build v0.15.0-3-gd5138a3
#
# WARNING: This tool is in the experimental stage.
# Please report bugs at: [https://github.com/informalsystems/apalache/issues]
#
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.
Checker options: filename=EWD840, init=, next=, inv= I@17:46:23.395
Tuning: I@17:46:23.885
PASS #0: SanyParser I@17:46:23.886
Parsing file /home/markus/src/TLA/_specs/models/tutorials/ewd840/EWD840.tla
Parsing file /tmp/Naturals.tla
PASS #1: TypeCheckerSnowcat I@17:46:24.608
> Running Snowcat .::. I@17:46:24.608
> Your types are great! I@17:46:24.971
> All expressions are typed I@17:46:24.972
PASS #2: ConfigurationPass I@17:46:25.011
> EWD840: Loading TLC configuration I@17:46:25.019
> No TLC configuration found. Skipping. I@17:46:25.029
> Command line option --init is not set. Using Init I@17:46:25.029
> Command line option --next is not set. Using Next I@17:46:25.030
> Set the initialization predicate to Init I@17:46:25.030
> Set the transition predicate to Next I@17:46:25.032
PASS #3: DesugarerPass I@17:46:25.109
> Desugaring... I@17:46:25.109
PASS #4: UnrollPass I@17:46:25.182
> Unroller I@17:46:25.281
PASS #5: PrimingPass I@17:46:25.368
> Introducing InitPrimed for Init' I@17:46:25.394
PASS #6: CoverAnalysisPass I@17:46:25.478
PASS #7: InlinePass I@17:46:25.479
> InlinerOfUserOper I@17:46:25.481
> LetInExpander I@17:46:25.561
> InlinerOfUserOper I@17:46:25.606
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next I@17:46:25.623
PASS #8: VCGen I@17:46:25.645
> No invariant given. Only deadlocks will be checked I@17:46:25.645
PASS #9: PreprocessingPass I@17:46:25.660
> Before preprocessing: unique renaming I@17:46:25.661
> Applying standard transformations: I@17:46:25.678
> PrimePropagation I@17:46:25.688
> Desugarer I@17:46:25.714
> UniqueRenamer I@17:46:25.739
> Normalizer I@17:46:25.785
> Keramelizer I@17:46:25.805
> After preprocessing: UniqueRenamer I@17:46:25.839
PASS #10: TransitionFinderPass I@17:46:25.883
> Found 1 initializing transitions I@17:46:25.980
> Found 4 transitions I@17:46:26.067
> No constant initializer I@17:46:26.070
> Applying unique renaming I@17:46:26.074
PASS #11: OptimizationPass I@17:46:26.130
> Applying optimizations: I@17:46:26.139
> ConstSimplifier I@17:46:26.141
> ExprOptimizer I@17:46:26.148
> ConstSimplifier I@17:46:26.153
PASS #12: AnalysisPass I@17:46:26.199
> Marking skolemizable existentials and sets to be expanded... I@17:46:26.205
> SkolemizationMarker I@17:46:26.208
> ExpansionMarker I@17:46:26.211
> Running analyzers... I@17:46:26.228
> Introduced expression grades I@17:46:26.247
> Introduced 2 formula hints I@17:46:26.247
PASS #13: PostTypeCheckerSnowcat I@17:46:26.247
> Running Snowcat .::. I@17:46:26.248
> Your types are great! I@17:46:26.566
> All expressions are typed I@17:46:26.567
PASS #14: BoundedChecker I@17:46:26.590
Step 0: picking a transition out of 1 transition(s) I@17:46:27.021
Step 1: picking a transition out of 4 transition(s) I@17:46:27.186
Step 2: picking a transition out of 4 transition(s) I@17:46:27.346
Step 3: picking a transition out of 4 transition(s) I@17:46:27.488
Step 4: picking a transition out of 4 transition(s) I@17:46:27.637
Step 5: picking a transition out of 4 transition(s) I@17:46:27.766
Step 6: picking a transition out of 4 transition(s) I@17:46:27.890
Step 7: picking a transition out of 4 transition(s) I@17:46:28.043
Step 8: picking a transition out of 4 transition(s) I@17:46:28.213
Step 9: picking a transition out of 4 transition(s) I@17:46:28.482
Step 10: picking a transition out of 4 transition(s) I@17:46:28.774
The outcome is: NoError I@17:46:28.785
PASS #15: Terminal I@17:46:28.787
Checker reports no error up to computation length 10 I@17:46:28.787
It took me 0 days 0 hours 0 min 5 sec I@17:46:28.788
Total time: 5.396 sec I@17:46:28.788
EXITCODE: OKmarkus@avocado:~/src/TLA/_specs/examples/specifications/ewd840(master)$ git diff EWD840.tla
diff --git a/specifications/ewd840/EWD840.tla b/specifications/ewd840/EWD840.tla
index 018d7ec..a7ecf1f 100644
--- a/specifications/ewd840/EWD840.tla
+++ b/specifications/ewd840/EWD840.tla
@@ -7,10 +7,20 @@
(***************************************************************************)
EXTENDS Naturals
-CONSTANT N
-ASSUME NAssumption == N \in Nat \ {0}
-
-VARIABLES active, color, tpos, tcolor
+\* CONSTANT N
+\* ASSUME NAssumption == N \in Nat \ {0}
+N == 7
+
+\* VARIABLES active, color, tpos, tcolor
+VARIABLES
+ \* @type: Int -> Bool;
+ active,
+ \* @type: Int -> Str;
+ color,
+ \* @type: Int;
+ tpos,
+ \* @type: Str;
+ tcolor
Node == 0 .. N-1
Color == {"white", "black"}markus@avocado:~/src/TLA/_specs/examples/specifications/ewd840(master)$ tlc EWD840
TLC2 Version 2.15 of Day Month 20?? (rev: ba14c21)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 54 and seed -8107755520121129892 with 1 worker on 4 cores with 5952MB heap and 64MB offheap memory [pid: 622554] (Linux 5.4.0-70-generic amd64, Ubuntu 11.0.10 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/markus/src/TLA/_specs/examples/specifications/ewd840/EWD840.tla
Parsing file /tmp/Naturals.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /home/markus/src/TLA/_specs/examples/specifications/ewd840/SyncTerminationDetection.tla
Semantic processing of module Naturals
Semantic processing of module SyncTerminationDetection
Semantic processing of module EWD840
Starting... (2021-04-03 17:44:40)
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Computed 64 initial states...
Computed 128 initial states...
Computed 256 initial states...
Computed 512 initial states...
Computed 1024 initial states...
Computed 2048 initial states...
Computed 4096 initial states...
Computed 8192 initial states...
Computed 16384 initial states...
Computed 32768 initial states...
Computed 65536 initial states...
Finished computing initial states: 114688 distinct states generated at 2021-04-03 17:44:42.
Progress(2) at 2021-04-03 17:44:45: 1,205,284 states generated (1,205,284 s/min), 118,336 distinct states found (118,336 ds/min), 67,549 states left on queue.
Error: Deadlock reached.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ tpos = 0
/\ active = ( 0 :> FALSE @@
1 :> FALSE @@
2 :> FALSE @@
3 :> FALSE @@
4 :> FALSE @@
5 :> FALSE @@
6 :> FALSE )
/\ tcolor = "black"
/\ color = ( 0 :> "white" @@
1 :> "white" @@
2 :> "white" @@
3 :> "white" @@
4 :> "white" @@
5 :> "white" @@
6 :> "white" )
State 2: <InitiateProbe line 40, col 3 to line 45, col 43 of module EWD840>
/\ tpos = 6
/\ active = ( 0 :> FALSE @@
1 :> FALSE @@
2 :> FALSE @@
3 :> FALSE @@
4 :> FALSE @@
5 :> FALSE @@
6 :> FALSE )
/\ tcolor = "white"
/\ color = ( 0 :> "white" @@
1 :> "white" @@
2 :> "white" @@
3 :> "white" @@
4 :> "white" @@
5 :> "white" @@
6 :> "white" )
State 3: <PassToken line 58, col 3 to line 63, col 43 of module EWD840>
/\ tpos = 5
/\ active = ( 0 :> FALSE @@
1 :> FALSE @@
2 :> FALSE @@
3 :> FALSE @@
4 :> FALSE @@
5 :> FALSE @@
6 :> FALSE )
/\ tcolor = "white"
/\ color = ( 0 :> "white" @@
1 :> "white" @@
2 :> "white" @@
3 :> "white" @@
4 :> "white" @@
5 :> "white" @@
6 :> "white" )
State 4: <PassToken line 58, col 3 to line 63, col 43 of module EWD840>
/\ tpos = 4
/\ active = ( 0 :> FALSE @@
1 :> FALSE @@
2 :> FALSE @@
3 :> FALSE @@
4 :> FALSE @@
5 :> FALSE @@
6 :> FALSE )
/\ tcolor = "white"
/\ color = ( 0 :> "white" @@
1 :> "white" @@
2 :> "white" @@
3 :> "white" @@
4 :> "white" @@
5 :> "white" @@
6 :> "white" )
State 5: <PassToken line 58, col 3 to line 63, col 43 of module EWD840>
/\ tpos = 3
/\ active = ( 0 :> FALSE @@
1 :> FALSE @@
2 :> FALSE @@
3 :> FALSE @@
4 :> FALSE @@
5 :> FALSE @@
6 :> FALSE )
/\ tcolor = "white"
/\ color = ( 0 :> "white" @@
1 :> "white" @@
2 :> "white" @@
3 :> "white" @@
4 :> "white" @@
5 :> "white" @@
6 :> "white" )
State 6: <PassToken line 58, col 3 to line 63, col 43 of module EWD840>
/\ tpos = 2
/\ active = ( 0 :> FALSE @@
1 :> FALSE @@
2 :> FALSE @@
3 :> FALSE @@
4 :> FALSE @@
5 :> FALSE @@
6 :> FALSE )
/\ tcolor = "white"
/\ color = ( 0 :> "white" @@
1 :> "white" @@
2 :> "white" @@
3 :> "white" @@
4 :> "white" @@
5 :> "white" @@
6 :> "white" )
State 7: <PassToken line 58, col 3 to line 63, col 43 of module EWD840>
/\ tpos = 1
/\ active = ( 0 :> FALSE @@
1 :> FALSE @@
2 :> FALSE @@
3 :> FALSE @@
4 :> FALSE @@
5 :> FALSE @@
6 :> FALSE )
/\ tcolor = "white"
/\ color = ( 0 :> "white" @@
1 :> "white" @@
2 :> "white" @@
3 :> "white" @@
4 :> "white" @@
5 :> "white" @@
6 :> "white" )
State 8: <PassToken line 58, col 3 to line 63, col 43 of module EWD840>
/\ tpos = 0
/\ active = ( 0 :> FALSE @@
1 :> FALSE @@
2 :> FALSE @@
3 :> FALSE @@
4 :> FALSE @@
5 :> FALSE @@
6 :> FALSE )
/\ tcolor = "white"
/\ color = ( 0 :> "white" @@
1 :> "white" @@
2 :> "white" @@
3 :> "white" @@
4 :> "white" @@
5 :> "white" @@
6 :> "white" )
3988314 states generated, 151126 distinct states found, 3753 states left on queue.
The depth of the complete state graph search is 8.
Finished in 09s at (2021-04-03 17:44:49) |
|
That seems to be an issue both in 0.11.0 and 0.15.0. A bug must have sneaked in. See #711. |
|
It's a bigger issue. So I have scheduled it in #712. |
|
We are not going to merge the current version in the multicore branch. Closing this issue. The related issue on deadlock detection is filed in #712. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The integration test nr. 20 fails, as deadlock detection is broken in the parallel checker:
apalache check --length=5 --inv=Inv test/tla/HandshakeWithTypes.tlaThe text was updated successfully, but these errors were encountered: