dejafu-0.9.1.2: Systematic testing for Haskell concurrency.

Copyright(c) 2016 Michael Walker
LicenseMIT
MaintainerMichael Walker <mike@barrucadu.co.uk>
Stabilityexperimental
PortabilityBangPatterns, GADTs, GeneralizedNewtypeDeriving
Safe HaskellNone
LanguageHaskell2010

Test.DejaFu.SCT

Contents

Description

Systematic testing for concurrent computations.

Synopsis

Running Concurrent Programs

data Way Source #

How to explore the possible executions of a concurrent program.

Since: 0.7.0.0

Instances

Show Way Source # 

Methods

showsPrec :: Int -> Way -> ShowS #

show :: Way -> String #

showList :: [Way] -> ShowS #

systematically Source #

Arguments

:: Bounds

The bounds to constrain the exploration.

-> Way 

Systematically execute a program, trying all distinct executions within the bounds.

This corresponds to sctBound.

Since: 0.7.0.0

randomly Source #

Arguments

:: RandomGen g 
=> g

The random generator to drive the scheduling.

-> Int

The number of executions to try.

-> Way 

Randomly execute a program, exploring a fixed number of executions.

Threads are scheduled by a weighted random selection, where weights are assigned randomly on thread creation.

This corresponds to sctWeightedRandom with weight re-use disabled, and is not guaranteed to find all distinct results (unlike systematically / sctBound).

Since: 0.7.0.0

uniformly Source #

Arguments

:: RandomGen g 
=> g

The random generator to drive the scheduling.

-> Int

The number of executions to try.

-> Way 

Randomly execute a program, exploring a fixed number of executions.

Threads are scheduled by a uniform random selection.

This corresponds to sctUniformRandom, and is not guaranteed to find all distinct results (unlike systematically / sctBound).

Since: 0.7.0.0

swarmy Source #

Arguments

:: RandomGen g 
=> g

The random generator to drive the scheduling.

-> Int

The number of executions to try.

-> Int

The number of executions to use the thread weights for.

-> Way 

Randomly execute a program, exploring a fixed number of executions.

Threads are scheduled by a weighted random selection, where weights are assigned randomly on thread creation.

This corresponds to sctWeightedRandom, and is not guaranteed to find all distinct results (unlike systematically / sctBound).

Since: 0.7.0.0

runSCT Source #

Arguments

:: MonadRef r n 
=> Way

How to run the concurrent program.

-> MemType

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

-> ConcT r n a

The computation to run many times.

-> n [(Either Failure a, Trace)] 

Explore possible executions of a concurrent program according to the given Way.

Since: 0.6.0.0

resultsSet Source #

Arguments

:: (MonadRef r n, Ord a) 
=> Way

How to run the concurrent program.

-> MemType

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

-> ConcT r n a

The computation to run many times.

-> n (Set (Either Failure a)) 

Return the set of results of a concurrent program.

Since: 0.6.0.0

Discarding variants

data Discard Source #

An Either Failure a -> Maybe Discard value can be used to selectively discard results.

Since: 0.7.1.0

Constructors

DiscardTrace

Discard the trace but keep the result. The result will appear to have an empty trace.

DiscardResultAndTrace

Discard the result and the trace. It will simply not be reported as a possible behaviour of the program.

runSCTDiscard Source #

Arguments

:: MonadRef r n 
=> (Either Failure a -> Maybe Discard)

Selectively discard results.

-> Way

How to run the concurrent program.

-> MemType

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

-> ConcT r n a

The computation to run many times.

-> n [(Either Failure a, Trace)] 

A variant of runSCT which can selectively discard results.

Since: 0.7.1.0

resultsSetDiscard Source #

Arguments

:: (MonadRef r n, Ord a) 
=> (Either Failure a -> Maybe Discard)

Selectively discard results. Traces are always discarded.

-> Way

How to run the concurrent program.

-> MemType

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

-> ConcT r n a

The computation to run many times.

-> n (Set (Either Failure a)) 

A variant of resultsSet which can selectively discard results.

Since: 0.7.1.0

Strict variants

runSCT' :: (MonadRef r n, NFData a) => Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)] Source #

A strict variant of runSCT.

Demanding the result of this will force it to normal form, which may be more efficient in some situations.

Since: 0.6.0.0

resultsSet' :: (MonadRef r n, Ord a, NFData a) => Way -> MemType -> ConcT r n a -> n (Set (Either Failure a)) Source #

A strict variant of resultsSet.

Demanding the result of this will force it to normal form, which may be more efficient in some situations.

Since: 0.6.0.0

runSCTDiscard' :: (MonadRef r n, NFData a) => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)] Source #

A strict variant of runSCTDiscard.

Demanding the result of this will force it to normal form, which may be more efficient in some situations.

Since: 0.7.1.0

resultsSetDiscard' :: (MonadRef r n, Ord a, NFData a) => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT r n a -> n (Set (Either Failure a)) Source #

A strict variant of resultsSetDiscard.

Demanding the result of this will force it to normal form, which may be more efficient in some situations.

Since: 0.7.1.0

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 a combination pre-emption, fair, and length bounding runner:

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

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

noBounds :: Bounds Source #

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 terminates!

Since: 0.3.0.0

sctBound Source #

Arguments

:: MonadRef r n 
=> MemType

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

-> Bounds

The combined bounds.

-> ConcT r n a

The computation to run many times

-> n [(Either Failure a, Trace)] 

SCT via BPOR.

Schedules are generated by running the computation with a deterministic scheduler with some initial list of decisions. 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.

Since: 0.5.0.0

sctBoundDiscard Source #

Arguments

:: MonadRef r n 
=> (Either Failure a -> Maybe Discard)

Selectively discard results.

-> MemType

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

-> Bounds

The combined bounds.

-> ConcT r n a

The computation to run many times

-> n [(Either Failure a, Trace)] 

A variant of sctBound which can selectively discard results.

Since: 0.7.1.0

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

Since: 0.2.0.0

Constructors

PreemptionBound Int 

Instances

Enum PreemptionBound Source # 
Eq PreemptionBound Source # 
Integral PreemptionBound Source # 
Num PreemptionBound Source # 
Ord PreemptionBound Source # 
Read PreemptionBound Source # 
Real PreemptionBound Source # 
Show PreemptionBound Source # 
NFData PreemptionBound Source #

Since: 0.5.1.0

Methods

rnf :: PreemptionBound -> () #

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

Since: 0.2.0.0

Constructors

FairBound Int 

Instances

Enum FairBound Source # 
Eq FairBound Source # 
Integral FairBound Source # 
Num FairBound Source # 
Ord FairBound Source # 
Read FairBound Source # 
Real FairBound Source # 
Show FairBound Source # 
NFData FairBound Source #

Since: 0.5.1.0

Methods

rnf :: FairBound -> () #

Length Bounding

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

newtype LengthBound Source #

Since: 0.2.0.0

Constructors

LengthBound Int 

Instances

Enum LengthBound Source # 
Eq LengthBound Source # 
Integral LengthBound Source # 
Num LengthBound Source # 
Ord LengthBound Source # 
Read LengthBound Source # 
Real LengthBound Source # 
Show LengthBound Source # 
NFData LengthBound Source #

Since: 0.5.1.0

Methods

rnf :: LengthBound -> () #

Random Scheduling

By greatly sacrificing completeness, testing of a large concurrent system can be greatly sped-up. Counter-intuitively, random scheduling has better bug-finding behaviour than just executing a program "for real" many times. This is perhaps because a random scheduler is more chaotic than the real scheduler.

sctUniformRandom Source #

Arguments

:: (MonadRef r n, RandomGen g) 
=> MemType

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

-> g

The random number generator.

-> Int

The number of executions to perform.

-> ConcT r n a

The computation to run many times.

-> n [(Either Failure a, Trace)] 

SCT via uniform random scheduling.

Schedules are generated by assigning to each new thread a random weight. Threads are then scheduled by a weighted random selection.

This is not guaranteed to find all distinct results.

Since: 0.7.0.0

sctWeightedRandom Source #

Arguments

:: (MonadRef r n, RandomGen g) 
=> MemType

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

-> g

The random number generator.

-> Int

The number of executions to perform.

-> Int

The number of executions to use the same set of weights for.

-> ConcT r n a

The computation to run many times.

-> n [(Either Failure a, Trace)] 

SCT via weighted random scheduling.

Schedules are generated by assigning to each new thread a random weight. Threads are then scheduled by a weighted random selection.

This is not guaranteed to find all distinct results.

Since: 0.7.0.0

sctUniformRandomDiscard Source #

Arguments

:: (MonadRef r n, RandomGen g) 
=> (Either Failure a -> Maybe Discard)

Selectively discard results.

-> MemType

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

-> g

The random number generator.

-> Int

The number of executions to perform.

-> ConcT r n a

The computation to run many times.

-> n [(Either Failure a, Trace)] 

A variant of sctUniformRandom which can selectively discard results.

Since: 0.7.1.0

sctWeightedRandomDiscard Source #

Arguments

:: (MonadRef r n, RandomGen g) 
=> (Either Failure a -> Maybe Discard)

Selectively discard results.

-> MemType

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

-> g

The random number generator.

-> Int

The number of executions to perform.

-> Int

The number of executions to use the same set of weights for.

-> ConcT r n a

The computation to run many times.

-> n [(Either Failure a, Trace)] 

A variant of sctWeightedRandom which can selectively discard results.

Since: 0.7.1.0