dejafu-1.0.0.0: A library for unit-testing concurrent programs.

Copyright (c) 2015--2017 Michael Walker MIT Michael Walker experimental LambdaCase, MultiParamTypeClasses, TupleSections None Haskell2010

Test.DejaFu

Description

dejafu is a library for unit-testing concurrent Haskell programs, written using the concurrency package's MonadConc typeclass.

A first test: This is a simple concurrent program which forks two threads and each races to write to the same MVar:

example = do
var <- newEmptyMVar
fork (putMVar var "hello")
fork (putMVar var "world")
readMVar var

We can test it with dejafu like so:

> autocheck example
[pass] No Exceptions
[fail] Consistent Result
"hello" S0----S1--S0--

"world" S0----S2--S0--

The autocheck function takes a concurrent program to test and looks for some common unwanted behaviours: deadlocks, uncaught exceptions in the main thread, and nondeterminism. Here we see the program is nondeterministic, dejafu gives us all the distinct results it found and, for each, a summarised execution trace leading to that result:

• "Sn" means that thread "n" started executing after the previous thread terminated or blocked.
• "Pn" means that thread "n" started executing, even though the previous thread could have continued running.
• Each "-" represents one "step" of the computation.

Failures: If a program doesn't terminate successfully, we say it has failed. dejafu can detect a few different types of failure:

• Deadlock, if every thread is blocked.
• STMDeadlock, if every thread is blocked and the main thread is blocked in an STM transaction.
• UncaughtException, if the main thread is killed by an exception.

There are two types of failure which dejafu itself may raise:

• Abort, used in systematic testing (the default) if there are no allowed decisions remaining. For example, by default any test case which takes more than 250 scheduling points to finish will be aborted. You can use the systematically function to supply (or disable) your own bounds.
• InternalError, used if something goes wrong. If you get this and aren't using a scheduler you wrote yourself, please file a bug.

Finally, there is one failure which can arise through improper use of dejafu:

• IllegalSubconcurrency, the "Test.DejaFu.Conc.subconcurrency" function is used when multiple threads exist, or is used inside another subconcurrency call.

Beware of liftIO: dejafu works by running your test case lots of times with different schedules. If you use liftIO at all, make sure that any IO you perform is deterministic when executed in the same order.

If you need to test things with nondeterministc IO, see the autocheckWay, dejafuWay, and dejafusWay functions: the randomly, uniformly, and swarmy testing modes can cope with nondeterminism.

Synopsis

# Unit testing

Arguments

 :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) => ConcT r n a The computation to test. -> n Bool

Automatically test a computation.

In particular, look for deadlocks, uncaught exceptions, and multiple return values. Returns True if all tests pass

> autocheck example
[pass] No Exceptions
[fail] Consistent Result
"hello" S0----S1--S0--

"world" S0----S2--S0--

Since: 1.0.0.0

Arguments

 :: (MonadConc n, MonadIO n, MonadRef r n, Show b) => String The name of the test. -> ProPredicate a b The predicate to check. -> ConcT r n a The computation to test. -> n Bool

Check a predicate and print the result to stdout, return True if it passes.

A dejafu test has two parts: the program you are testing, and a predicate to determine if the test passes. Predicates can look for anything, including checking for some expected nondeterminism.

> dejafu "Test Name" alwaysSame example
[fail] Test Name
"hello" S0----S1--S0--

"world" S0----S2--S0--

Since: 1.0.0.0

Arguments

 :: (MonadConc n, MonadIO n, MonadRef r n, Show b) => [(String, ProPredicate a b)] The list of predicates (with names) to check. -> ConcT r n a The computation to test. -> n Bool

Variant of dejafu which takes a collection of predicates to test, returning True if all pass.

> dejafus [("A", alwaysSame), ("B", deadlocksNever)] example
[fail] A
"hello" S0----S1--S0--

"world" S0----S2--S0--
[pass] B

Since: 1.0.0.0

## Configuration

There are a few knobs to tweak to control the behaviour of dejafu. The defaults should generally be good enough, but if not you have a few tricks available.

• The Way, which controls how schedules are explored.
• The MemType, which controls how reads and writes to CRefs (or IORefs) behave.
• The Discard function, which saves memory by throwing away uninteresting results during exploration.

Arguments

 :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show 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 test. -> n Bool

Variant of autocheck which takes a way to run the program and a memory model.

> autocheckWay defaultWay defaultMemType relaxed
[pass] No Exceptions
[fail] Consistent Result
(False,True) S0---------S1----S0--S2----S0--

(False,False) S0---------S1--P2----S1--S0---

(True,False) S0---------S2----S1----S0---

(True,True) S0---------S1-C-S2----S1---S0---

> autocheckWay defaultWay SequentialConsistency relaxed
[pass] No Exceptions
[fail] Consistent Result
(False,True) S0---------S1----S0--S2----S0--

(True,True) S0---------S1-P2----S1---S0---

(True,False) S0---------S2----S1----S0---

Since: 1.0.0.0

Arguments

 :: (MonadConc n, MonadIO n, MonadRef r n, Show b) => Way How to run the concurrent program. -> MemType The memory model to use for non-synchronised CRef operations. -> String The name of the test. -> ProPredicate a b The predicate to check. -> ConcT r n a The computation to test. -> n Bool

Variant of dejafu which takes a way to run the program and a memory model.

> import System.Random

> dejafuWay (randomly (mkStdGen 0) 100) defaultMemType "Randomly!" alwaysSame example
[fail] Randomly!
"hello" S0----S1--S0--

"world" S0----S2--S0--

> dejafuWay (randomly (mkStdGen 1) 100) defaultMemType "Randomly!" alwaysSame example
[fail] Randomly!
"hello" S0----S1--S0--

"world" S0----S2--S1-S0--

Since: 1.0.0.0

Arguments

 :: (MonadConc n, MonadIO n, MonadRef r n, Show b) => Way How to run the concurrent program. -> MemType The memory model to use for non-synchronised CRef operations. -> [(String, ProPredicate a b)] The list of predicates (with names) to check. -> ConcT r n a The computation to test. -> n Bool

Variant of dejafus which takes a way to run the program and a memory model.

> dejafusWay defaultWay SequentialConsistency [("A", alwaysSame), ("B", exceptionsNever)] relaxed
[fail] A
(False,True) S0---------S1----S0--S2----S0--

(True,True) S0---------S1-P2----S1---S0---

(True,False) S0---------S2----S1----S0---
[pass] B

Since: 1.0.0.0

Arguments

 :: (MonadConc n, MonadIO n, MonadRef r n, Show b) => (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. -> String The name of the test. -> ProPredicate a b The predicate to check. -> ConcT r n a The computation to test. -> n Bool

Variant of dejafuWay which can selectively discard results.

> dejafuDiscard (\_ -> Just DiscardTrace) defaultWay defaultMemType "Discarding" alwaysSame example

"world" <trace discarded>

Since: 1.0.0.0

### Defaults

A default way to execute concurrent programs: systematically using defaultBounds.

Since: 0.6.0.0

The default memory model: TotalStoreOrder

Since: 0.2.0.0

Since: 0.7.1.0

### Exploration

data Way Source #

How to explore the possible executions of a concurrent program.

Since: 0.7.0.0

Instances

 Source # MethodsshowsPrec :: Int -> Way -> ShowS #show :: Way -> String #showList :: [Way] -> ShowS #

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

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

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

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

#### Schedule bounding

Schedule bounding is used by the systematically approach to limit the search-space, which in general will be huge.

There are three types of bounds used:

• The PreemptionBound, which bounds the number of pre-emptive context switches. Empirical evidence suggests 2 is a good value for this, if you have a small test case.
• The FairBound, which bounds the difference between how many times threads can yield. This is necessary to test certain kinds of potentially non-terminating behaviour, such as spinlocks.
• The LengthBound, which bounds how long a test case can run, in terms of scheduling decisions. This is necessary to test certain kinds of potentially non-terminating behaviour, such as livelocks.

Schedule bounding is not used by the non-systematic exploration behaviours.

data Bounds Source #

Since: 0.2.0.0

Constructors

 Bounds Fields

Instances

 Source # Methods(==) :: Bounds -> Bounds -> Bool #(/=) :: Bounds -> Bounds -> Bool # Source # Methods(<) :: Bounds -> Bounds -> Bool #(<=) :: Bounds -> Bounds -> Bool #(>) :: Bounds -> Bounds -> Bool #(>=) :: Bounds -> Bounds -> Bool #max :: Bounds -> Bounds -> Bounds #min :: Bounds -> Bounds -> Bounds # Source # Methods Source # MethodsshowsPrec :: Int -> Bounds -> ShowS #showList :: [Bounds] -> ShowS # Source # Since: 0.5.1.0 Methodsrnf :: Bounds -> () #

All bounds enabled, using their default values.

Since: 0.2.0.0

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

newtype PreemptionBound Source #

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.

Since: 0.2.0.0

Constructors

 PreemptionBound Int

Instances

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

Since: 0.2.0.0

newtype FairBound Source #

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.

Since: 0.2.0.0

Constructors

 FairBound Int

Instances

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

A sensible default fair bound: 5.

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

Since: 0.2.0.0

newtype LengthBound Source #

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

Since: 0.2.0.0

Constructors

 LengthBound Int

Instances

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

Since: 0.2.0.0

### Memory model

When executed on a multi-core processor some CRef / IORef programs can exhibit "relaxed memory" behaviours, where the apparent behaviour of the program is not a simple interleaving of the actions of each thread.

Example: This is a simple program which creates two CRefs containing False, and forks two threads. Each thread writes True to one of the CRefs and reads the other. The value that each thread reads is communicated back through an MVar:

relaxed = do
r1 <- newCRef False
r2 <- newCRef False
x <- spawn $writeCRef r1 True >> readCRef r2 y <- spawn$ writeCRef r2 True >> readCRef r1
(,) <$> readMVar x <*> readMVar y We see something surprising if we ask for the results: > autocheck relaxed [pass] Never Deadlocks [pass] No Exceptions [fail] Consistent Result (False,True) S0---------S1----S0--S2----S0-- (False,False) S0---------S1--P2----S1--S0--- (True,False) S0---------S2----S1----S0--- (True,True) S0---------S1-C-S2----S1---S0--- It's possible for both threads to read the value False, even though each writes True to the other CRef before reading. This is because processors are free to re-order reads and writes to independent memory addresses in the name of performance. Execution traces for relaxed memory computations can include "C" actions, as above, which show where CRef writes were explicitly committed, and made visible to other threads. However, modelling this behaviour can require more executions. If you do not care about the relaxed-memory behaviour of your program, use the SequentialConsistency model. data MemType Source # The memory model to use for non-synchronised CRef operations. Since: 0.4.0.0 Constructors  SequentialConsistency The most intuitive model: a program behaves as a simple interleaving of the actions in different threads. When a CRef is written to, that write is immediately visible to all threads. TotalStoreOrder Each thread has a write buffer. A thread sees its writes immediately, but other threads will only see writes when they are committed, which may happen later. Writes are committed in the same order that they are created. PartialStoreOrder Each CRef has a write buffer. A thread sees its writes immediately, but other threads will only see writes when they are committed, which may happen later. Writes to different CRefs are not necessarily committed in the same order that they are created. Instances  Source # Methods Source # MethodsenumFrom :: MemType -> [MemType] #enumFromThen :: MemType -> MemType -> [MemType] #enumFromTo :: MemType -> MemType -> [MemType] #enumFromThenTo :: MemType -> MemType -> MemType -> [MemType] # Source # Methods(==) :: MemType -> MemType -> Bool #(/=) :: MemType -> MemType -> Bool # Source # Methods(<) :: MemType -> MemType -> Bool #(<=) :: MemType -> MemType -> Bool #(>) :: MemType -> MemType -> Bool #(>=) :: MemType -> MemType -> Bool # Source # Methods Source # MethodsshowList :: [MemType] -> ShowS # Source # Since: 0.5.1.0 Methodsrnf :: MemType -> () # ### Reducing memory usage Sometimes we know that a result is uninteresting and cannot affect the result of a test, in which case there is no point in keeping it around. Execution traces can be large, so any opportunity to get rid of them early is possibly a great saving of memory. A discard function, which has type Either Failure a -> Maybe Discard, can selectively discard results or execution traces before the schedule exploration finishes, allowing them to be garbage collected sooner. Note: This is only relevant if you are producing your own predicates. The predicates and helper functions provided by this module do discard results and traces wherever possible. 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. Instances  Source # Methods Source # MethodsenumFrom :: Discard -> [Discard] #enumFromThen :: Discard -> Discard -> [Discard] #enumFromTo :: Discard -> Discard -> [Discard] #enumFromThenTo :: Discard -> Discard -> Discard -> [Discard] # Source # Methods(==) :: Discard -> Discard -> Bool #(/=) :: Discard -> Discard -> Bool # Source # Methods(<) :: Discard -> Discard -> Bool #(<=) :: Discard -> Discard -> Bool #(>) :: Discard -> Discard -> Bool #(>=) :: Discard -> Discard -> Bool # Source # Methods Source # MethodsshowList :: [Discard] -> ShowS # Source # Methodsrnf :: Discard -> () # ## Manual testing The standard testing functions print their result to stdout, and throw away some information. The traces are pretty-printed, and if there are many failures, only the first few are shown. If you need more information, use these functions. data Result a Source # The results of a test, including the number of cases checked to determine the final boolean outcome. Since: 1.0.0.0 Constructors  Result Fields_pass :: BoolWhether the test passed or not._failures :: [(Either Failure a, Trace)]The failing cases, if any._failureMsg :: StringA message to display on failure, if nonempty Instances  Source # Methodsfmap :: (a -> b) -> Result a -> Result b #(<$) :: a -> Result b -> Result a # Source # Methodsfold :: Monoid m => Result m -> m #foldMap :: Monoid m => (a -> m) -> Result a -> m #foldr :: (a -> b -> b) -> b -> Result a -> b #foldr' :: (a -> b -> b) -> b -> Result a -> b #foldl :: (b -> a -> b) -> b -> Result a -> b #foldl' :: (b -> a -> b) -> b -> Result a -> b #foldr1 :: (a -> a -> a) -> Result a -> a #foldl1 :: (a -> a -> a) -> Result a -> a #toList :: Result a -> [a] #null :: Result a -> Bool #length :: Result a -> Int #elem :: Eq a => a -> Result a -> Bool #maximum :: Ord a => Result a -> a #minimum :: Ord a => Result a -> a #sum :: Num a => Result a -> a #product :: Num a => Result a -> a # Eq a => Eq (Result a) Source # Methods(==) :: Result a -> Result a -> Bool #(/=) :: Result a -> Result a -> Bool # Show a => Show (Result a) Source # MethodsshowsPrec :: Int -> Result a -> ShowS #show :: Result a -> String #showList :: [Result a] -> ShowS # NFData a => NFData (Result a) Source # Methodsrnf :: Result a -> () #

data Failure Source #

An indication of how a concurrent computation failed.

The Eq, Ord, and NFData instances compare/evaluate the exception with show in the UncaughtException case.

Since: 0.9.0.0

Constructors

 InternalError Will be raised if the scheduler does something bad. This should never arise unless you write your own, faulty, scheduler! If it does, please file a bug report. Abort The scheduler chose to abort execution. This will be produced if, for example, all possible decisions exceed the specified bounds (there have been too many pre-emptions, the computation has executed for too long, or there have been too many yields). Deadlock Every thread is blocked, and the main thread is not blocked in an STM transaction. STMDeadlock Every thread is blocked, and the main thread is blocked in an STM transaction. UncaughtException SomeException An uncaught exception bubbled to the top of the computation. IllegalSubconcurrency Calls to subconcurrency were nested, or attempted when multiple threads existed.

Instances

 Source # Methods(==) :: Failure -> Failure -> Bool #(/=) :: Failure -> Failure -> Bool # Source # Methods(<) :: Failure -> Failure -> Bool #(<=) :: Failure -> Failure -> Bool #(>) :: Failure -> Failure -> Bool #(>=) :: Failure -> Failure -> Bool # Source # MethodsshowList :: [Failure] -> ShowS # Source # Methodsrnf :: Failure -> () #

Arguments

 :: (MonadConc n, MonadRef r n) => ProPredicate a b The predicate to check -> ConcT r n a The computation to test -> n (Result b)

Run a predicate over all executions within the default schedule bounds.

The exact executions tried, and the order in which results are found, is unspecified and may change between releases. This may affect which failing traces are reported, when there is a failure.

Since: 1.0.0.0

Arguments

 :: (MonadConc n, MonadRef r n) => Way How to run the concurrent program. -> MemType The memory model to use for non-synchronised CRef operations. -> ProPredicate a b The predicate to check -> ConcT r n a The computation to test -> n (Result b)

Variant of runTest which takes a way to run the program and a memory model.

The exact executions tried, and the order in which results are found, is unspecified and may change between releases. This may affect which failing traces are reported, when there is a failure.

Since: 1.0.0.0

## Predicates

A dejafu test has two parts: the concurrent program to test, and a predicate to determine if the test passes, based on the results of the schedule exploration.

All of these predicates discard results and traces as eagerly as possible, to reduce memory usage.

type Predicate a = ProPredicate a a Source #

A Predicate is a function which collapses a list of results into a Result, possibly discarding some on the way.

Predicate cannot be a functor as the type parameter is used both co- and contravariantly.

Since: 1.0.0.0

data ProPredicate a b Source #

A ProPredicate is a function which collapses a list of results into a Result, possibly discarding some on the way.

Since: 1.0.0.0

Constructors

 ProPredicate Fieldspdiscard :: Either Failure a -> Maybe DiscardSelectively discard results before computing the result.peval :: [(Either Failure a, Trace)] -> Result bCompute the result with the un-discarded results.

Instances

 Source # Methodsdimap :: (a -> b) -> (c -> d) -> ProPredicate b c -> ProPredicate a d #lmap :: (a -> b) -> ProPredicate b c -> ProPredicate a c #rmap :: (b -> c) -> ProPredicate a b -> ProPredicate a c #(#.) :: Coercible * c b => (b -> c) -> ProPredicate a b -> ProPredicate a c #(.#) :: Coercible * b a => ProPredicate b c -> (a -> b) -> ProPredicate a c # Source # Methodsfmap :: (a -> b) -> ProPredicate x a -> ProPredicate x b #(<$) :: a -> ProPredicate x b -> ProPredicate x a # Check that a computation never aborts. Since: 1.0.0.0 Check that a computation always aborts. Since: 1.0.0.0 Check that a computation aborts at least once. Since: 1.0.0.0 Check that a computation never deadlocks. Since: 1.0.0.0 Check that a computation always deadlocks. Since: 1.0.0.0 Check that a computation deadlocks at least once. Since: 1.0.0.0 Check that a computation never fails with an uncaught exception. Since: 1.0.0.0 Check that a computation always fails with an uncaught exception. Since: 1.0.0.0 Check that a computation fails with an uncaught exception at least once. Since: 1.0.0.0 ### Helpers Helper functions to produce your own predicates. Such predicates discard results and traces as eagerly as possible, to reduce memory usage. representative :: Eq b => ProPredicate a b -> ProPredicate a b Source # Reduce the list of failures in a ProPredicate to one representative trace for each unique result. This may throw away "duplicate" failures which have a unique cause but happen to manifest in the same way. However, it is convenient for filtering out true duplicates. Since: 1.0.0.0 alwaysSame :: Eq a => Predicate a Source # Check that the result of a computation is always the same. In particular this means either: (a) it always fails in the same way, or (b) it never fails and the values returned are all equal. alwaysSame = alwaysSameBy (==) Since: 1.0.0.0 alwaysSameOn :: Eq b => (Either Failure a -> b) -> Predicate a Source # Check that the result of a computation is always the same by comparing the result of a function on every result. alwaysSameOn = alwaysSameBy ((==) on f) Since: 1.0.0.0 alwaysSameBy :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a Source # Check that the result of a computation is always the same, using some transformation on results. Since: 1.0.0.0 Check that the result of a computation is not always the same. Since: 1.0.0.0 alwaysTrue :: (Either Failure a -> Bool) -> Predicate a Source # Check that the result of a unary boolean predicate is always true. Since: 1.0.0.0 somewhereTrue :: (Either Failure a -> Bool) -> Predicate a Source # Check that the result of a unary boolean predicate is true at least once. Since: 1.0.0.0 alwaysNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b Source # Check that a Maybe-producing function always returns Nothing. Since: 1.0.0.0 somewhereNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b Source # Check that a Maybe-producing function returns Nothing at least once. Since: 1.0.0.0 gives :: (Eq a, Show a) => [Either Failure a] -> Predicate a Source # Predicate for when there is a known set of results where every result must be exhibited at least once. Since: 1.0.0.0 gives' :: (Eq a, Show a) => [a] -> Predicate a Source # Variant of gives that doesn't allow for expected failures. Since: 1.0.0.0 ### Failures Helper functions to identify failures. Check if a failure is an InternalError. Since: 0.9.0.0 Check if a failure is an Abort. Since: 0.9.0.0 Check if a failure is a Deadlock or an STMDeadlock. Since: 0.9.0.0 Check if a failure is an UncaughtException Since: 0.9.0.0 Check if a failure is an IllegalSubconcurrency Since: 0.9.0.0 # Property testing dejafu can also use a property-testing style to test stateful operations for a variety of inputs. Inputs are generated using the [leancheck](https:/hackage.haskell.orgpackage/leancheck) library for enumerative testing. Testing MVar operations with multiple producers: These are a little different to the property tests you may be familiar with from libraries like QuickCheck (and leancheck). As we're testing properties of stateful and concurrent things, we need to provide some extra information. A property consists of two signatures and a relation between them. A signature contains: • An initialisation function, to construct the initial state. • An observation function, to take a snapshot of the state at the end. • An interference function, to mess with the state in some way. • The expression to evaluate, as a function over the state. sig e = Sig { initialise = maybe newEmptyMVar newMVar , observe = \v _ -> tryReadMVar v , interfere = \v _ -> putMVar v 42 , expression = void . e } This is a signature for operations over Num n => MVar n values where there are multiple producers. The initialisation function takes a Maybe n and constructs an MVar n, empty if it gets Nothing; the observation function reads the MVar; and the interference function puts a new value in. Given this signature, we can check if readMVar is the same as a takeMVar followed by a putMVar: > check$ sig readMVar === sig (\v -> takeMVar v >>= putMVar v)
*** Failure: (seed Just 0)
left:  [(Nothing,Just 0)]
right: [(Nothing,Just 0),(Just Deadlock,Just 42)]

The two expressions are not equivalent, and we get a counterexample: if the MVar is nonempty, then the left expression (readMVar) will preserve the value, but the right expression (v -> takeMVar v >>= putMVar v) may cause it to change. This is because of the concurrent interference we have provided: the left term never empties a full MVar, but the Right term does.