Closed MattWindsor91 closed 4 years ago
It turns out that the first one is not the case: the input test appears to have them in the wrong order to begin with! The second bit is the real issue.
For viewers at home, an example test case is this:
C test_10
// Hint: try simulating with herd7 <test_10.litmus>
// WARNING: C litmus output is experimental!
// Declaring global variables.
{
x = 0;
y = 0;
}
// Thread 0
void P0(atomic_int *x, atomic_int *y) {
int r1 = 0;
int r0 = 0;
r0 = atomic_load_explicit(y, memory_order_acquire);
r1 = atomic_load_explicit(x, memory_order_relaxed);
}
// Thread 1
void P1(atomic_int *x, atomic_int *y) {
atomic_store_explicit(x, 1, memory_order_relaxed);
atomic_store_explicit(y, 1, memory_order_release);
}
exists (0:r0 == 1 /\ 0:r1 == 0 /\ x == 1 /\ y == 1)
Note that r1
is declared before r0
, and should ideally appear in the parameter list before it.
In a particular delitmusify run, I saw the local variables
r0
andr1
on thread 0 get assigned to parameter slots 9 and 8 respectively, even though the actual parameters generated in the output were in the opposite order.Methinks there are two issues: