Add spontaneous evictions.HEADmain

1 files changed, 39 insertions, 16 deletions

diff --git a/spin/snoopy.pml b/spin/snoopy.pml
index 1aff5af..3d22d21 100644
--- a/spin/snoopy.pml
+++ b/spin/snoopy.pml
@@ -1,6 +1,6 @@
 mtype {
     I, M,               // valid cache line states: invalid, modified
-    U, X,               // fill/snoop responses that are not valid cache line states: unknown (from DRAM only), fail (you have to try again)
+    U, X,               // evict/fill/snoop responses that are not valid cache line states: unknown (from DRAM only), fail (you have to try again)
     ItoM, MtoI,         // commands from peers
     Busy,               // used as both cache line state and evil buffer command to denote activity on behalf of other addresses
 }
@@ -23,7 +23,7 @@ proctype cache(int recvqbase; int sendqbase; int npeers)
 #define SQ(i) qs[sendqbase+i]
 
     mtype cstate = I;       // I, M, or Busy
-    mtype ebcmd = I;        // I, ItoM, or Busy
+    mtype ebcmd = I;        // I, ItoM, MtoI, or Busy
     int ebstate = I;        // I, M, or U
     int enotsent = 0;       // bitmask of snoops remaining to send
     int enotrcvd = 0;       // bitmask of replies remaining to receive
@@ -36,26 +36,48 @@ proctype cache(int recvqbase; int sendqbase; int npeers)
     :: 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 == I && ebcmd == MtoI && enotsent != 0 -> ERESET() -> SQ(i)!M
         :: else -> SQ(i)!X
         fi }
 
+    // Receive eviction request from peer
+    :: atomic { RQ(i)?MtoI -> if
+        :: cstate == M || ebcmd == MtoI -> assert(false)
+        :: cstate == I && ebcmd == I -> cstate = M -> SQ(i)!I
+//        :: cstate == I && ebcmd == ItoM -> ebstate = M -> enotsent = 0 -> SQ(i)!I // Missing logic: cut-through send to esource, clear out eb when enotrcvd is already 0
+        :: cstate == I && ebcmd == ItoM -> SQ(i)!X
+        :: cstate == I && ebcmd == Busy -> cstate = M -> SQ(i)!I
+        :: cstate == Busy && ebcmd == I -> assert(i != npeers-1) -> ebcmd = MtoI -> enotsent = 1 << (npeers-1) -> SQ(i)!I
+        :: cstate == Busy && ebcmd != I -> SQ(i)!X
+        fi }
+
     // 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)?M -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> ebstate = M -> if
+    :: atomic { RQ(i)?I -> assert((enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> if
+        :: ebcmd == ItoM -> enotrcvd = enotrcvd & ~(1 << i)
+        :: ebcmd == MtoI -> ERESET()
+        :: else -> assert(false)
+        fi }
+    :: atomic { RQ(i)?M -> assert(ebcmd == ItoM) -> assert((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 }
-    :: 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
-        :: atomic { ereverse > npeers && esource == -1 && enotsent == ALLPEERS -> ERESET() }
-        :: atomic { ereverse > npeers && esource != -1 && enotsent == ALLPEERS & ~(1 << esource) -> SQ(esource)!X -> ERESET() }
-        :: else
+    :: atomic { RQ(i)?U -> assert(ebcmd == ItoM) -> assert((enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> if :: ebstate == I -> ebstate = U :: else fi }
+    :: atomic { RQ(i)?X -> assert((enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> enotsent = enotsent | (1 << i) -> if
+        :: ebcmd == ItoM -> ereverse = ereverse + 1 -> if
+            :: atomic { ereverse > npeers && esource == -1 && enotsent == ALLPEERS -> ERESET() }
+            :: atomic { ereverse > npeers - 1 && esource != -1 && enotsent == ALLPEERS & ~(1 << esource) -> SQ(esource)!X -> ERESET() }
+            :: else
+            fi
+        :: ebcmd == MtoI
+        :: else -> assert(false)
         fi }
 
     // Send not-yet-sent snoops
     :: atomic { ebcmd == ItoM && (enotsent & (1 << i)) -> enotsent = enotsent & ~(1 << i) -> enotrcvd = enotrcvd | (1 << i) -> SQ(i)!ItoM }
 
+    // Send not-yet-sent evictions
+    :: atomic { ebcmd == MtoI && (enotsent & (1 << i)) -> enotsent = enotsent & ~(1 << i) -> enotrcvd = enotrcvd | (1 << i) -> SQ(i)!MtoI }
+
     // Complete requests from peers (sending response if not sent earlier)
     :: atomic { ebcmd == ItoM && enotsent == 0 && enotrcvd == 0 && esource != -1 -> if
         :: ebstate == I -> SQ(esource)!I
@@ -70,20 +92,21 @@ proctype cache(int recvqbase; int sendqbase; int npeers)
         :: else -> assert(false)
         fi -> ERESET() }
 
-#if 0
     // Simulate local cache being occupied by other address
-    :: atomic { if :: cstate == I -> cstate = Busy :: cstate == Busy -> cstate = I :: else fi }
+    :: atomic { cstate == I -> cstate = Busy }
+    :: atomic { cstate == Busy -> cstate = I }
 
     // Simulate evilbuffers conducting transaction for other address
-    :: atomic { if :: ebcmd == I -> ebcmd = Busy :: ebcmd == Busy -> ebcmd = I :: else fi }
-#endif
+    :: atomic { ebcmd == I -> ebcmd = Busy }
+    :: atomic { ebcmd == Busy -> ebcmd = I }
+
+    // Simulate local cache spontaneously evicting
+    :: atomic { cstate == M && ebcmd == I -> cstate = I -> ebcmd = MtoI -> enotsent = 1 << (npeers-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
 
     // 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 }