1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
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);
}
}
|
