1*4882a593SmuzhiyunC WRC+poonceonces+Once 2*4882a593Smuzhiyun 3*4882a593Smuzhiyun(* 4*4882a593Smuzhiyun * Result: Sometimes 5*4882a593Smuzhiyun * 6*4882a593Smuzhiyun * This litmus test is an extension of the message-passing pattern, 7*4882a593Smuzhiyun * where the first write is moved to a separate process. Note that this 8*4882a593Smuzhiyun * test has no ordering at all. 9*4882a593Smuzhiyun *) 10*4882a593Smuzhiyun 11*4882a593Smuzhiyun{} 12*4882a593Smuzhiyun 13*4882a593SmuzhiyunP0(int *x) 14*4882a593Smuzhiyun{ 15*4882a593Smuzhiyun WRITE_ONCE(*x, 1); 16*4882a593Smuzhiyun} 17*4882a593Smuzhiyun 18*4882a593SmuzhiyunP1(int *x, int *y) 19*4882a593Smuzhiyun{ 20*4882a593Smuzhiyun int r0; 21*4882a593Smuzhiyun 22*4882a593Smuzhiyun r0 = READ_ONCE(*x); 23*4882a593Smuzhiyun WRITE_ONCE(*y, 1); 24*4882a593Smuzhiyun} 25*4882a593Smuzhiyun 26*4882a593SmuzhiyunP2(int *x, int *y) 27*4882a593Smuzhiyun{ 28*4882a593Smuzhiyun int r0; 29*4882a593Smuzhiyun int r1; 30*4882a593Smuzhiyun 31*4882a593Smuzhiyun r0 = READ_ONCE(*y); 32*4882a593Smuzhiyun r1 = READ_ONCE(*x); 33*4882a593Smuzhiyun} 34*4882a593Smuzhiyun 35*4882a593Smuzhiyunexists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) 36