dejafu-0.3.2.0: Overloadable primitives for testable, potentially non-deterministic, concurrency.

Copyright (c) 2016 Michael Walker MIT Michael Walker experimental CPP, RankNTypes None Haskell2010

Test.DejaFu.SCT

Description

Systematic testing for concurrent computations.

Synopsis

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

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 -> BacktrackFunc ThreadId ThreadAction Lookahead DepState 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.

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 Source #

Constructors

 Bounds Fields

All bounds enabled, using their default values.

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!

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

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

 Methods Methods Methods Methods Methods Methods Methods MethodsshowList :: [PreemptionBound] -> ShowS # Methodsrnf :: 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.

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.

Variant of sctPreBound for computations which do IO.

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.

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

 MethodsenumFrom :: FairBound -> [FairBound] # Methods Methods Methods Methods Methods Methods MethodsshowList :: [FairBound] -> ShowS # Methodsrnf :: FairBound -> () #

A sensible default fair bound: 5.

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

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.

Variant of sctFairBound for computations which do IO.

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

 Methods Methods Methods Methods Methods Methods Methods MethodsshowList :: [LengthBound] -> ShowS # Methodsrnf :: 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.

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.

Variant of sctFairBound for computations which do IO.

# Backtracking

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 FieldsbcktThreadid :: tidThe thread running at this stepbcktDecision :: (Decision tid, action)What happened at this step.bcktRunnable :: Map tid lookaheadThe threads runnable at this stepbcktBacktracks :: Map tid BoolThe list of alternative threads to run, and whether those alternatives were added conservatively due to the bound.bcktState :: stateSome domain-specific state at this point.

Instances

 (Show tid, Show action, Show lookahead, Show state) => Show (BacktrackStep tid action lookahead state) MethodsshowsPrec :: Int -> BacktrackStep tid action lookahead state -> ShowS #show :: BacktrackStep tid action lookahead state -> String #showList :: [BacktrackStep tid action lookahead state] -> ShowS # (NFData tid, NFData action, NFData lookahead, NFData state) => NFData (BacktrackStep tid action lookahead state) Methodsrnf :: BacktrackStep tid action lookahead state -> () #

type BacktrackFunc tid action lookahead s = [BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s] #

A backtracking step is a point in the execution where another decision needs to be made, in order to explore interesting new schedules. A backtracking function takes the steps identified so far and a point and a thread to backtrack to, and inserts at least that backtracking point. More may be added to compensate for the effects of the bounding function. For example, under pre-emption bounding a conservative backtracking point is added at the prior context switch.

In general, a backtracking function should identify one or more backtracking points, and then use backtrackAt to do the actual work.