| Copyright | (c) 2018 Michael Walker |
|---|---|
| License | MIT |
| Maintainer | Michael Walker <mike@barrucadu.co.uk> |
| Stability | experimental |
| Portability | RankNTypes |
| Safe Haskell | None |
| Language | Haskell2010 |
Test.DejaFu.Settings
Contents
Description
Configuration for the SCT functions.
Synopsis
- data Settings n a
- defaultSettings :: Applicative n => Settings n a
- fromWayAndMemType :: Applicative n => Way -> MemType -> Settings n a
- data Way
- defaultWay :: Way
- lway :: Lens' (Settings n a) Way
- systematically :: Bounds -> Way
- randomly :: RandomGen g => g -> Int -> Way
- uniformly :: RandomGen g => g -> Int -> Way
- data Bounds = Bounds {}
- newtype PreemptionBound = PreemptionBound Int
- newtype FairBound = FairBound Int
- defaultBounds :: Bounds
- defaultPreemptionBound :: PreemptionBound
- defaultFairBound :: FairBound
- noBounds :: Bounds
- newtype LengthBound = LengthBound Int
- llengthBound :: Lens' (Settings n a) (Maybe LengthBound)
- data MemType
- defaultMemType :: MemType
- lmemtype :: Lens' (Settings n a) MemType
- data Discard
- ldiscard :: Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
- learlyExit :: Lens' (Settings n a) (Maybe (Either Condition a -> Bool))
- lequality :: Lens' (Settings n a) (Maybe (a -> a -> Bool))
- lsimplify :: Lens' (Settings n a) Bool
- lsafeIO :: Lens' (Settings n a) Bool
- lshowAborts :: Lens' (Settings n a) Bool
- ldebugShow :: Lens' (Settings n a) (Maybe (a -> String))
- ldebugPrint :: Lens' (Settings n a) (Maybe (String -> n ()))
- ldebugFatal :: Lens' (Settings n a) Bool
- get :: Lens' s a -> s -> a
- set :: Lens' s a -> a -> s -> s
SCT configuration
defaultSettings :: Applicative n => Settings n a Source #
Default SCT settings: just combine all the other defaults.
Since: 1.2.0.0
fromWayAndMemType :: Applicative n => Way -> MemType -> Settings n a Source #
The Way
How to explore the possible executions of a concurrent program.
Since: 0.7.0.0
defaultWay :: Way Source #
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.
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 is not guaranteed to find all distinct results (unlike
systematically).
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 is not guaranteed to find all distinct results (unlike
systematically).
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 bound:
- 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: 2.0.0.0
Constructors
| Bounds | |
Fields | |
Instances
| Eq Bounds Source # | |
| Ord Bounds Source # | |
| Read Bounds Source # | |
| Show Bounds Source # | |
| Generic Bounds Source # | |
| NFData Bounds Source # | |
Defined in Test.DejaFu.Types | |
| type Rep Bounds Source # | |
Defined in Test.DejaFu.Types type Rep Bounds = D1 (MetaData "Bounds" "Test.DejaFu.Types" "dejafu-2.3.0.0-CH3NTXDh8GWHZYQQRWnPX9" False) (C1 (MetaCons "Bounds" PrefixI True) (S1 (MetaSel (Just "boundPreemp") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe PreemptionBound)) :*: S1 (MetaSel (Just "boundFair") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe FairBound)))) | |
newtype PreemptionBound Source #
Restrict the number of pre-emptive context switches allowed in an execution.
A pre-emption bound of zero disables pre-emptions entirely.
Since: 0.2.0.0
Constructors
| PreemptionBound Int |
Instances
Restrict the maximum difference between the number of yield or delay operations different threads have performed.
A fair bound of zero disables yields and delays entirely.
Since: 0.2.0.0
Instances
defaultBounds :: Bounds Source #
All bounds enabled, using their default values.
There is no default length bound, so set one if your computation may not terminate!
Since: 1.8.0.0
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
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
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
Length bounding
Length bounding can be used to test potentially nonterminating computations. Any execution exceeding the length bound gets discarded.
While PreemptionBound and FairBound are only used by
systematically, all Ways use the length bound.
newtype LengthBound Source #
Restrict the maximum length (in terms of primitive actions) of an execution.
A length bound of zero immediately aborts the execution.
Since: 0.2.0.0
Constructors
| LengthBound Int |
Instances
llengthBound :: Lens' (Settings n a) (Maybe LengthBound) Source #
A lens into the length bound.
Since: 2.0.0.0
The MemType
When executed on a multi-core processor some IORef / 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 IORefs
containing False, and forks two threads. Each thread writes
True to one of the IORefs and reads the other. The value that
each thread reads is communicated back through an MVar:
>>> :{
let relaxed = do
r1 <- newIORef False
r2 <- newIORef False
x <- spawn $ writeIORef r1 True >> readIORef r2
y <- spawn $ writeIORef r2 True >> readIORef 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---
FalseIt's possible for both threads to read the value False, even
though each writes True to the other IORef 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 IORef 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 IORef 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 |
Instances
| Bounded MemType Source # | |
| Enum MemType Source # | |
| Eq MemType Source # | |
| Ord MemType Source # | |
| Read MemType Source # | |
| Show MemType Source # | |
| Generic MemType Source # | |
| NFData MemType Source # | Since: 0.5.1.0 |
Defined in Test.DejaFu.Types | |
| type Rep MemType Source # | Since: 1.3.1.0 |
Defined in Test.DejaFu.Types type Rep MemType = D1 (MetaData "MemType" "Test.DejaFu.Types" "dejafu-2.3.0.0-CH3NTXDh8GWHZYQQRWnPX9" False) (C1 (MetaCons "SequentialConsistency" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "TotalStoreOrder" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "PartialStoreOrder" PrefixI False) (U1 :: Type -> Type))) | |
defaultMemType :: MemType Source #
The default memory model: TotalStoreOrder
Since: 0.2.0.0
Discard functions
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 Condition a -> Maybe
Discard, can selectively discard results or execution traces
before the schedule exploration finishes, allowing them to be
garbage collected sooner.
Note: The predicates and helper functions in Test.DejaFu come with discard functions built in, to discard results and traces wherever possible.
An Either Condition 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
| Bounded Discard Source # | |
| Enum Discard Source # | |
| Eq Discard Source # | |
| Ord Discard Source # | |
| Read Discard Source # | |
| Show Discard Source # | |
| Generic Discard Source # | |
| NFData Discard Source # | |
Defined in Test.DejaFu.Types | |
| type Rep Discard Source # | Since: 1.3.1.0 |
ldiscard :: Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard)) Source #
A lens into the discard function.
Since: 1.2.0.0
Early exit
Sometimes we don't want to wait for all executions to be
explored, we just want to stop as soon as a particular result is
found. An early-exit predicate, which has type Either Condition
a -> Bool, can opt to halt execution when such a result is
found.
All results found up to, and including, the one which terminates the exploration are reported.
Usage in combination with a discard function: A discard
function can be used in combination with early-exit. As usual,
results or traces will be discarded as appropriate. If a single
result causes the early-exit function to return True and the
discard function to return Just DiscardResultAndTrace, the
exploration will end early, but the result will not be included
in the output.
learlyExit :: Lens' (Settings n a) (Maybe (Either Condition a -> Bool)) Source #
A lens into the early-exit predicate.
Since: 1.2.0.0
Representative traces
There may be many different execution traces which give rise to the same result, but some traces can be more complex than others.
By supplying an equality predicate on results, all but the simplest trace for each distinct result can be thrown away.
Slippage: Just comparing results can lead to different errors
which happen to have the same result comparing as equal. For
example, all deadlocks have the same result (Left Deadlock),
but may have different causes. See issue #241.
lequality :: Lens' (Settings n a) (Maybe (a -> a -> Bool)) Source #
A lens into the equality predicate.
Since: 1.3.2.0
Trace simplification
There may be many ways to reveal the same bug, and dejafu is not guaranteed to find the simplest way first. This is particularly problematic with random testing, where the schedules generated tend to involve a lot of context switching. Simplification produces smaller traces, which still have the same essential behaviour.
Performance: Simplification in dejafu, unlike shrinking in most random testing tools, is quite cheap. Simplification is guaranteed to preserve semantics, so the test case does not need to be re-run repeatedly during the simplification process. The test case is re-run only once, after the process completes, for implementation reasons.
Concurrency tests can be rather large, however. So
simplification is disabled by default, and it is highly
recommended to also use lequality, to reduce the number of
traces to simplify.
Safe IO
Normally, dejafu has to assume any IO action can influence any other IO action, as there is no way to peek inside them. However, this adds considerable overhead to systematic testing. A perfectly legitimate use of IO is in managing thread-local state, such as a PRNG; in this case, there is no point in exploring interleavings of IO actions from other threads.
Warning: Enabling this option is unsound if your IO is not thread safe!
Abort conditions
Occasionally in an execution dejafu will discover that no
available scheduling decisions are within the specified bounds,
and aborts the execution to move onto the next. This is
signalled by an Abort condition. By default, abort conditions
are not returned from the SCT functions.
lshowAborts :: Lens' (Settings n a) Bool Source #
A lens into the show-aborts flag.
Since: 1.12.0.0
Debug output
You can opt to receive debugging messages by setting debugging print and show functions. Enabling debugging doesn't change any behaviour, it just causes messages to be printed. These options are most likely not useful for anyone not developing dejafu.
ldebugShow :: Lens' (Settings n a) (Maybe (a -> String)) Source #
A lens into the debug show function.
Since: 1.2.0.0
ldebugPrint :: Lens' (Settings n a) (Maybe (String -> n ())) Source #
A lens into the debug print function.
Since: 1.2.0.0
The debugging output includes both recoverable errors and informative messages. Those recoverable errors can be made fatal instead.
ldebugFatal :: Lens' (Settings n a) Bool Source #
A lens into the make-recoverable-errors-fatal flag.
Since: 1.3.2.0