async-dejafu, hunit-dejafu, and tasty-dejafu only get a minor bump
because the API didn't change, only the dependencies. I'm not entirely
sure how to fit that properly into the PVP.
This massively reduces the number of schedules tried for the litmus
tests, as expected, which is great! Interestingly, it does result in
more unique results being discovered for intelWP27 and intelWP28. This
is surprising DPOR is supposed to be complete. Perhaps this indicates
some unsoundness in the way I have integrated schedule bounding with
relaxed memory.
For some reason, this causes significantly more schedules to be explored
in some of the litmus tests, in particular intelWP27 and intelWP28. I've
not dug too deeply, but it's probably something which should be
addresed.
There should be one buffer for each (thread, ref) pair, not simply for
each ref. The former is too strict as it enforces a total order on the
commits to the same ref, yielding some bizarro memory model which is
both stricter and more relaxed than TSO.
This does add extra schedules when testing PSO. But that is to be
expected, as this makes PSO executions less deterministic. Unfortunately
this additional nondeterminism is required by the memory model.
An unsynchronised write and a commit to the same CRef are independent if
the buffer is nonempty, because the commit will take from the front of
the buffer and the write will append to the end.
See [RMMVerification], lemma 5.25. It doesn't translate directly because
of the different models, but it's the same optimisation in spirit.
