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.
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.
