Copyright	(c) 2015--2019 Michael Walker
License	MIT
Maintainer	Michael Walker <mike@barrucadu.co.uk>
Stability	experimental
Portability	TupleSections
Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.DejaFu

Contents

Unit testing
Property-based testing
Expressing concurrent programs
- Setup and teardown
- Invariants

Description

dejafu is a library for unit-testing concurrent Haskell programs which are written using the <https://hackage.haskell.org/package/concurrency concurrency> package's MonadConc typeclass.

For more in-depth documentation, including migration guides from earlier versions of dejafu, see the <https://dejafu.docs.barrucadu.co.uk/ website>.

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.

Memory models: dejafu supports three different memory models, which affect how one thread's IORef updates become visible to other threads.

Sequential consistency: a program behaves as a simple interleaving of the actions in different threads. When an IORef is written to, that write is immediately visible to all threads.
Total store order (TSO): 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.
Partial store order (PSO): each IORef 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 IORefs are not necessarily committed in the same order that they are created.

This small example shows the difference between sequential consistency and TSO:

>>> :{
let relaxed = do
      r1 <- newIORef False
      r2 <- newIORef False
      x <- spawn $ writeIORef r1 True >> readIORef r2
      y <- spawn $ writeIORef r2 True >> readIORef r1
      (,) <$> readMVar x <*> readMVar y
:}

The autocheckWay function will let us specify the memory model:

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

>>> autocheckWay defaultWay TotalStoreOrder 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

The result (False,False) is possible using TSO and PSO, but not sequential consistency. The "C" in the trace shows where a commit action occurred, which makes a write to an IORef visible to all threads.

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.

Synopsis

autocheck :: (MonadDejaFu n, MonadIO n, Eq a, Show a) => Program pty n a -> n Bool
dejafu :: (MonadDejaFu n, MonadIO n, Show b) => String -> ProPredicate a b -> Program pty n a -> n Bool
dejafus :: (MonadDejaFu n, MonadIO n, Show b) => [(String, ProPredicate a b)] -> Program pty n a -> n Bool
autocheckWay :: (MonadDejaFu n, MonadIO n, Eq a, Show a) => Way -> MemType -> Program pty n a -> n Bool
dejafuWay :: (MonadDejaFu n, MonadIO n, Show b) => Way -> MemType -> String -> ProPredicate a b -> Program pty n a -> n Bool
dejafusWay :: (MonadDejaFu n, MonadIO n, Show b) => Way -> MemType -> [(String, ProPredicate a b)] -> Program pty n a -> n Bool
autocheckWithSettings :: (MonadDejaFu n, MonadIO n, Eq a, Show a) => Settings n a -> Program pty n a -> n Bool
dejafuWithSettings :: (MonadDejaFu n, MonadIO n, Show b) => Settings n a -> String -> ProPredicate a b -> Program pty n a -> n Bool
dejafusWithSettings :: (MonadDejaFu n, MonadIO n, Show b) => Settings n a -> [(String, ProPredicate a b)] -> Program pty n a -> n Bool
module Test.DejaFu.Settings
data Result a = Result {
- _pass :: Bool
- _failures :: [(Either Condition a, Trace)]
- _failureMsg :: String
}
runTest :: MonadDejaFu n => ProPredicate a b -> Program pty n a -> n (Result b)
runTestWay :: MonadDejaFu n => Way -> MemType -> ProPredicate a b -> Program pty n a -> n (Result b)
runTestWithSettings :: MonadDejaFu n => Settings n a -> ProPredicate a b -> Program pty n a -> n (Result b)
type Predicate a = ProPredicate a a
data ProPredicate a b = ProPredicate {
- pdiscard :: Either Condition a -> Maybe Discard
- peval :: [(Either Condition a, Trace)] -> Result b
}
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 Condition a -> Bool) -> Predicate a
somewhereTrue :: (Either Condition a -> Bool) -> Predicate a
alwaysNothing :: (Either Condition a -> Maybe (Either Condition b)) -> ProPredicate a b
somewhereNothing :: (Either Condition a -> Maybe (Either Condition b)) -> ProPredicate a b
gives :: (Eq a, Show a) => [Either Condition a] -> Predicate a
gives' :: (Eq a, Show a) => [a] -> Predicate a
data Condition
- = Abort
- | Deadlock
- | UncaughtException SomeException
- | InvariantFailure SomeException
isAbort :: Condition -> Bool
isDeadlock :: Condition -> Bool
isUncaughtException :: Condition -> Bool
isInvariantFailure :: Condition -> Bool
module Test.DejaFu.Refinement
data Program pty n a
data Basic
type ConcT = Program Basic
type ConcIO = ConcT IO
data WithSetup x
data WithSetupAndTeardown x y
withSetup :: Program Basic n x -> (x -> Program Basic n a) -> Program (WithSetup x) n a
withTeardown :: (x -> Either Condition y -> Program Basic n a) -> Program (WithSetup x) n y -> Program (WithSetupAndTeardown x y) n a
withSetupAndTeardown :: Program Basic n x -> (x -> Either Condition y -> Program Basic n a) -> (x -> Program Basic n y) -> Program (WithSetupAndTeardown x y) n a
data Invariant n a
registerInvariant :: Invariant n a -> Program Basic n ()
inspectIORef :: ModelIORef n a -> Invariant n a
inspectMVar :: ModelMVar n a -> Invariant n (Maybe a)
inspectTVar :: ModelTVar n a -> Invariant n a

Unit testing

autocheck Source #

Arguments

:: (MonadDejaFu n, MonadIO n, Eq a, Show a)
=> Program pty 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: 2.1.0.0

dejafu Source #

Arguments

:: (MonadDejaFu n, MonadIO n, Show b)
=> String	The name of the test.
-> ProPredicate a b	The predicate to check.
-> Program pty 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: 2.1.0.0

dejafus Source #

Arguments

:: (MonadDejaFu n, MonadIO n, Show b)
=> [(String, ProPredicate a b)]	The list of predicates (with names) to check.
-> Program pty 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: 2.1.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 Source #

Arguments

:: (MonadDejaFu 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.
-> Program pty 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: 2.1.0.0

dejafuWay Source #

Arguments

:: (MonadDejaFu 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.
-> Program pty 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---P2--S0--
False

Since: 2.1.0.0

dejafusWay Source #

Arguments

:: (MonadDejaFu 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.
-> Program pty 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: 2.1.0.0

autocheckWithSettings Source #

Arguments

:: (MonadDejaFu n, MonadIO n, Eq a, Show a)
=> Settings n a	The SCT settings.
-> Program pty 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: 2.1.0.0

dejafuWithSettings Source #

Arguments

:: (MonadDejaFu n, MonadIO n, Show b)
=> Settings n a	The SCT settings.
-> String	The name of the test.
-> ProPredicate a b	The predicate to check.
-> Program pty 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---P2--S0--
False

Since: 2.1.0.0

dejafusWithSettings Source #

Arguments

:: (MonadDejaFu n, MonadIO n, Show b)
=> Settings n a	The SCT settings.
-> [(String, ProPredicate a b)]	The list of predicates (with names) to check.
-> Program pty 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: 2.1.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 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 :: 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

Instances details

Foldable Result Source #
Instance details Defined in Test.DejaFu Methods fold :: Monoid m => Result m -> m # foldMap :: Monoid m => (a -> m) -> Result a -> 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 #
Functor Result Source #
Instance details Defined in Test.DejaFu Methods fmap :: (a -> b) -> Result a -> Result b # (<$) :: a -> Result b -> Result a #
Show a => Show (Result a) Source #
Instance details Defined in Test.DejaFu Methods showsPrec :: Int -> Result a -> ShowS # show :: Result a -> String # showList :: [Result a] -> ShowS #
NFData a => NFData (Result a) Source #
Instance details Defined in Test.DejaFu Methods rnf :: Result a -> () #
Eq a => Eq (Result a) Source #
Instance details Defined in Test.DejaFu Methods (==) :: Result a -> Result a -> Bool # (/=) :: Result a -> Result a -> Bool #

runTest Source #

Arguments

:: MonadDejaFu n
=> ProPredicate a b	The predicate to check
-> Program pty 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: 2.1.0.0

runTestWay Source #

Arguments

:: MonadDejaFu 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
-> Program pty 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: 2.1.0.0

runTestWithSettings Source #

Arguments

:: MonadDejaFu n
=> Settings n a	The SCT settings.
-> ProPredicate a b	The predicate to check
-> Program pty n a	The computation to test
-> n (Result b)

Variant of runTest which takes a settings record.

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

Instances details

Profunctor ProPredicate Source #
Instance details 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 # (#.) :: forall a b c q. Coercible c b => q b c -> ProPredicate a b -> ProPredicate a c # (.#) :: forall a b c q. Coercible b a => ProPredicate b c -> q a b -> ProPredicate a c #
Functor (ProPredicate x) Source #
Instance details Defined in Test.DejaFu Methods fmap :: (a -> b) -> ProPredicate x a -> ProPredicate x b # (<$) :: a -> ProPredicate x b -> ProPredicate x a #

successful :: Predicate a Source #

Check that a computation never produces a Left value.

Since: 1.9.1.0

alwaysSame :: Eq a => Predicate a Source #

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

alwaysSame = alwaysSameBy (==)

Since: 1.10.0.0

notAlwaysSame :: Eq a => Predicate a Source #

Check that a computation never fails, and gives multiple distinct Right 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 Conditions, 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 Conditions, 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 Conditions, 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 Conditions, 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 Conditions, 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 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 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), Right, 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) Right 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 Right 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 Source #

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

Since: 1.0.0.0

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

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

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 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 Left results.

gives' = gives . map Right

Since: 1.0.0.0

Conditions

Helper functions to identify conditions.

data Condition Source #

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 and InvariantFailure cases.

Since: 2.0.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
UncaughtException SomeException	An uncaught exception bubbled to the top of the computation.
InvariantFailure SomeException	An uncaught exception caused an invariant to fail.

Instances

Instances details

Generic Condition Source #
Instance details Defined in Test.DejaFu.Types Associated Types type Rep Condition :: Type -> Type # Methods from :: Condition -> Rep Condition x # to :: Rep Condition x -> Condition #
Show Condition Source #
Instance details Defined in Test.DejaFu.Types Methods showsPrec :: Int -> Condition -> ShowS # show :: Condition -> String # showList :: [Condition] -> ShowS #
NFData Condition Source #
Instance details Defined in Test.DejaFu.Types Methods rnf :: Condition -> () #
Eq Condition Source #
Instance details Defined in Test.DejaFu.Types Methods (==) :: Condition -> Condition -> Bool # (/=) :: Condition -> Condition -> Bool #
Ord Condition Source #
Instance details 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 #
type Rep Condition Source #
Instance details Defined in Test.DejaFu.Types type Rep Condition = D1 ('MetaData "Condition" "Test.DejaFu.Types" "dejafu-2.4.0.5-G4EEj1kXZBX5wEYbPUnAst" 'False) ((C1 ('MetaCons "Abort" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Deadlock" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UncaughtException" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SomeException)) :+: C1 ('MetaCons "InvariantFailure" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SomeException))))

isAbort :: Condition -> Bool Source #

Check if a condition is an Abort.

Since: 0.9.0.0

isDeadlock :: Condition -> Bool Source #

Check if a condition is a Deadlock.

Since: 0.9.0.0

isUncaughtException :: Condition -> Bool Source #

Check if a condition is an UncaughtException

Since: 0.9.0.0

isInvariantFailure :: Condition -> Bool Source #

Check if a condition is an InvariantFailure

Since: 2.0.0.0

Property-based testing

dejafu can also use a property-based testing style to test stateful operations for a variety of inputs. Inputs are generated using the 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

Expressing concurrent programs

data Program pty n a Source #

A representation of a concurrent program for testing.

To construct these, use the MonadConc instance, or see withSetup, withTeardown, and withSetupAndTeardown.

Since: 2.0.0.0

Instances

Instances details

pty ~ Basic => MonadTrans (Program pty) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Program Methods lift :: Monad m => m a -> Program pty m a #
pty ~ Basic => MonadFail (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods fail :: String -> Program pty n a #
(pty ~ Basic, MonadIO n) => MonadIO (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Program Methods liftIO :: IO a -> Program pty n a #
pty ~ Basic => Applicative (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods pure :: a -> Program pty n a # (<>) :: Program pty n (a -> b) -> Program pty n a -> Program pty n b # liftA2 :: (a -> b -> c) -> Program pty n a -> Program pty n b -> Program pty n c # (>) :: Program pty n a -> Program pty n b -> Program pty n b # (<*) :: Program pty n a -> Program pty n b -> Program pty n a #
pty ~ Basic => Functor (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods fmap :: (a -> b) -> Program pty n a -> Program pty n b # (<$) :: a -> Program pty n b -> Program pty n a #
pty ~ Basic => Monad (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods (>>=) :: Program pty n a -> (a -> Program pty n b) -> Program pty n b # (>>) :: Program pty n a -> Program pty n b -> Program pty n b # return :: a -> Program pty n a #
(pty ~ Basic, Monad n) => MonadConc (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Program Associated Types type STM (Program pty n) :: Type -> Type # type MVar (Program pty n) :: Type -> Type # type IORef (Program pty n) :: Type -> Type # type Ticket (Program pty n) :: Type -> Type # type ThreadId (Program pty n) # Methods forkWithUnmask :: ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n)) # forkWithUnmaskN :: String -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n)) # forkOnWithUnmask :: Int -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n)) # forkOnWithUnmaskN :: String -> Int -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n)) # forkOSWithUnmask :: ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n)) # forkOSWithUnmaskN :: String -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n)) # supportsBoundThreads :: Program pty n Bool # isCurrentThreadBound :: Program pty n Bool # getNumCapabilities :: Program pty n Int # setNumCapabilities :: Int -> Program pty n () # myThreadId :: Program pty n (ThreadId (Program pty n)) # yield :: Program pty n () # threadDelay :: Int -> Program pty n () # newEmptyMVar :: Program pty n (MVar (Program pty n) a) # newEmptyMVarN :: String -> Program pty n (MVar (Program pty n) a) # putMVar :: MVar (Program pty n) a -> a -> Program pty n () # tryPutMVar :: MVar (Program pty n) a -> a -> Program pty n Bool # readMVar :: MVar (Program pty n) a -> Program pty n a # tryReadMVar :: MVar (Program pty n) a -> Program pty n (Maybe a) # takeMVar :: MVar (Program pty n) a -> Program pty n a # tryTakeMVar :: MVar (Program pty n) a -> Program pty n (Maybe a) # newIORef :: a -> Program pty n (IORef (Program pty n) a) # newIORefN :: String -> a -> Program pty n (IORef (Program pty n) a) # readIORef :: IORef (Program pty n) a -> Program pty n a # atomicModifyIORef :: IORef (Program pty n) a -> (a -> (a, b)) -> Program pty n b # writeIORef :: IORef (Program pty n) a -> a -> Program pty n () # atomicWriteIORef :: IORef (Program pty n) a -> a -> Program pty n () # readForCAS :: IORef (Program pty n) a -> Program pty n (Ticket (Program pty n) a) # peekTicket' :: Proxy (Program pty n) -> Ticket (Program pty n) a -> a # casIORef :: IORef (Program pty n) a -> Ticket (Program pty n) a -> a -> Program pty n (Bool, Ticket (Program pty n) a) # modifyIORefCAS :: IORef (Program pty n) a -> (a -> (a, b)) -> Program pty n b # modifyIORefCAS_ :: IORef (Program pty n) a -> (a -> a) -> Program pty n () # atomically :: STM (Program pty n) a -> Program pty n a # newTVarConc :: a -> Program pty n (TVar (STM (Program pty n)) a) # readTVarConc :: TVar (STM (Program pty n)) a -> Program pty n a # throwTo :: Exception e => ThreadId (Program pty n) -> e -> Program pty n () # getMaskingState :: Program pty n MaskingState # unsafeUnmask :: Program pty n a -> Program pty n a #
pty ~ Basic => MonadCatch (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Program Methods catch :: Exception e => Program pty n a -> (e -> Program pty n a) -> Program pty n a #
pty ~ Basic => MonadMask (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Program Methods mask :: ((forall a. Program pty n a -> Program pty n a) -> Program pty n b) -> Program pty n b # uninterruptibleMask :: ((forall a. Program pty n a -> Program pty n a) -> Program pty n b) -> Program pty n b # generalBracket :: Program pty n a -> (a -> ExitCase b -> Program pty n c) -> (a -> Program pty n b) -> Program pty n (b, c) #
pty ~ Basic => MonadThrow (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Program Methods throwM :: Exception e => e -> Program pty n a #
type IORef (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Program type IORef (Program pty n) = ModelIORef n
type MVar (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Program type MVar (Program pty n) = ModelMVar n
type STM (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Program type STM (Program pty n) = ModelSTM n
type ThreadId (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Program type ThreadId (Program pty n) = ThreadId
type Ticket (Program pty n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Program type Ticket (Program pty n) = ModelTicket

data Basic Source #

A type used to constrain Program: a Program Basic is a "basic" program with no set-up or teardown.

Construct with the MonadConc instance.

Since: 2.0.0.0

type ConcT = Program Basic Source #

Since: 1.4.0.0

type ConcIO = ConcT IO Source #

A MonadConc implementation using IO.

Since: 0.4.0.0

Setup and teardown

data WithSetup x Source #

A type used to constrain Program: a Program (WithSetup x) is a program with some set-up action producing a value of type x.

Construct with withSetup.

Since: 2.0.0.0

data WithSetupAndTeardown x y Source #

A type used to constrain Program: a Program (WithSetupAndTeardown x y) is a program producing a value of type y with some set-up action producing a value of type x and a teardown action producing the final result.

Construct with withTeardown or withSetupAndTeardown.

Since: 2.0.0.0

withSetup Source #

Arguments

:: Program Basic n x	Setup action
-> (x -> Program Basic n a)	Main program
-> Program (WithSetup x) n a

A concurrent program with some set-up action.

In terms of results, this is the same as setup >>= program. However, the setup action will be snapshotted (see recordSnapshot and runSnapshot) by the testing functions. This means that even if dejafu runs this program many many times, the setup action will only be run the first time, and its effects remembered for subsequent executions.

Since: 2.0.0.0

withTeardown Source #

Arguments

:: (x -> Either Condition y -> Program Basic n a)	Teardown action
-> Program (WithSetup x) n y	Main program
-> Program (WithSetupAndTeardown x y) n a

A concurrent program with some set-up and teardown actions.

This is similar to

do
  x <- setup
  y <- program x
  teardown x y

But with two differences:

The setup action can be snapshotted, as described for withSetup
The teardown action will be executed even if the main action fails to produce a value.

Since: 2.0.0.0

withSetupAndTeardown Source #

Arguments

:: Program Basic n x	Setup action
-> (x -> Either Condition y -> Program Basic n a)	Teardown action
-> (x -> Program Basic n y)	Main program
-> Program (WithSetupAndTeardown x y) n a

A combination of withSetup and withTeardown for convenience.

withSetupAndTeardown setup teardown =
  withTeardown teardown . withSetup setup

Since: 2.0.0.0

Invariants

data Invariant n a Source #

Invariants are atomic actions which can inspect the shared state of your computation, and terminate it on failure. Invariants have no visible effects, and are checked after each scheduling point.

To be checked, an invariant must be created during the setup phase of your Program, using registerInvariant. The invariant will then be checked in the main phase (but not in the setup or teardown phase). As a consequence of this, any shared state you want your invariant to check must also be created in the setup phase, and passed into the main phase as a parameter.

Since: 2.0.0.0

Instances

Instances details

MonadFail (Invariant n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods fail :: String -> Invariant n a #
Applicative (Invariant n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods pure :: a -> Invariant n a # (<>) :: Invariant n (a -> b) -> Invariant n a -> Invariant n b # liftA2 :: (a -> b -> c) -> Invariant n a -> Invariant n b -> Invariant n c # (>) :: Invariant n a -> Invariant n b -> Invariant n b # (<*) :: Invariant n a -> Invariant n b -> Invariant n a #
Functor (Invariant n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods fmap :: (a -> b) -> Invariant n a -> Invariant n b # (<$) :: a -> Invariant n b -> Invariant n a #
Monad (Invariant n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods (>>=) :: Invariant n a -> (a -> Invariant n b) -> Invariant n b # (>>) :: Invariant n a -> Invariant n b -> Invariant n b # return :: a -> Invariant n a #
MonadCatch (Invariant n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods catch :: Exception e => Invariant n a -> (e -> Invariant n a) -> Invariant n a #
MonadThrow (Invariant n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.Common Methods throwM :: Exception e => e -> Invariant n a #

registerInvariant :: Invariant n a -> Program Basic n () Source #

Call this in the setup phase to register new invariant which will be checked after every scheduling point in the main phase. Invariants are atomic actions which can inspect the shared state of your computation.

If the invariant throws an exception, the execution will be aborted with n InvariantFailure. Any teardown action will still be run.

Since: 2.0.0.0

inspectIORef :: ModelIORef n a -> Invariant n a Source #

Read the content of an IORef.

This returns the globally visible value, which may not be the same as the value visible to any particular thread when using a memory model other than SequentialConsistency.

Since: 2.0.0.0

inspectMVar :: ModelMVar n a -> Invariant n (Maybe a) Source #

Read the content of an MVar.

This is essentially tryReadMVar.

Since: 2.0.0.0

inspectTVar :: ModelTVar n a -> Invariant n a Source #

Read the content of a TVar.

This is essentially readTVar.

Since: 2.0.0.0