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) 39