Test.DejaFu.SCT

Systematic testing for concurrent computations.

Bounded Partial-order Reduction

We can characterise the state of a concurrent computation by considering the ordering of dependent events. This is a partial order: independent events can be performed in any order without affecting the result, and so are not ordered.

Partial-order reduction is a technique for computing these partial orders, and only testing one total order for each partial order. This cuts down the amount of work to be done significantly. Bounded partial-order reduction is a further optimisation, which only considers schedules within some bound.

This module provides both a generic function for BPOR, and also a pre-emption bounding BPOR runner, which is used by the Test.DejaFu module.

See Bounded partial-order reduction, K. Coons, M. Musuvathi, K. McKinley for more details.

data BacktrackStep tid action lookahead state :: * -> * -> * -> * -> *

One step of the execution, including information for backtracking purposes. This backtracking information is used to generate new schedules.

Constructors

BacktrackStep

Fields

bcktThreadid :: tid

The thread running at this step

bcktDecision :: (Decision tid, action)

What happened at this step.

bcktRunnable :: Map tid lookahead

The threads runnable at this step

bcktBacktracks :: Map tid Bool

The list of alternative threads to run, and whether those alternatives were added conservatively due to the bound.

bcktState :: state

Some domain-specific state at this point.

Instances

(Show tid, Show action, Show lookahead, Show state) => Show (BacktrackStep tid action lookahead state)

(NFData tid, NFData action, NFData lookahead, NFData state) => NFData (BacktrackStep tid action lookahead state)

sctBounded

Arguments

:: MemType

The memory model to use for non-synchronised CRef operations.

-> BoundFunc ThreadId ThreadAction Lookahead

Check if a prefix trace is within the bound

-> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState])

Add a new backtrack point, this takes the history of the execution so far, the index to insert the backtracking point, and the thread to backtrack to. This may insert more than one backtracking point.

-> (forall t. ConcST t a)

-> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]

SCT via BPOR.

Schedules are generated by running the computation with a deterministic scheduler with some initial list of decisions, after which the supplied function is called. At each step of execution, possible-conflicting actions are looked for, if any are found, "backtracking points" are added, to cause the events to happen in a different order in a future execution.

Note that unlike with non-bounded partial-order reduction, this may do some redundant work as the introduction of a bound can make previously non-interfering events interfere with each other.

sctBoundedIO :: MemType -> BoundFunc ThreadId ThreadAction Lookahead -> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState]) -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]

Variant of sctBounded for computations which do IO.

Combination Bounds

Combination schedule bounding, where individual bounds are enabled if they are set.

• Pre-emption + fair bounding is useful for programs which use loop/yield control flows but are otherwise terminating.
• Pre-emption, fair + length bounding is useful for non-terminating programs, and used by the testing functionality in Test.DejaFu.

data Bounds

Constructors

Bounds

Fields

boundPreemp :: Maybe PreemptionBound

boundFair :: Maybe FairBound

boundLength :: Maybe LengthBound

defaultBounds :: Bounds

All bounds enabled, using their default values.

noBounds :: Bounds

No bounds enabled. This forces the scheduler to just use partial-order reduction and sleep sets to prune the search space. This will ONLY work if your computation always terminated!

sctBound

Arguments

:: MemType

The memory model to use for non-synchronised CRef operations.

-> Bounds

The combined bounds.

-> (forall t. ConcST t a)

The computation to run many times

-> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]

An SCT runner using a bounded scheduler

sctBoundIO :: MemType -> Bounds -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]

Variant of sctBound for computations which do IO.

Individual Bounds

Pre-emption Bounding

BPOR using pre-emption bounding. This adds conservative backtracking points at the prior context switch whenever a non-conervative backtracking point is added, as alternative decisions can influence the reachability of different states.

See the BPOR paper for more details.

newtype PreemptionBound :: *

Constructors

PreemptionBound Int

Instances

Enum PreemptionBound

Eq PreemptionBound

Integral PreemptionBound

Num PreemptionBound

Ord PreemptionBound

Read PreemptionBound

Real PreemptionBound

Show PreemptionBound

NFData PreemptionBound

defaultPreemptionBound :: PreemptionBound

A sensible default preemption bound: 2.

See Concurrency Testing Using Schedule Bounding: an Empirical Study, P. Thomson, A. F. Donaldson, A. Betts for justification.

sctPreBound

Arguments

:: MemType

The memory model to use for non-synchronised CRef operations.

-> PreemptionBound

The maximum number of pre-emptions to allow in a single execution

-> (forall t. ConcST t a)

The computation to run many times

-> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]

An SCT runner using a pre-emption bounding scheduler.

sctPreBoundIO :: MemType -> PreemptionBound -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]

Variant of sctPreBound for computations which do IO.

pBacktrack

Arguments

:: [BacktrackStep ThreadId ThreadAction Lookahead s]

The current backtracking points.

-> Int

The point to backtrack to.

-> ThreadId

The thread to backtrack to.

-> [BacktrackStep ThreadId ThreadAction Lookahead s]

Add a backtrack point, and also conservatively add one prior to the most recent transition before that point. This may result in the same state being reached multiple times, but is needed because of the artificial dependency imposed by the bound.

pBound :: PreemptionBound -> BoundFunc ThreadId ThreadAction Lookahead

Pre-emption bound function. This is different to preempBound in that it does not count pre-emptive context switches to a commit thread.

Fair Bounding

BPOR using fair bounding. This bounds the maximum difference between the number of yield operations different threads have performed.

See the BPOR paper for more details.

newtype FairBound :: *

Constructors

FairBound Int

Instances

Enum FairBound

Eq FairBound

Integral FairBound

Num FairBound

Ord FairBound

Read FairBound

Real FairBound

Show FairBound

NFData FairBound

defaultFairBound :: FairBound

A sensible default fair bound: 5.

This comes from playing around myself, but there is probably a better default.

sctFairBound

Arguments

:: MemType

The memory model to use for non-synchronised CRef operations.

-> FairBound

The maximum difference between the number of yield operations performed by different threads.

-> (forall t. ConcST t a)

The computation to run many times

-> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]

An SCT runner using a fair bounding scheduler.

sctFairBoundIO :: MemType -> FairBound -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]

Variant of sctFairBound for computations which do IO.

fBacktrack

Arguments

:: [BacktrackStep ThreadId ThreadAction Lookahead s]

The current backtracking points.

-> Int

The point to backtrack to.

-> ThreadId

The thread to backtrack to.

-> [BacktrackStep ThreadId ThreadAction Lookahead s]

Add a backtrack point. If the thread isn't runnable, or performs a release operation, add all runnable threads.

fBound :: FairBound -> BoundFunc ThreadId ThreadAction Lookahead

Fair bound function

Length Bounding

BPOR using length bounding. This bounds the maximum length (in terms of primitive actions) of an execution.

newtype LengthBound :: *

Constructors

LengthBound Int

Instances

Enum LengthBound

Eq LengthBound

Integral LengthBound

Num LengthBound

Ord LengthBound

Read LengthBound

Real LengthBound

Show LengthBound

NFData LengthBound

defaultLengthBound :: LengthBound

A sensible default length bound: 250.

Based on the assumption that anything which executes for much longer (or even this long) will take ages to test.

sctLengthBound

Arguments

:: MemType

The memory model to use for non-synchronised CRef operations.

-> LengthBound

The maximum length of a schedule, in terms of primitive actions.

-> (forall t. ConcST t a)

The computation to run many times

-> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]

An SCT runner using a length bounding scheduler.

sctLengthBoundIO :: MemType -> LengthBound -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]

Variant of sctFairBound for computations which do IO.