Safe Haskell | None |
---|---|
Language | Haskell2010 |
Systematic testing for concurrent computations.
- data BacktrackStep tid action lookahead state :: * -> * -> * -> * -> * = BacktrackStep {
- bcktThreadid :: tid
- bcktDecision :: (Decision tid, action)
- bcktRunnable :: Map tid lookahead
- bcktBacktracks :: Map tid Bool
- bcktState :: state
- sctBounded :: MemType -> BoundFunc ThreadId ThreadAction Lookahead -> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState]) -> (forall t. ConcST t a) -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- 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)]
- data Bounds = Bounds {}
- defaultBounds :: Bounds
- noBounds :: Bounds
- sctBound :: MemType -> Bounds -> (forall t. ConcST t a) -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- sctBoundIO :: MemType -> Bounds -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- newtype PreemptionBound :: * = PreemptionBound Int
- defaultPreemptionBound :: PreemptionBound
- sctPreBound :: MemType -> PreemptionBound -> (forall t. ConcST t a) -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- sctPreBoundIO :: MemType -> PreemptionBound -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- pBacktrack :: [BacktrackStep ThreadId ThreadAction Lookahead s] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead s]
- pBound :: PreemptionBound -> BoundFunc ThreadId ThreadAction Lookahead
- newtype FairBound :: * = FairBound Int
- defaultFairBound :: FairBound
- sctFairBound :: MemType -> FairBound -> (forall t. ConcST t a) -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- sctFairBoundIO :: MemType -> FairBound -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- fBacktrack :: [BacktrackStep ThreadId ThreadAction Lookahead s] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead s]
- fBound :: FairBound -> BoundFunc ThreadId ThreadAction Lookahead
- newtype LengthBound :: * = LengthBound Int
- defaultLengthBound :: LengthBound
- sctLengthBound :: MemType -> LengthBound -> (forall t. ConcST t a) -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
- sctLengthBoundIO :: MemType -> LengthBound -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
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.
BacktrackStep | |
|
:: MemType | The memory model to use for non-synchronised |
-> 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)] Source #
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
.
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!
:: MemType | The memory model to use for non-synchronised |
-> 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)] Source #
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 :: * #
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.
:: MemType | The memory model to use for non-synchronised |
-> 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)] Source #
Variant of sctPreBound
for computations which do IO
.
:: [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 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.
:: MemType | The memory model to use for non-synchronised |
-> 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)] Source #
Variant of sctFairBound
for computations which do IO
.
:: [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.
Length Bounding
BPOR using length bounding. This bounds the maximum length (in terms of primitive actions) of an execution.
newtype 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.
:: MemType | The memory model to use for non-synchronised |
-> 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)] Source #
Variant of sctFairBound
for computations which do IO
.