Test Andy22

The herd model allows the test. The relevant point is the absence of dependence from the read of the swap to the write of the swap. However, notice the ppo arrow, though from (a) to (b). But rule 13 [R];(addr|data);[W];po-loc-no-w;[R] ∈ ppo is specific in that its initial segment applies to data and address dependencies, not to generic ppo.

RISCV Andy22
{
0:x7=A; 0:x8=B;
1:x7=A; 1:x8=B;
}
 P0                    | P1           ;
 ori x1,x0,1           | lw x3,0(x8)  ;
 amoswap.w x5,x1,0(x7) | sw x3,0(x7)  ;
 lw x2,0(x7)           |              ;
 sw x2,0(x8)           |              ;
exists
(0:x5=1 /\ 0:x2=1 /\ 1:x3=1)