1 files changed, 115 insertions, 0 deletions

diff --git a/spin/snoopy.pml b/spin/snoopy.pml
new file mode 100644
index 0000000..4774b1a
--- /dev/null
+++ b/spin/snoopy.pml
@@ -0,0 +1,115 @@
+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)
+    ItoM, MtoI,         // commands from peers
+    Busy,               // used as both cache line state and evil buffer command to denote activity on behalf of other addresses
+}
+
+proctype dram(chan recvq; chan sendq)
+{
+    do
+    :: atomic { recvq?ItoM -> sendq!U }
+    :: atomic { recvq?MtoI -> sendq!I }
+    od
+}
+
+chan qs[6] = [1] of { mtype };
+
+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]
+
+    mtype cstate = I;       // I, M, or Busy
+    mtype ebcmd = I;        // I, ItoM, 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
+    int ereverse = 0;       // count of reverse progress
+    int esource = -1;       // source of command (-1 is originated locally)
+    int i = 0;              // current peer
+
+    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
+        :: else -> 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
+        :: 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
+        :: 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
+        :: else
+        fi }
+
+    // Send not-yet-sent snoops
+    :: atomic { ebcmd == ItoM && (enotsent & (1 << i)) -> enotsent = enotsent & ~(1 << i) -> enotrcvd = enotrcvd | (1 << i) -> SQ(i)!ItoM }
+
+    // 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
+        :: ebstate == M
+        :: ebstate == U -> SQ(esource)!U
+        :: else -> assert(false)
+        fi -> ebcmd = I -> ebstate = I -> ereverse = 0 -> esource = -1 }
+
+    // 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 }
+
+        :: else -> atomic { if
+            // Simulate local cache being occupied by other address
+            :: atomic { cstate == I -> cstate = Busy }
+            :: atomic { cstate == Busy -> cstate = I }
+
+            // Simulate evilbuffers conducting transaction for other address
+            :: atomic { ebcmd == I -> ebcmd = Busy }
+            :: atomic { ebcmd == Busy -> ebcmd = I }
+
+            // 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 }
+
+            // Cycle through connections to all peers to ensure fairness
+            :: atomic { i = (i + 1) % npeers }
+            fi }
+    od
+
+#undef ALLPEERS
+#undef RQ
+#undef SQ
+}
+
+//  C1   C2
+//    \  /
+//     C3
+//     |
+//    DRAM
+//
+// [0] is c1-to-c3
+// [1] is c2-to-c3
+// [2] is dram-to-c3
+// [3] is c3-to-c1
+// [4] is c3-to-c2
+// [5] is c3-to-dram
+
+init
+{
+    atomic {
+        run cache(3, 0, 1);     // C1   (will be proc 1)
+        run cache(4, 1, 1);     // C2   (will be proc 2)
+        run cache(0, 3, 3);     // C3   (will be proc 3)
+        run dram(qs[5], qs[2]); // dram (will be proc 4)
+    }
+}