dejafu-0.9.0.2: Systematic testing for Haskell concurrency.

Copyright (c) 2016 Michael Walker MIT Michael Walker experimental RankNTypes None Haskell2010

Test.DejaFu

Description

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.

example1 :: MonadConc m => m Int
example1 = do
a <- newEmptyMVar
b <- newEmptyMVar

c <- newMVar 0

let lock m = putMVar m ()
let unlock = takeMVar

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

takeMVar j1
takeMVar j2

takeMVar 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 example1
[pass] No Exceptions (checked: 12)
[fail] Consistent Result (checked: 11)
0 S0------------S2-----------------S1-----------------S0----

False

It identifies the deadlock, and also the possible results the computation can produce, and displays a simplified trace leading to each failing outcome. The trace contains thread numbers, and the names (which can be set by the programmer) are displayed beneath. 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.

Synopsis

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

These functions use a Total Store Order (TSO) memory model for unsynchronised actions, see "Testing under Alternative Memory Models" for some explanation of this.

Arguments

 :: (Eq a, Show a) => (forall t. ConcST 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.

Since: 0.1.0.0

Arguments

 :: Show a => (forall t. ConcST 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.

Since: 0.1.0.0

Arguments

 :: Show a => (forall t. ConcST 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.

Since: 0.1.0.0

autocheckIO :: (Eq a, Show a) => ConcIO a -> IO Bool Source #

Variant of autocheck for computations which do IO.

Since: 0.2.0.0

dejafuIO :: Show a => ConcIO a -> (String, Predicate a) -> IO Bool Source #

Variant of dejafu for computations which do IO.

Since: 0.2.0.0

dejafusIO :: Show a => ConcIO a -> [(String, Predicate a)] -> IO Bool Source #

Variant of dejafus for computations which do IO.

Since: 0.2.0.0

# Testing with different settings

data Way Source #

How to explore the possible executions of a concurrent program.

Since: 0.7.0.0

Instances

 Source # MethodsshowsPrec :: Int -> Way -> ShowS #show :: Way -> String #showList :: [Way] -> ShowS #

A default way to execute concurrent programs: systematically using defaultBounds.

Since: 0.6.0.0

Arguments

 :: Bounds The bounds to constrain the exploration. -> Way

Systematically execute a program, trying all distinct executions within the bounds.

This corresponds to sctBound.

Since: 0.7.0.0

Arguments

 :: RandomGen g => g The random generator to drive the scheduling. -> Int The number of executions to try. -> Way

Randomly execute a program, exploring a fixed number of executions.

Threads are scheduled by a weighted random selection, where weights are assigned randomly on thread creation.

This corresponds to sctWeightedRandom with weight re-use disabled, and is not guaranteed to find all distinct results (unlike systematically / sctBound).

Since: 0.7.0.0

Arguments

 :: RandomGen g => g The random generator to drive the scheduling. -> Int The number of executions to try. -> Way

Randomly execute a program, exploring a fixed number of executions.

Threads are scheduled by a uniform random selection.

This corresponds to sctUniformRandom, and is not guaranteed to find all distinct results (unlike systematically / sctBound).

Since: 0.7.0.0

Arguments

 :: RandomGen g => g The random generator to drive the scheduling. -> Int The number of executions to try. -> Int The number of executions to use the thread weights for. -> Way

Randomly execute a program, exploring a fixed number of executions.

Threads are scheduled by a weighted random selection, where weights are assigned randomly on thread creation.

This corresponds to sctWeightedRandom, and is not guaranteed to find all distinct results (unlike systematically / sctBound).

Since: 0.7.0.0

Arguments

 :: (Eq a, Show a) => Way How to run the concurrent program. -> MemType The memory model to use for non-synchronised CRef operations. -> (forall t. ConcST t a) The computation to test -> IO Bool

Variant of autocheck which takes a way to run the program and a memory model.

Schedule 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 part of what dejafus uses.

Warning: Using largers bounds will almost certainly significantly increase the time taken to test!

Since: 0.6.0.0

autocheckWayIO :: (Eq a, Show a) => Way -> MemType -> ConcIO a -> IO Bool Source #

Variant of autocheckWay for computations which do IO.

Since: 0.6.0.0

Arguments

 :: Show a => Way How to run the concurrent program. -> MemType The memory model to use for non-synchronised CRef operations. -> (forall t. ConcST t a) The computation to test -> (String, Predicate a) The predicate (with a name) to check -> IO Bool

Variant of dejafu which takes a way to run the program and a memory model.

Since: 0.6.0.0

dejafuWayIO :: Show a => Way -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool Source #

Variant of dejafuWay for computations which do IO.

Since: 0.6.0.0

Arguments

 :: Show a => Way How to run the concurrent program. -> MemType The memory model to use for non-synchronised CRef operations. -> (forall t. ConcST 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 way to run the program and a memory model.

Since: 0.6.0.0

dejafusWayIO :: Show a => Way -> MemType -> ConcIO a -> [(String, Predicate a)] -> IO Bool Source #

Variant of dejafusWay for computations which do IO.

Since: 0.6.0.0

An Either Failure a -> Maybe Discard value can be used to selectively discard results.

Since: 0.7.1.0

Constructors

 DiscardTrace Discard the trace but keep the result. The result will appear to have an empty trace. DiscardResultAndTrace Discard the result and the trace. It will simply not be reported as a possible behaviour of the program.

Instances

Since: 0.7.1.0

Arguments

 :: Show a => (Either Failure a -> Maybe Discard) Selectively discard results. -> Way How to run the concurrent program. -> MemType The memory model to use for non-synchronised CRef operations. -> (forall t. ConcST t a) The computation to test -> (String, Predicate a) The predicate (with a name) to check -> IO Bool

Variant of dejafuWay which can selectively discard results.

Since: 0.7.1.0

dejafuDiscardIO :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool Source #

Variant of dejafuDiscard for computations which do IO.

Since: 0.7.1.0

## Memory Models

Threads running under modern multicore processors do not behave as a simple interleaving of the individual thread actions. Processors do all sorts of complex things to increase speed, such as buffering writes. For concurrent programs which make use of non-synchronised functions (such as readCRef coupled with writeCRef) different memory models may yield different results.

As an example, consider this program (modified from the Data.IORef documentation). Two CRefs are created, and two threads spawned to write to and read from both. Each thread returns the value it observes.

example2 :: MonadConc m => m (Bool, Bool)
example2 = do
r1 <- newCRef False
r2 <- newCRef False

x <- spawn $writeCRef r1 True >> readCRef r2 y <- spawn$ writeCRef r2 True >> readCRef r1

(,) <$> readMVar x <*> readMVar y Under a sequentially consistent memory model the possible results are (True, True), (True, False), and (False, True). Under total or partial store order, (False, False) is also a possible result, even though there is no interleaving of the threads which can lead to this. We can see this by testing with different memory models: > autocheckWay defaultWay SequentialConsistency example2 [pass] Never Deadlocks (checked: 6) [pass] No Exceptions (checked: 6) [fail] Consistent Result (checked: 5) (False,True) S0-------S1-----S0--S2-----S0--- (True,False) S0-------S1-P2-----S1----S0---- (True,True) S0-------S1--P2-----S1---S0---- (False,True) S0-------S1---P2-----S1--S0---- (True,False) S0-------S2-----S1-----S0---- ... False > autocheckWay defaultWay TotalStoreOrder example2 [pass] Never Deadlocks (checked: 303) [pass] No Exceptions (checked: 303) [fail] Consistent Result (checked: 302) (False,True) S0-------S1-----C-S0--S2-----C-S0--- (True,False) S0-------S1-P2-----C-S1----S0---- (True,True) S0-------S1-P2--C-S1----C-S0--S2---S0--- (False,True) S0-------S1-P2--P1--C-C-S1--S0--S2---S0--- (False,False) S0-------S1-P2--P1----S2---C-C-S0---- ... False Traces for non-sequentially-consistent memory models show where writes to CRefs are committed, which makes a write visible to all threads rather than just the one which performed the write. Only writeCRef is broken up into separate write and commit steps, atomicModifyCRef is still atomic and imposes a memory barrier. data MemType Source # The memory model to use for non-synchronised CRef operations. Since: 0.4.0.0 Constructors  SequentialConsistency The most intuitive model: a program behaves as a simple interleaving of the actions in different threads. When a CRef is written to, that write is immediately visible to all threads. TotalStoreOrder 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. PartialStoreOrder Each CRef 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 CRefs are not necessarily committed in the same order that they are created. Instances  Source # Methods Source # MethodsenumFrom :: MemType -> [MemType] #enumFromThen :: MemType -> MemType -> [MemType] #enumFromTo :: MemType -> MemType -> [MemType] #enumFromThenTo :: MemType -> MemType -> MemType -> [MemType] # Source # Methods(==) :: MemType -> MemType -> Bool #(/=) :: MemType -> MemType -> Bool # Source # Methods(<) :: MemType -> MemType -> Bool #(<=) :: MemType -> MemType -> Bool #(>) :: MemType -> MemType -> Bool #(>=) :: MemType -> MemType -> Bool # Source # Methods Source # MethodsshowList :: [MemType] -> ShowS # Source # Since: 0.5.1.0 Methodsrnf :: MemType -> () # The default memory model: TotalStoreOrder Since: 0.2.0.0 ## Schedule Bounding Schedule bounding is an optimisation which only considers schedules within some bound. This sacrifices completeness outside of the bound, but can drastically reduce the number of schedules to test, and is in fact necessary for non-terminating programs. The standard testing mechanism uses a combination of pre-emption bounding, fair bounding, and length bounding. Pre-emption + fair bounding is useful for programs which use loop/yield control flows but are otherwise terminating. Length bounding makes it possible to test potentially non-terminating programs. data Bounds Source # Since: 0.2.0.0 Constructors  Bounds Fields Instances  Source # Methods(==) :: Bounds -> Bounds -> Bool #(/=) :: Bounds -> Bounds -> Bool # Source # Methods(<) :: Bounds -> Bounds -> Bool #(<=) :: Bounds -> Bounds -> Bool #(>) :: Bounds -> Bounds -> Bool #(>=) :: Bounds -> Bounds -> Bool #max :: Bounds -> Bounds -> Bounds #min :: Bounds -> Bounds -> Bounds # Source # Methods Source # MethodsshowsPrec :: Int -> Bounds -> ShowS #showList :: [Bounds] -> ShowS # Source # Since: 0.5.1.0 Methodsrnf :: Bounds -> () # All bounds enabled, using their default values. Since: 0.2.0.0 No bounds enabled. This forces the scheduler to just use partial-order reduction and sleep sets to prune the search space. This will ONLY work if your computation always terminates! Since: 0.3.0.0 newtype PreemptionBound Source # Since: 0.2.0.0 Constructors  PreemptionBound Int Instances  Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # MethodsshowList :: [PreemptionBound] -> ShowS # Source # Since: 0.5.1.0 Methodsrnf :: PreemptionBound -> () # A sensible default preemption bound: 2. See Concurrency Testing Using Schedule Bounding: an Empirical Study, P. Thomson, A. F. Donaldson, A. Betts for justification. Since: 0.2.0.0 newtype FairBound Source # Since: 0.2.0.0 Constructors  FairBound Int Instances  Source # MethodsenumFrom :: FairBound -> [FairBound] # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # MethodsshowList :: [FairBound] -> ShowS # Source # Since: 0.5.1.0 Methodsrnf :: FairBound -> () # A sensible default fair bound: 5. This comes from playing around myself, but there is probably a better default. Since: 0.2.0.0 newtype LengthBound Source # Since: 0.2.0.0 Constructors  LengthBound Int Instances  Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # MethodsshowList :: [LengthBound] -> ShowS # Source # Since: 0.5.1.0 Methodsrnf :: LengthBound -> () # A sensible default length bound: 250. Based on the assumption that anything which executes for much longer (or even this long) will take ages to test. Since: 0.2.0.0 # 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 Source # The results of a test, including the number of cases checked to determine the final boolean outcome. Since: 0.2.0.0 Constructors  Result Fields_pass :: BoolWhether the test passed or not._casesChecked :: IntThe number of cases checked._failures :: [(Either Failure a, Trace)]The failing cases, if any._failureMsg :: StringA message to display on failure, if nonempty Instances  Source # Methodsfmap :: (a -> b) -> Result a -> Result b #(<$) :: a -> Result b -> Result a # Source # Methodsfold :: 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) Source # Methods(==) :: Result a -> Result a -> Bool #(/=) :: Result a -> Result a -> Bool # Show a => Show (Result a) Source # MethodsshowsPrec :: Int -> Result a -> ShowS #show :: Result a -> String #showList :: [Result a] -> ShowS # NFData a => NFData (Result a) Source # Since: 0.5.1.0 Methodsrnf :: Result a -> () #

data Failure Source #

An indication of how a concurrent computation failed.

The Eq, Ord, and NFData instances compare/evaluate the exception with show in the UncaughtException case.

Since: 0.9.0.0

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. 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 The computation became blocked indefinitely on MVars. STMDeadlock The computation became blocked indefinitely on TVars. UncaughtException SomeException An uncaught exception bubbled to the top of the computation. IllegalSubconcurrency Calls to subconcurrency were nested, or attempted when multiple threads existed.

Instances

 Source # Methods(==) :: Failure -> Failure -> Bool #(/=) :: Failure -> Failure -> Bool # Source # Methods(<) :: Failure -> Failure -> Bool #(<=) :: Failure -> Failure -> Bool #(>) :: Failure -> Failure -> Bool #(>=) :: Failure -> Failure -> Bool # Source # MethodsshowList :: [Failure] -> ShowS # Source # Methodsrnf :: Failure -> () #

Arguments

 :: Predicate a The predicate to check -> (forall t. ConcST t a) The computation to test -> Result a

Run a predicate over all executions within the default schedule bounds.

Since: 0.1.0.0

Arguments

 :: Way How to run the concurrent program. -> MemType The memory model to use for non-synchronised CRef operations. -> Predicate a The predicate to check -> (forall t. ConcST t a) The computation to test -> Result a

Variant of runTest which takes a way to run the program and a memory model.

Since: 0.6.0.0

runTestM :: MonadRef r n => Predicate a -> ConcT r n a -> n (Result a) Source #

Monad-polymorphic variant of runTest.

Since: 0.4.0.0

runTestWayM :: MonadRef r n => Way -> MemType -> Predicate a -> ConcT r n a -> n (Result a) Source #

Monad-polymorphic variant of runTest'.

Since: 0.6.0.0

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

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

Since: 0.1.0.0

representative :: Eq a => Predicate a -> Predicate a Source #

Reduce the list of failures in a Predicate 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: 0.2.0.0

Check that a computation never aborts.

Since: 0.2.0.0

Check that a computation always aborts.

Since: 0.2.0.0

Check that a computation aborts at least once.

Since: 0.2.0.0

Check that a computation never deadlocks.

Since: 0.1.0.0

Check that a computation always deadlocks.

Since: 0.1.0.0

Check that a computation deadlocks at least once.

Since: 0.1.0.0

Check that a computation never fails with an uncaught exception.

Since: 0.1.0.0

Check that a computation always fails with an uncaught exception.

Since: 0.1.0.0

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

Since: 0.1.0.0

alwaysSame :: Eq a => Predicate a Source #

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.

Since: 0.1.0.0

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

Since: 0.1.0.0

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

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

Since: 0.1.0.0

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

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.

Since: 0.1.0.0

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

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

Since: 0.1.0.0

gives :: (Eq a, Show a) => [Either Failure a] -> Predicate a Source #

Predicate for when there is a known set of results where every result must be exhibited at least once.

Since: 0.2.0.0

gives' :: (Eq a, Show a) => [a] -> Predicate a Source #

Variant of gives that doesn't allow for expected failures.

Since: 0.2.0.0

## Failures

Check if a failure is an InternalError.

@since undefined

Check if a failure is an Abort.

@since undefined

Check if a failure is a Deadlock or an STMDeadlock.

@since undefined

Check if a failure is an UncaughtException

@since undefined

Check if a failure is an IllegalSubconcurrency

@since undefined

# Refinement property testing

Consider this statement about MVars: "using readMVar is better than takeMVar followed by putMVar because the former is atomic but the latter is not."

Deja Fu can test properties like that:

sig e = Sig
{ initialise = maybe newEmptyMVar newMVar
, observe    = \v _ -> tryReadMVar v
, interfere  = \v s -> tryTakeMVar v >> maybe (pure ()) (void . tryPutMVar v) s
, expression = e
}

> check \$ sig (void . readMVar) equivalentTo sig (\v -> takeMVar v >>= putMVar v)
*** Failure: (seed Just ())
left:  [(Nothing,Just ())]