Messy spin snapshot with bug demobug-skip-introduces-failure

2 files changed, 41 insertions, 27 deletions

diff --git a/spin/Makefile b/spin/Makefile
index 73669f9..cb862cf 100644
--- a/spin/Makefile
+++ b/spin/Makefile
@@ -5,7 +5,7 @@ clean:
 
 %.pml.trail: %.pml
         @rm -f $@
-        spin -search -bitstate -l $< | egrep '^(pan|spin):'
+        spin -search -bit $< | egrep '^(pan|spin):'
         [ ! -e $@ ] || spin -c -g -l -p -replay $<
 
 .SECONDARY:
diff --git a/spin/snoopy.pml b/spin/snoopy.pml
index 4774b1a..0b4de5d 100644
--- a/spin/snoopy.pml
+++ b/spin/snoopy.pml
@@ -20,70 +20,84 @@ proctype cache(int recvqbase; int sendqbase; int npeers)
 #define ALLPEERS ((1 << npeers) - 1)
 #define RQ(i) qs[recvqbase+i]
 #define SQ(i) qs[sendqbase+i]
+#define ERESET() atomic { ebcmd = I; ebstate = I; enotsent = 0; enotrcvd = 0; ereverse = 0; esource = -1; }
+#define P() noprogress = 0
 
     mtype cstate = I;       // I, M, or Busy
     mtype ebcmd = I;        // I, ItoM, or Busy
-    int ebstate = I;        // I, M, or U
+    mtype ebstate = I;      // I, M, or U
     int enotsent = 0;       // bitmask of snoops remaining to send
     int enotrcvd = 0;       // bitmask of replies remaining to receive
     int ereverse = 0;       // count of reverse progress
     int esource = -1;       // source of command (-1 is originated locally)
     int i = 0;              // current peer
+    int fairmask = 0;       // fairness mask to ensure servicing all peers
+    int noprogress = 0;     // increment loop breaker
 
     do
     // Receive fill request from peer
     :: atomic { RQ(i)?ItoM -> if
         :: cstate == M -> cstate = I -> SQ(i)!M
-        :: cstate == I && ebcmd == I -> ebcmd = ItoM -> enotsent = ALLPEERS & ~(1 << i) -> esource = i
+        :: cstate != M && ebcmd == I -> ebcmd = ItoM -> enotsent = ALLPEERS & ~(1 << i) -> esource = i
         :: else -> SQ(i)!X
-        fi }
+        fi -> P() }
 
     // Receive fill responses from peers
-    :: atomic { RQ(i)?I -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) }
+    :: atomic { RQ(i)?I -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> P() }
     :: atomic { RQ(i)?M -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> ebstate = M -> if
         :: esource != -1 -> SQ(esource)!M
         :: else /* ideally put it into the cache right away */
-        fi }
-    :: atomic { RQ(i)?U -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> if :: ebstate == I -> ebstate = U :: else fi }
+        fi -> P() }
+    :: atomic { RQ(i)?U -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> if :: ebstate == I -> ebstate = U :: else fi -> P() }
     :: atomic { RQ(i)?X -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> enotsent = enotsent | (1 << i) -> ereverse = ereverse + 1 -> if
         // To prevent deadlock, if we get X'd too many times abandon the transaction and send X to its source
-        :: ereverse > npeers && esource == -1 && enotsent == ALLPEERS -> ebcmd = I -> ebstate = I -> enotsent = 0 -> ereverse = 0 -> esource = -1
-        :: ereverse > npeers && esource != -1 && enotsent == ALLPEERS & ~(1 << esource) -> SQ(esource)!X -> ebcmd = I -> ebstate = I -> enotsent = 0 -> ereverse = 0 -> esource = -1
+        :: ereverse > npeers && esource == -1 && enotsent == ALLPEERS -> ERESET()
+        :: ereverse > npeers && esource != -1 && enotsent == ALLPEERS & ~(1 << esource) -> SQ(esource)!X -> ERESET()
         :: else
-        fi }
+        fi -> P() }
 
     // Send not-yet-sent snoops
-    :: atomic { ebcmd == ItoM && (enotsent & (1 << i)) -> enotsent = enotsent & ~(1 << i) -> enotrcvd = enotrcvd | (1 << i) -> SQ(i)!ItoM }
+    :: atomic { ebcmd == ItoM && (enotsent & (1 << i)) -> enotsent = enotsent & ~(1 << i) -> enotrcvd = enotrcvd | (1 << i) -> SQ(i)!ItoM -> P() }
 
-    // Complete requests from peers (sending response if not sent earlier)
+    // Complete requests from peers (sending response to source if not already sent earlier)
     :: atomic { ebcmd == ItoM && enotsent == 0 && enotrcvd == 0 && esource != -1 -> if
         :: ebstate == I -> SQ(esource)!I
-        :: ebstate == M
+        :: ebstate == M -> skip
         :: ebstate == U -> SQ(esource)!U
         :: else -> assert(false)
-        fi -> ebcmd = I -> ebstate = I -> ereverse = 0 -> esource = -1 }
+        fi -> ERESET() -> P() }
 
     // Complete locally-originated request when cache space is available to hold the data
     :: atomic { ebcmd == ItoM && enotsent == 0 && enotrcvd == 0 && esource == -1 && cstate == I -> if
         :: (ebstate == M | ebstate == U) -> cstate = M
         :: else -> assert(false)
-        fi -> ebcmd = I -> ebstate = I }
+        fi -> ERESET() -> P() } -> skip
 
-        :: else -> atomic { if
-            // Simulate local cache being occupied by other address
-            :: atomic { cstate == I -> cstate = Busy }
-            :: atomic { cstate == Busy -> cstate = I }
+#if 0
+    // Simulate local resources in use due to activity at other addresses
+    :: atomic { if :: cstate == I -> cstate = Busy :: cstate == Busy -> cstate = I fi }
+    :: atomic { if :: ebcmd == I -> ebcmd = Busy :: ebcmd == Busy -> ebcmd = I }
+#endif
 
-            // Simulate evilbuffers conducting transaction for other address
-            :: atomic { ebcmd == I -> ebcmd = Busy }
-            :: atomic { ebcmd == Busy -> ebcmd = I }
+#if 0 // these assertions further explode the states
+    // If we're not in a transaction assert that the evil buffer is fully reset (just to make sure we've limited reachable states)
+    :: atomic { ebcmd == Busy || ebcmd == I -> assert(ebstate == I && enotsent == 0 && enotrcvd == 0 && ereverse == 0 && esource == -1) }
+    // If we're in ItoM transaction assert that it's not in the cache
+    :: atomic { ebcmd == ItoM -> assert(cstate == I || cstate == Busy) }
+#endif
 
-            // Launch locally-requested fills; rely on deadlock avoidance above to protect from multiple peers simultaneously deciding to do this
-            :: atomic { ebcmd == I -> ebcmd = ItoM -> enotsent = ALLPEERS -> enotrcvd = 0 -> ereverse = 0 -> esource = -1 }
+    // Launch locally-requested fills; rely on deadlock avoidance above to protect from multiple peers simultaneously deciding to do this
+    :: atomic { cstate != M && ebcmd == I -> ebcmd = ItoM -> enotsent = ALLPEERS -> esource = -1 -> P() }
 
-            // Cycle through connections to all peers to ensure fairness
-            :: atomic { i = (i + 1) % npeers }
-            fi }
+#if 1
+    // Cycle through connections to all peers to ensure fairness
+    :: atomic { noprogress < 2 -> i = (i + 1) % npeers -> if :: i == 0 -> noprogress = noprogress + 1 :: else fi }
+#else
+    :: atomic { noprogress < 2 && npeers >= 1 && (fairmask & 1) == 0 -> i = 0 -> fairmask = fairmask | 1 }
+    :: atomic { noprogress < 2 && npeers >= 2 && (fairmask & 2) == 0 -> i = 1 -> fairmask = fairmask | 2 }
+    :: atomic { noprogress < 2 && npeers >= 3 && (fairmask & 4) == 0 -> i = 2 -> fairmask = fairmask | 4 }
+    :: atomic { fairmask == (1 << npeers) - 1 -> fairmask = 0 -> noprogress = noprogress + 1 }
+#endif
     od
 
 #undef ALLPEERS