questionable hacks

1 files changed, 22 insertions, 16 deletions

diff --git a/spin/snoopy.pml b/spin/snoopy.pml
index 4774b1a..1aff5af 100644
--- a/spin/snoopy.pml
+++ b/spin/snoopy.pml
@@ -18,6 +18,7 @@ chan qs[6] = [1] of { mtype };
 proctype cache(int recvqbase; int sendqbase; int npeers)
 {
 #define ALLPEERS ((1 << npeers) - 1)
+#define ERESET() atomic { ebcmd = I; ebstate = I; enotsent = 0; enotrcvd = 0; ereverse = 0; esource = -1; }
 #define RQ(i) qs[recvqbase+i]
 #define SQ(i) qs[sendqbase+i]
 
@@ -47,8 +48,8 @@ proctype cache(int recvqbase; int sendqbase; int npeers)
     :: 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 }
     :: 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
+        :: atomic { ereverse > npeers && esource == -1 && enotsent == ALLPEERS -> ERESET() }
+        :: atomic { ereverse > npeers && esource != -1 && enotsent == ALLPEERS & ~(1 << esource) -> SQ(esource)!X -> ERESET() }
         :: else
         fi }
 
@@ -61,29 +62,34 @@ proctype cache(int recvqbase; int sendqbase; int npeers)
         :: ebstate == M
         :: ebstate == U -> SQ(esource)!U
         :: else -> assert(false)
-        fi -> ebcmd = I -> ebstate = I -> ereverse = 0 -> esource = -1 }
+        fi -> ERESET() }
 
     // 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() }
 
-        :: 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 cache being occupied by other address
+    :: atomic { if :: cstate == I -> cstate = Busy :: cstate == Busy -> cstate = I :: else fi }
 
-            // Simulate evilbuffers conducting transaction for other address
-            :: atomic { ebcmd == I -> ebcmd = Busy }
-            :: atomic { ebcmd == Busy -> ebcmd = I }
+    // Simulate evilbuffers conducting transaction for other address
+    :: atomic { if :: ebcmd == I -> ebcmd = Busy :: ebcmd == Busy -> ebcmd = I :: else fi }
+#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 }
+#if 0
+    // 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
 
-            // Cycle through connections to all peers to ensure fairness
-            :: atomic { i = (i + 1) % npeers }
-            fi }
+    // 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 }
+
+    // Cycle through connections to all peers to ensure fairness
+    :: atomic { i = (i + 1) % npeers }
     od
 
 #undef ALLPEERS