dejafu-0.7.0.2: Systematic testing for Haskell concurrency.

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

Test.DejaFu.SCT

Contents

Description

Systematic testing for concurrent computations.

Synopsis

Running Concurrent Programs

data Way #

How to explore the possible executions of a concurrent program.

Since: 0.7.0.0

Instances

Show Way # 

Methods

showsPrec :: Int -> Way -> ShowS #

show :: Way -> String #

showList :: [Way] -> ShowS #

systematically #

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 #

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 #

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 #

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 #

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

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

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 #

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

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

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

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 #

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 #

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

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 #

Since: 0.2.0.0

Constructors

PreemptionBound Int 

Instances

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

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 #

Since: 0.2.0.0

Constructors

FairBound Int 

Instances

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

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 #

Since: 0.2.0.0

Constructors

LengthBound Int 

Instances

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

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 #

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 #

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