Test.DejaFu

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:

>>> :{
let 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] Successful
[fail] Deterministic
    "hello" S0----S1--S0--

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

The autocheck function takes a concurrent program to test and looks for concurrency errors 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 are two failures which can arise through improper use of dejafu:

• IllegalDontCheck, the "Test.DejaFu.Conc.dontCheck" function is used as anything other than the fist action in the main thread.
• 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 and uniformly testing modes can cope with nondeterminism.

Unit testing

autocheck

Arguments

:: (MonadConc n, MonadIO n, Eq a, Show a)

=> ConcT n a

The computation to test.

-> n Bool

Automatically test a computation.

In particular, concurrency errors and nondeterminism. Returns True if all tests pass

>>> autocheck example
[pass] Successful
[fail] Deterministic
    "hello" S0----S1--S0--

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

Since: 1.0.0.0

dejafu

Arguments

:: (MonadConc n, MonadIO n, Show b)

=> String

The name of the test.

-> ProPredicate a b

The predicate to check.

-> ConcT 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--
False

Since: 1.0.0.0

dejafus

Arguments

:: (MonadConc n, MonadIO n, Show b)

=> [(String, ProPredicate a b)]

The list of predicates (with names) to check.

-> ConcT 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
False

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 main two are: the Way, which controls how schedules are explored; and the MemType, which controls how reads and writes to CRefs behave; see Test.DejaFu.Settings for a complete listing.

autocheckWay

Arguments

:: (MonadConc n, MonadIO n, Eq a, Show a)

=> Way

How to run the concurrent program.

-> MemType

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

-> ConcT 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] Successful
[fail] Deterministic
    (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---
False

>>> autocheckWay defaultWay SequentialConsistency relaxed
[pass] Successful
[fail] Deterministic
    (False,True) S0---------S1----S0--S2----S0--

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

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

Since: 1.0.0.0

dejafuWay

Arguments

:: (MonadConc n, MonadIO 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 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--
False

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

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

Since: 1.0.0.0

dejafusWay

Arguments

:: (MonadConc n, MonadIO 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 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
False

Since: 1.0.0.0

autocheckWithSettings

Arguments

:: (MonadConc n, MonadIO n, Eq a, Show a)

=> Settings n a

The SCT settings.

-> ConcT n a

The computation to test.

-> n Bool

Variant of autocheck which takes a settings record.

>>> autocheckWithSettings (fromWayAndMemType defaultWay defaultMemType) relaxed
[pass] Successful
[fail] Deterministic
    (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---
False

>>> autocheckWithSettings (fromWayAndMemType defaultWay SequentialConsistency) relaxed
[pass] Successful
[fail] Deterministic
    (False,True) S0---------S1----S0--S2----S0--

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

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

Since: 1.2.0.0

dejafuWithSettings

Arguments

:: (MonadConc n, MonadIO n, Show b)

=> Settings n a

The SCT settings.

-> String

The name of the test.

-> ProPredicate a b

The predicate to check.

-> ConcT n a

The computation to test.

-> n Bool

Variant of dejafu which takes a settings record.

>>> import System.Random

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

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

Since: 1.2.0.0

dejafusWithSettings

Arguments

:: (MonadConc n, MonadIO n, Show b)

=> Settings n a

The SCT settings.

-> [(String, ProPredicate a b)]

The list of predicates (with names) to check.

-> ConcT n a

The computation to test.

-> n Bool

Variant of dejafus which takes a settings record.

>>> dejafusWithSettings (fromWayAndMemType 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
False

Since: 1.2.0.0

module Test.DejaFu.Settings

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

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 :: Bool

  Whether the test passed or not.

• _failures :: [(Either Failure a, Trace)]

  The failing cases, if any.

• _failureMsg :: String

  A message to display on failure, if nonempty

Instances

Functor Result

Methods

fmap :: (a -> b) -> Result a -> Result b

(<$) :: a -> Result b -> Result a

Foldable Result

Methods

fold :: 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)

Methods

(==) :: Result a -> Result a -> Bool

(/=) :: Result a -> Result a -> Bool

Show a => Show (Result a)

Methods

showsPrec :: Int -> Result a -> ShowS

show :: Result a -> String

showList :: [Result a] -> ShowS

NFData a => NFData (Result a)

Methods

rnf :: Result a -> ()

data Failure

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: 1.1.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.

IllegalDontCheck

A call to dontCheck was attempted after the first action of the initial thread.

Instances

Eq Failure

Methods

(==) :: Failure -> Failure -> Bool

(/=) :: Failure -> Failure -> Bool

Ord Failure

Methods

compare :: Failure -> Failure -> Ordering

(<) :: Failure -> Failure -> Bool

(<=) :: Failure -> Failure -> Bool

(>) :: Failure -> Failure -> Bool

(>=) :: Failure -> Failure -> Bool

max :: Failure -> Failure -> Failure

min :: Failure -> Failure -> Failure

Show Failure

Methods

showsPrec :: Int -> Failure -> ShowS

show :: Failure -> String

showList :: [Failure] -> ShowS

Generic Failure

Since: 1.3.1.0

Associated Types

type Rep Failure :: * -> *

Methods

from :: Failure -> Rep Failure x

to :: Rep Failure x -> Failure

NFData Failure

Methods

rnf :: Failure -> ()

type Rep Failure

type Rep Failure = D1 * (MetaData "Failure" "Test.DejaFu.Types" "dejafu-1.10.0.0-EWUW2sYCpGM1Zul9NOYGPp" False) ((:+:) * ((:+:) * (C1 * (MetaCons "InternalError" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "Abort" PrefixI False) (U1 *)) (C1 * (MetaCons "Deadlock" PrefixI False) (U1 *)))) ((:+:) * ((:+:) * (C1 * (MetaCons "STMDeadlock" PrefixI False) (U1 *)) (C1 * (MetaCons "UncaughtException" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SomeException)))) ((:+:) * (C1 * (MetaCons "IllegalSubconcurrency" PrefixI False) (U1 *)) (C1 * (MetaCons "IllegalDontCheck" PrefixI False) (U1 *)))))

runTest

Arguments

:: MonadConc n

=> ProPredicate a b

The predicate to check

-> ConcT 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

runTestWay

Arguments

:: MonadConc 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 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

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

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

Fields

• pdiscard :: Either Failure a -> Maybe Discard

  Selectively discard results before computing the result.

• peval :: [(Either Failure a, Trace)] -> Result b

  Compute the result with the un-discarded results.

Instances

Profunctor ProPredicate

Methods

dimap :: (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

Functor (ProPredicate x)

Methods

fmap :: (a -> b) -> ProPredicate x a -> ProPredicate x b

(<$) :: a -> ProPredicate x b -> ProPredicate x a

successful :: Predicate a

Check that a computation never fails.

Since: 1.9.1.0

alwaysSame :: Eq a => Predicate a

Check that a computation always gives the same, successful, result.

alwaysSame = alwaysSameBy (==)

Since: 1.10.0.0

notAlwaysSame :: Eq a => Predicate a

Check that a computation never fails, and gives multiple distinct successful results.

notAlwaysSame = notAlwaysSameBy (==)

Since: 1.10.0.0

abortsNever :: Predicate a

Check that a computation never aborts.

Any result other than an abort, including other Failures, is allowed.

Since: 1.0.0.0

abortsAlways :: Predicate a

Check that a computation always aborts.

Since: 1.0.0.0

abortsSometimes :: Predicate a

Check that a computation aborts at least once.

Any result other than an abort, including other Failures, is allowed.

Since: 1.0.0.0

deadlocksNever :: Predicate a

Check that a computation never deadlocks.

Any result other than a deadlock, including other Failures, is allowed.

Since: 1.0.0.0

deadlocksAlways :: Predicate a

Check that a computation always deadlocks.

Since: 1.0.0.0

deadlocksSometimes :: Predicate a

Check that a computation deadlocks at least once.

Any result other than a deadlock, including other Failures, is allowed.

Since: 1.0.0.0

exceptionsNever :: Predicate a

Check that a computation never fails with an uncaught exception.

Any result other than an uncaught exception, including other Failures, is allowed.

Since: 1.0.0.0

exceptionsAlways :: Predicate a

Check that a computation always fails with an uncaught exception.

Since: 1.0.0.0

exceptionsSometimes :: Predicate a

Check that a computation fails with an uncaught exception at least once.

Any result other than an uncaught exception, including other Failures, is allowed.

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

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

alwaysSameOn :: Eq b => (a -> b) -> Predicate a

Check that a computation always gives the same (according to the provided function), successful, result.

alwaysSameOn = alwaysSameBy ((==) `on` f)

Since: 1.10.0.0

alwaysSameBy :: (a -> a -> Bool) -> Predicate a

Check that the result of a computation is always the same, using some transformation on results.

Since: 1.10.0.0

notAlwaysSameOn :: Eq b => (a -> b) -> Predicate a

Check that a computation never fails, and gives multiple distinct (according to the provided function) successful results.

notAlwaysSameOn = notAlwaysSameBy ((==) `on` f)

Since: 1.10.0.0

notAlwaysSameBy :: (a -> a -> Bool) -> Predicate a

Check that a computation never fails, and gives multiple distinct successful results, by applying a transformation on results.

This inverts the condition, so (eg) notAlwaysSameBy (==) will pass if there are unequal results.

Since: 1.10.0.0

alwaysTrue :: (Either Failure a -> Bool) -> Predicate a

Check that the result of a unary boolean predicate is always true.

Since: 1.0.0.0

somewhereTrue :: (Either Failure a -> Bool) -> Predicate a

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

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

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

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

Variant of gives that doesn't allow for expected failures.

Since: 1.0.0.0

Failures

Helper functions to identify failures.

isInternalError :: Failure -> Bool

Check if a failure is an InternalError.

Since: 0.9.0.0

isAbort :: Failure -> Bool

Check if a failure is an Abort.

Since: 0.9.0.0

isDeadlock :: Failure -> Bool

Check if a failure is a Deadlock or an STMDeadlock.

Since: 0.9.0.0

isUncaughtException :: Failure -> Bool

Check if a failure is an UncaughtException

Since: 0.9.0.0

isIllegalSubconcurrency :: Failure -> Bool

Check if a failure is an IllegalSubconcurrency

Since: 0.9.0.0

isIllegalDontCheck :: Failure -> Bool

Check if a failure is an IllegalDontCheck

Since: 1.1.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.

>>> import Control.Monad (void)
>>> :{
let 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)]
False

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.

module Test.DejaFu.Refinement

Deprecated

dejafuDiscard

Arguments

:: (MonadConc n, MonadIO 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 n a

The computation to test.

-> n Bool

Deprecated: Use dejafuWithSettings instead

Variant of dejafuWay which can selectively discard results.

>>> dejafuDiscard (\_ -> Just DiscardTrace) defaultWay defaultMemType "Discarding" alwaysSame example
[fail] Discarding
    "hello" <trace discarded>

    "world" <trace discarded>
False

Since: 1.0.0.0