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