https://gcc.gnu.org/bugzilla/show_bug.cgi?id=111235
--- Comment #5 from Luke Geeson <luke.geeson at cs dot ucl.ac.uk> ---
Thank you for fixing this, Wilco! I will now test this bug using the code
emitted by Godbolt.
Consider again the same source program. When run through gcc with the same
flags we get the ARM assembly test:
```
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 ;
BEQ L3 | MOV R1,#1 ;
L2: STR R2, [%P0_P0_r0]| STR R1, [%P1_x] ;
BX LR | STR R2, [%P1_P1_r0] ;
L3: MOV R1, #1 | ;
STR R1, [%P0_y] | ;
B L2 | ;
exists (P0_r0=1 /\ P1_r0=1)
```
Which under the arm model has the outcomes:
```
[P0_r0]=0; [P1_r0]=0;
[P0_r0]=1; [P1_r0]=0;
```
As you can see the buggy behaviour has gone away, the bug is fixed.
