1*4882a593SmuzhiyunC CoWR+poonceonce+Once 2*4882a593Smuzhiyun 3*4882a593Smuzhiyun(* 4*4882a593Smuzhiyun * Result: Never 5*4882a593Smuzhiyun * 6*4882a593Smuzhiyun * Test of write-read coherence, that is, whether or not a write to a 7*4882a593Smuzhiyun * given variable and a later read from that same variable are ordered. 8*4882a593Smuzhiyun *) 9*4882a593Smuzhiyun 10*4882a593Smuzhiyun{} 11*4882a593Smuzhiyun 12*4882a593SmuzhiyunP0(int *x) 13*4882a593Smuzhiyun{ 14*4882a593Smuzhiyun int r0; 15*4882a593Smuzhiyun 16*4882a593Smuzhiyun WRITE_ONCE(*x, 1); 17*4882a593Smuzhiyun r0 = READ_ONCE(*x); 18*4882a593Smuzhiyun} 19*4882a593Smuzhiyun 20*4882a593SmuzhiyunP1(int *x) 21*4882a593Smuzhiyun{ 22*4882a593Smuzhiyun WRITE_ONCE(*x, 2); 23*4882a593Smuzhiyun} 24*4882a593Smuzhiyun 25*4882a593Smuzhiyunexists (x=1 /\ 0:r0=2) 26