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.

Conditions: A program may fail to terminate in a way which produces a value. dejafu can detect a few such cases:

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

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 IORefs 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 IORef 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 IORef 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 IORef 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 Condition a, Trace)]

  The failing cases, if any.

• _failureMsg :: String

  A message to display on failure, if nonempty

Instances

Functor Result

Defined in Test.DejaFu

Methods

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

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

Foldable Result

Defined in Test.DejaFu

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)

Defined in Test.DejaFu

Methods

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

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

Show a => Show (Result a)

Defined in Test.DejaFu

Methods

showsPrec :: Int -> Result a -> ShowS

show :: Result a -> String

showList :: [Result a] -> ShowS

NFData a => NFData (Result a)

Defined in Test.DejaFu

Methods

rnf :: Result a -> ()

data Condition

An indication of how a concurrent computation terminated, if it didn't produce a value.

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

Since: 1.12.0.0

Constructors

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.

Instances

Eq Condition

Defined in Test.DejaFu.Types

Methods

(==) :: Condition -> Condition -> Bool

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

Ord Condition

Defined in Test.DejaFu.Types

Methods

compare :: Condition -> Condition -> Ordering

(<) :: Condition -> Condition -> Bool

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

(>) :: Condition -> Condition -> Bool

(>=) :: Condition -> Condition -> Bool

max :: Condition -> Condition -> Condition

min :: Condition -> Condition -> Condition

Show Condition

Defined in Test.DejaFu.Types

Methods

showsPrec :: Int -> Condition -> ShowS

show :: Condition -> String

showList :: [Condition] -> ShowS

Generic Condition

Defined in Test.DejaFu.Types

Associated Types

type Rep Condition :: Type -> Type

Methods

from :: Condition -> Rep Condition x

to :: Rep Condition x -> Condition

NFData Condition

Defined in Test.DejaFu.Types

Methods

rnf :: Condition -> ()

type Rep Condition

Defined in Test.DejaFu.Types

type Rep Condition = D1 (MetaData "Condition" "Test.DejaFu.Types" "dejafu-1.12.0.0-DIjpmnM3gUIFghrMy7zMb1" False) ((C1 (MetaCons "Abort" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Deadlock" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "STMDeadlock" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "UncaughtException" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SomeException))))

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 IORef 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 Condition a -> Maybe Discard

  Selectively discard results before computing the result.

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

  Compute the result with the un-discarded results.

Instances

Profunctor ProPredicate

Defined in Test.DejaFu

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 => q b c -> ProPredicate a b -> ProPredicate a c

(.#) :: Coercible b a => ProPredicate b c -> q a b -> ProPredicate a c

Functor (ProPredicate x)

Defined in Test.DejaFu

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 Conditions, 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 Conditions, is allowed.

Since: 1.0.0.0

deadlocksNever :: Predicate a

Check that a computation never deadlocks.

Any result other than a deadlock, including other Conditions, 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 Conditions, 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 Conditions, 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 Conditions, 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 Condition a -> Bool) -> Predicate a

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

Since: 1.0.0.0

somewhereTrue :: (Either Condition 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 Condition a -> Maybe (Either Condition b)) -> ProPredicate a b

Check that a Maybe-producing function always returns Nothing.

Since: 1.0.0.0

somewhereNothing :: (Either Condition a -> Maybe (Either Condition 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 Condition 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 non-success conditions.

Since: 1.0.0.0

Conditions

Helper functions to identify conditions.

isAbort :: Condition -> Bool

Check if a condition is an Abort.

Since: 0.9.0.0

isDeadlock :: Condition -> Bool

Check if a condition is a Deadlock or an STMDeadlock.

Since: 0.9.0.0

isUncaughtException :: Condition -> Bool

Check if a condition is an UncaughtException

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.

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

type Failure = Condition

Deprecated: The Failure type has been split up into Condition and Error, with different semantics.

A type synonym for Condition, use that instead.

Since: 1.12.0.0

dejafuDiscard

Arguments

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

=> (Either Condition a -> Maybe Discard)

Selectively discard results.

-> Way

How to run the concurrent program.

-> MemType

The memory model to use for non-synchronised IORef 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