Open reeselevine opened 1 week ago
Although, adding this constraint causes many of the existing tests to fail, so need to look into this a little more.
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.
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";
If I have the following simple test, which checks whether a load returns a previous store, the test fails (a satisfiable solution is found).
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 formE1 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 torf
fixes the problem, which can be done inlitmus.cpp
by adding the following code to lines 534-547: