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

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

[patrick at rivosinc dot com]

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)

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

[palmer at gcc dot gnu.org]

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

--- Comment #1 from palmer at gcc dot gnu.org ---
I'm not quite sure what the rules on targeting 12 for this one: it's not
technically a regression, as it's always been broken, but it is a bug.  I'd err
on the side of taking a fix, as we're just strengthening the GCC implementation
so it should be pretty safe.  That said, anything related to memory models has
the potential for complicated fallout so I could understand wanting to wait
just to play it safe.

Patrick has a patch in progress.

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

[patrick at rivosinc dot com]

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

--- Comment #2 from Patrick O'Neill <patrick at rivosinc dot com> ---
Created attachment 52577
  --> https://gcc.gnu.org/bugzilla/attachment.cgi?id=52577&action=edit
Patch v1

Patch submitted to mailing list.

Subject: [PATCH] RISCV: Strengthen libatomic lrsc pairs

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

[Andrew Waterman]

Appendix A of the RISC-V ISA manual says that lr.w.aq + sc.w.aqrl
should suffice.  I see the patch puts aqrl on both the load and store,
which, while correct, appears to be stronger than necessary.

(cc Dan Lustig)


On Mon, Mar 7, 2022 at 3:25 PM patrick at rivosinc dot com via
Gcc-bugs <gcc-bugs@gcc.gnu.org> wrote:
>
> 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)

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

[andrew at sifive dot com]

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

--- Comment #3 from Andrew Waterman <andrew at sifive dot com> ---
Appendix A of the RISC-V ISA manual says that lr.w.aq + sc.w.aqrl
should suffice.  I see the patch puts aqrl on both the load and store,
which, while correct, appears to be stronger than necessary.

(cc Dan Lustig)


On Mon, Mar 7, 2022 at 3:25 PM patrick at rivosinc dot com via
Gcc-bugs <gcc-bugs@gcc.gnu.org> wrote:
>
> 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)

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

[Andrew Waterman]

Correction: Appendix A recommends lr.w.aqrl + sc.w.rl.
https://github.com/riscv/riscv-isa-manual/blob/9ec8c0105dbf1492b57f6cafdb90a268628f476a/src/memory.tex#L1150-L1152

On Mon, Mar 7, 2022 at 3:51 PM Andrew Waterman <andrew@sifive.com> wrote:
>
> Appendix A of the RISC-V ISA manual says that lr.w.aq + sc.w.aqrl
> should suffice.  I see the patch puts aqrl on both the load and store,
> which, while correct, appears to be stronger than necessary.
>
> (cc Dan Lustig)
>
>
> On Mon, Mar 7, 2022 at 3:25 PM patrick at rivosinc dot com via
> Gcc-bugs <gcc-bugs@gcc.gnu.org> wrote:
> >
> > 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)

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

[andrew at sifive dot com]

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

--- Comment #4 from Andrew Waterman <andrew at sifive dot com> ---
Correction: Appendix A recommends lr.w.aqrl + sc.w.rl.
https://github.com/riscv/riscv-isa-manual/blob/9ec8c0105dbf1492b57f6cafdb90a268628f476a/src/memory.tex#L1150-L1152

On Mon, Mar 7, 2022 at 3:51 PM Andrew Waterman <andrew@sifive.com> wrote:
>
> Appendix A of the RISC-V ISA manual says that lr.w.aq + sc.w.aqrl
> should suffice.  I see the patch puts aqrl on both the load and store,
> which, while correct, appears to be stronger than necessary.
>
> (cc Dan Lustig)
>
>
> On Mon, Mar 7, 2022 at 3:25 PM patrick at rivosinc dot com via
> Gcc-bugs <gcc-bugs@gcc.gnu.org> wrote:
> >
> > 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)

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

[patrick at rivosinc dot com]

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

--- Comment #5 from Patrick O'Neill <patrick at rivosinc dot com> ---
IIUC, Appendix A is incorrect.

We cannot allow any memory ops to enter within the LR/SC pair, since a
reordering like that is visible to other threads.

Here's a litmus test showing this fact:

(*
  LR/SC with .aq .rl bits does not allow read operations to be reordered
  within/beneath it.
*)

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

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

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

In a sequentially consistent atomic operation (which this LRSC pair is
emulating), it is not possible for both x5 to be loaded with a 1 and the
LR/SC pair to load/operate on a 0.

With the pairing of LR.aq/SC.aqrl this outcome is possible.

Similarly, for LR.aqrl/SC.rl, a similar reordering needs to be forbidden:

RISCV LRSC-WRITE

(* 
  LR/SC with .aq .rl bits does not allow write operations to be reordered
  within/above it.
*)

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

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

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

In a sequentially consistent atomic operation, it is not possible for
both Hart 1's x9 to be loaded with a 1 and Hart 1's x7 to be loaded with a 0
(as long as the SC succeeds, which b=1 enforces).

That outcome is possible with LR.aqrl/SC.rl since operations can get
reordered within the LR/SC pairing.

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

[patrick at rivosinc dot com]

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

--- Comment #6 from Patrick O'Neill <patrick at rivosinc dot com> ---
I just reviewed the manual - I was incorrect. Appendix A is correct. I forgot
that the RISCV implementation used leading fences. The second litmus test is no
longer valid since a simple load/store with no fence would not occur in
outputted RISCV asm. The load/store would have a leading fence that would
prevent it from entering the LR/SC pairing.

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

[patrick at rivosinc dot com]

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

Patrick O'Neill <patrick at rivosinc dot com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
  Attachment #52577|0                           |1
        is obsolete|                            |

--- Comment #7 from Patrick O'Neill <patrick at rivosinc dot com> ---
Created attachment 52578
  --> https://gcc.gnu.org/bugzilla/attachment.cgi?id=52578&action=edit
Patch v2

Patch submitted to mailing list.

Subject: [PATCH v2] RISCV: Strengthen libatomic lrsc pairs

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

[Andrew Waterman]

Cool, thanks, Patrick.


On Mon, Mar 7, 2022 at 6:58 PM patrick at rivosinc dot com via
Gcc-bugs <gcc-bugs@gcc.gnu.org> wrote:
>
> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104831
>
> Patrick O'Neill <patrick at rivosinc dot com> changed:
>
>            What    |Removed                     |Added
> ----------------------------------------------------------------------------
>   Attachment #52577|0                           |1
>         is obsolete|                            |
>
> --- Comment #7 from Patrick O'Neill <patrick at rivosinc dot com> ---
> Created attachment 52578
>   --> https://gcc.gnu.org/bugzilla/attachment.cgi?id=52578&action=edit
> Patch v2
>
> Patch submitted to mailing list.
>
> Subject: [PATCH v2] RISCV: Strengthen libatomic lrsc pairs

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

[andrew at sifive dot com]

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

--- Comment #8 from Andrew Waterman <andrew at sifive dot com> ---
Cool, thanks, Patrick.


On Mon, Mar 7, 2022 at 6:58 PM patrick at rivosinc dot com via
Gcc-bugs <gcc-bugs@gcc.gnu.org> wrote:
>
> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104831
>
> Patrick O'Neill <patrick at rivosinc dot com> changed:
>
>            What    |Removed                     |Added
> ----------------------------------------------------------------------------
>   Attachment #52577|0                           |1
>         is obsolete|                            |
>
> --- Comment #7 from Patrick O'Neill <patrick at rivosinc dot com> ---
> Created attachment 52578
>   --> https://gcc.gnu.org/bugzilla/attachment.cgi?id=52578&action=edit
> Patch v2
>
> Patch submitted to mailing list.
>
> Subject: [PATCH v2] RISCV: Strengthen libatomic lrsc pairs

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

[patrick at rivosinc dot com]

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

--- Comment #9 from Patrick O'Neill <patrick at rivosinc dot com> ---
Adding this comment to summarize why LR.aq/SC.rl doesn't appear to be
an issue.

The re-orderings shown in the previous litmus tests are allowed by the
C++/GCC definition of SEQ_CST. My reasoning in prior comments are
incorrect and should be disregarded.

The ISA manual table A.6 recommends the LR.aqrl/SC.rl pairing for
SEQ_CST because of A.6's SEQ_CST store mapping. When the SEQ_CST store
is implemented as:
fence rw,w + sw
There needs to be ordering enforced to prevent the store from being
reordered into the middle of the LR/SC pairing [1][2].

GCC has a different mapping for SEQ_CST store:
fence iorw,ow + amoswap.rl
This prevents the reordering as seen in the example [2], so we can
safely use LR.aq/SC.rl pairings [3].

Relevant litmus tests:

[1] CDSChecker Litmus test - seq_cst W-RMW
#include <stdlib.h>
#include <stdio.h>
#include <threads.h>
#include <atomic>

#include "model-assert.h"

/*
 * This shows that the c memory model enforces
 * SEQ_CST W->(RMW) ordering
 */

std::atomic_int x;
std::atomic_int y;

int resx, resy;

static void a(void *obj)
{
       x.store(1, std::memory_order_seq_cst);
       resy = y.fetch_add(1, std::memory_order_seq_cst);
}

static void b(void *obj)
{
       y.store(42, std::memory_order_seq_cst);
       resx = x.load(std::memory_order_seq_cst);
}

int user_main(int argc, char **argv)
{
       thrd_t t1, t2;

       atomic_init(&x, 0);
       atomic_init(&y, 0);

       printf("Main thread: creating 2 threads\n");

       thrd_create(&t1, (thrd_start_t)&a, NULL);
       thrd_create(&t2, (thrd_start_t)&b, NULL);

       thrd_join(t1);
       thrd_join(t2);

       printf("x: %d\n", resy);
       printf("y: %d\n", resx);

       MODEL_ASSERT(!(resy == 0 && resx == 0));

       printf("Main thread is finished\n");

       return 0;
}

[2] Herd7 Write-RMW litmus test - ISA Manual A.6 Mapping
RISCV W-RMW

(*
Table A.6 Seq_cst store along with LR.aq/SC.rl is insufficient for a
seq_cst store, seq_cst RMW mapping.
*)

{
0:x7=A; 0:x8=B;
1:x7=A; 1:x8=B;
}

    P0                  | P1          ;
    ori x1,x0,1         | ori x1,x0,1 ;
    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 x1,x1,0(x7) | lw x2,0(x8) ;

exists
(0:x3=0 /\ 1:x2=0)

[3] Herd7 Write-RMW litmus test - GCC Mapping
RISCV W-RMW

(*
GCC's current mapping for seq_cst store along with LR.aq/SC.rl is
sufficient for a seq_cst store, seq_cst RMW mapping.
*)

{
0:x7=A; 0:x8=B;
1:x7=A; 1:x8=B;
}

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

~exists (0:x3=0 /\ 1:x2=0)

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

[palmer at gcc dot gnu.org]

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

palmer at gcc dot gnu.org changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
           Assignee|unassigned at gcc dot gnu.org      |patrick at rivosinc dot com
             Status|UNCONFIRMED                 |ASSIGNED
     Ever confirmed|0                           |1
   Last reconfirmed|                            |2023-09-25

--- Comment #10 from palmer at gcc dot gnu.org ---
This should be fixed, looks like we just forgot to close the bug.  I've
assigned it to Patrick to make sure everything's finished.

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

[patrick at rivosinc dot com]

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

Patrick O'Neill <patrick at rivosinc dot com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
         Resolution|---                         |FIXED
             Status|ASSIGNED                    |RESOLVED

--- Comment #11 from Patrick O'Neill <patrick at rivosinc dot com> ---
This has been resolved on trunk:
https://inbox.sourceware.org/gcc-patches/20230427162301.1151333-1-patrick@rivosinc.com/
The cover letter there contains a lot more context about why the mappings are
wrong and why we implemented a strengthened version of Table A.6.
These mappings are included in the RISC-V PSABI doc:
https://github.com/riscv-non-isa/riscv-elf-psabi-doc/pull/378

And this series has been backported to be included in GCC 13.3 (along with a
bugfix):
https://inbox.sourceware.org/gcc-patches/20230725180206.284777-1-patrick@rivosinc.com/

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

[pinskia at gcc dot gnu.org]

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

Andrew Pinski <pinskia at gcc dot gnu.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
   Target Milestone|---                         |13.3