Copyright	(c) 2016 Michael Walker
License	MIT
Maintainer	Michael Walker <mike@barrucadu.co.uk>
Stability	stable
Portability	CPP, FlexibleContexts, FlexibleInstances, GADTs, ImpredicativeTypes, RankNTypes, TypeSynonymInstances
Safe Haskell	None
Language	Haskell2010

Test.Tasty.DejaFu

Contents

Unit testing
Property testing
- IO
- Re-exports
Refinement property testing
- Re-exports
Orphan instances

Description

This module allows using Deja Fu predicates with Tasty to test the behaviour of concurrent systems.

Synopsis

Unit testing

This is supported by the IsTest instances for ConcST and ConcIO. These instances try all executions, reporting as failures the cases which return a Just string.

instance Typeable t => IsTest (ConcST t (Maybe String)) instance IsTest (ConcIO (Maybe String)) instance IsOption Bounds instance IsOption MemType

Property testing

testAuto #

Arguments

:: (Eq a, Show a)
=> (forall t. ConcST t a)	The computation to test
-> TestTree

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

Since: 0.2.0.0

testDejafu #

Arguments

:: Show a
=> (forall t. ConcST t a)	The computation to test
-> TestName	The name of the test.
-> Predicate a	The predicate to check
-> TestTree

Check that a predicate holds.

Since: 0.2.0.0

testDejafus #

Arguments

:: Show a
=> (forall t. ConcST t a)	The computation to test
-> [(TestName, Predicate a)]	The list of predicates (with names) to check
-> TestTree

Variant of testDejafu which takes a collection of predicates to test. This will share work between the predicates, rather than running the concurrent computation many times for each predicate.

Since: 0.2.0.0

testAutoWay #

Arguments

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

Variant of testAuto which tests a computation under a given execution way and memory model.

Since: 0.5.0.0

testDejafuWay #

Arguments

:: Show a
=> Way	How to execute the concurrent program.
-> MemType	The memory model to use for non-synchronised `CRef` operations.
-> (forall t. ConcST t a)	The computation to test
-> TestName	The name of the test.
-> Predicate a	The predicate to check
-> TestTree

Variant of testDejafu which takes a way to execute the program and a memory model.

Since: 0.5.0.0

testDejafusWay #

Arguments

:: Show a
=> Way	How to execute the concurrent program.
-> MemType	The memory model to use for non-synchronised `CRef` operations.
-> (forall t. ConcST t a)	The computation to test
-> [(TestName, Predicate a)]	The list of predicates (with names) to check
-> TestTree

Variant of testDejafus which takes a way to execute the program and a memory model.

Since: 0.5.0.0

`IO`

testAutoIO :: (Eq a, Show a) => ConcIO a -> TestTree #

Variant of testAuto for computations which do IO.

Since: 0.2.0.0

testDejafuIO :: Show a => ConcIO a -> TestName -> Predicate a -> TestTree #

Variant of testDejafu for computations which do IO.

Since: 0.2.0.0

testDejafusIO :: Show a => ConcIO a -> [(TestName, Predicate a)] -> TestTree #

Variant of testDejafus for computations which do IO.

Since: 0.2.0.0

testAutoWayIO :: (Eq a, Show a) => Way -> MemType -> ConcIO a -> TestTree #

Variant of testAutoWay for computations which do IO.

Since: 0.5.0.0

testDejafuWayIO :: Show a => Way -> MemType -> ConcIO a -> TestName -> Predicate a -> TestTree #

Variant of testDejafuWay for computations which do IO.

Since: 0.5.0.0

testDejafusWayIO :: Show a => Way -> MemType -> ConcIO a -> [(TestName, Predicate a)] -> TestTree #

Variant of dejafusWay for computations which do IO.

Since: 0.5.0.0

Re-exports

data Way :: * #

How to explore the possible executions of a concurrent program.

Since: 0.7.0.0

Instances

Show Way
Methods showsPrec :: Int -> Way -> ShowS # show :: Way -> String # showList :: [Way] -> ShowS #

defaultWay :: Way #

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

Since: 0.6.0.0

systematically #

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

randomly #

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

uniformly #

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

swarmy #

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

data Bounds :: * #

Since: 0.2.0.0

Constructors

Bounds
Fields boundPreemp :: Maybe PreemptionBound boundFair :: Maybe FairBound boundLength :: Maybe LengthBound

Instances

Eq Bounds
Methods (==) :: Bounds -> Bounds -> Bool # (/=) :: Bounds -> Bounds -> Bool #
Ord Bounds
Methods compare :: Bounds -> Bounds -> Ordering # (<) :: Bounds -> Bounds -> Bool # (<=) :: Bounds -> Bounds -> Bool # (>) :: Bounds -> Bounds -> Bool # (>=) :: Bounds -> Bounds -> Bool # max :: Bounds -> Bounds -> Bounds # min :: Bounds -> Bounds -> Bounds #
Read Bounds
Methods readsPrec :: Int -> ReadS Bounds # readList :: ReadS [Bounds] # readPrec :: ReadPrec Bounds # readListPrec :: ReadPrec [Bounds] #
Show Bounds
Methods showsPrec :: Int -> Bounds -> ShowS # show :: Bounds -> String # showList :: [Bounds] -> ShowS #
NFData Bounds	Since: 0.5.1.0
Methods rnf :: Bounds -> () #

defaultBounds :: Bounds #

All bounds enabled, using their default values.

Since: 0.2.0.0

data MemType :: * #

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 `CRef`s are not necessarily committed in the same order that they are created.

Instances

Bounded MemType
Methods minBound :: MemType # maxBound :: MemType #
Enum MemType
Methods succ :: MemType -> MemType # pred :: MemType -> MemType # toEnum :: Int -> MemType # fromEnum :: MemType -> Int # enumFrom :: MemType -> [MemType] # enumFromThen :: MemType -> MemType -> [MemType] # enumFromTo :: MemType -> MemType -> [MemType] # enumFromThenTo :: MemType -> MemType -> MemType -> [MemType] #
Eq MemType
Methods (==) :: MemType -> MemType -> Bool # (/=) :: MemType -> MemType -> Bool #
Ord MemType
Methods compare :: MemType -> MemType -> Ordering # (<) :: MemType -> MemType -> Bool # (<=) :: MemType -> MemType -> Bool # (>) :: MemType -> MemType -> Bool # (>=) :: MemType -> MemType -> Bool # max :: MemType -> MemType -> MemType # min :: MemType -> MemType -> MemType #
Read MemType
Methods readsPrec :: Int -> ReadS MemType # readList :: ReadS [MemType] # readPrec :: ReadPrec MemType # readListPrec :: ReadPrec [MemType] #
Show MemType
Methods showsPrec :: Int -> MemType -> ShowS # show :: MemType -> String # showList :: [MemType] -> ShowS #
NFData MemType	Since: 0.5.1.0
Methods rnf :: MemType -> () #

defaultMemType :: MemType #

The default memory model: TotalStoreOrder

Since: 0.2.0.0

Refinement property testing

testProperty #

Arguments

:: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p))
=> TestName	The name of the test.
-> p	The property to check.
-> TestTree

Check a refinement property with a variety of seed values and variable assignments.

Since: 0.6.0.0

Re-exports

data Sig s o x :: * -> * -> * -> * #

A concurrent function and some information about how to execute it and observe its effect.

s is the state type (MVar ConcIO a in the example)
o is the observation type (Maybe a in the example)
x is the seed type (Maybe a in the example)

Since: 0.7.0.0

Constructors

Sig
Fields initialise :: x -> ConcIO s Create a new instance of the state variable. observe :: s -> x -> ConcIO o The observation to make. interfere :: s -> x -> ConcIO () Set the state value. This doesn't need to be atomic, or even guaranteed to work, its purpose is to cause interference. expression :: s -> ConcIO () The expression to evaluate.

data RefinementProperty o x :: * -> * -> * #

A property which can be given to check.

Since: 0.7.0.0

Instances

Testable (RefinementProperty o x)
Associated Types type O (RefinementProperty o x) :: * # type X (RefinementProperty o x) :: * # Methods rpropTiers :: RefinementProperty o x -> [[([String], RefinementProperty (O (RefinementProperty o x)) (X (RefinementProperty o x)))]]
type X (RefinementProperty o x)
type X (RefinementProperty o x) = x
type O (RefinementProperty o x)
type O (RefinementProperty o x) = o

class Testable a #

Things which can be tested.

Since: 0.7.0.0

Minimal complete definition

rpropTiers

Associated Types

type O a :: * #

The observation value type. This is used to compare the results.

type X a :: * #

The seed value type. This is used to construct the concurrent states.

Instances

(Listable a, Show a, Testable b) => Testable (a -> b)
Associated Types type O (a -> b) :: * # type X (a -> b) :: * # Methods rpropTiers :: (a -> b) -> [[([String], RefinementProperty (O (a -> b)) (X (a -> b)))]]
Testable (RefinementProperty o x)
Associated Types type O (RefinementProperty o x) :: * # type X (RefinementProperty o x) :: * # Methods rpropTiers :: RefinementProperty o x -> [[([String], RefinementProperty (O (RefinementProperty o x)) (X (RefinementProperty o x)))]]

class Listable a where #

A type is Listable when there exists a function that is able to list (ideally all of) its values.

Ideally, instances should be defined by a tiers function that returns a (potentially infinite) list of finite sub-lists (tiers): the first sub-list contains elements of size 0, the second sub-list contains elements of size 1 and so on. Size here is defined by the implementor of the type-class instance.

For algebraic data types, the general form for tiers is

tiers = cons<N> ConstructorA
     \/ cons<N> ConstructorB
     \/ ...
     \/ cons<N> ConstructorZ

where N is the number of arguments of each constructor A...Z.

Instances can be alternatively defined by list. In this case, each sub-list in tiers is a singleton list (each succeeding element of list has +1 size).

The function deriveListable from Test.LeanCheck.Derive can automatically derive instances of this typeclass.

A Listable instance for functions is also available but is not exported by default. Import Test.LeanCheck.Function if you need to test higher-order properties.

Minimal complete definition

list | tiers

Methods

tiers :: [[a]] #

list :: [a] #

Instances

Listable Bool	tiers :: [[Bool]] = [[False,True]] list :: [[Bool]] = [False,True]
Methods tiers :: [[Bool]] # list :: [Bool] #
Listable Char
Methods tiers :: [[Char]] # list :: [Char] #
Listable Double
Methods tiers :: [[Double]] # list :: [Double] #
Listable Float
Methods tiers :: [[Float]] # list :: [Float] #
Listable Int	tiers :: [[Int]] = [[0], [1], [-1], [2], [-2], [3], [-3], ...] list :: [Int] = [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...]
Methods tiers :: [[Int]] # list :: [Int] #
Listable Integer
Methods tiers :: [[Integer]] # list :: [Integer] #
Listable Ordering
Methods tiers :: [[Ordering]] # list :: [Ordering] #
Listable ()
Methods tiers :: [[()]] # list :: [()] #
Listable a => Listable [a]	tiers :: [[ [Int] ]] = [ [ [] ] , [ [0] ] , [ [0,0], [1] ] , [ [0,0,0], [0,1], [1,0], [-1] ] , ... ] list :: [ [Int] ] = [ [], [0], [0,0], [1], [0,0,0], [0,1], [1,0], [-1], ... ]
Methods tiers :: [[[a]]] # list :: [[a]] #
Listable a => Listable (Maybe a)	tiers :: [[Maybe Int]] = [[Nothing], [Just 0], [Just 1], [Just -1], ...] tiers :: [[Maybe Bool]] = [[Nothing], [Just False, Just True]]
Methods tiers :: [[Maybe a]] # list :: [Maybe a] #
(Listable a, Listable b) => Listable (Either a b)
Methods tiers :: [[Either a b]] # list :: [Either a b] #
(Listable a, Listable b) => Listable (a, b)	tiers :: [[(Int,Int)]] = [ [(0,0)], [(0,1),(1,0)], [(0,-1),(1,1),(-1,0)], ...] list :: [(Int,Int)] = [ (0,0), (0,1), (1,0), (0,-1), (1,1), (-1,0), ...]
Methods tiers :: [[(a, b)]] # list :: [(a, b)] #
(Listable a, Listable b, Listable c) => Listable (a, b, c)
Methods tiers :: [[(a, b, c)]] # list :: [(a, b, c)] #
(Listable a, Listable b, Listable c, Listable d) => Listable (a, b, c, d)
Methods tiers :: [[(a, b, c, d)]] # list :: [(a, b, c, d)] #
(Listable a, Listable b, Listable c, Listable d, Listable e) => Listable (a, b, c, d, e)	Instances for `Listable` sixtuples up to 12-tuples are exported by default form Test.LeanCheck but are hidden from Haddock documentation. These instances are defined in Test.LeanCheck.Basic.
Methods tiers :: [[(a, b, c, d, e)]] # list :: [(a, b, c, d, e)] #

expectFailure :: RefinementProperty o x -> RefinementProperty o x #

Indicates that the property is supposed to fail.

refines :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x #

Observational refinement.

True iff the result-set of the left expression is a subset (not necessarily proper) of the result-set of the right expression.

The two signatures can have different state types, this lets you compare the behaviour of different data structures. The observation and seed types must match, however.

Since: 0.7.0.0

(=>=) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x #

Infix synonym for refines.

You might think this should be =<=, so it looks kind of like a funny subset operator, with A =<= B meaning "the result-set of A is a subset of the result-set of B". Unfortunately you would be wrong. The operator used in the literature for refinement has the open end pointing at the LESS general term and the closed end at the MORE general term. It is read as "is refined by", not "refines". So for consistency with the literature, the open end of =>= points at the less general term, and the closed end at the more general term, to give the same argument order as refines.

Since: 0.7.0.0

strictlyRefines :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x #

Strict observational refinement.

True iff the result-set of the left expression is a proper subset of the result-set of the right expression.

The two signatures can have different state types, this lets you compare the behaviour of different data structures. The observation and seed types must match, however.

Since: 0.7.0.0

(->-) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x #

Infix synonym for strictlyRefines

Since: 0.7.0.0

equivalentTo :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x #

Observational equivalence.

True iff the result-set of the left expression is equal to the result-set of the right expression.

The two signatures can have different state types, this lets you compare the behaviour of different data structures. The observation and seed types must match, however.

Since: 0.7.0.0

(===) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x #

Infix synonym for equivalentTo.

Since: 0.7.0.0

Orphan instances

IsOption Way #	Since: 0.5.0.0
Methods defaultValue :: Way # parseValue :: String -> Maybe Way # optionName :: Tagged * Way String # optionHelp :: Tagged * Way String # optionCLParser :: Parser Way #
IsOption MemType #	Since: 0.3.0.0
Methods defaultValue :: MemType # parseValue :: String -> Maybe MemType # optionName :: Tagged * MemType String # optionHelp :: Tagged * MemType String # optionCLParser :: Parser MemType #
IsTest (ConcIO (Maybe String)) #	Since: 0.3.0.0
Methods run :: OptionSet -> ConcIO (Maybe String) -> (Progress -> IO ()) -> IO Result # testOptions :: Tagged * (ConcIO (Maybe String)) [OptionDescription] #
Typeable * t => IsTest (ConcST t (Maybe String)) #	Since: 0.3.0.0
Methods run :: OptionSet -> ConcST t (Maybe String) -> (Progress -> IO ()) -> IO Result # testOptions :: Tagged * (ConcST t (Maybe String)) [OptionDescription] #