| Copyright | (c) 2016 Michael Walker |
|---|---|
| License | MIT |
| Maintainer | Michael Walker <mike@barrucadu.co.uk> |
| Stability | experimental |
| Portability | CPP |
| Safe Haskell | None |
| Language | Haskell2010 |
Test.DejaFu.SCT
Contents
Description
Systematic testing for concurrent computations.
- sctBounded :: MonadRef r n => MemType -> BoundFunc ThreadId ThreadAction Lookahead -> BacktrackFunc ThreadId ThreadAction Lookahead DepState -> Conc n r a -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- data Bounds = Bounds {}
- defaultBounds :: Bounds
- noBounds :: Bounds
- sctBound :: MonadRef r n => MemType -> Bounds -> Conc n r a -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- newtype PreemptionBound :: * = PreemptionBound Int
- defaultPreemptionBound :: PreemptionBound
- sctPreBound :: MonadRef r n => MemType -> PreemptionBound -> Conc n r a -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- pBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s
- pBound :: PreemptionBound -> BoundFunc ThreadId ThreadAction Lookahead
- newtype FairBound :: * = FairBound Int
- defaultFairBound :: FairBound
- sctFairBound :: MonadRef r n => MemType -> FairBound -> Conc n r a -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- fBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s
- fBound :: FairBound -> BoundFunc ThreadId ThreadAction Lookahead
- newtype LengthBound :: * = LengthBound Int
- defaultLengthBound :: LengthBound
- sctLengthBound :: MonadRef r n => MemType -> LengthBound -> Conc n r a -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- data BacktrackStep tid action lookahead state :: * -> * -> * -> * -> * = BacktrackStep {
- bcktThreadid :: tid
- bcktDecision :: (Decision tid, action)
- bcktRunnable :: Map tid lookahead
- bcktBacktracks :: Map tid Bool
- bcktState :: state
- type BacktrackFunc tid action lookahead s = [BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s]
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
| :: MonadRef r n | |
| => MemType | The memory model to use for non-synchronised |
| -> 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. |
| -> Conc n r a | |
| -> n [(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.
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.
Constructors
| Bounds | |
Fields | |
defaultBounds :: Bounds Source #
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
| :: MonadRef r n | |
| => MemType | The memory model to use for non-synchronised |
| -> Bounds | The combined bounds. |
| -> Conc n r a | The computation to run many times |
| -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] |
An SCT runner using a bounded scheduler
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 |
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.
Arguments
| :: MonadRef r n | |
| => MemType | The memory model to use for non-synchronised |
| -> PreemptionBound | The maximum number of pre-emptions to allow in a single execution |
| -> Conc n r a | The computation to run many times |
| -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] |
An SCT runner using a pre-emption bounding scheduler.
pBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s Source #
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 Source #
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.
defaultFairBound :: FairBound #
A sensible default fair bound: 5.
This comes from playing around myself, but there is probably a better default.
Arguments
| :: MonadRef r n | |
| => MemType | The memory model to use for non-synchronised |
| -> FairBound | The maximum difference between the number of yield operations performed by different threads. |
| -> Conc n r a | The computation to run many times |
| -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] |
An SCT runner using a fair bounding scheduler.
fBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s Source #
Add a backtrack point. If the thread isn't runnable, or performs a release operation, add all runnable threads.
Length Bounding
BPOR using length bounding. This bounds the maximum length (in terms of primitive actions) of an execution.
newtype LengthBound :: * #
Constructors
| LengthBound Int |
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.
Arguments
| :: MonadRef r n | |
| => MemType | The memory model to use for non-synchronised |
| -> LengthBound | The maximum length of a schedule, in terms of primitive actions. |
| -> Conc n r a | The computation to run many times |
| -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] |
An SCT runner using a length bounding scheduler.
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 | |
Fields
| |
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.