[Bug translation/111235] New: [Armv7-a]: Control-dependency between atomic accesses removed by -O1.

["luke.geeson at cs dot ucl.ac.uk" <gcc-bugzilla@gcc.gnu.org>]

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

            Bug ID: 111235
           Summary: [Armv7-a]: Control-dependency between atomic accesses
                    removed by -O1.
           Product: gcc
           Version: 14.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: translation
          Assignee: unassigned at gcc dot gnu.org
          Reporter: luke.geeson at cs dot ucl.ac.uk
  Target Milestone: ---

Consider the following litmus test that captures bad behaviour:
```
C test

{ *x = 0; *y = 0; } // fixed initial state where x and y are 0

// Concurrent threads
P0 (atomic_int* y,int* x) {
  int r0 = *x;
  if (r0 == 1) {
    atomic_store_explicit(y,1,memory_order_relaxed);
  }
}

P1 (atomic_int* y,int* x) {
  int r0 = atomic_load_explicit(y,memory_order_acquire);
  *x = 1;
}

// predicate over final state - does this outcome occur?
exists (P0:r0=1 /\ P1:r0=1)
```
where 'P0:r0 = 0' means thread P0, local variable r0 has value 0.

When simulating this test under the C/C++ model from its initial state, the
outcome of execution in the exists clause is forbidden by the source model. The
allowed outcomes are:
```
{P0:r0=0; P1:r0=0;}
{P0:r0=1; P1:r0=0;}   
```

When compiling to target armv7-a using either GCC or LLVM trunk
(https://godbolt.org/z/nxWTbEfK1), the compiled program has the following
outcomes when simulated under the armv7 model:
```
{P0:r0=0; P1:r0=0;}                                           
{P0:r0=1; P1:r0=0;}
{P0:r0=1; P1:r0=1;} <--- forbidden by source model, bug!
```
Since the `CMP;MOVEQ   r1, #1;STREQ` sequence is predicated on the result of
CMP, but the STREQ can be reordered before the LDR of x on thread P0, allowing
the outcome {P0:r0=1; P1:r0=1;}. 

The issue is that the control dependency between the load and store on P0 has
been removed by the compiler. Both GCC and LLVM produce the following (replace
symbolic registers e.g. %P0_x with concrete registers containing x).

```
ARM test

{ [P0_r0]=0;[P1_r0]=0;[x]=0;[y]=0;
  %P0_P0_r0=P0_r0;%P0_x=x;%P0_y=y;
  %P1_P1_r0=P1_r0;%P1_x=x;%P1_y=y }
(*****************************************************************)
(*                 the Telechat toolsuite                        *)
(*                                                               *)
(* Luke Geeson, University College London, UK.                   *)
(* gcc -O1 -march=armv7-a -pthread --std=c11 -marm -fno-section-anchors*)
(*                                                               *)
(*****************************************************************)
  P0                   |  P1                   ;
   LDR R2,[%P0_x]      |   LDR R2,[%P1_y]      ;
   CMP R2,#1           |   DMB ISH             ;
   MOVEQ R1,#1         |   MOV R1,#1           ;
   STREQ R1,[%P0_y]    |   STR R1,[%P1_x]      ;
   STR R2,[%P0_P0_r0]  |   STR R2,[%P1_P1_r0]  ;
   BX LR               |   BX LR               ;


exists (P0_r0=1 /\ P1_r0=1) <--- yes, allowed by arm.cat, bug!
```
The forbidden {P0:r0=1; P1:r0=1;} behaviour disappears in GCC when optimising
using -O2 or above, since R2 is reused in the STREQ when the EQ condition holds
- a data dependency masks the loss of the control dependency. This buggy
behaviour remains in clang -O2 and above however
(https://godbolt.org/z/hGv7P3vGW).

To fix this - mark relaxed atomic load/stores as not predicated, and ideally
use an explicit branch to enforce the control dependency so that it is not
lost:
```
ARM test-fixed

{ [P0_r0]=0;[P1_r0]=0;[x]=0;[y]=0;
  %P0_P0_r0=P0_r0;%P0_x=x;%P0_y=y;
  %P1_P1_r0=P1_r0;%P1_x=x;%P1_y=y }

  P0                   |  P1                   ;
   LDR R0,[%P0_x]      |   MOV R2,#1           ;
   CMP R0,#1           |   LDR R0,[%P1_y]      ;
   BNE L0x2c           |   DMB ISH             ;
   MOV R2,#1           |   STR R2,[%P1_x]      ;
   STR R2,[%P0_y]      |   STR R0,[%P1_P1_r0]  ;
  L0x2c:               |                       ;
   STR R0,[%P0_P0_r0]  |                       ;


exists (P0_r0=1 /\ P1_r0=1)
```
This prevents the buggy behaviour.

We will follow up by reporting the bug for GCC.