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.
The final write-to-a-reference is now in the Stop action. This is a
fairly large change as it was easiest to do this by also removing the
Ref and Fixed types, and going for a typeclass for monadic references.
Fixes#43.
Only consider STM transactions dependent if there is overlap in the
TVars they reference. Lookahead is the same worst-case behaviour as
before, as that information isn't available then.
Keep track of thread masking states and only consider a 'throwTo' as
dependent if the action being thrown at can be interrupted. This halves
the execution time of the testsuite on my linode (~190s to ~90s).
Requires dpor-0.2, as thread IDs must be known when stepping the state.
Closes#32, although I feel like there might be yet more gains possible.
-- unconfirmed hunch follows --
I feel like there might be a bug lurking here, but I haven't been able
to exhibit one.
My intuition is that because throwing an exception which can't interrupt
WILL block and so enable other threads, this might have issues in
combination with preemption bounding, although the testsuite still
passes.
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.
