Add various spin models, including one that might actually work.

1 files changed, 132 insertions, 0 deletions

diff --git a/spin/mesi.pml b/spin/mesi.pml
new file mode 100644
index 0000000..5bb1c69
--- /dev/null
+++ b/spin/mesi.pml
@@ -0,0 +1,132 @@
+// vim: set sw=3 :
+
+mtype { FETCH, FETCHDONE, STORE, STOREDONE, FILLREQ, FILLRESP, EVICT, SNOOP, SNOOPRESP, NACK, M, E, S, I }
+#define CACHE00 0
+#define CACHE01 1
+#define CACHE10 2
+#define NUM_CACHES 3
+
+// System diagram
+//
+// CPU0    CPU1
+// |       |
+// CACHE00  CACHE01
+// |       |
+// CACHE10-+
+// |
+// DRAM
+//
+// c2m queues are named c2m_<receiving process>, e.g. c2m_cache10
+//
+// m2c queues are stored in the global m2c_info array so that they can be found as needed for snoops
+
+typedef m2c_info_t {
+   chan m2c;
+   int snoops_from;
+}
+
+m2c_info_t m2c_info[2];
+
+#define C2M_T [0] of {mtype /* message type */, chan /* response channel */, mtype /* have */, mtype /* want */}
+#define M2C_T [0] of {mtype /* message type */, mtype /* result */}
+
+proctype dram(chan c2m)
+{
+   chan r;
+   mtype want;
+   do
+   :: c2m?FETCH,r,_,_ -> r!FETCHDONE,S
+   :: c2m?STORE,r,_,_ -> r!STOREDONE,M
+   :: c2m?FILLREQ,r,_,want -> r!FILLRESP,want
+   :: c2m?EVICT,r,_,want
+   od
+}
+
+proctype cache(chan up; chan down; chan m2c; int whoami)
+{
+   chan r;
+   mtype cachestate = I; // this should be part of a global array so we can assert that at most one cache has M or E state
+   do
+   :: up?FETCH,r,_,_ -> if
+      :: /* no buffer available */ r!NACK,I
+      :: cachestate != I -> r!FETCHDONE,S
+      :: cachestate == I -> down!FILLREQ,m2c,cachestate,S ->
+         do
+         :: if
+            :: atomic { m2c?FILLRESP,cachestate -> r!FETCHDONE,S -> break }
+            :: atomic { m2c?NACK,_ -> down!FILLREQ,m2c,cachestate,S }
+            :: atomic { m2c?SNOOP,_ -> down!SNOOPRESP,m2c,cachestate,I }
+            fi
+         od
+      fi
+   :: up?STORE,r,_,_
+   :: up?FILLREQ,r,_,S
+   :: up?FILLREQ,r,_,E
+   :: up?EVICT,r,M,I -> atomic { assert(cachestate == I) -> cachestate = M }
+   :: up?EVICT,r,M,I -> atomic { assert(cachestate == I) -> down!EVICT,m2c,M,I }
+   :: m2c?SNOOP,E -> atomic { down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
+   :: m2c?SNOOP,E -> if
+      :: atomic { cachestate == M -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
+      :: atomic { cachestate == E -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
+      :: atomic { cachestate == S -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
+      :: atomic { cachestate == I -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
+      fi
+   :: m2c?SNOOP,S -> if
+      :: atomic { cachestate == M -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
+      :: atomic { cachestate == E -> down!SNOOPRESP,m2c,cachestate,S -> cachestate = S }
+      :: atomic { cachestate == S -> down!SNOOPRESP,m2c,cachestate,cachestate }
+      :: atomic { cachestate == I -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,downgraded_cachestate -> cachestate = downgraded_cachestate }
+      fi
+   :: atomic { cachestate == M -> down!EVICT,m2c,cachestate,I -> cachestate = I }
+   od
+}
+
+proctype cpu(chan c2m; chan m2c)
+{
+progress:
+   do
+   :: do
+      :: c2m!FETCH,m2c,I,S -> if
+         :: m2c?FETCHDONE,_ -> break
+         :: m2c?NACK,_
+         fi
+      od
+   :: do
+      :: c2m!STORE,m2c,I,M -> if
+         :: m2c?STOREDONE,_ -> break
+         :: m2c?NACK,_
+         fi
+      od
+   od
+}
+
+init
+{
+   // downstream channels
+   chan c2m_cache00 = C2M_T;
+   chan c2m_cache01 = C2M_T;
+   chan c2m_cache10 = C2M_T;
+   chan c2m_dram = C2M_T;
+
+   // upstream channels
+   chan m2c_cpu0 = M2C_T;
+   chan m2c_cpu1 = M2C_T;
+   chan m2c_cache00 = M2C_T;
+   chan m2c_cache01 = M2C_T;
+   chan m2c_cache10 = M2C_T;
+
+   atomic
+   {
+      // construct snoop table
+      m2c_info[0].m2c = m2c_cache00; m2c_info[0].snoops_from = CACHE10;
+      m2c_info[1].m2c = m2c_cache01; m2c_info[1].snoops_from = CACHE10;
+
+      // construct processes
+      run cpu(c2m_cache00, m2c_cpu0);
+      run cpu(c2m_cache01, m2c_cpu1);
+      run cache(c2m_cache00, c2m_cache10, m2c_cache00, CACHE00);
+      run cache(c2m_cache01, c2m_cache10, m2c_cache01, CACHE01);
+      run cache(c2m_cache10, c2m_dram, m2c_cache10, CACHE10);
+      run dram(c2m_dram);
+   }
+}