In LKMM, a failing cmpxchg is just a once access with no implied barriers.
Per my understanding, GenMC currently inserts atomic-related mb() around cmpxchg
https://github.com/MPI-SWS/genmc/blob/master/include/lkmm.h#L133
which in LKMM also provide ordering in case the RMW fails:
P0(int *x, int *y, int *z)
{
WRITE_ONCE(*x, 1);
smp_store_release(y, 1);
}
P1(int *x, int *y, int *z)
{
int r = 2;
if (atomic_cmpxchg(y, 2, 2)) {
smp_mb__after_atomic();
r = READ_ONCE(*x);
}
}
exists (1:r=0) // impossible