| Copyright | (c) 2015--2017 Michael Walker |
|---|---|
| License | MIT |
| Maintainer | Michael Walker <mike@barrucadu.co.uk> |
| Stability | experimental |
| Portability | LambdaCase, MultiParamTypeClasses, TupleSections |
| Safe Haskell | None |
| Language | Haskell2010 |
Test.DejaFu
Contents
Description
dejafu is a library for unit-testing concurrent Haskell programs,
written using the concurrency
package's MonadConc typeclass.
A first test: This is a simple concurrent program which forks two
threads and each races to write to the same MVar:
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] Never Deadlocks
[pass] No Exceptions
[fail] Consistent Result
"hello" S0----S1--S0--
"world" S0----S2--S0--The autocheck function takes a concurrent program to test and looks
for some common unwanted behaviours: deadlocks, uncaught exceptions in
the main thread, 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.
Failures: If a program doesn't terminate successfully, we say it has failed. dejafu can detect a few different types of failure:
Deadlock, if every thread is blocked.STMDeadlock, if every thread is blocked and the main thread is blocked in an STM transaction.UncaughtException, if the main thread is killed by an exception.
There are two types of failure which dejafu itself may raise:
Abort, used in systematic testing (the default) if there are no allowed decisions remaining. For example, by default any test case which takes more than 250 scheduling points to finish will be aborted. You can use thesystematicallyfunction to supply (or disable) your own bounds.InternalError, used if something goes wrong. If you get this and aren't using a scheduler you wrote yourself, please file a bug.
Finally, there is one failure which can arise through improper use of dejafu:
IllegalSubconcurrency, the "Test.DejaFu.Conc.subconcurrency" function is used when multiple threads exist, or is used inside anothersubconcurrencycall.
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, uniformly, and swarmy testing modes can cope with
nondeterminism.
- autocheck :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) => ConcT r n a -> n Bool
- dejafu :: (MonadConc n, MonadIO n, MonadRef r n, Show b) => String -> ProPredicate a b -> ConcT r n a -> n Bool
- dejafus :: (MonadConc n, MonadIO n, MonadRef r n, Show b) => [(String, ProPredicate a b)] -> ConcT r n a -> n Bool
- autocheckWay :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) => Way -> MemType -> ConcT r n a -> n Bool
- dejafuWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b) => Way -> MemType -> String -> ProPredicate a b -> ConcT r n a -> n Bool
- dejafusWay :: (MonadConc n, MonadIO n, MonadRef r n, Show b) => Way -> MemType -> [(String, ProPredicate a b)] -> ConcT r n a -> n Bool
- dejafuDiscard :: (MonadConc n, MonadIO n, MonadRef r n, Show b) => (Either Failure a -> Maybe Discard) -> Way -> MemType -> String -> ProPredicate a b -> ConcT r n a -> n Bool
- defaultWay :: Way
- defaultMemType :: MemType
- defaultDiscarder :: Either Failure a -> Maybe Discard
- data 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
- noBounds :: Bounds
- newtype PreemptionBound = PreemptionBound Int
- defaultPreemptionBound :: PreemptionBound
- newtype FairBound = FairBound Int
- defaultFairBound :: FairBound
- newtype LengthBound = LengthBound Int
- defaultLengthBound :: LengthBound
- data MemType
- data Discard
- data Result a = Result {}
- data Failure
- runTest :: (MonadConc n, MonadRef r n) => ProPredicate a b -> ConcT r n a -> n (Result b)
- runTestWay :: (MonadConc n, MonadRef r n) => Way -> MemType -> ProPredicate a b -> ConcT r n a -> n (Result b)
- type Predicate a = ProPredicate a a
- data ProPredicate a b = ProPredicate {}
- abortsNever :: Predicate a
- abortsAlways :: Predicate a
- abortsSometimes :: Predicate a
- deadlocksNever :: Predicate a
- deadlocksAlways :: Predicate a
- deadlocksSometimes :: Predicate a
- exceptionsNever :: Predicate a
- exceptionsAlways :: Predicate a
- exceptionsSometimes :: Predicate a
- representative :: Eq b => ProPredicate a b -> ProPredicate a b
- alwaysSame :: Eq a => Predicate a
- alwaysSameOn :: Eq b => (Either Failure a -> b) -> Predicate a
- alwaysSameBy :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a
- notAlwaysSame :: Eq a => Predicate a
- alwaysTrue :: (Either Failure a -> Bool) -> Predicate a
- somewhereTrue :: (Either Failure a -> Bool) -> Predicate a
- alwaysNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b
- somewhereNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b
- gives :: (Eq a, Show a) => [Either Failure a] -> Predicate a
- gives' :: (Eq a, Show a) => [a] -> Predicate a
- isInternalError :: Failure -> Bool
- isAbort :: Failure -> Bool
- isDeadlock :: Failure -> Bool
- isUncaughtException :: Failure -> Bool
- isIllegalSubconcurrency :: Failure -> Bool
- module Test.DejaFu.Refinement
Unit testing
Arguments
| :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) | |
| => ConcT r n a | The computation to test. |
| -> n Bool |
Automatically test a computation.
In particular, look for deadlocks, uncaught exceptions, and
multiple return values. Returns True if all tests pass
> autocheck example
[pass] Never Deadlocks
[pass] No Exceptions
[fail] Consistent Result
"hello" S0----S1--S0--
"world" S0----S2--S0--Since: 1.0.0.0
Arguments
| :: (MonadConc n, MonadIO n, MonadRef r n, Show b) | |
| => String | The name of the test. |
| -> ProPredicate a b | The predicate to check. |
| -> ConcT r 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--Since: 1.0.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.
Arguments
| :: (MonadConc n, MonadIO n, MonadRef r n, Eq a, Show a) | |
| => Way | How to run the concurrent program. |
| -> MemType | The memory model to use for non-synchronised |
| -> ConcT r 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] Never Deadlocks
[pass] No Exceptions
[fail] Consistent Result
(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---
> autocheckWay defaultWay SequentialConsistency relaxed
[pass] Never Deadlocks
[pass] No Exceptions
[fail] Consistent Result
(False,True) S0---------S1----S0--S2----S0--
(True,True) S0---------S1-P2----S1---S0---
(True,False) S0---------S2----S1----S0---Since: 1.0.0.0
Arguments
| :: (MonadConc n, MonadIO n, MonadRef r n, Show b) | |
| => Way | How to run the concurrent program. |
| -> MemType | The memory model to use for non-synchronised |
| -> String | The name of the test. |
| -> ProPredicate a b | The predicate to check. |
| -> ConcT r 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--
> dejafuWay (randomly (mkStdGen 1) 100) defaultMemType "Randomly!" alwaysSame example
[fail] Randomly!
"hello" S0----S1--S0--
"world" S0----S2--S1-S0--Since: 1.0.0.0
Arguments
| :: (MonadConc n, MonadIO n, MonadRef r n, Show b) | |
| => Way | How to run the concurrent program. |
| -> MemType | The memory model to use for non-synchronised |
| -> [(String, ProPredicate a b)] | The list of predicates (with names) to check. |
| -> ConcT r 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] BSince: 1.0.0.0
Arguments
| :: (MonadConc n, MonadIO n, MonadRef r n, Show b) | |
| => (Either Failure a -> Maybe Discard) | Selectively discard results. |
| -> Way | How to run the concurrent program. |
| -> MemType | The memory model to use for non-synchronised |
| -> String | The name of the test. |
| -> ProPredicate a b | The predicate to check. |
| -> ConcT r n a | The computation to test. |
| -> n Bool |
Variant of dejafuWay which can selectively discard results.
> dejafuDiscard (\_ -> Just DiscardTrace) defaultWay defaultMemType "Discarding" alwaysSame example
[fail] Discarding
"hello" <trace discarded>
"world" <trace discarded>Since: 1.0.0.0
Defaults
defaultWay :: Way Source #
A default way to execute concurrent programs: systematically
using defaultBounds.
Since: 0.6.0.0
defaultMemType :: MemType Source #
The default memory model: TotalStoreOrder
Since: 0.2.0.0
defaultDiscarder :: Either Failure a -> Maybe Discard Source #
Do not discard any results.
Since: 0.7.1.0
Exploration
How to explore the possible executions of a concurrent program.
Since: 0.7.0.0
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
Schedule bounding
Schedule bounding is used by the systematically approach to limit
the search-space, which in general will be huge.
There are three types of bounds used:
- The
PreemptionBound, which bounds the number of pre-emptive context switches. Empirical evidence suggests2is a good value for this, if you have a small test case. - The
FairBound, which bounds the difference between how many times threads can yield. This is necessary to test certain kinds of potentially non-terminating behaviour, such as spinlocks. - The
LengthBound, which bounds how long a test case can run, in terms of scheduling decisions. This is necessary to test certain kinds of potentially non-terminating behaviour, such as livelocks.
Schedule bounding is not used by the non-systematic exploration behaviours.
Since: 0.2.0.0
Constructors
| Bounds | |
Fields | |
defaultBounds :: Bounds Source #
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 #
BPOR using pre-emption bounding. This adds conservative backtracking points at the prior context switch whenever a non-conervative backtracking point is added, as alternative decisions can influence the reachability of different states.
See the BPOR paper for more details.
Since: 0.2.0.0
Constructors
| PreemptionBound Int |
Instances
defaultPreemptionBound :: PreemptionBound Source #
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
BPOR using fair bounding. This bounds the maximum difference between the number of yield operations different threads have performed.
See the BPOR paper for more details.
Since: 0.2.0.0
defaultFairBound :: FairBound Source #
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 #
BPOR using length bounding. This bounds the maximum length (in terms of primitive actions) of an execution.
Since: 0.2.0.0
Constructors
| LengthBound Int |
Instances
defaultLengthBound :: LengthBound Source #
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
Memory model
When executed on a multi-core processor some CRef / IORef programs
can exhibit "relaxed memory" behaviours, where the apparent
behaviour of the program is not a simple interleaving of the actions
of each thread.
Example: This is a simple program which creates two CRefs
containing False, and forks two threads. Each thread writes True
to one of the CRefs and reads the other. The value that each thread
reads is communicated back through an MVar:
relaxed = 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
We see something surprising if we ask for the results:
> autocheck relaxed
[pass] Never Deadlocks
[pass] No Exceptions
[fail] Consistent Result
(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---It's possible for both threads to read the value False, even though
each writes True to the other CRef before reading. This is
because processors are free to re-order reads and writes to
independent memory addresses in the name of performance.
Execution traces for relaxed memory computations can include "C"
actions, as above, which show where CRef writes were explicitly
committed, and made visible to other threads.
However, modelling this behaviour can require more executions. If you
do not care about the relaxed-memory behaviour of your program, use
the SequentialConsistency model.
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 |
| 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 |
Reducing memory usage
Sometimes we know that a result is uninteresting and cannot affect the result of a test, in which case there is no point in keeping it around. Execution traces can be large, so any opportunity to get rid of them early is possibly a great saving of memory.
A discard function, which has type Either Failure a -> Maybe
Discard, can selectively discard results or execution traces before
the schedule exploration finishes, allowing them to be garbage
collected sooner.
Note: This is only relevant if you are producing your own predicates. The predicates and helper functions provided by this module do discard results and traces wherever possible.
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. |
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.
The results of a test, including the number of cases checked to determine the final boolean outcome.
Since: 1.0.0.0
Constructors
| Result | |
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 | Every thread is blocked, and the main thread is not blocked in an STM transaction. |
| STMDeadlock | Every thread is blocked, and the main thread is blocked in an STM transaction. |
| UncaughtException SomeException | An uncaught exception bubbled to the top of the computation. |
| IllegalSubconcurrency | Calls to |
Arguments
| :: (MonadConc n, MonadRef r n) | |
| => ProPredicate a b | The predicate to check |
| -> ConcT r 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: 1.0.0.0
Arguments
| :: (MonadConc n, MonadRef r n) | |
| => Way | How to run the concurrent program. |
| -> MemType | The memory model to use for non-synchronised |
| -> ProPredicate a b | The predicate to check |
| -> ConcT r 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: 1.0.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 Source #
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 Source #
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 | |
Instances
abortsNever :: Predicate a Source #
Check that a computation never aborts.
Since: 1.0.0.0
abortsAlways :: Predicate a Source #
Check that a computation always aborts.
Since: 1.0.0.0
abortsSometimes :: Predicate a Source #
Check that a computation aborts at least once.
Since: 1.0.0.0
deadlocksNever :: Predicate a Source #
Check that a computation never deadlocks.
Since: 1.0.0.0
deadlocksAlways :: Predicate a Source #
Check that a computation always deadlocks.
Since: 1.0.0.0
deadlocksSometimes :: Predicate a Source #
Check that a computation deadlocks at least once.
Since: 1.0.0.0
exceptionsNever :: Predicate a Source #
Check that a computation never fails with an uncaught exception.
Since: 1.0.0.0
exceptionsAlways :: Predicate a Source #
Check that a computation always fails with an uncaught exception.
Since: 1.0.0.0
exceptionsSometimes :: Predicate a Source #
Check that a computation fails with an uncaught exception at least once.
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 Source #
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
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.
alwaysSame = alwaysSameBy (==)
Since: 1.0.0.0
alwaysSameOn :: Eq b => (Either Failure a -> b) -> Predicate a Source #
Check that the result of a computation is always the same by comparing the result of a function on every result.
alwaysSameOn = alwaysSameBy ((==) `on` f)
Since: 1.0.0.0
alwaysSameBy :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a Source #
Check that the result of a computation is always the same, using some transformation on results.
Since: 1.0.0.0
notAlwaysSame :: Eq a => Predicate a Source #
Check that the result of a computation is not always the same.
Since: 1.0.0.0
alwaysTrue :: (Either Failure a -> Bool) -> Predicate a Source #
Check that the result of a unary boolean predicate is always true.
Since: 1.0.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: 1.0.0.0
alwaysNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b Source #
Check that a Maybe-producing function always returns Nothing.
Since: 1.0.0.0
somewhereNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b Source #
Check that a Maybe-producing function returns Nothing at
least once.
Since: 1.0.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: 1.0.0.0
gives' :: (Eq a, Show a) => [a] -> Predicate a Source #
Variant of gives that doesn't allow for expected failures.
Since: 1.0.0.0
Failures
Helper functions to identify failures.
isInternalError :: Failure -> Bool Source #
Check if a failure is an InternalError.
Since: 0.9.0.0
isDeadlock :: Failure -> Bool Source #
Check if a failure is a Deadlock or an STMDeadlock.
Since: 0.9.0.0
isUncaughtException :: Failure -> Bool Source #
Check if a failure is an UncaughtException
Since: 0.9.0.0
isIllegalSubconcurrency :: Failure -> Bool Source #
Check if a failure is an IllegalSubconcurrency
Since: 0.9.0.0
Property testing
dejafu can also use a property-testing style to test stateful operations for a variety of inputs. Inputs are generated using the [leancheck](https:/hackage.haskell.orgpackage/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.
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)]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