[Bug target/104831] New: RISCV libatomic LR.aq/SC.rl pair insufficient for SEQ_CST

[patrick at rivosinc dot com via Gcc-bugs]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104831

            Bug ID: 104831
           Summary: RISCV libatomic LR.aq/SC.rl pair insufficient for
                    SEQ_CST
           Product: gcc
           Version: 12.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: target
          Assignee: unassigned at gcc dot gnu.org
          Reporter: patrick at rivosinc dot com
  Target Milestone: ---

Currently, libatomic's _sync_fetch_and_#op# and 
__sync_val_compare_and_swap methods are not sufficiently strong for the
ATOMIC_SEQ_CST memory model.

This can be shown using the following herd litmus test:
RISCV LRSC-LIB-CALL

(* 
  Current LR/SC pair as implemented in libatomic library call
*)

{
0:x6=a; 0:x8=b; 0:x10=c;
1:x6=a; 1:x8=b; 1:x10=c;
}

 P0                  | P1           ;
 ori x1,x0,1         | lw x9,0(x10) ;
 sw x1,0(x10)        | fence rw,rw  ;
 lr.w.aq x7,0(x8)    | lw x5,0(x6)  ;
 ori x7,x0,1         |              ;
 sc.w.rl x3,x7,0(x8) |              ;
 sw x1,0(x6)         |              ;

~exists (1:x9=1 /\ 1:x5=0 /\ b=1)