Skip to content

Commit

Permalink
Erik's mods to EWD998 from class on 2022-07-12
Browse files Browse the repository at this point in the history 
Primarily closely read the paper's description of the algorithm and made changes to match the spec to the text description. One of the biggest changes was that nodes get marked as tainted when they RECEIVE a message, not when they SEND a message. Whoops! There were also minor changes necessary to match the token's initial state (I think we previously marked it tainted at the start if the initiator is tainted, but that's not right, the token always starts untained and the initiator's taint status gets checked when the token makes its way back around).

I also had to make small adjustments to the ATD spec, most notably to change the WF criteria to only check for Terminate, instead of Next. Not sure if that's "cheating", but I think it makes sense based on my understanding: as with EWD998, we don't want to force nodes to send/rcv messages indefinitely, we just want to ensure that we detect termination.

I validated this up to 3 nodes, and am trying on 4, though it has been running for multiple hours and generated 10M+ states without finishing...
  • Loading branch information
@xkrogen
xkrogen committed Jul 13, 2022
1 parent 17a216d commit a70049b
Show file tree
Hide file tree
Showing 4 changed files with 112 additions and 253 deletions.
29 changes: 14 additions & 15 deletions AsyncTerminationDetection.tla
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,31 +73,29 @@ RecvMsg(rcv) ==
/\ UNCHANGED terminationDetected

SendMsg(snd, rcv) ==
/\ pending' = [ pending EXCEPT ![rcv] = @ + 1]
/\ active[snd] = TRUE
\* /\ active' = [ active EXCEPT ![rcv] = FALSE ]
/\ UNCHANGED active \* ??? Should a node deactivate after sending?
/\ UNCHANGED terminationDetected
/\ pending' = [ pending EXCEPT ![rcv] = @ + 1]
/\ UNCHANGED <<active, terminationDetected>>

Terminate(n) ==
\* /\ active[n] = TRUE
/\ active' = [ active EXCEPT ![n] = FALSE ]
/\ UNCHANGED pending
/\ pending' = pending
\* /\ \/ terminationDetected' = terminated'
\* \/ terminationDetected' = FALSE
/\ terminationDetected' \in {terminated', FALSE}
/\ UNCHANGED <<pending>>
/\ terminationDetected' \in {terminated', terminationDetected}

Next ==
\E i,j \in Node:
\/ SendMsg(i,j)
\/ RecvMsg(i)
\/ Terminate(i)
\/ SendMsg(i,j)
\/ RecvMsg(i)
\/ Terminate(i)

-------------------

Spec ==
Init /\ [][Next]_vars /\ WF_vars(Next)
\* TODO is it okay to remove the `WF_vars(Next)` here?
\* It seems necessary to match the fairness provided by EWD998 which does
\* not require us to Send/Rcv messages, only pass/initiate tokens.
\* Init /\ [][Next]_vars /\ WF_vars(Next)
Init /\ [][Next]_vars /\ \E i \in Node: WF_vars(Terminate(i))

TypeOK ==
\* /\ \A i \in Node: pending[i] \in Nat
Expand Down Expand Up @@ -125,7 +123,8 @@ Constraint ==

MCInit ==
/\ active \in [ Node -> BOOLEAN ]
/\ pending \in [ Node -> 0..3 ]
\* /\ pending \in [ Node -> 0..3 ]
/\ pending \in [ Node -> {0} ]
/\ terminationDetected \in {FALSE, terminated}


Expand Down
2 changes: 1 addition & 1 deletion EWD998.cfg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ SPECIFICATION Spec

INVARIANT TypeOK

CONSTANT N = 3
CONSTANT N = 4
CONSTRAINT Constraint
CONSTANT Init <- MCInit

Expand Down
199 changes: 47 additions & 152 deletions EWD998.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,18 +2,18 @@
TLC2 Version 2.18 of Day Month 20?? (rev: 6ee6e9f)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 46 and seed 7528897163723597087 with 1 worker on 8 cores with 3559MB heap and 64MB offheap memory [pid: 9164] (Linux 5.4.0-1074-azure amd64, Oracle Corporation 17.0.2 x86_64, MSBDiskFPSet, DiskStateQueue).
Running breadth-first search Model-Checking with fp 57 and seed 3965354632801637035 with 1 worker on 16 cores with 7282MB heap and 64MB offheap memory [pid: 78154] (Mac OS X 12.4 x86_64, Microsoft 11.0.13 x86_64, MSBDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /workspaces/ewd998/EWD998.tla
Parsing file /tmp/tlc-8984331708763874482/Integers.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.5.2815/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-8984331708763874482/TLC.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.5.2815/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-8984331708763874482/Naturals.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.5.2815/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /workspaces/ewd998/AsyncTerminationDetection.tla
Parsing file /tmp/tlc-8984331708763874482/Sequences.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.5.2815/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-8984331708763874482/FiniteSets.tla (jar:file:/home/codespace/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-2022.5.2815/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /Users/ekrogen/dev/tlaplus-workshop/EWD998.tla
Parsing file /private/var/folders/n2/jm3shyv54sn4rf9mbr_6_k14000gvs/T/tlc-13028608698643914715/Integers.tla (jar:file:/Users/ekrogen/.vscode/extensions/alygin.vscode-tlaplus-nightly-2022.5.2815/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /private/var/folders/n2/jm3shyv54sn4rf9mbr_6_k14000gvs/T/tlc-13028608698643914715/TLC.tla (jar:file:/Users/ekrogen/.vscode/extensions/alygin.vscode-tlaplus-nightly-2022.5.2815/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /private/var/folders/n2/jm3shyv54sn4rf9mbr_6_k14000gvs/T/tlc-13028608698643914715/Naturals.tla (jar:file:/Users/ekrogen/.vscode/extensions/alygin.vscode-tlaplus-nightly-2022.5.2815/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /Users/ekrogen/dev/tlaplus-workshop/AsyncTerminationDetection.tla
Parsing file /private/var/folders/n2/jm3shyv54sn4rf9mbr_6_k14000gvs/T/tlc-13028608698643914715/Sequences.tla (jar:file:/Users/ekrogen/.vscode/extensions/alygin.vscode-tlaplus-nightly-2022.5.2815/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /private/var/folders/n2/jm3shyv54sn4rf9mbr_6_k14000gvs/T/tlc-13028608698643914715/FiniteSets.tla (jar:file:/Users/ekrogen/.vscode/extensions/alygin.vscode-tlaplus-nightly-2022.5.2815/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Expand All @@ -25,7 +25,7 @@ Semantic processing of module EWD998
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2022-07-12 22:11:51)
Starting... (2022-07-12 18:06:50)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 1 branches.
Expand All @@ -39,150 +39,45 @@ Computed 2 initial states...
@!@!@STARTMSG 2269:0 @!@!@
Computed 4 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 8 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 8 distinct states generated at 2022-07-12 22:11:52.
Finished computing initial states: 16 distinct states generated at 2022-07-12 18:06:50.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2110:1 @!@!@
Invariant IInv is violated.
@!@!@ENDMSG 2110 @!@!@
@!@!@STARTMSG 2121:1 @!@!@
The behavior up to this point is:
@!@!@ENDMSG 2121 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ network = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ inflight = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ token = [pos |-> 0, tainted |-> TRUE, value |-> 0]
/\ msgSentNotTainted = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ p0 = TRUE
/\ p1 = FALSE
/\ p2 = FALSE
/\ p3 = FALSE
/\ p4 = TRUE

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
2: <SendMsg line 107, col 5 to line 113, col 28 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ network = (0 :> 1 @@ 1 :> 0 @@ 2 :> 0)
/\ inflight = (0 :> 0 @@ 1 :> 0 @@ 2 :> 1)
/\ token = [pos |-> 0, tainted |-> TRUE, value |-> 0]
/\ msgSentNotTainted = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ p0 = TRUE
/\ p1 = FALSE
/\ p2 = FALSE
/\ p3 = FALSE
/\ p4 = TRUE

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
3: <RecvMsg line 99, col 5 to line 103, col 47 of module EWD998>
/\ active = (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ network = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ inflight = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ token = [pos |-> 0, tainted |-> TRUE, value |-> 0]
/\ msgSentNotTainted = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ p0 = TRUE
/\ p1 = FALSE
/\ p2 = FALSE
/\ p3 = FALSE
/\ p4 = TRUE

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
4: <Terminate line 117, col 5 to line 118, col 66 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ network = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ inflight = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ token = [pos |-> 0, tainted |-> TRUE, value |-> 0]
/\ msgSentNotTainted = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ p0 = TRUE
/\ p1 = FALSE
/\ p2 = FALSE
/\ p3 = FALSE
/\ p4 = TRUE

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
5: <InitiateToken line 67, col 5 to line 75, col 48 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ network = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ inflight = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ token = [pos |-> 2, tainted |-> FALSE, value |-> -1]
/\ msgSentNotTainted = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ p0 = TRUE
/\ p1 = FALSE
/\ p2 = FALSE
/\ p3 = TRUE
/\ p4 = FALSE

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
6: <Terminate line 117, col 5 to line 118, col 66 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ network = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ inflight = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ token = [pos |-> 2, tainted |-> FALSE, value |-> -1]
/\ msgSentNotTainted = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ p0 = TRUE
/\ p1 = FALSE
/\ p2 = FALSE
/\ p3 = TRUE
/\ p4 = FALSE

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
7: <PassToken line 78, col 5 to line 87, col 49 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ network = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ inflight = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ token = [pos |-> 1, tainted |-> TRUE, value |-> 0]
/\ msgSentNotTainted = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ p0 = TRUE
/\ p1 = FALSE
/\ p2 = FALSE
/\ p3 = FALSE
/\ p4 = TRUE

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
8: <PassToken line 78, col 5 to line 87, col 49 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ network = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ inflight = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ token = [pos |-> 0, tainted |-> TRUE, value |-> 0]
/\ msgSentNotTainted = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ p0 = TRUE
/\ p1 = FALSE
/\ p2 = FALSE
/\ p3 = FALSE
/\ p4 = TRUE

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
9: <InitiateToken line 67, col 5 to line 75, col 48 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ network = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ inflight = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ token = [pos |-> 2, tainted |-> FALSE, value |-> -1]
/\ msgSentNotTainted = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ p0 = TRUE
/\ p1 = FALSE
/\ p2 = FALSE
/\ p3 = FALSE
/\ p4 = FALSE

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking temporal properties for the current state space with 2834 total distinct states at (2022-07-12 18:06:53)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 00s at 2022-07-12 18:06:53
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(5) at 2022-07-12 18:06:53: 90,980 states generated (90,980 s/min), 9,131 distinct states found (9,131 ds/min), 6,296 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking temporal properties for the current state space with 96397 total distinct states at (2022-07-12 18:07:53)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 01s at 2022-07-12 18:07:55
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(9) at 2022-07-12 18:07:55: 3,289,870 states generated (3,198,890 s/min), 188,656 distinct states found (179,525 ds/min), 92,259 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking temporal properties for the current state space with 191499 total distinct states at (2022-07-12 18:08:55)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 02s at 2022-07-12 18:08:58
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(10) at 2022-07-12 18:08:58: 6,557,037 states generated (3,267,167 s/min), 345,207 distinct states found (156,551 ds/min), 153,707 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking temporal properties for the current state space with 288690 total distinct states at (2022-07-12 18:09:58)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 04s at 2022-07-12 18:10:02
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(9) at 2022-07-12 22:11:53: 103,207 states generated (2,937,580 s/min), 8,905 distinct states found (253,462 ds/min), 3,541 states left on queue.
Progress(11) at 2022-07-12 18:10:02: 9,914,417 states generated (3,357,380 s/min), 497,396 distinct states found (152,189 ds/min), 208,705 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
103207 states generated, 8905 distinct states found, 3541 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 9.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 2112ms at (2022-07-12 22:11:53)
@!@!@ENDMSG 2186 @!@!@
Loading

0 comments on commit a70049b

Please sign in to comment.