Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1 | C ISA2+poonceonces |
| 2 | |
Paul E. McKenney | 8f32543 | 2018-02-20 15:25:04 -0800 | [diff] [blame] | 3 | (* |
| 4 | * Result: Sometimes |
| 5 | * |
| 6 | * Given a release-acquire chain ordering the first process's store |
| 7 | * against the last process's load, is ordering preserved if all of the |
| 8 | * smp_store_release() invocations are replaced by WRITE_ONCE() and all |
| 9 | * of the smp_load_acquire() invocations are replaced by READ_ONCE()? |
| 10 | *) |
| 11 | |
Akira Yokosawa | 5c587f9 | 2020-11-28 08:43:45 +0900 | [diff] [blame] | 12 | {} |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 13 | |
| 14 | P0(int *x, int *y) |
| 15 | { |
| 16 | WRITE_ONCE(*x, 1); |
| 17 | WRITE_ONCE(*y, 1); |
| 18 | } |
| 19 | |
| 20 | P1(int *y, int *z) |
| 21 | { |
| 22 | int r0; |
| 23 | |
| 24 | r0 = READ_ONCE(*y); |
| 25 | WRITE_ONCE(*z, 1); |
| 26 | } |
| 27 | |
| 28 | P2(int *x, int *z) |
| 29 | { |
| 30 | int r0; |
| 31 | int r1; |
| 32 | |
| 33 | r0 = READ_ONCE(*z); |
| 34 | r1 = READ_ONCE(*x); |
| 35 | } |
| 36 | |
| 37 | exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) |