You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
The text was updated successfully, but these errors were encountered:
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:
The text was updated successfully, but these errors were encountered: