|
214 | 214 | # An acquire atomic operation followed by a memory access also matches above |
215 | 215 | -safe [A Amo.Swp PodW* ExpObs] [A Amo.Swp PosWR ExpObs] |
216 | 216 | -safe [A Amo.Cas PodW* ExpObs] [A Amo.Cas PosWR ExpObs] |
| 217 | +-safe [A Amo.StAdd PodW* ExpObs] [A Amo.StAdd PosWR ExpObs] |
| 218 | +-safe [A Amo.LdAdd PodW* ExpObs] [A Amo.LdAdd PosWR ExpObs] |
217 | 219 | -safe [A LxSx PodW* ExpObs] [A LxSx PosWR ExpObs] |
218 | | --safe [Q Amo.Swp PodW* ExpObs] [Q Amo.Swp PosWR ExpObs] |
219 | | --safe [Q Amo.Cas PodW* ExpObs] [Q Amo.Cas PosWR ExpObs] |
220 | 220 | -safe [Q LxSx PodW* ExpObs] [Q LxSx PosWR ExpObs] |
221 | 221 | #[A|Q rmw PosWW] is stronger than `Pos*W` |
222 | | -#-safe [A Amo.Swp PosWW] [A Amo.Cas PosWW] [Q Amo.Swp PosWW] [Q Amo.Cas PosWW] [A LxSx PosWW] [Q LxSx PosWW] |
| 222 | +#-safe [A Amo.Swp PosWW] [A Amo.Cas PosWW] [A Amo.StAdd PosWW] [A Amo.LdAdd PosWW] [A LxSx PosWW] [Q LxSx PosWW] |
223 | 223 |
|
224 | 224 | # TODO |
225 | 225 | # let bob = [Exp & M | Imp & Tag & R]; po; [L] |
|
229 | 229 | # A memory access followed by a release atomic operation also matches above. |
230 | 230 | -safe [ExpObs Pod*R Amo.Swp L] |
231 | 231 | -safe [ExpObs Pod*R Amo.Cas L] |
| 232 | +-safe [ExpObs Pod*R Amo.StAdd L] |
| 233 | +-safe [ExpObs Pod*R Amo.LdAdd L] |
232 | 234 | -safe [ExpObs Pod*R LxSx L] |
233 | 235 | # `[Pos*R rmw L]` is stronger than `Pos*W` |
234 | 236 | #-safe [Pos*R Amo.Swp L] [Pos*R Amo.Cas L] [Pos*R LxSx L] |
|
240 | 242 | # TODO |
241 | 243 | # le aob = [Exp & M]; rmw; lrs; [A | Q] |
242 | 244 | # let lrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R] |
243 | | --safe [LxSx PosWR A] [Amo.Swp PosWR A] [Amo.Cas PosWR A] |
244 | | --safe [LxSx PosWR Q] [Amo.Swp PosWR Q] [Amo.Cas PosWR Q] |
| 245 | +-safe [LxSx PosWR A] [Amo.Swp PosWR A] [Amo.Cas PosWR A] [Amo.StAdd PosWR A] [Amo.LdAdd PosWR A] |
| 246 | +-safe [LxSx PosWR Q] [Amo.Swp PosWR Q] [Amo.Cas PosWR Q] [Amo.StAdd PosWR Q] [Amo.LdAdd PosWR Q] |
245 | 247 |
|
246 | 248 | # TODO |
247 | 249 | #let bob = [range([A];amo;[L])]; po; [Exp & M | Imp & Tag & R | MMU & FAULT] |
|
252 | 254 | # `[A]; amo; [range([A];amo;[L])]; po; [Exp & M | Imp & Tag & R | MMU & FAULT]` |
253 | 255 | -safe [A Amo.Swp L PodW* ExpObs] [A Amo.Swp L PosWR ExpObs] |
254 | 256 | -safe [A Amo.Cas L PodW* ExpObs] [A Amo.Cas L PosWR ExpObs] |
| 257 | +-safe [A Amo.StAdd L PodW* ExpObs] [A Amo.StAdd L PosWR ExpObs] |
| 258 | +-safe [A Amo.LdAdd L PodW* ExpObs] [A Amo.LdAdd L PosWR ExpObs] |
255 | 259 | -safe [A LxSx L PodW* ExpObs] [A LxSx L PosWR ExpObs] |
256 | 260 | # `[A rmw L PosWW]` is stronger than `Pos*W` |
257 | 261 | #-safe [A Amo.Swp L PosWW] [A Amo.Cas L PosWW] [A LxSx L PosWW] |
|
262 | 266 | # This particular edges cannot be auto generated from other safe edges. |
263 | 267 | -safe [ExpObs Po**R A Amo.Swp L Po*W* ExpObs] |
264 | 268 | -safe [ExpObs Po**R A Amo.Cas L Po*W* ExpObs] |
| 269 | +-safe [ExpObs Po**R A Amo.StAdd L Po*W* ExpObs] |
| 270 | +-safe [ExpObs Po**R A Amo.LdAdd L Po*W* ExpObs] |
265 | 271 |
|
266 | 272 | # TODO |
267 | 273 | ### Hat |
|
278 | 284 | -safe [Hat DMB.LDdR* ExpObs] |
279 | 285 | -safe [Hat DSB.LDdR* ExpObs] |
280 | 286 | -safe [Hat A PodR* ExpObs] [Hat Q PodR* ExpObs] |
281 | | --safe [Hat Amo.Swp] [Hat Amo.Cas] [Hat LxSx] |
| 287 | +-safe [Hat Amo.Swp] [Hat Amo.Cas] [Hat Amo.StAdd] [Hat Amo.LdAdd] [Hat LxSx] |
282 | 288 |
|
283 | 289 | ### Note for consuming the generated tests |
284 | 290 | # When verifying all the generated tests are indeed forbidden via `herd7`, |
|
0 commit comments