https://gcc.gnu.org/bugzilla/show_bug.cgi?id=111246
--- Comment #6 from Luke Geeson <luke.geeson at cs dot ucl.ac.uk> ---
Apologies - I've been thinking in syncs and fences too much!
Yes I mean `lwsync`, for clarity I repeat the above so you know it is the
correct fix:
```
lukegeeson@machine:~/Dev/tv-dev/herdtools7$ cat test.litmus
PPC test-fixed
{ [P1_r0]=0;[x]=0;[y]=0;
uint64_t %P0_x=x; uint64_t %P0_y=y;
uint64_t %P1_P1_r0=P1_r0;uint64_t %P1_x=x;
uint64_t %P1_y=y }
(*****************************************************************)
(* the Telechat toolsuite *)
(* *)
(* Luke Geeson, University College London, UK. *)
(* *)
(*****************************************************************)
P0 | P1 ;
li r10,2 | sync ;
stw r10,0(%P0_x) | lwz r9,0(%P1_y) ;
lwsync | cmpw r9,r9 ;
sync | b L0x50 ;
li r10,1 | L0x50: lwsync ;
stw r10,0(%P0_y) | li r8,1 ;
| stw r8,0(%P1_x) ;
| stw r9,0(%P1_P1_r0) ;
exists ([x]=2 /\ P1_r0=1)
lukegeeson@machine:~/Dev/tv-dev/herdtools7$ ./_build/install/default/bin/herd7
-model ppc.cat -I herd/libdir test.litmus
Test test-fixed Allowed
States 3
[P1_r0]=0; [x]=1;
[P1_r0]=0; [x]=2;
[P1_r0]=1; [x]=1;
No
Witnesses
Positive: 0 Negative: 3
Condition exists ([x]=2 /\ [P1_r0]=1)
Observation test-fixed Never 0 3
Time test-fixed 0.01
Hash=b215018fe694934d3b5fd1dc5eef48e9
```
