No-Thin-Air axiom testing

[tonghaining]

Hello, I conducted several test cases and it seems the No-Thin-Air axiom is not being obeyed. If the test case below has been written correctly according to the grammar rules, then I think "r0 == 42 && r1 == 42" should be a forbidden outcome. Could you take a look? Thanks!

`
.global x;
.global y;

d0.b0.t0 {
ld.weak r0, [x];
st.weak [y], r0;
}

d0.b1.t1 {
ld.weak r1, [y];
st.weak [x], r1;
}

assert (r0 != 42 || r1 != 42) as no_thin_air;
`

[daniellustig]

Thank you for the report. Indeed, the tool does not currently track dependency ordering in litmus tests it parses. (Although the Alloy model does model the dep relation, the test parser leaves it empty.)

There's nothing preventing the parser from tracking dependencies properly. The issue is just that PTX only uses dependency ordering for the no-thin-air axiom, and that axiom wasn't a focus of the mixed proxy memory model paper this tool was developed to study. We just prioritized other aspects of the model over this one.

I will leave this issue open in case I find time to support tracking of dependency ordering in the future.