Test.DejaFu

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:

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

Unit testing

autocheck

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

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

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

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

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----S2--S1-S0--
False

Since: 2.1.0.0

dejafusWay

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

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

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----S2--S1-S0--
False

Since: 2.1.0.0

dejafusWithSettings

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

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

runTest

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

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

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

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 produces a Left value.

Since: 1.9.1.0

alwaysSame :: Eq a => Predicate a

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

alwaysSame = alwaysSameBy (==)

Since: 1.10.0.0

notAlwaysSame :: Eq a => Predicate a

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

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

gives' = gives . map Right

Since: 1.0.0.0

Conditions

Helper functions to identify conditions.

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

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-2.1.0.0-JJVzrY3ZK7kAGEFuYdaBQg" 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

Check if a condition is an Abort.

Since: 0.9.0.0

isDeadlock :: Condition -> Bool

Check if a condition is a Deadlock.

Since: 0.9.0.0

isUncaughtException :: Condition -> Bool

Check if a condition is an UncaughtException

Since: 0.9.0.0

isInvariantFailure :: Condition -> Bool

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

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

pty ~ Basic => MonadTrans (Program pty)

Defined in Test.DejaFu.Conc.Internal.Program

Methods

lift :: Monad m => m a -> Program pty m a

pty ~ Basic => Monad (Program pty n)

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

fail :: String -> Program pty n a

pty ~ Basic => Functor (Program pty n)

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 => MonadFail (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fail :: String -> Program pty n a

pty ~ Basic => Applicative (Program pty n)

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, MonadIO n) => MonadIO (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

Methods

liftIO :: IO a -> Program pty n a

(pty ~ Basic, Monad n) => MonadConc (Program pty n)

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

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

readTVarConc :: TVar (STM (Program pty n)) a -> Program pty n a

throwTo :: Exception e => ThreadId (Program pty n) -> e -> Program pty n ()

pty ~ Basic => MonadThrow (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

Methods

throwM :: Exception e => e -> Program pty n a

pty ~ Basic => MonadCatch (Program pty n)

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)

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)

type ThreadId (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type ThreadId (Program pty n) = ThreadId

type Ticket (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type Ticket (Program pty n) = ModelTicket

type IORef (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type IORef (Program pty n) = ModelIORef n

type MVar (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type MVar (Program pty n) = ModelMVar n

type STM (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type STM (Program pty n) = ModelSTM n

data Basic

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

Since: 1.4.0.0

type ConcIO = ConcT IO

A MonadConc implementation using IO.

Since: 0.4.0.0

Setup and teardown

data WithSetup x

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

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

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

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

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

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)

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

fail :: String -> Invariant n a

Functor (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fmap :: (a -> b) -> Invariant n a -> Invariant n b

(<$) :: a -> Invariant n b -> Invariant n a

MonadFail (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fail :: String -> Invariant n a

Applicative (Invariant n)

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

MonadThrow (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

throwM :: Exception e => e -> Invariant n a

MonadCatch (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

catch :: Exception e => Invariant n a -> (e -> Invariant n a) -> Invariant n a

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

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

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)

Read the content of an MVar.

This is essentially tryReadMVar.

Since: 2.0.0.0

inspectTVar :: ModelTVar n a -> Invariant n a

Read the content of a TVar.

This is essentially readTVar.

Since: 2.0.0.0