Thread global variable sets should be unified

Consider the following example:

C deacon2018_big
{ x = 0; y = 0; }

void P0(atomic_int *x, atomic_int *y) {
  atomic_store_explicit(x, 1, memory_order_relaxed);
  atomic_thread_fence(memory_order_release);
  atomic_store_explicit(y, 1, memory_order_relaxed);
}

void P1(atomic_int *x, atomic_int *y) {
  int r0 = 0;

  atomic_fetch_add_explicit(y, 1, memory_order_relaxed);  // STADD
  atomic_thread_fence(memory_order_acquire);
  r0 = atomic_load_explicit(x, memory_order_relaxed);
}

void P2(atomic_int *y) {
  int r1 = 0;
  r1 = atomic_load_explicit(y, memory_order_relaxed);
}

exists (1:r0 == 0 /\ 2:r1 == 2)

Herd and Litmus accept this program, but ACT doesn't, with the error Threads disagree on global variables sets. This is because ACT is treating the fact that P2 doesn't name x as a discrepancy between the global variables sets, when it shouldn't.

The way this error should work is, instead of requiring equality of the variables sets, we should instead try to get the set union of the variables, and raise an error only if two threads declare the same variable name with a different type.

c4-project / c4f

Thread global variable sets should be unified #204