0001 C WRC+pooncerelease+fencermbonceonce+Once
0002
0003 (*
0004 * Result: Never
0005 *
0006 * This litmus test is an extension of the message-passing pattern, where
0007 * the first write is moved to a separate process. Because it features
0008 * a release and a read memory barrier, it should be forbidden. More
0009 * specifically, this litmus test is forbidden because smp_store_release()
0010 * is A-cumulative in LKMM.
0011 *)
0012
0013 {}
0014
0015 P0(int *x)
0016 {
0017 WRITE_ONCE(*x, 1);
0018 }
0019
0020 P1(int *x, int *y)
0021 {
0022 int r0;
0023
0024 r0 = READ_ONCE(*x);
0025 smp_store_release(y, 1);
0026 }
0027
0028 P2(int *x, int *y)
0029 {
0030 int r0;
0031 int r1;
0032
0033 r0 = READ_ONCE(*y);
0034 smp_rmb();
0035 r1 = READ_ONCE(*x);
0036 }
0037
0038 exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)
