| 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 | } |