Test.DejaFu

Deterministic testing for concurrent computations.

As an example, consider this program, which has two locks and a shared variable. Two threads are spawned, which claim the locks, update the shared variable, and release the locks. The main thread waits for them both to terminate, and returns the final result.

bad :: MonadConc m => m Int
bad = do
  a <- newEmptyCVar
  b <- newEmptyCVar

  c <- newCVar 0

  j1 <- spawn $ lock a >> lock b >> modifyCVar_ c (return . succ) >> unlock b >> unlock a
  j2 <- spawn $ lock b >> lock a >> modifyCVar_ c (return . pred) >> unlock a >> unlock b

  takeCVar j1
  takeCVar j2

  takeCVar c

The correct result is 0, as it starts out as 0 and is incremented and decremented by threads 1 and 2, respectively. However, note the order of acquisition of the locks in the two threads. If thread 2 pre-empts thread 1 between the acquisition of the locks (or if thread 1 pre-empts thread 2), a deadlock situation will arise, as thread 1 will have lock a and be waiting on b, and thread 2 will have b and be waiting on a.

Here is what Deja Fu has to say about it:

> autocheck bad
[fail] Never Deadlocks (checked: 2)
        [deadlock] S0---------S1--P2---S1-
[pass] No Exceptions (checked: 11)
[fail] Consistent Result (checked: 10)
        0 S0---------S1---------------S0--S2---------------S0----
        [deadlock] S0---------S1--P2---S1-
False

It identifies the deadlock, and also the possible results the computation can produce, and displays a simplified trace leading to each failing outcome. It also returns False as there are test failures. The automatic testing functionality is good enough if you only want to check your computation is deterministic, but if you have more specific requirements (or have some expected and tolerated level of nondeterminism), you can write tests yourself using the dejafu* functions.

Warning: If your computation under test does IO, the IO will be executed lots of times! Be sure that it is deterministic enough not to invalidate your test results. Mocking may be useful where possible.

Testing

Testing in Deja Fu is similar to unit testing, the programmer produces a self-contained monadic action to execute under different schedules, and supplies a list of predicates to apply to the list of results produced.

If you simply wish to check that something is deterministic, see the autocheck and autocheckIO functions.

autocheck

Arguments

:: (Eq a, Show a)

=> (forall t. Conc t a)

The computation to test

-> IO Bool

Automatically test a computation. In particular, look for deadlocks, uncaught exceptions, and multiple return values.

This uses the Conc monad for testing, which is an instance of MonadConc. If you need to test something which also uses MonadIO, use autocheckIO.

dejafu

Arguments

:: (Eq a, Show a)

=> (forall t. Conc t a)

The computation to test

-> (String, Predicate a)

The predicate (with a name) to check

-> IO Bool

Check a predicate and print the result to stdout, return True if it passes.

dejafus

Arguments

:: (Eq a, Show a)

=> (forall t. Conc t a)

The computation to test

-> [(String, Predicate a)]

The list of predicates (with names) to check

-> IO Bool

Variant of dejafu which takes a collection of predicates to test, returning True if all pass.

dejafus'

Arguments

:: (Eq a, Show a)

=> Int

The maximum number of pre-emptions to allow in a single execution

-> (forall t. Conc t a)

The computation to test

-> [(String, Predicate a)]

The list of predicates (with names) to check

-> IO Bool

Variant of dejafus which takes a pre-emption bound.

Pre-emption bounding is used to filter the large number of possible schedules, and can be iteratively increased for further coverage guarantees. Empirical studies (Concurrency Testing Using Schedule Bounding: an Empirical Study, P. Thompson, A. Donaldson, and A. Betts) have found that many concurrency bugs can be exhibited with as few as two threads and two pre-emptions, which is what dejafus uses.

Warning: Using a larger pre-emption bound will almost certainly significantly increase the time taken to test!

autocheckIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> IO Bool

Variant of autocheck for computations which do IO.

dejafuIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> (String, Predicate a) -> IO Bool

Variant of dejafu for computations which do IO.

dejafusIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> [(String, Predicate a)] -> IO Bool

Variant of dejafus for computations which do IO.

dejafusIO' :: (Eq a, Show a) => Int -> (forall t. ConcIO t a) -> [(String, Predicate a)] -> IO Bool

Variant of dejafus' for computations which do IO.

Results

The results of a test can be pretty-printed to the console, as with the above functions, or used in their original, much richer, form for debugging purposes. These functions provide full access to this data type which, most usefully, contains a detailed trace of execution, showing what each thread did at each point.

data Result a

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

Constructors

Result

Fields

_pass :: Bool

Whether the test passed or not.

_casesChecked :: Int

The number of cases checked.

_failures :: [(Either Failure a, Trace)]

The failing cases, if any.

Instances

Functor Result

Foldable Result

Eq a => Eq (Result a)

Show a => Show (Result a)

NFData a => NFData (Result a)

data Failure

An indication of how a concurrent computation failed.

Constructors

InternalError

Will be raised if the scheduler does something bad. This should never arise unless you write your own, faulty, scheduler! If it does, please file a bug report.

Deadlock

The computation became blocked indefinitely on CVars.

STMDeadlock

The computation became blocked indefinitely on CTVars.

UncaughtException

An uncaught exception bubbled to the top of the computation.

FailureInNoTest

A computation annotated with _concNoTest produced a failure, rather than a result.

Instances

Eq Failure

Show Failure

NFData Failure

runTest

Arguments

:: Predicate a

The predicate to check

-> (forall t. Conc t a)

The computation to test

-> Result a

Run a predicate over all executions with two or fewer pre-emptions.

runTest'

Arguments

:: Int

The maximum number of pre-emptions to allow in a single execution

-> Predicate a

The predicate to check

-> (forall t. Conc t a)

The computation to test

-> Result a

Variant of runTest which takes a pre-emption bound.

runTestIO :: Predicate a -> (forall t. ConcIO t a) -> IO (Result a)

Variant of runTest for computations which do IO.

runTestIO' :: Int -> Predicate a -> (forall t. ConcIO t a) -> IO (Result a)

Variant of runTest' for computations which do IO.

Predicates

Predicates evaluate a list of results of execution and decide whether some test case has passed or failed. They can be lazy and make use of short-circuit evaluation to avoid needing to examine the entire list of results, and can check any property which can be defined for the return type of your monadic action.

A collection of common predicates are provided, along with the helper functions alwaysTrue, alwaysTrue2 and somewhereTrue to lfit predicates over a single result to over a collection of results.

type Predicate a = [(Either Failure a, Trace)] -> Result a

A Predicate is a function which collapses a list of results into a Result.

deadlocksNever :: Predicate a

Check that a computation never deadlocks.

deadlocksAlways :: Predicate a

Check that a computation always deadlocks.

deadlocksSometimes :: Predicate a

Check that a computation deadlocks at least once.

exceptionsNever :: Predicate a

Check that a computation never fails with an uncaught exception.

exceptionsAlways :: Predicate a

Check that a computation always fails with an uncaught exception.

exceptionsSometimes :: Predicate a

Check that a computation fails with an uncaught exception at least once.

alwaysSame :: Eq a => Predicate a

Check that the result of a computation is always the same. In particular this means either: (a) it always fails in the same way, or (b) it never fails and the values returned are all equal.

notAlwaysSame :: Eq a => Predicate a

Check that the result of a computation is not always the same.

alwaysTrue :: (Either Failure a -> Bool) -> Predicate a

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

alwaysTrue2 :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a

Check that the result of a binary boolean predicate is true between all pairs of results. Only properties which are transitive and symmetric should be used here.

If the predicate fails, both (result,trace) tuples will be added to the failures list.

somewhereTrue :: (Either Failure a -> Bool) -> Predicate a

Check that the result of a unary boolean predicate is true at least once.