0b55f123 |
1 | /* snooping cache algorithm |
2 | */ |
3 | #define QSZ 2 |
4 | |
5 | mtype = { r, w, raw, |
6 | RD, WR, RX, |
7 | MX, MXdone, |
8 | req0, req1, |
9 | CtoB, BtoC, |
10 | grant, done |
11 | }; |
12 | |
13 | chan tocpu0 = [QSZ] of { mtype }; |
14 | chan fromcpu0 = [QSZ] of { mtype }; |
15 | chan tobus0 = [QSZ] of { mtype }; |
16 | chan frombus0 = [QSZ] of { mtype }; |
17 | chan grant0 = [QSZ] of { mtype }; |
18 | |
19 | chan tocpu1 = [QSZ] of { mtype }; |
20 | chan fromcpu1 = [QSZ] of { mtype }; |
21 | chan tobus1 = [QSZ] of { mtype }; |
22 | chan frombus1 = [QSZ] of { mtype }; |
23 | chan grant1 = [QSZ] of { mtype }; |
24 | |
25 | chan claim0 = [QSZ] of { mtype }; |
26 | chan claim1 = [QSZ] of { mtype }; |
27 | chan release0 = [QSZ] of { mtype }; |
28 | chan release1 = [QSZ] of { mtype }; |
29 | |
30 | #define W 1 |
31 | #define R 2 |
32 | #define X 3 |
33 | |
34 | proctype cpu0() |
35 | { |
36 | xs fromcpu0; |
37 | xr tocpu0; |
38 | do |
39 | :: fromcpu0!r -> tocpu0?done |
40 | :: fromcpu0!w -> tocpu0?done |
41 | :: fromcpu0!raw -> tocpu0?done |
42 | od |
43 | } |
44 | |
45 | proctype cpu1() |
46 | { |
47 | xs fromcpu1; |
48 | xr tocpu1; |
49 | do |
50 | :: fromcpu1!r -> tocpu1?done |
51 | :: fromcpu1!w -> tocpu1?done |
52 | :: fromcpu1!raw -> tocpu1?done |
53 | od |
54 | } |
55 | |
56 | proctype cache0() |
57 | { byte state = X; |
58 | byte which; |
59 | |
60 | xr frombus0; |
61 | xr fromcpu0; |
62 | xs tocpu0; |
63 | xs tobus0; |
64 | xr grant0; |
65 | xs claim0; |
66 | xs release0; |
67 | resume: |
68 | do |
69 | :: frombus0?RD -> |
70 | if |
71 | :: (state == W) -> state = R; tobus0!CtoB |
72 | :: (state != W) -> tobus0!done |
73 | fi |
74 | :: frombus0?MX -> state = X; tobus0!MXdone |
75 | :: frombus0?RX -> |
76 | if |
77 | :: (state == W) -> state = X; tobus0!CtoB |
78 | :: (state == R) -> state = X; tobus0!done |
79 | :: (state == X) -> tobus0!done |
80 | fi |
81 | |
82 | :: fromcpu0?r -> |
83 | if |
84 | :: (state != X) -> tocpu0!done |
85 | :: (state == X) -> which = RD; goto buscycle |
86 | fi |
87 | :: fromcpu0?w -> |
88 | if |
89 | :: (state == W) -> tocpu0!done |
90 | :: (state != W) -> which = MX; goto buscycle |
91 | fi |
92 | :: fromcpu0?raw -> |
93 | if |
94 | :: (state == W) -> tocpu0!done |
95 | :: (state != W) -> which = RX; goto buscycle |
96 | fi |
97 | od; |
98 | buscycle: |
99 | claim0!req0; |
100 | do |
101 | :: frombus0?RD -> |
102 | if |
103 | :: (state == W) -> state = R; tobus0!CtoB |
104 | :: (state != W) -> tobus0!done |
105 | fi |
106 | :: frombus0?MX -> state = X; tobus0!MXdone |
107 | :: frombus0?RX -> |
108 | if |
109 | :: (state == W) -> state = X; tobus0!CtoB |
110 | :: (state == R) -> state = X; tobus0!done |
111 | :: (state == X) -> tobus0!done |
112 | fi |
113 | :: grant0?grant -> |
114 | if |
115 | :: (which == RD) -> state = R |
116 | :: (which == MX) -> state = W |
117 | :: (which == RX) -> state = W |
118 | fi; |
119 | tocpu0!done; |
120 | break |
121 | od; |
122 | release0!done; |
123 | |
124 | if |
125 | :: (which == RD) -> tobus0!RD -> frombus0?BtoC |
126 | :: (which == MX) -> tobus0!MX -> frombus0?done |
127 | :: (which == RX) -> tobus0!RX -> frombus0?BtoC |
128 | fi; |
129 | goto resume |
130 | } |
131 | |
132 | proctype cache1() |
133 | { byte state = X; |
134 | byte which; |
135 | |
136 | xr frombus1; |
137 | xr fromcpu1; |
138 | xs tobus1; |
139 | xs tocpu1; |
140 | xr grant1; |
141 | xs claim1; |
142 | xs release1; |
143 | resume: |
144 | do |
145 | :: frombus1?RD -> |
146 | if |
147 | :: (state == W) -> state = R; tobus1!CtoB |
148 | :: (state != W) -> tobus1!done |
149 | fi |
150 | :: frombus1?MX -> state = X; tobus1!MXdone |
151 | :: frombus1?RX -> |
152 | if |
153 | :: (state == W) -> state = X; tobus1!CtoB |
154 | :: (state == R) -> state = X; tobus1!done |
155 | :: (state == X) -> tobus1!done |
156 | fi |
157 | |
158 | :: fromcpu1?r -> |
159 | if |
160 | :: (state != X) -> tocpu1!done |
161 | :: (state == X) -> which = RD; goto buscycle |
162 | fi |
163 | :: fromcpu1?w -> |
164 | if |
165 | :: (state == W) -> tocpu1!done |
166 | :: (state != W) -> which = MX; goto buscycle |
167 | fi |
168 | :: fromcpu1?raw -> |
169 | if |
170 | :: (state == W) -> tocpu1!done |
171 | :: (state != W) -> which = RX; goto buscycle |
172 | fi |
173 | od; |
174 | buscycle: |
175 | claim1!req1; |
176 | do |
177 | :: frombus1?RD -> |
178 | if |
179 | :: (state == W) -> state = R; tobus1!CtoB |
180 | :: (state != W) -> tobus1!done |
181 | fi |
182 | :: frombus1?MX -> state = X; tobus1!MXdone |
183 | :: frombus1?RX -> |
184 | if |
185 | :: (state == W) -> state = X; tobus1!CtoB |
186 | :: (state == R) -> state = X; tobus1!done |
187 | :: (state == X) -> tobus1!done |
188 | fi |
189 | :: grant1?grant -> |
190 | if |
191 | :: (which == RD) -> state = R |
192 | :: (which == MX) -> state = W |
193 | :: (which == RX) -> state = W |
194 | fi; |
195 | tocpu1!done; |
196 | break |
197 | od; |
198 | release1!done; |
199 | |
200 | if |
201 | :: (which == RD) -> tobus1!RD -> frombus1?BtoC |
202 | :: (which == MX) -> tobus1!MX -> frombus1?done |
203 | :: (which == RX) -> tobus1!RX -> frombus1?BtoC |
204 | fi; |
205 | goto resume |
206 | } |
207 | |
208 | proctype busarbiter() |
209 | { |
210 | xs grant0; |
211 | xs grant1; |
212 | xr claim0; |
213 | xr claim1; |
214 | xr release0; |
215 | xr release1; |
216 | |
217 | do |
218 | :: claim0?req0 -> grant0!grant; release0?done |
219 | :: claim1?req1 -> grant1!grant; release1?done |
220 | od |
221 | } |
222 | |
223 | proctype bus() /* models real bus + main memory */ |
224 | { |
225 | xs frombus1; |
226 | xs frombus0; |
227 | xr tobus0; |
228 | xr tobus1; |
229 | |
230 | do |
231 | :: tobus0?CtoB -> frombus1!BtoC |
232 | :: tobus1?CtoB -> frombus0!BtoC |
233 | |
234 | :: tobus0?done -> /* M -> B */ frombus1!BtoC |
235 | :: tobus1?done -> /* M -> B */ frombus0!BtoC |
236 | |
237 | :: tobus0?MXdone -> /* B -> M */ frombus1!done |
238 | :: tobus1?MXdone -> /* B -> M */ frombus0!done |
239 | |
240 | :: tobus0?RD -> frombus1!RD |
241 | :: tobus1?RD -> frombus0!RD |
242 | |
243 | :: tobus0?MX -> frombus1!MX |
244 | :: tobus1?MX -> frombus0!MX |
245 | |
246 | :: tobus0?RX -> frombus1!RX |
247 | :: tobus1?RX -> frombus0!RX |
248 | od |
249 | } |
250 | |
251 | init { |
252 | atomic { |
253 | run cpu0(); run cpu1(); |
254 | run cache0(); run cache1(); |
255 | run bus(); run busarbiter() |
256 | } |
257 | } |