0001 C Z6.0+pooncelock+pooncelock+pombonce
0002
0003 (*
0004 * Result: Sometimes
0005 *
0006 * This example demonstrates that a pair of accesses made by different
0007 * processes each while holding a given lock will not necessarily be
0008 * seen as ordered by a third process not holding that lock.
0009 *)
0010
0011 {}
0012
0013 P0(int *x, int *y, spinlock_t *mylock)
0014 {
0015 spin_lock(mylock);
0016 WRITE_ONCE(*x, 1);
0017 WRITE_ONCE(*y, 1);
0018 spin_unlock(mylock);
0019 }
0020
0021 P1(int *y, int *z, spinlock_t *mylock)
0022 {
0023 int r0;
0024
0025 spin_lock(mylock);
0026 r0 = READ_ONCE(*y);
0027 WRITE_ONCE(*z, 1);
0028 spin_unlock(mylock);
0029 }
0030
0031 P2(int *x, int *z)
0032 {
0033 int r1;
0034
0035 WRITE_ONCE(*z, 2);
0036 smp_mb();
0037 r1 = READ_ONCE(*x);
0038 }
0039
0040 exists (1:r0=1 /\ z=2 /\ 2:r1=0)
