Skip to content

Commit

Permalink
Trace validation found another divergence within ~30 seconds after ge…
Browse files Browse the repository at this point in the history 
…nerating approximately 10k states.

The initiator initiates another token round even when the previous token round is conclusive. The system is in this state after a token round with all nodes white and inactive except for an active but white initiator.

This is a first attempt at a bugfix.

```
<< "Failed matching the trace to (a prefix of) a behavior:",
   [ pkt |->
         [ vc |->
               [ 1 |-> 342,
                 3 |-> 300,
                 0 |-> 216,
                 2 |-> 341,
                 5 |-> 313,
                 4 |-> 313,
                 6 |-> 320,
                 7 |-> 413 ],
           msg |-> [type |-> "pl"],
           snd |-> 0,
           rcv |-> 7 ],
     event |-> "<" ],
   "TLA+ debugger breakpoint hit count 2576" >>  FALSE
Error: Assumption line 212, col 5 to line 215, col 84 of module EWD998ChanTrace is false.
...
```
  • Loading branch information
@lemmy
lemmy committed Apr 10, 2023
1 parent bb52145 commit 5665744
Show file tree
Hide file tree
Showing 2 changed files with 81 additions and 12 deletions.
23 changes: 11 additions & 12 deletions specifications/ewd998/impl/src/EWD998.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ public EWD998(final Map<Integer, Pair> nodes, final int myId, final boolean isIn
inbox.put(pkt);
}

boolean terminationDetected = false;
boolean isConclusiveRound = false;

// --------------------------------------------------------------------------------- //

Expand Down Expand Up @@ -162,8 +162,7 @@ public EWD998(final Map<Integer, Pair> nodes, final int myId, final boolean isIn
/\ ...
/\ UNCHANGED <<active, counter, pending>>
*/
terminationDetected = tokenQ + counter == 0 && color == Color.white && tokenColor == Color.white
&& !active;
isConclusiveRound = tokenQ + counter == 0 && color == Color.white && tokenColor == Color.white;
}
} else if (msg.get(TYPE).equals(PL)) {
/*
Expand Down Expand Up @@ -246,7 +245,13 @@ public EWD998(final Map<Integer, Pair> nodes, final int myId, final boolean isIn
// /\ ...
// /\ token.pos = i
if (tokenColor != null) {
if (isInitiator) {
if (isInitiator && isConclusiveRound && !active) {
// Send the trm message to all nodes (us included).
for (Integer n : nodes.keySet()) {
sendMsg(myId, n, getTrm());
}
tokenColor = null;
} else if (isInitiator && !isConclusiveRound) {
/*
terminationDetected ==
/\ token.pos = 0
Expand All @@ -263,14 +268,8 @@ public EWD998(final Map<Integer, Pair> nodes, final int myId, final boolean isIn
/\ color' = [ color EXCEPT ![0] = "white" ]
/\ UNCHANGED <<active, counter, pending>>
*/
if (!terminationDetected) {
sendMsg(myId, nodes.size() - 1, getTok(0, Color.white));
color = Color.white;
} else {
for (Integer n : nodes.keySet()) {
sendMsg(myId, n, getTrm());
}
}
sendMsg(myId, nodes.size() - 1, getTok(0, Color.white));
color = Color.white;
tokenColor = null;
} else if (!active) {
/*
Expand Down
70 changes: 70 additions & 0 deletions specifications/ewd998/trace-unstable.ndjson
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
{"N":3}
{"event":"<","node":0,"pkt":{"snd":0,"rcv":0,"msg":{"type":"tok","q":0,"color":"black"},"vc":{"0":1,"1":0,"2":0}}}
{"event":">","node":0,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":2,"1":0,"2":0}}}
{"event":"<","node":1,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":2,"1":1,"2":0}}}
{"event":">","node":0,"pkt":{"snd":0,"rcv":2,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":3,"1":0,"2":0}}}
{"event":"<","node":2,"pkt":{"snd":0,"rcv":2,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":3,"1":0,"2":1}}}
{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":3,"1":0,"2":2}}}
{"event":"d","node":2,"pkt":{"vc":{"0":3,"1":0,"2":3}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":3,"1":2,"2":2}}}
{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":3,"1":0,"2":4}}}
{"event":"d","node":1,"pkt":{"vc":{"0":3,"1":3,"2":2}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":3,"1":4,"2":4}}}
{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":3,"1":5,"2":4}}}
{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":4,"1":5,"2":4}}}
{"event":">","node":0,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":5,"1":5,"2":4}}}
{"event":"<","node":1,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":5,"1":6,"2":4}}}
{"event":">","node":0,"pkt":{"snd":0,"rcv":2,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":6,"1":5,"2":4}}}
{"event":"<","node":2,"pkt":{"snd":0,"rcv":2,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":6,"1":5,"2":5}}}
{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":6,"1":5,"2":6}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":6,"1":7,"2":6}}}
{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":6,"1":8,"2":6}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":6,"1":9,"2":6}}}
{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":7,"1":8,"2":6}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":6,"1":10,"2":6}}}
{"event":">","node":0,"pkt":{"snd":0,"rcv":2,"msg":{"type":"pl"},"vc":{"0":8,"1":8,"2":6}}}
{"event":"d","node":0,"pkt":{"vc":{"0":9,"1":8,"2":6}}}
{"event":"<","node":2,"pkt":{"snd":0,"rcv":2,"msg":{"type":"pl"},"vc":{"0":8,"1":8,"2":7}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":6,"1":11,"2":6}}}
{"event":">","node":1,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":6,"1":12,"2":6}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":6,"1":13,"2":6}}}
{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":8,"1":8,"2":8}}}
{"event":"<","node":2,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":8,"1":12,"2":9}}}
{"event":">","node":2,"pkt":{"snd":2,"rcv":0,"msg":{"type":"pl"},"vc":{"0":8,"1":12,"2":10}}}
{"event":"<","node":0,"pkt":{"snd":2,"rcv":0,"msg":{"type":"pl"},"vc":{"0":10,"1":12,"2":10}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":8,"1":14,"2":8}}}
{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":8,"1":15,"2":8}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":8,"1":16,"2":8}}}
{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":11,"1":15,"2":10}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":8,"1":17,"2":8}}}
{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":8,"1":18,"2":8}}}
{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":12,"1":18,"2":10}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":8,"1":19,"2":8}}}
{"event":"d","node":1,"pkt":{"vc":{"0":8,"1":20,"2":8}}}
{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"black"},"vc":{"0":8,"1":21,"2":8}}}
{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"black"},"vc":{"0":13,"1":21,"2":10}}}
{"event":">","node":0,"pkt":{"snd":0,"rcv":2,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":14,"1":21,"2":10}}}
{"event":"<","node":2,"pkt":{"snd":0,"rcv":2,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":14,"1":21,"2":11}}}
{"event":"<","node":2,"pkt":{"snd":0,"rcv":2,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":14,"1":21,"2":12}}}
{"event":"<","node":2,"pkt":{"snd":0,"rcv":2,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":14,"1":21,"2":13}}}
{"event":"d","node":2,"pkt":{"vc":{"0":14,"1":21,"2":14}}}
{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"black"},"vc":{"0":14,"1":21,"2":15}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"black"},"vc":{"0":14,"1":22,"2":15}}}
{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"black"},"vc":{"0":14,"1":23,"2":15}}}
{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"black"},"vc":{"0":15,"1":23,"2":15}}}
{"event":">","node":0,"pkt":{"snd":0,"rcv":2,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":16,"1":23,"2":15}}}
{"event":"<","node":2,"pkt":{"snd":0,"rcv":2,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":16,"1":23,"2":16}}}
{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":16,"1":23,"2":17}}}
{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":16,"1":24,"2":17}}}
{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":16,"1":25,"2":17}}}
{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":17,"1":25,"2":17}}}
{"event":">","node":0,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":18,"1":25,"2":17}}}
{"event":"d","node":0,"pkt":{"vc":{"0":19,"1":25,"2":17}}}
{"event":"<","node":1,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":18,"1":26,"2":17}}}
{"event":">","node":0,"pkt":{"snd":0,"rcv":0,"msg":{"type":"trm"},"vc":{"0":20,"1":25,"2":17}}}
{"event":">","node":0,"pkt":{"snd":0,"rcv":1,"msg":{"type":"trm"},"vc":{"0":21,"1":25,"2":17}}}
{"event":">","node":0,"pkt":{"snd":0,"rcv":2,"msg":{"type":"trm"},"vc":{"0":22,"1":25,"2":17}}}
{"event":"<","node":0,"pkt":{"snd":0,"rcv":0,"msg":{"type":"trm"},"vc":{"0":23,"1":25,"2":17}}}
{"event":"<","node":2,"pkt":{"snd":0,"rcv":2,"msg":{"type":"trm"},"vc":{"0":22,"1":25,"2":18}}}
{"event":">","node":1,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":18,"1":27,"2":17}},"failure":"java.net.ConnectException: Connection refused"}
{"event":"<","node":1,"pkt":{"snd":0,"rcv":1,"msg":{"type":"trm"},"vc":{"0":21,"1":28,"2":17}}}

0 comments on commit 5665744

Please sign in to comment.