1*4882a593SmuzhiyunC ISA2+poonceonces 2*4882a593Smuzhiyun 3*4882a593Smuzhiyun(* 4*4882a593Smuzhiyun * Result: Sometimes 5*4882a593Smuzhiyun * 6*4882a593Smuzhiyun * Given a release-acquire chain ordering the first process's store 7*4882a593Smuzhiyun * against the last process's load, is ordering preserved if all of the 8*4882a593Smuzhiyun * smp_store_release() invocations are replaced by WRITE_ONCE() and all 9*4882a593Smuzhiyun * of the smp_load_acquire() invocations are replaced by READ_ONCE()? 10*4882a593Smuzhiyun *) 11*4882a593Smuzhiyun 12*4882a593Smuzhiyun{} 13*4882a593Smuzhiyun 14*4882a593SmuzhiyunP0(int *x, int *y) 15*4882a593Smuzhiyun{ 16*4882a593Smuzhiyun WRITE_ONCE(*x, 1); 17*4882a593Smuzhiyun WRITE_ONCE(*y, 1); 18*4882a593Smuzhiyun} 19*4882a593Smuzhiyun 20*4882a593SmuzhiyunP1(int *y, int *z) 21*4882a593Smuzhiyun{ 22*4882a593Smuzhiyun int r0; 23*4882a593Smuzhiyun 24*4882a593Smuzhiyun r0 = READ_ONCE(*y); 25*4882a593Smuzhiyun WRITE_ONCE(*z, 1); 26*4882a593Smuzhiyun} 27*4882a593Smuzhiyun 28*4882a593SmuzhiyunP2(int *x, int *z) 29*4882a593Smuzhiyun{ 30*4882a593Smuzhiyun int r0; 31*4882a593Smuzhiyun int r1; 32*4882a593Smuzhiyun 33*4882a593Smuzhiyun r0 = READ_ONCE(*z); 34*4882a593Smuzhiyun r1 = READ_ONCE(*x); 35*4882a593Smuzhiyun} 36*4882a593Smuzhiyun 37*4882a593Smuzhiyunexists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) 38