The litmus test in this RFC is flawed since it does not assert that the
LR/SC pair succeeds. The condition in the RFC is permitted iff the LR/SC
pair fails. After correcting this flaw [1][2], the litmus test condition
is correctly forbidden.
This correction does not mean that the A.6 mapping is guaranteed to be
fully compatible with the current GCC/LLVM mapping. This just means that
this particular case does not appear to be an issue.
Thanks,
Patrick
[1] Corrected herd7 litmus test:
RISCV W-RMW
{
0:x7=A; 0:x8=B; 0:x1=1;
1:x7=A; 1:x8=B; 1:x1=1;
}
P0 | P1 ;
fence rw,w | fence rw,rw ;
sw x1,0(x8) | sw x1,0(x7) ;
lr.w.aq x3,0(x7) | fence rw,rw ;
sc.w.rl x2,x1,0(x7) | lw x2,0(x8) ;
~exists (0:x2=0 /\ 0:x3=0 /\ 1:x2=0)
[2] Corrected herd7 litmus test (with retry-loop):
RISCV W-RMW
{
0:x7=A; 0:x8=B; 0:x1=1;
1:x7=A; 1:x8=B; 1:x1=1;
}
P0 | P1 ;
fence rw,w | sw x1,0(x7) ;
sw x1,0(x8) | fence rw,rw ;
LC00: | lw x2,0(x8) ;
lr.w.aq x3,0(x7) | ;
sc.w.rl x2,x1,0(x7) | ;
bne x2,x0,LC00 | ;
~exists (0:x2=0 /\ 0:x3=0 /\ 1:x2=0)
