Test CMPXCHG-OK

X86_64 CMPXCHG-OK
{
int x;
int y;
0:rbx=2;
}

 P0                     | P1             ;
 movl $1,(x)            | movl $1,(y)    ;
 lock; cmpxchg (z),%ebx | mfence         ;
 movl (y),%ecx          | movl (x),%ecx  ;
exists (z=2 /\ 0:rcx=0 /\ 1:rcx=0)