| C ISA2+poonceonces |
| |
| (* |
| * Result: Sometimes |
| * |
| * Given a release-acquire chain ordering the first process's store |
| * against the last process's load, is ordering preserved if all of the |
| * smp_store_release() invocations are replaced by WRITE_ONCE() and all |
| * of the smp_load_acquire() invocations are replaced by READ_ONCE()? |
| *) |
| |
| { |
| int x; |
| int y; |
| int z; |
| } |
| |
| P0(int *x, int *y) |
| { |
| WRITE_ONCE(*x, 1); |
| WRITE_ONCE(*y, 1); |
| } |
| |
| P1(int *y, int *z) |
| { |
| int r0; |
| |
| r0 = READ_ONCE(*y); |
| WRITE_ONCE(*z, 1); |
| } |
| |
| P2(int *x, int *z) |
| { |
| int r0; |
| int r1; |
| |
| r0 = READ_ONCE(*z); |
| r1 = READ_ONCE(*x); |
| } |
| |
| exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) |
