summaryrefslogtreecommitdiff
path: root/spin
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--spin/Makefile11
-rw-r--r--spin/mesi.pml132
-rw-r--r--spin/mi.pml80
-rw-r--r--spin/snoopy.pml115
4 files changed, 338 insertions, 0 deletions
diff --git a/spin/Makefile b/spin/Makefile
new file mode 100644
index 0000000..73669f9
--- /dev/null
+++ b/spin/Makefile
@@ -0,0 +1,11 @@
1default: $(addsuffix .trail, $(wildcard *.pml))
2
3clean:
4 rm -f pan* *.pml.*
5
6%.pml.trail: %.pml
7 @rm -f $@
8 spin -search -bitstate -l $< | egrep '^(pan|spin):'
9 [ ! -e $@ ] || spin -c -g -l -p -replay $<
10
11.SECONDARY:
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 @@
1// vim: set sw=3 :
2
3mtype { FETCH, FETCHDONE, STORE, STOREDONE, FILLREQ, FILLRESP, EVICT, SNOOP, SNOOPRESP, NACK, M, E, S, I }
4#define CACHE00 0
5#define CACHE01 1
6#define CACHE10 2
7#define NUM_CACHES 3
8
9// System diagram
10//
11// CPU0 CPU1
12// | |
13// CACHE00 CACHE01
14// | |
15// CACHE10-+
16// |
17// DRAM
18//
19// c2m queues are named c2m_<receiving process>, e.g. c2m_cache10
20//
21// m2c queues are stored in the global m2c_info array so that they can be found as needed for snoops
22
23typedef m2c_info_t {
24 chan m2c;
25 int snoops_from;
26}
27
28m2c_info_t m2c_info[2];
29
30#define C2M_T [0] of {mtype /* message type */, chan /* response channel */, mtype /* have */, mtype /* want */}
31#define M2C_T [0] of {mtype /* message type */, mtype /* result */}
32
33proctype dram(chan c2m)
34{
35 chan r;
36 mtype want;
37 do
38 :: c2m?FETCH,r,_,_ -> r!FETCHDONE,S
39 :: c2m?STORE,r,_,_ -> r!STOREDONE,M
40 :: c2m?FILLREQ,r,_,want -> r!FILLRESP,want
41 :: c2m?EVICT,r,_,want
42 od
43}
44
45proctype cache(chan up; chan down; chan m2c; int whoami)
46{
47 chan r;
48 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
49 do
50 :: up?FETCH,r,_,_ -> if
51 :: /* no buffer available */ r!NACK,I
52 :: cachestate != I -> r!FETCHDONE,S
53 :: cachestate == I -> down!FILLREQ,m2c,cachestate,S ->
54 do
55 :: if
56 :: atomic { m2c?FILLRESP,cachestate -> r!FETCHDONE,S -> break }
57 :: atomic { m2c?NACK,_ -> down!FILLREQ,m2c,cachestate,S }
58 :: atomic { m2c?SNOOP,_ -> down!SNOOPRESP,m2c,cachestate,I }
59 fi
60 od
61 fi
62 :: up?STORE,r,_,_
63 :: up?FILLREQ,r,_,S
64 :: up?FILLREQ,r,_,E
65 :: up?EVICT,r,M,I -> atomic { assert(cachestate == I) -> cachestate = M }
66 :: up?EVICT,r,M,I -> atomic { assert(cachestate == I) -> down!EVICT,m2c,M,I }
67 :: m2c?SNOOP,E -> atomic { down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
68 :: m2c?SNOOP,E -> if
69 :: atomic { cachestate == M -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
70 :: atomic { cachestate == E -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
71 :: atomic { cachestate == S -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
72 :: atomic { cachestate == I -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
73 fi
74 :: m2c?SNOOP,S -> if
75 :: atomic { cachestate == M -> down!SNOOPRESP,m2c,cachestate,I -> cachestate = I }
76 :: atomic { cachestate == E -> down!SNOOPRESP,m2c,cachestate,S -> cachestate = S }
77 :: atomic { cachestate == S -> down!SNOOPRESP,m2c,cachestate,cachestate }
78 :: atomic { cachestate == I -> /* fixme propagate snoop upstream */ /* fixme wait for responses, possibly changing cachestate */ down!SNOOPRESP,m2c,cachestate,downgraded_cachestate -> cachestate = downgraded_cachestate }
79 fi
80 :: atomic { cachestate == M -> down!EVICT,m2c,cachestate,I -> cachestate = I }
81 od
82}
83
84proctype cpu(chan c2m; chan m2c)
85{
86progress:
87 do
88 :: do
89 :: c2m!FETCH,m2c,I,S -> if
90 :: m2c?FETCHDONE,_ -> break
91 :: m2c?NACK,_
92 fi
93 od
94 :: do
95 :: c2m!STORE,m2c,I,M -> if
96 :: m2c?STOREDONE,_ -> break
97 :: m2c?NACK,_
98 fi
99 od
100 od
101}
102
103init
104{
105 // downstream channels
106 chan c2m_cache00 = C2M_T;
107 chan c2m_cache01 = C2M_T;
108 chan c2m_cache10 = C2M_T;
109 chan c2m_dram = C2M_T;
110
111 // upstream channels
112 chan m2c_cpu0 = M2C_T;
113 chan m2c_cpu1 = M2C_T;
114 chan m2c_cache00 = M2C_T;
115 chan m2c_cache01 = M2C_T;
116 chan m2c_cache10 = M2C_T;
117
118 atomic
119 {
120 // construct snoop table
121 m2c_info[0].m2c = m2c_cache00; m2c_info[0].snoops_from = CACHE10;
122 m2c_info[1].m2c = m2c_cache01; m2c_info[1].snoops_from = CACHE10;
123
124 // construct processes
125 run cpu(c2m_cache00, m2c_cpu0);
126 run cpu(c2m_cache01, m2c_cpu1);
127 run cache(c2m_cache00, c2m_cache10, m2c_cache00, CACHE00);
128 run cache(c2m_cache01, c2m_cache10, m2c_cache01, CACHE01);
129 run cache(c2m_cache10, c2m_dram, m2c_cache10, CACHE10);
130 run dram(c2m_dram);
131 }
132}
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 @@
1// vim: set sw=3 :
2
3mtype {
4 I, M,
5 ItoM, MtoI, // from upstream
6 SnoopItoM, // from downstream
7 Fetch, Store,
8 Busy, Done, Fail
9}
10
11m_type cachestate; // I, M, Busy
12m_type evilstate; // I, Free, ItoM, MtoI
13int evilsource; // which upstream is the evilstate "on behalf of"; -1 is downstream
14int evilnotsent; // bitmask of upstreams we have not yet sent snoops to
15int evilnotreplied; // bitmask of upstreams that have not yet replied to snoops
16int evilnewstate; // new M/E/S/I state
17
18evil buffer:
19 state
20 bitmask of upstreams we have not yet snooped
21 bitmask of upstreams that have not yet replied
22 source of this buffer's transaction
23
24proctype cache()
25{
26 do
27 :: i = (i + 1) % N
28 :: assert(cachestate == I || cachestate == M || cachestate == Busy)
29 :: assert(evilstate == I || evilstate == ItoM || evilstate == MtoI || evilstate == SnoopItoM || evilstate == Busy)
30 :: atomic { cachestate == I -> cachestate = Busy }
31 :: atomic { cachestate == Busy -> cachestate = I }
32 :: atomic { evilstate == I -> assert(evilsource == -1 && evilnotsent == 0 && evilnotreplied == 0 && evilnewstate == I) -> evilstate = Busy }
33 :: atomic { evilstate == Busy -> assert(evilsource == -1 && evilnotsent == 0 && evilnotreplied == 0 && evilnewstate == I) -> evilstate = I }
34
35 :: downrecvq?SnoopItoM -> if
36 :: cachestate == M -> cachestate = I -> downsendq!M
37 :: else -> if
38 :: evilstate == I -> evilstate = SnoopItoM -> evilnotsent = (1 << N) - 1
39 :: else -> assert(evilstate != SnoopItoM) -> downsendq!Fail
40 fi
41 fi
42 :: atomic { (evilstate == ItoM || evilstate == SnoopItoM) && evilnotsent & (1 << i) && can send to upstream i -> evilnotsent &= ~(1 << i) -> evilnotreplied |= 1 << i -> upsendq[i]!SnoopItoM }
43 :: 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 }
44 :: atomic { uprecvq[i]?I -> assert(evilstate == ItoM || evilstate == SnoopItoM) -> assert((evilnotsent & (1 << i)) == 0 && (evilnotreplied & (1 << i)) != 0)) -> evilnotreplied &= ~(1 << i) }
45 :: 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 }
46
47
48
49
50
51
52
53
54 :: atomic { downrep[i] is empty -> if
55 :: upreq[i]?Fetch -> if
56 :: atomic { cachestate == Busy -> uprep[i]!Fail }
57 :: atomic { cachestate == M -> uprep[i]!Done }
58 :: cachestate == I -> do
59 :: uprep[i]!Fail
60 :: atomic { evilstate == I -> evilstate = ItoM -> evilsource = i -> downreq!ItoM -> uprep[i]!Busy }
61 od
62 fi
63 :: upreq[i]?Store -> if
64 :: atomic { cachestate == Busy -> uprep[i]!Fail }
65 :: atomic { cachestate == M -> uprep[i]!Done }
66 :: cachestate == I -> do
67 :: uprep[i]!Fail
68 :: atomic { evilstate == I -> evilstate = ItoM -> evilsource = i -> downreq!ItoM -> uprep[i]!Busy }
69 od
70 fi
71 :: upreq[i]?ItoM -> if
72 :: atomic { cachestate == M -> cachestate = I -> uprep[i]!ItoM }
73 :: atomic { cachestate == I && evilstate == I -> if
74 :: can send downstream -> evilstate = SnoopItoM -> evilsource = i -> assert(evilwaiting == 0) ->
75 j = 0 -> do :: j < N -> if :: i != j -> upsnoop[j]!SnoopItoM -> evilwaiting |= 1 << j :: else fi -> j = j + 1 :: else -> break fi od ->
76 uprep[i]!Busy
77 :: !can send downstream -> uprep[i]!Fail
78 fi }
79 fi
80
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 @@
1mtype {
2 I, M, // valid cache line states: invalid, modified
3 U, X, // fill/snoop responses that are not valid cache line states: unknown (from DRAM only), fail (you have to try again)
4 ItoM, MtoI, // commands from peers
5 Busy, // used as both cache line state and evil buffer command to denote activity on behalf of other addresses
6}
7
8proctype dram(chan recvq; chan sendq)
9{
10 do
11 :: atomic { recvq?ItoM -> sendq!U }
12 :: atomic { recvq?MtoI -> sendq!I }
13 od
14}
15
16chan qs[6] = [1] of { mtype };
17
18proctype cache(int recvqbase; int sendqbase; int npeers)
19{
20#define ALLPEERS ((1 << npeers) - 1)
21#define RQ(i) qs[recvqbase+i]
22#define SQ(i) qs[sendqbase+i]
23
24 mtype cstate = I; // I, M, or Busy
25 mtype ebcmd = I; // I, ItoM, or Busy
26 int ebstate = I; // I, M, or U
27 int enotsent = 0; // bitmask of snoops remaining to send
28 int enotrcvd = 0; // bitmask of replies remaining to receive
29 int ereverse = 0; // count of reverse progress
30 int esource = -1; // source of command (-1 is originated locally)
31 int i = 0; // current peer
32
33 do
34 // Receive fill request from peer
35 :: atomic { RQ(i)?ItoM -> if
36 :: cstate == M -> cstate = I -> SQ(i)!M
37 :: cstate == I && ebcmd == I -> ebcmd = ItoM -> enotsent = ALLPEERS & ~(1 << i) -> esource = i
38 :: else -> SQ(i)!X
39 fi }
40
41 // Receive fill responses from peers
42 :: atomic { RQ(i)?I -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) }
43 :: atomic { RQ(i)?M -> assert(ebcmd == ItoM && (enotsent & (1 << i)) == 0 && (enotrcvd & (1 << i)) != 0) -> enotrcvd = enotrcvd & ~(1 << i) -> ebstate = M -> if
44 :: esource != -1 -> SQ(esource)!M
45 :: else /* ideally put it into the cache right away */
46 fi }
47 :: 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 }
48 :: 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
49 // To prevent deadlock, if we get X'd too many times abandon the transaction and send X to its source
50 :: ereverse > npeers && esource == -1 && enotsent == ALLPEERS -> ebcmd = I -> ebstate = I -> enotsent = 0 -> ereverse = 0 -> esource = -1
51 :: ereverse > npeers && esource != -1 && enotsent == ALLPEERS & ~(1 << esource) -> SQ(esource)!X -> ebcmd = I -> ebstate = I -> enotsent = 0 -> ereverse = 0 -> esource = -1
52 :: else
53 fi }
54
55 // Send not-yet-sent snoops
56 :: atomic { ebcmd == ItoM && (enotsent & (1 << i)) -> enotsent = enotsent & ~(1 << i) -> enotrcvd = enotrcvd | (1 << i) -> SQ(i)!ItoM }
57
58 // Complete requests from peers (sending response if not sent earlier)
59 :: atomic { ebcmd == ItoM && enotsent == 0 && enotrcvd == 0 && esource != -1 -> if
60 :: ebstate == I -> SQ(esource)!I
61 :: ebstate == M
62 :: ebstate == U -> SQ(esource)!U
63 :: else -> assert(false)
64 fi -> ebcmd = I -> ebstate = I -> ereverse = 0 -> esource = -1 }
65
66 // Complete locally-originated request when cache space is available to hold the data
67 :: atomic { ebcmd == ItoM && enotsent == 0 && enotrcvd == 0 && esource == -1 && cstate == I -> if
68 :: (ebstate == M | ebstate == U) -> cstate = M
69 :: else -> assert(false)
70 fi -> ebcmd = I -> ebstate = I }
71
72 :: else -> atomic { if
73 // Simulate local cache being occupied by other address
74 :: atomic { cstate == I -> cstate = Busy }
75 :: atomic { cstate == Busy -> cstate = I }
76
77 // Simulate evilbuffers conducting transaction for other address
78 :: atomic { ebcmd == I -> ebcmd = Busy }
79 :: atomic { ebcmd == Busy -> ebcmd = I }
80
81 // Launch locally-requested fills; rely on deadlock avoidance above to protect from multiple peers simultaneously deciding to do this
82 :: atomic { ebcmd == I -> ebcmd = ItoM -> enotsent = ALLPEERS -> enotrcvd = 0 -> ereverse = 0 -> esource = -1 }
83
84 // Cycle through connections to all peers to ensure fairness
85 :: atomic { i = (i + 1) % npeers }
86 fi }
87 od
88
89#undef ALLPEERS
90#undef RQ
91#undef SQ
92}
93
94// C1 C2
95// \ /
96// C3
97// |
98// DRAM
99//
100// [0] is c1-to-c3
101// [1] is c2-to-c3
102// [2] is dram-to-c3
103// [3] is c3-to-c1
104// [4] is c3-to-c2
105// [5] is c3-to-dram
106
107init
108{
109 atomic {
110 run cache(3, 0, 1); // C1 (will be proc 1)
111 run cache(4, 1, 1); // C2 (will be proc 2)
112 run cache(0, 3, 3); // C3 (will be proc 3)
113 run dram(qs[5], qs[2]); // dram (will be proc 4)
114 }
115}
generated by cgit v1.2.3 (git 2.51.0) at 2026-04-18 23:14:49 -0700