blob: b321aa6f4ea52d4125b750cd6517d1feddb522d0 [file] [log] [blame]
Paul E. McKenney1c27b642018-01-18 19:58:55 -08001C ISA2+poonceonces
2
Paul E. McKenney8f325432018-02-20 15:25:04 -08003(*
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 Yokosawa5c587f92020-11-28 08:43:45 +090012{}
Paul E. McKenney1c27b642018-01-18 19:58:55 -080013
14P0(int *x, int *y)
15{
16 WRITE_ONCE(*x, 1);
17 WRITE_ONCE(*y, 1);
18}
19
20P1(int *y, int *z)
21{
22 int r0;
23
24 r0 = READ_ONCE(*y);
25 WRITE_ONCE(*z, 1);
26}
27
28P2(int *x, int *z)
29{
30 int r0;
31 int r1;
32
33 r0 = READ_ONCE(*z);
34 r1 = READ_ONCE(*x);
35}
36
37exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)