Conceptually, commits are happening truly in parallel
nondeterministically, and the commit threads are introduced to unify
this source of nondeterminism with the scheduling decisions. Commit
threads are not real threads, and switching to one is not a real context
switch, it therefore doesn't count as a preemption.
For example, this execution clearly has no preemptions in:
S1---C-S1---
It would be absurd to say it has 1 preemption. But what about this?
S1---C-S2---
This clearly DOES have a preemption. S1 was preempted by C (but we don't
count that), and then S2 started to execute! Control should have been
returned to S1.
Prior to now, this case was not considered specially. So every commit
effectively gives rise to a free preemption! This is bad for two
reasons:
- More schedules get executed, so testing takes longer.
- This is actually, in a sense, unsound! Results are potentially being
reported which could NEVER arise under ANY real-world execution
subject to those bounds!
It is because of this latter point that some of the expected results in
test litmusWP27 have been removed. They require more than the standard
two preemptions to observe.
Closes#39.
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.
