| C ISA2+pooncelock+pooncelock+pombonce |
| |
| (* |
| * Result: Never |
| * |
| * This test shows that write-write ordering provided by locks |
| * (in P0() and P1()) is visible to external process P2(). |
| *) |
| |
| {} |
| |
| P0(int *x, int *y, spinlock_t *mylock) |
| { |
| spin_lock(mylock); |
| WRITE_ONCE(*x, 1); |
| WRITE_ONCE(*y, 1); |
| spin_unlock(mylock); |
| } |
| |
| P1(int *y, int *z, spinlock_t *mylock) |
| { |
| int r0; |
| |
| spin_lock(mylock); |
| r0 = READ_ONCE(*y); |
| WRITE_ONCE(*z, 1); |
| spin_unlock(mylock); |
| } |
| |
| P2(int *x, int *z) |
| { |
| int r1; |
| int r2; |
| |
| r2 = READ_ONCE(*z); |
| smp_mb(); |
| r1 = READ_ONCE(*x); |
| } |
| |
| exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0) |
