171b7ff5eSAndrea ParriC WRC+pooncerelease+fencermbonceonce+Once
271b7ff5eSAndrea Parri
371b7ff5eSAndrea Parri(*
471b7ff5eSAndrea Parri * Result: Never
571b7ff5eSAndrea Parri *
671b7ff5eSAndrea Parri * This litmus test is an extension of the message-passing pattern, where
771b7ff5eSAndrea Parri * the first write is moved to a separate process.  Because it features
871b7ff5eSAndrea Parri * a release and a read memory barrier, it should be forbidden.  More
971b7ff5eSAndrea Parri * specifically, this litmus test is forbidden because smp_store_release()
1071b7ff5eSAndrea Parri * is A-cumulative in LKMM.
1171b7ff5eSAndrea Parri *)
1271b7ff5eSAndrea Parri
13*5c587f9bSAkira Yokosawa{}
1471b7ff5eSAndrea Parri
1571b7ff5eSAndrea ParriP0(int *x)
1671b7ff5eSAndrea Parri{
1771b7ff5eSAndrea Parri	WRITE_ONCE(*x, 1);
1871b7ff5eSAndrea Parri}
1971b7ff5eSAndrea Parri
2071b7ff5eSAndrea ParriP1(int *x, int *y)
2171b7ff5eSAndrea Parri{
2271b7ff5eSAndrea Parri	int r0;
2371b7ff5eSAndrea Parri
2471b7ff5eSAndrea Parri	r0 = READ_ONCE(*x);
2571b7ff5eSAndrea Parri	smp_store_release(y, 1);
2671b7ff5eSAndrea Parri}
2771b7ff5eSAndrea Parri
2871b7ff5eSAndrea ParriP2(int *x, int *y)
2971b7ff5eSAndrea Parri{
3071b7ff5eSAndrea Parri	int r0;
3171b7ff5eSAndrea Parri	int r1;
3271b7ff5eSAndrea Parri
3371b7ff5eSAndrea Parri	r0 = READ_ONCE(*y);
3471b7ff5eSAndrea Parri	smp_rmb();
3571b7ff5eSAndrea Parri	r1 = READ_ONCE(*x);
3671b7ff5eSAndrea Parri}
3771b7ff5eSAndrea Parri
3871b7ff5eSAndrea Parriexists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)
39