1C WRC+pooncerelease+fencermbonceonce+Once
 2
 3(*
 4 * Result: Never
 5 *
 6 * This litmus test is an extension of the message-passing pattern, where
 7 * the first write is moved to a separate process.  Because it features
 8 * a release and a read memory barrier, it should be forbidden.  More
 9 * specifically, this litmus test is forbidden because smp_store_release()
10 * is A-cumulative in LKMM.
11 *)
12
13{}
14
15P0(int *x)
16{
17	WRITE_ONCE(*x, 1);
18}
19
20P1(int *x, int *y)
21{
22	int r0;
23
24	r0 = READ_ONCE(*x);
25	smp_store_release(y, 1);
26}
27
28P2(int *x, int *y)
29{
30	int r0;
31	int r1;
32
33	r0 = READ_ONCE(*y);
34	smp_rmb();
35	r1 = READ_ONCE(*x);
36}
37
38exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)

 1C WRC+pooncerelease+fencermbonceonce+Once
 2
 3(*
 4 * Result: Never
 5 *
 6 * This litmus test is an extension of the message-passing pattern, where
 7 * the first write is moved to a separate process.  Because it features
 8 * a release and a read memory barrier, it should be forbidden.  More
 9 * specifically, this litmus test is forbidden because smp_store_release()
10 * is A-cumulative in LKMM.
11 *)
12
13{}
14
15P0(int *x)
16{
17	WRITE_ONCE(*x, 1);
18}
19
20P1(int *x, int *y)
21{
22	int r0;
23
24	r0 = READ_ONCE(*x);
25	smp_store_release(y, 1);
26}
27
28P2(int *x, int *y)
29{
30	int r0;
31	int r1;
32
33	r0 = READ_ONCE(*y);
34	smp_rmb();
35	r1 = READ_ONCE(*x);
36}
37
38exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)