LISA RW-rwa+RW-ra+RW-rra+CK (* * Result: Sometimes, due to release-acquire being only locally transitive. * I believe that this is allowed by PowerPC. *) { } P0 | P1 | P2 | P3 ; w[once] y 1 | r[acquire] r1 x1 | r[acquire] r1 x2 | w[once] z 1 ; w[release] x1 1 | w[release] x2 1 | r[once] r2 z | f[mb] ; | | | r[once] r1 y ; Observed 3:r1=0; 2:r2=0; 2:r1=1; 1:r1=1;