New coverage report, as there have been a bunch of new tests since the
one in the CONTRIBUTING file was generated:
54% expressions used (4311/7948)
51% boolean coverage (67/131)
47% guards (50/106), 31 always True, 6 always False, 19 unevaluated
57% 'if' conditions (11/19), 2 always True, 1 always False, 5 unevaluated
100% qualifiers (6/6)
61% alternatives used (413/671)
83% local declarations used (212/254)
28% top-level declarations used (313/1099)
This makes `stepThread` messier, and doesn't actually prevent nesting
currently - although it does prevent usage when there are multiple
threads, which may be enough.
Removing the stuff broke some of the litmus tests, which is bad. It
probably means that those actions were being put into sleep sets, and so
hiding actually interesting interleavings from the POR implementation. I
need to improve the lookahead behaviour to ignore these invisible
actions.
Closes#46.
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.
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.
