Failed atomic_cmpxchg

[hernanponcedeleon]

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.