Copyright | (c) 2015--2019 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 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.readthedocs.io 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:

`>>>`

[pass] Successful [fail] Deterministic "hello" S0----S1--S0-- "world" S0----S2--S0-- False`autocheck example`

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

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

`>>>`

[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 SequentialConsistency 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 TotalStoreOrder relaxed`

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

Automatically test a computation.

In particular, concurrency errors and nondeterminism. Returns
`True`

if all tests pass

`>>>`

[pass] Successful [fail] Deterministic "hello" S0----S1--S0-- "world" S0----S2--S0-- False`autocheck example`

*Since: 2.1.0.0*

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

`>>>`

[fail] Test Name "hello" S0----S1--S0-- "world" S0----S2--S0-- False`dejafu "Test Name" alwaysSame example`

*Since: 2.1.0.0*

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

## 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 `IORef`

s behave; see Test.DejaFu.Settings for a
complete listing.

:: (MonadDejaFu n, MonadIO n, Eq a, Show a) | |

=> Way | How to run the concurrent program. |

-> MemType | The memory model to use for non-synchronised |

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

`>>>`

[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 defaultMemType 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 SequentialConsistency relaxed`

*Since: 2.1.0.0*

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

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

`>>>`

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

`>>>`

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

*Since: 2.1.0.0*

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

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

`>>>`

[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`dejafusWay defaultWay SequentialConsistency [("A", alwaysSame), ("B", exceptionsNever)] relaxed`

*Since: 2.1.0.0*

autocheckWithSettings Source #

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

`>>>`

[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 defaultMemType) 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`autocheckWithSettings (fromWayAndMemType defaultWay SequentialConsistency) relaxed`

*Since: 2.1.0.0*

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

`>>>`

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

*Since: 2.1.0.0*

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

`>>>`

[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`dejafusWithSettings (fromWayAndMemType defaultWay SequentialConsistency) [("A", alwaysSame), ("B", exceptionsNever)] relaxed`

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

The results of a test, including the number of cases checked to determine the final boolean outcome.

*Since: 1.0.0.0*

## Instances

Functor Result Source # | |

Foldable Result Source # | |

Defined in Test.DejaFu 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 # elem :: Eq a => a -> Result a -> Bool # maximum :: Ord a => Result a -> a # minimum :: Ord a => Result a -> a # | |

Eq a => Eq (Result a) Source # | |

Show a => Show (Result a) Source # | |

NFData a => NFData (Result a) Source # | |

Defined in Test.DejaFu |

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

:: MonadDejaFu n | |

=> Way | How to run the concurrent program. |

-> MemType | The memory model to use for non-synchronised |

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

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

## Instances

Profunctor ProPredicate Source # | |

Defined in Test.DejaFu 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) Source # | |

Defined in Test.DejaFu 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 `Condition`

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

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

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

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

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

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), `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*

### Conditions

Helper functions to identify conditions.

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*

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

Eq Condition Source # | |

Ord Condition Source # | |

Defined in Test.DejaFu.Types | |

Show Condition Source # | |

Generic Condition Source # | |

NFData Condition Source # | |

Defined in Test.DejaFu.Types | |

type Rep Condition Source # | |

Defined in Test.DejaFu.Types type Rep Condition = D1 (MetaData "Condition" "Test.DejaFu.Types" "dejafu-2.1.0.3-B07A0RVIeLE2QS4wxW6YYC" 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)))) |

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`

:

`>>>`

*** Failure: (seed Just 0) left: [(Nothing,Just 0)] right: [(Nothing,Just 0),(Just Deadlock,Just 42)] False`check $ sig readMVar === sig (\v -> takeMVar v >>= putMVar v)`

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

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

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*

## Setup and teardown

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*

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*

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

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

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

Monad (Invariant n) Source # | |

Functor (Invariant n) Source # | |

MonadFail (Invariant n) Source # | |

Defined in Test.DejaFu.Conc.Internal.Common | |

Applicative (Invariant n) Source # | |

Defined in Test.DejaFu.Conc.Internal.Common | |

MonadThrow (Invariant n) Source # | |

Defined in Test.DejaFu.Conc.Internal.Common | |

MonadCatch (Invariant n) Source # | |

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*