Copyright | (c) 2016 Michael Walker |
---|---|
License | MIT |
Maintainer | Michael Walker <mike@barrucadu.co.uk> |
Stability | stable |
Portability | CPP, FlexibleContexts, FlexibleInstances, GADTs, ImpredicativeTypes, LambdaCase, RankNTypes, TypeSynonymInstances |
Safe Haskell | None |
Language | Haskell2010 |
This module allows using Deja Fu predicates with Tasty to test the behaviour of concurrent systems.
- testAuto :: (Eq a, Show a) => (forall t. ConcST t a) -> TestTree
- testDejafu :: Show a => (forall t. ConcST t a) -> TestName -> Predicate a -> TestTree
- testDejafus :: Show a => (forall t. ConcST t a) -> [(TestName, Predicate a)] -> TestTree
- testAutoWay :: (Eq a, Show a) => Way -> MemType -> (forall t. ConcST t a) -> TestTree
- testDejafuWay :: Show a => Way -> MemType -> (forall t. ConcST t a) -> TestName -> Predicate a -> TestTree
- testDejafusWay :: Show a => Way -> MemType -> (forall t. ConcST t a) -> [(TestName, Predicate a)] -> TestTree
- testDejafuDiscard :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> (forall t. ConcST t a) -> String -> Predicate a -> TestTree
- testAutoIO :: (Eq a, Show a) => ConcIO a -> TestTree
- testDejafuIO :: Show a => ConcIO a -> TestName -> Predicate a -> TestTree
- testDejafusIO :: Show a => ConcIO a -> [(TestName, Predicate a)] -> TestTree
- testAutoWayIO :: (Eq a, Show a) => Way -> MemType -> ConcIO a -> TestTree
- testDejafuWayIO :: Show a => Way -> MemType -> ConcIO a -> TestName -> Predicate a -> TestTree
- testDejafusWayIO :: Show a => Way -> MemType -> ConcIO a -> [(TestName, Predicate a)] -> TestTree
- testDejafuDiscardIO :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcIO a -> String -> Predicate a -> TestTree
- data Way :: *
- defaultWay :: Way
- systematically :: Bounds -> Way
- randomly :: RandomGen g => g -> Int -> Way
- uniformly :: RandomGen g => g -> Int -> Way
- swarmy :: RandomGen g => g -> Int -> Int -> Way
- data Bounds :: * = Bounds {}
- defaultBounds :: Bounds
- data MemType :: *
- defaultMemType :: MemType
- data Discard :: *
- defaultDiscarder :: Either Failure a -> Maybe Discard
- testProperty :: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) => TestName -> p -> TestTree
- testPropertyFor :: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) => Int -> Int -> TestName -> p -> TestTree
- data Sig s o x :: * -> * -> * -> * = Sig {
- initialise :: x -> ConcIO s
- observe :: s -> x -> ConcIO o
- interfere :: s -> x -> ConcIO ()
- expression :: s -> ConcIO ()
- data RefinementProperty o x :: * -> * -> *
- class Testable a where
- class Listable a where
- expectFailure :: RefinementProperty o x -> RefinementProperty o x
- refines :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
- (=>=) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
- strictlyRefines :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
- (->-) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
- equivalentTo :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
- (===) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
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
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
:: 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
:: 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
:: (Eq a, Show a) | |
=> Way | How to execute the concurrent program. |
-> MemType | The memory model to use for non-synchronised |
-> (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
:: Show a | |
=> Way | How to execute the concurrent program. |
-> MemType | The memory model to use for non-synchronised |
-> (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
:: Show a | |
=> Way | How to execute the concurrent program. |
-> MemType | The memory model to use for non-synchronised |
-> (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
:: Show a | |
=> (Either Failure a -> Maybe Discard) | Selectively discard results. |
-> Way | How to execute the concurrent program. |
-> MemType | The memory model to use for non-synchronised |
-> (forall t. ConcST t a) | The computation to test |
-> String | The name of the test. |
-> Predicate a | The predicate to check |
-> TestTree |
Variant of testDejafuWay
which can selectively discard results.
Since: 0.7.0.0
IO
testDejafuIO :: Show a => ConcIO a -> TestName -> Predicate a -> TestTree Source #
Variant of testDejafu
for computations which do IO
.
Since: 0.2.0.0
testDejafusIO :: Show a => ConcIO a -> [(TestName, Predicate a)] -> TestTree Source #
Variant of testDejafus
for computations which do IO
.
Since: 0.2.0.0
testAutoWayIO :: (Eq a, Show a) => Way -> MemType -> ConcIO a -> TestTree Source #
Variant of testAutoWay
for computations which do IO
.
Since: 0.5.0.0
testDejafuWayIO :: Show a => Way -> MemType -> ConcIO a -> TestName -> Predicate a -> TestTree Source #
Variant of testDejafuWay
for computations which do IO
.
Since: 0.5.0.0
testDejafusWayIO :: Show a => Way -> MemType -> ConcIO a -> [(TestName, Predicate a)] -> TestTree Source #
Variant of dejafusWay
for computations which do IO
.
Since: 0.5.0.0
testDejafuDiscardIO :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcIO a -> String -> Predicate a -> TestTree Source #
Variant of testDejafuDiscard
for computations which do IO
.
Since: 0.7.0.0
Re-exports
How to explore the possible executions of a concurrent program.
Since: 0.7.0.0
defaultWay :: Way #
A default way to execute concurrent programs: systematically
using defaultBounds
.
Since: 0.6.0.0
Systematically execute a program, trying all distinct executions within the bounds.
This corresponds to sctBound
.
Since: 0.7.0.0
:: 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
:: 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
:: 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
Since: 0.2.0.0
defaultBounds :: Bounds #
All bounds enabled, using their default values.
Since: 0.2.0.0
The memory model to use for non-synchronised CRef
operations.
Since: 0.4.0.0
SequentialConsistency | The most intuitive model: a program behaves as a simple
interleaving of the actions in different threads. When a |
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 |
The default memory model: TotalStoreOrder
Since: 0.2.0.0
An Either Failure a -> Maybe Discard
value can be used to
selectively discard results.
Since: 0.7.1.0
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. |
Refinement property testing
:: (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
:: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) | |
=> Int | The number of seed values to try. |
-> Int | The number of variable assignments per seed value to try. |
-> TestName | The name of the test. |
-> p | The property to check. |
-> TestTree |
Like testProperty
, but takes a number of cases to check.
The maximum number of cases tried by testPropertyFor n m
will be
n * m
.
Since: 0.7.1.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
Sig | |
|
data RefinementProperty o x :: * -> * -> * #
A property which can be given to check
.
Since: 0.7.0.0
Testable (RefinementProperty o x) | |
type X (RefinementProperty o x) | |
type O (RefinementProperty o x) | |
Things which can be tested.
Since: 0.7.0.0
rpropTiers
The observation value type. This is used to compare the results.
The seed value type. This is used to construct the concurrent states.
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.
Listable Bool | tiers :: [[Bool]] = [[False,True]] list :: [[Bool]] = [False,True] |
Listable Char | |
Listable Double | |
Listable 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, ...] |
Listable Integer | |
Listable Ordering | |
Listable () | |
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], ... ] |
Listable a => Listable (Maybe a) | tiers :: [[Maybe Int]] = [[Nothing], [Just 0], [Just 1], ...] tiers :: [[Maybe Bool]] = [[Nothing], [Just False, Just True]] |
(Listable a, Listable b) => Listable (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), ...] |
(Listable a, Listable b, Listable c) => Listable (a, b, c) | |
(Listable a, Listable b, Listable c, Listable d) => Listable (a, b, c, d) | |
(Listable a, Listable b, Listable c, Listable d, Listable e) => Listable (a, b, c, d, e) | Instances for |
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