RISCV LR-SC-diff-loc4
"Atomicity Axiom: [..] then 's' must precede 'w' in the global memory order [..]"
{
0:x6=x; 0:x8=y;
1:x6=y; 1:x8=z; 1:x3=x;
}
P0 | P1 ;
lw x5,0(x6) | lw x5,0(x6) ;
fence rw,rw | ori x7,x0,1 ;
ori x7,x0,1 | sw.rl x7,0(x8) ;
sw x7,0(x8) | lr.w x9,0(x8) ;
| ori x1,x0,1 ;
| sc.w x2,x1,0(x3) ;
Observed
x=1; 1:x9=1; 1:x5=1; 1:x2=0; 0:x5=1;
and x=1; 1:x9=1; 1:x5=0; 1:x2=0; 0:x5=1;
and x=1; 1:x9=1; 1:x5=1; 1:x2=0; 0:x5=0;
and x=1; 1:x9=1; 1:x5=0; 1:x2=0; 0:x5=0;