1*4882a593SmuzhiyunC IRIW+poonceonces+OnceOnce 2*4882a593Smuzhiyun 3*4882a593Smuzhiyun(* 4*4882a593Smuzhiyun * Result: Sometimes 5*4882a593Smuzhiyun * 6*4882a593Smuzhiyun * Test of independent reads from independent writes with nothing 7*4882a593Smuzhiyun * between each pairs of reads. In other words, is anything at all 8*4882a593Smuzhiyun * needed to cause two different reading processes to agree on the order 9*4882a593Smuzhiyun * of a pair of writes, where each write is to a different variable by a 10*4882a593Smuzhiyun * different process? 11*4882a593Smuzhiyun *) 12*4882a593Smuzhiyun 13*4882a593Smuzhiyun{} 14*4882a593Smuzhiyun 15*4882a593SmuzhiyunP0(int *x) 16*4882a593Smuzhiyun{ 17*4882a593Smuzhiyun WRITE_ONCE(*x, 1); 18*4882a593Smuzhiyun} 19*4882a593Smuzhiyun 20*4882a593SmuzhiyunP1(int *x, int *y) 21*4882a593Smuzhiyun{ 22*4882a593Smuzhiyun int r0; 23*4882a593Smuzhiyun int r1; 24*4882a593Smuzhiyun 25*4882a593Smuzhiyun r0 = READ_ONCE(*x); 26*4882a593Smuzhiyun r1 = READ_ONCE(*y); 27*4882a593Smuzhiyun} 28*4882a593Smuzhiyun 29*4882a593SmuzhiyunP2(int *y) 30*4882a593Smuzhiyun{ 31*4882a593Smuzhiyun WRITE_ONCE(*y, 1); 32*4882a593Smuzhiyun} 33*4882a593Smuzhiyun 34*4882a593SmuzhiyunP3(int *x, int *y) 35*4882a593Smuzhiyun{ 36*4882a593Smuzhiyun int r0; 37*4882a593Smuzhiyun int r1; 38*4882a593Smuzhiyun 39*4882a593Smuzhiyun r0 = READ_ONCE(*y); 40*4882a593Smuzhiyun r1 = READ_ONCE(*x); 41*4882a593Smuzhiyun} 42*4882a593Smuzhiyun 43*4882a593Smuzhiyunexists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0) 44