Skip to content

@barrucadu barrucadu tagged this May 2, 2016 · 733 commits to master since this tag

This closes a performance loophole / soundness issue when testing relaxed
memory. Below is the relevant commit message:

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

https://hackage.haskell.org/package/dejafu-0.3.1.0
Assets 2
You can’t perform that action at this time.