Dat3M
Dat3M copied to clipboard
Failed atomic_cmpxchg
We currently report a wrong result for this test
C C-atomic-cmpxchg-failure-02
{
atomic_t x = ATOMIC_INIT(0);
atomic_t z = ATOMIC_INIT(0);
}
P0(atomic_t *x, atomic_t *z) {
int r0; int r1;
r0 = atomic_cmpxchg_acquire(z,2,1);
r1 = atomic_read(x);
}
P1(atomic_t *x, atomic_t *z) {
atomic_set(x,1);
atomic_set_release(z,1);
}
exists (0:r0 = 1 /\ 0:r1 = 0)
Here there is a discussion about the issue. The problem is that right now we don't support dynamic tagging, i.e. non-static unary predicates.