1 /* snooping cache algorithm
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 };
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 };
25 chan claim0 = [QSZ] of { mtype };
26 chan claim1 = [QSZ] of { mtype };
27 chan release0 = [QSZ] of { mtype };
28 chan release1 = [QSZ] of { mtype };
39 :: fromcpu0!r -> tocpu0?done
40 :: fromcpu0!w -> tocpu0?done
41 :: fromcpu0!raw -> tocpu0?done
50 :: fromcpu1!r -> tocpu1?done
51 :: fromcpu1!w -> tocpu1?done
52 :: fromcpu1!raw -> tocpu1?done
71 :: (state == W) -> state = R; tobus0!CtoB
72 :: (state != W) -> tobus0!done
74 :: frombus0?MX -> state = X; tobus0!MXdone
77 :: (state == W) -> state = X; tobus0!CtoB
78 :: (state == R) -> state = X; tobus0!done
79 :: (state == X) -> tobus0!done
84 :: (state != X) -> tocpu0!done
85 :: (state == X) -> which = RD; goto buscycle
89 :: (state == W) -> tocpu0!done
90 :: (state != W) -> which = MX; goto buscycle
94 :: (state == W) -> tocpu0!done
95 :: (state != W) -> which = RX; goto buscycle
103 :: (state == W) -> state = R; tobus0!CtoB
104 :: (state != W) -> tobus0!done
106 :: frombus0?MX -> state = X; tobus0!MXdone
109 :: (state == W) -> state = X; tobus0!CtoB
110 :: (state == R) -> state = X; tobus0!done
111 :: (state == X) -> tobus0!done
115 :: (which == RD) -> state = R
116 :: (which == MX) -> state = W
117 :: (which == RX) -> state = W
125 :: (which == RD) -> tobus0!RD -> frombus0?BtoC
126 :: (which == MX) -> tobus0!MX -> frombus0?done
127 :: (which == RX) -> tobus0!RX -> frombus0?BtoC
147 :: (state == W) -> state = R; tobus1!CtoB
148 :: (state != W) -> tobus1!done
150 :: frombus1?MX -> state = X; tobus1!MXdone
153 :: (state == W) -> state = X; tobus1!CtoB
154 :: (state == R) -> state = X; tobus1!done
155 :: (state == X) -> tobus1!done
160 :: (state != X) -> tocpu1!done
161 :: (state == X) -> which = RD; goto buscycle
165 :: (state == W) -> tocpu1!done
166 :: (state != W) -> which = MX; goto buscycle
170 :: (state == W) -> tocpu1!done
171 :: (state != W) -> which = RX; goto buscycle
179 :: (state == W) -> state = R; tobus1!CtoB
180 :: (state != W) -> tobus1!done
182 :: frombus1?MX -> state = X; tobus1!MXdone
185 :: (state == W) -> state = X; tobus1!CtoB
186 :: (state == R) -> state = X; tobus1!done
187 :: (state == X) -> tobus1!done
191 :: (which == RD) -> state = R
192 :: (which == MX) -> state = W
193 :: (which == RX) -> state = W
201 :: (which == RD) -> tobus1!RD -> frombus1?BtoC
202 :: (which == MX) -> tobus1!MX -> frombus1?done
203 :: (which == RX) -> tobus1!RX -> frombus1?BtoC
208 proctype busarbiter()
218 :: claim0?req0 -> grant0!grant; release0?done
219 :: claim1?req1 -> grant1!grant; release1?done
223 proctype bus() /* models real bus + main memory */
231 :: tobus0?CtoB -> frombus1!BtoC
232 :: tobus1?CtoB -> frombus0!BtoC
234 :: tobus0?done -> /* M -> B */ frombus1!BtoC
235 :: tobus1?done -> /* M -> B */ frombus0!BtoC
237 :: tobus0?MXdone -> /* B -> M */ frombus1!done
238 :: tobus1?MXdone -> /* B -> M */ frombus0!done
240 :: tobus0?RD -> frombus1!RD
241 :: tobus1?RD -> frombus0!RD
243 :: tobus0?MX -> frombus1!MX
244 :: tobus1?MX -> frombus0!MX
246 :: tobus0?RX -> frombus1!RX
247 :: tobus1?RX -> frombus0!RX
253 run cpu0(); run cpu1();
254 run cache0(); run cache1();
255 run bus(); run busarbiter()