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.