From 7e93a297c4ac68a51b5b5847979827a8c5975ceb Mon Sep 17 00:00:00 2001
From: Julian Blake Kongslie
Date: Sun, 19 Mar 2023 14:22:39 -0700
Subject: Add various spin models, including one that might actually work.

---
 spin/mi.pml | 80 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 80 insertions(+)
 create mode 100644 spin/mi.pml

(limited to 'spin/mi.pml')

diff --git a/spin/mi.pml b/spin/mi.pml
new file mode 100644
index 0000000..52a384e
--- /dev/null
+++ b/spin/mi.pml
@@ -0,0 +1,80 @@
+// vim: set sw=3 :
+
+mtype {
+   I, M,
+   ItoM, MtoI, // from upstream
+   SnoopItoM, // from downstream
+   Fetch, Store,
+   Busy, Done, Fail
+}
+
+m_type cachestate; // I, M, Busy
+m_type evilstate; // I, Free, ItoM, MtoI
+int evilsource; // which upstream is the evilstate "on behalf of"; -1 is downstream
+int evilnotsent; // bitmask of upstreams we have not yet sent snoops to
+int evilnotreplied; // bitmask of upstreams that have not yet replied to snoops
+int evilnewstate; // new M/E/S/I state
+
+evil buffer:
+   state
+   bitmask of upstreams we have not yet snooped
+   bitmask of upstreams that have not yet replied
+   source of this buffer's transaction
+
+proctype cache()
+{
+   do
+   :: i = (i + 1) % N
+   :: assert(cachestate == I || cachestate == M || cachestate == Busy)
+   :: assert(evilstate == I || evilstate == ItoM || evilstate == MtoI || evilstate == SnoopItoM || evilstate == Busy)
+   :: atomic { cachestate == I -> cachestate = Busy }
+   :: atomic { cachestate == Busy -> cachestate = I }
+   :: atomic { evilstate == I -> assert(evilsource == -1 && evilnotsent == 0 && evilnotreplied == 0 && evilnewstate == I) -> evilstate = Busy }
+   :: atomic { evilstate == Busy -> assert(evilsource == -1 && evilnotsent == 0 && evilnotreplied == 0 && evilnewstate == I) -> evilstate = I }
+
+   :: downrecvq?SnoopItoM -> if
+      :: cachestate == M -> cachestate = I -> downsendq!M
+      :: else -> if
+         :: evilstate == I -> evilstate = SnoopItoM -> evilnotsent = (1 << N) - 1
+         :: else -> assert(evilstate != SnoopItoM) -> downsendq!Fail
+         fi
+      fi
+   :: atomic { (evilstate == ItoM || evilstate == SnoopItoM) && evilnotsent & (1 << i) && can send to upstream i -> evilnotsent &= ~(1 << i) -> evilnotreplied |= 1 << i -> upsendq[i]!SnoopItoM }
+   :: atomic { (evilstate == ItoM || evilstate == SnoopItoM) && evilnotsent == 0 && evilnotreplied == 0 -> if :: evilnewstate == I -> if :: evilstate == ItoM -> upsendq[evilsource]!I :: else -> downsendq!I fi :: else -> evilnewstate = I fi -> evilstate = I -> evilsource = -1 }
+   :: atomic { uprecvq[i]?I -> assert(evilstate == ItoM || evilstate == SnoopItoM) -> assert((evilnotsent & (1 << i)) == 0 && (evilnotreplied & (1 << i)) != 0)) -> evilnotreplied &= ~(1 << i) }
+   :: atomic { uprecvq[i]?M -> assert(evilstate == ItoM || evilstate == SnoopItoM) -> assert((evilnotsent & (1 << i)) == 0 && (evilnotreplied & (1 << i)) != 0)) -> evilnotreplied &= ~(1 << i) -> evilnewstate = M -> if :: evilstate == ItoM -> upsendq[evilsource]!M :: else -> downsendq!M fi }
+
+
+
+
+
+
+
+
+   :: atomic { downrep[i] is empty -> if
+      :: upreq[i]?Fetch -> if
+         :: atomic { cachestate == Busy -> uprep[i]!Fail }
+         :: atomic { cachestate == M -> uprep[i]!Done }
+         :: cachestate == I -> do
+            :: uprep[i]!Fail
+            :: atomic { evilstate == I -> evilstate = ItoM -> evilsource = i -> downreq!ItoM -> uprep[i]!Busy }
+            od
+         fi
+      :: upreq[i]?Store -> if
+         :: atomic { cachestate == Busy -> uprep[i]!Fail }
+         :: atomic { cachestate == M -> uprep[i]!Done }
+         :: cachestate == I -> do
+            :: uprep[i]!Fail
+            :: atomic { evilstate == I -> evilstate = ItoM -> evilsource = i -> downreq!ItoM -> uprep[i]!Busy }
+            od
+         fi
+      :: upreq[i]?ItoM -> if
+         :: atomic { cachestate == M -> cachestate = I -> uprep[i]!ItoM }
+         :: atomic { cachestate == I && evilstate == I -> if
+            :: can send downstream -> evilstate = SnoopItoM -> evilsource = i -> assert(evilwaiting == 0) ->
+               j = 0 -> do :: j < N -> if :: i != j -> upsnoop[j]!SnoopItoM -> evilwaiting |= 1 << j :: else fi -> j = j + 1 :: else -> break fi od ->
+               uprep[i]!Busy
+            :: !can send downstream -> uprep[i]!Fail
+            fi }
+         fi
+
-- 
cgit v1.2.3