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.
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) | ;
(0:x5=1 /\ 0:x2=1 /\ 1:x3=1)