Re: [RFC 0/7] RISCV: Implement ISA Manual Table A.6 Mappings

[Patrick O'Neill <patrick@rivosinc.com>]

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)