Issue in constraint generation enforcing reads-from

[reeselevine]

If I have the following simple test, which checks whether a load returns a previous store, the test fails (a satisfiable solution is found).

NEWWG
NEWSG
NEWTHREAD
st.sc0 c = 1
ld.sc0 c = 2
NOSOLUTION consistent[X] && #dr=0

Looking at the counterexample generated, the issue appears to be that Alloy happily puts a reads-from relation between the two instructions, despite 2 not being the value written previously. When putting ld.sc0 c = 0, the test passes, because a constraint of the form E1 in X.RFINIT is correctly generated. The issue exists for both atomic/non-atomic instructions.

I don't think the problem is with the model, it looks like adding a not in constraint to rf fixes the problem, which can be done in litmus.cpp by adding the following code to lines 534-547:

            } else if (instState.loadStore[i].var == instState.loadStore[j].var &&
                instState.isWrite(i) && instState.isRead(j) &&
                instState.getWriteValue(i) != instState.getReadValue(j)) {
                o << "    (E" << i << "->E" << j << ") not in X.rf\n";

[reeselevine]

Although, adding this constraint causes many of the existing tests to fail, so need to look into this a little more.

[reeselevine]

Ok, needed to add a couple checks to deal with cases where write/read values are unconstrained. The full condition now is:

            } else if (instState.loadStore[i].var == instState.loadStore[j].var &&
                instState.isWrite(i) && instState.isRead(j) &&
                instState.getWriteValue(i) != -1 &&
                instState.getReadValue(j) != -1 &&
                instState.getWriteValue(i) != instState.getReadValue(j)) {

All tests pass when generated using this condition.

[reeselevine]

I'm running into one other potentially buggy test outcome. Given this test:

NEWWG
NEWSG
NEWTHREAD
st.sc0 a = 1
ld.sc0 b = 1
NOSOLUTION consistent[X] && #dr=0

A solution is found where b reads from the initial state. However, my understanding is that we assume the initial state of memory is 0, so this should not occur.

Adding another constraint when generating rf fixes this, and all other tests pass as well. The > 0 condition is needed to account for unconstrained reads which may read from the initial state.

            } else if (i == j && instState.isRead(j) && instState.getReadValue(j) > 0) {
                o << "    E" << j << " not in X.RFINIT\n";