Copyright | (c) 2015--2018 Michael Walker |
---|---|
License | MIT |
Maintainer | Michael Walker <mike@barrucadu.co.uk> |
Stability | experimental |
Portability | TupleSections |
Safe Haskell | None |
Language | Haskell2010 |
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 thesystematically
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 anothersubconcurrency
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.
- autocheck :: (MonadConc n, MonadIO n, Eq a, Show a) => ConcT n a -> n Bool
- dejafu :: (MonadConc n, MonadIO n, Show b) => String -> ProPredicate a b -> ConcT n a -> n Bool
- dejafus :: (MonadConc n, MonadIO n, Show b) => [(String, ProPredicate a b)] -> ConcT n a -> n Bool
- autocheckWay :: (MonadConc n, MonadIO n, Eq a, Show a) => Way -> MemType -> ConcT n a -> n Bool
- dejafuWay :: (MonadConc n, MonadIO n, Show b) => Way -> MemType -> String -> ProPredicate a b -> ConcT n a -> n Bool
- dejafusWay :: (MonadConc n, MonadIO n, Show b) => Way -> MemType -> [(String, ProPredicate a b)] -> ConcT n a -> n Bool
- autocheckWithSettings :: (MonadConc n, MonadIO n, Eq a, Show a) => Settings n a -> ConcT n a -> n Bool
- dejafuWithSettings :: (MonadConc n, MonadIO n, Show b) => Settings n a -> String -> ProPredicate a b -> ConcT n a -> n Bool
- dejafusWithSettings :: (MonadConc n, MonadIO n, Show b) => Settings n a -> [(String, ProPredicate a b)] -> ConcT n a -> n Bool
- module Test.DejaFu.Settings
- data Result a = Result {}
- data Failure
- runTest :: MonadConc n => ProPredicate a b -> ConcT n a -> n (Result b)
- runTestWay :: MonadConc n => Way -> MemType -> ProPredicate a b -> ConcT n a -> n (Result b)
- type Predicate a = ProPredicate a a
- data ProPredicate a b = ProPredicate {}
- successful :: Predicate a
- alwaysSame :: Eq a => Predicate a
- notAlwaysSame :: Eq a => Predicate a
- abortsNever :: Predicate a
- abortsAlways :: Predicate a
- abortsSometimes :: Predicate a
- deadlocksNever :: Predicate a
- deadlocksAlways :: Predicate a
- deadlocksSometimes :: Predicate a
- exceptionsNever :: Predicate a
- exceptionsAlways :: Predicate a
- exceptionsSometimes :: Predicate a
- representative :: Eq b => ProPredicate a b -> ProPredicate a b
- alwaysSameOn :: Eq b => (a -> b) -> Predicate a
- alwaysSameBy :: (a -> a -> Bool) -> Predicate a
- notAlwaysSameOn :: Eq b => (a -> b) -> Predicate a
- notAlwaysSameBy :: (a -> a -> Bool) -> Predicate a
- alwaysTrue :: (Either Failure a -> Bool) -> Predicate a
- somewhereTrue :: (Either Failure a -> Bool) -> Predicate a
- alwaysNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b
- somewhereNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b
- gives :: (Eq a, Show a) => [Either Failure a] -> Predicate a
- gives' :: (Eq a, Show a) => [a] -> Predicate a
- isInternalError :: Failure -> Bool
- isAbort :: Failure -> Bool
- isDeadlock :: Failure -> Bool
- isUncaughtException :: Failure -> Bool
- isIllegalSubconcurrency :: Failure -> Bool
- isIllegalDontCheck :: Failure -> Bool
- module Test.DejaFu.Refinement
- dejafuDiscard :: (MonadConc n, MonadIO n, Show b) => (Either Failure a -> Maybe Discard) -> Way -> MemType -> String -> ProPredicate a b -> ConcT n a -> n Bool
Unit testing
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
:: (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
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 CRef
s behave; see Test.DejaFu.Settings for a
complete listing.
:: (MonadConc n, MonadIO n, Eq a, Show a) | |
=> Way | How to run the concurrent program. |
-> MemType | The memory model to use for non-synchronised |
-> 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
:: (MonadConc n, MonadIO n, Show b) | |
=> Way | How to run the concurrent program. |
-> MemType | The memory model to use for non-synchronised |
-> 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
:: (MonadConc n, MonadIO n, Show b) | |
=> Way | How to run the concurrent program. |
-> MemType | The memory model to use for non-synchronised |
-> [(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 Source #
:: (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
:: (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
:: (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.
The results of a test, including the number of cases checked to determine the final boolean outcome.
Since: 1.0.0.0
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
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 |
IllegalDontCheck | A call to |
:: 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
:: MonadConc n | |
=> Way | How to run the concurrent program. |
-> MemType | The memory model to use for non-synchronised |
-> 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 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
successful :: Predicate a Source #
Check that a computation never fails.
Since: 1.9.1.0
alwaysSame :: Eq a => Predicate a Source #
Check that a computation always gives the same, successful, result.
alwaysSame = alwaysSameBy (==)
Since: 1.10.0.0
notAlwaysSame :: Eq a => Predicate a Source #
Check that a computation never fails, and gives multiple distinct successful results.
notAlwaysSame = notAlwaysSameBy (==)
Since: 1.10.0.0
abortsNever :: Predicate a Source #
Check that a computation never aborts.
Any result other than an abort, including other Failure
s, is
allowed.
Since: 1.0.0.0
abortsAlways :: Predicate a Source #
Check that a computation always aborts.
Since: 1.0.0.0
abortsSometimes :: Predicate a Source #
Check that a computation aborts at least once.
Any result other than an abort, including other Failure
s, is
allowed.
Since: 1.0.0.0
deadlocksNever :: Predicate a Source #
Check that a computation never deadlocks.
Any result other than a deadlock, including other Failure
s, is
allowed.
Since: 1.0.0.0
deadlocksAlways :: Predicate a Source #
Check that a computation always deadlocks.
Since: 1.0.0.0
deadlocksSometimes :: Predicate a Source #
Check that a computation deadlocks at least once.
Any result other than a deadlock, including other Failure
s, is
allowed.
Since: 1.0.0.0
exceptionsNever :: Predicate a Source #
Check that a computation never fails with an uncaught exception.
Any result other than an uncaught exception, including other
Failure
s, is allowed.
Since: 1.0.0.0
exceptionsAlways :: Predicate a Source #
Check that a computation always fails with an uncaught exception.
Since: 1.0.0.0
exceptionsSometimes :: Predicate a Source #
Check that a computation fails with an uncaught exception at least once.
Any result other than an uncaught exception, including other
Failure
s, 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 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
alwaysSameOn :: Eq b => (a -> b) -> Predicate a Source #
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 Source #
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 Source #
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 Source #
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 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.
isInternalError :: Failure -> Bool Source #
Check if a failure is an InternalError
.
Since: 0.9.0.0
isDeadlock :: Failure -> Bool Source #
Check if a failure is a Deadlock
or an STMDeadlock
.
Since: 0.9.0.0
isUncaughtException :: Failure -> Bool Source #
Check if a failure is an UncaughtException
Since: 0.9.0.0
isIllegalSubconcurrency :: Failure -> Bool Source #
Check if a failure is an IllegalSubconcurrency
Since: 0.9.0.0
isIllegalDontCheck :: Failure -> Bool Source #
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
:: (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 |
-> 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