MemSynth results in Herd format

PPC ambig1
{ A=0; B=0; 0:r2=B; 0:r4=A; 1:r2=A; 1:r5=B; }
P0            | P1            ;
lwz r1,0(r2)  | lwz r1,0(r2)  ;
sync          | xor r3,r1,r1  ;
li r3,1       | li r4,1       ;
stw r3,0(r4)  | stwx r4,r3,r5 ;
exists (0:r1=1 /\ 1:r1=1)

PPC ambig2
{ A=0; B=0; 0:r2=B; 0:r4=A; 1:r2=A; 1:r5=B; }
P0            | P1            ;
lwz r1,0(r2)  | lwz r1,0(r2)  ;
lwsync        | xor r3,r1,r1  ;
li r3,1       | li r4,1       ;
stw r3,0(r4)  | stwx r4,r3,r5 ;
exists (0:r1=1 /\ 1:r1=1)```

PPC ambig3
{ A=0; B=0; 0:r2=B; 0:r4=A; 1:r2=A; 1:r4=B; }
P0           | P1           ;
lwz r1,0(r2) | lwz r1,0(r2) ;
lwsync       | lwsync       ;
li r3,1      | li r3,1      ;
stw r3,0(r4) | stw r3,0(r4) ;
exists (0:r1=1 /\ 1:r1=1)

PPC ambig4
{ A=0; B=0; 0:r2=B; 0:r5=A; 1:r2=A; 1:r4=B; }
P0            | P1            ;
lwz r1,0(r2)  | lwz r1,0(r2)  ;
sync          | lwsync        ;
xor r3,r1,r1  | li r3,1       ;
li r4,1       | stw r3,0(r4)  ;
stwx r4,r3,r5 |               ;
exists (0:r1=1 /\ 1:r1=1)

PPC ambig5
{ A=0; B=0; 0:r2=A; 0:r5=B; 1:r2=B; 1:r4=A; }
P0            | P1            ;
lwz r1,0(r2)  | li r1,1       ;
xor r3,r1,r1  | stw r1,0(r2)  ;
lwzx r4,r3,r5 | lwsync        ;
lwz r6,0(r5)  | li r3,1       ;
              | stw r3,0(r4)  ;
exists (0:r1=1 /\ 0:r4=0 /\ 0:r6=1)

PPC ambig6
{ A=0; B=0; 0:r2=B; 0:r4=A; 1:r2=A; 1:r5=B; }
P0            | P1            ;
lwz r1,0(r2)  | lwz r1,0(r2)  ;
sync          | xor r3,r1,r1  ;
lwsync        | li r4,1       ;
li r3,1       | stwx r4,r3,r5 ;
stw r3,0(r4)  |               ;
exists (0:r1=1 /\ 1:r1=1)

PPC ambig7
{ A=0; B=0; 0:r2=B; 0:r5=A; 1:r2=A; 1:r5=B; }
P0            | P1            ;
lwz r1,0(r2)  | lwz r1,0(r2)  ;
xor r3,r1,r1  | xor r3,r1,r1  ;
li r4,1       | li r4,1       ;
stwx r4,r3,r5 | stwx r4,r3,r5 ;
sync          |               ;
li r6,1       |               ;
stw r6,0(r5)  |               ;
exists (0:r1=1 /\ 1:r1=1)

PPC ambig8
{ A=0; B=0; 0:r2=B; 0:r4=A; 1:r2=A; 1:r5=B; }
P0            | P1            ;
lwz r1,0(r2)  | lwz r1,0(r2)  ;
sync          | xor r3,r1,r1  ;
li r3,1       | li r4,1       ;
stw r3,0(r4)  | stwx r4,r3,r5 ;
xor r5,r1,r1  |               ;
lwzx r6,r5,r4 |               ;
exists (0:r1=1 /\ 0:r6=1 /\ 1:r1=1)

PPC ambig9
{ A=0; B=0; 0:r2=B; 0:r5=A; 1:r2=A; 1:r5=B; }
P0            | P1            ;
li r1,1       | lwz r1,0(r2)  ;
stw r1,0(r2)  | xor r3,r1,r1  ;
lwz r3,0(r2)  | lwzx r4,r3,r5 ;
lwsync        |               ;
li r4,1       |               ;
stw r4,0(r5)  |               ;
exists (0:r3=1 /\ 1:r1=1 /\ 1:r4=0)

X86 ambig1
{ B=0; A=0; 1:EAX=1; }
P0           | P1           ;
MOV EAX,[A]  | MOV [B],$1   ;
MOV EBX,[B]  | XCHG [A],EAX ;
exists (0:EAX = 1 /\ 0:EBX = 0)

X86 ambig2
{ A=0; B=0; 1:EAX=1; 1:EBX=1; }
P0           | P1           ;
MOV EAX,[B]  | XCHG [A],EAX ;
MOV EBX,[A]  | XCHG [B],EBX ;
exists (0:EAX = 1 /\ 0:EBX = 0)

X86 ambig3
{ A=0; B=0; 0:EBX=1; }
P0           | P1           ;
MOV EAX,[B]  | MOV EAX,[A]  ;
XCHG [A],EBX | MOV [B],$1   ;
exists (0:EAX = 1 /\ 1:EAX = 1)

X86 ambig4
{ B=0; A=0; 1:EAX=1; }
P0           | P1           ;
MOV [A],$1   | XCHG [B],EAX ;
MFENCE       | MOV EBX,[A]  ;
MOV EAX,[B]  |              ;
exists (0:EAX = 0 /\ 1:EBX = 0)