| b.liu | e958203 | 2025-04-17 19:18:16 +0800 | [diff] [blame] | 1 | C S+poonceonces |
| 2 | |
| 3 | (* |
| 4 | * Result: Sometimes |
| 5 | * |
| 6 | * Starting with a two-process release-acquire chain ordering P0()'s |
| 7 | * first store against P1()'s final load, if the smp_store_release() |
| 8 | * is replaced by WRITE_ONCE() and the smp_load_acquire() replaced by |
| 9 | * READ_ONCE(), is ordering preserved? |
| 10 | *) |
| 11 | |
| 12 | {} |
| 13 | |
| 14 | P0(int *x, int *y) |
| 15 | { |
| 16 | WRITE_ONCE(*x, 2); |
| 17 | WRITE_ONCE(*y, 1); |
| 18 | } |
| 19 | |
| 20 | P1(int *x, int *y) |
| 21 | { |
| 22 | int r0; |
| 23 | |
| 24 | r0 = READ_ONCE(*y); |
| 25 | WRITE_ONCE(*x, 1); |
| 26 | } |
| 27 | |
| 28 | exists (x=2 /\ 1:r0=1) |