| 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.
- 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
- newtype LengthBound = LengthBound Int
- defaultBounds :: Bounds
- defaultPreemptionBound :: PreemptionBound
- defaultFairBound :: FairBound
- defaultLengthBound :: LengthBound
- noBounds :: Bounds
- data MemType
- defaultMemType :: MemType
- lmemtype :: Lens' (Settings n a) MemType
- data Discard
- ldiscard :: Lens' (Settings n a) (Maybe (Either Failure a -> Maybe Discard))
- learlyExit :: Lens' (Settings n a) (Maybe (Either Failure a -> Bool))
- lequality :: Lens' (Settings n a) (Maybe (a -> a -> Bool))
- lsimplify :: 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
- swarmy :: RandomGen g => g -> Int -> Int -> Way
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 bounds
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: 0.2.0.0
Constructors
| Bounds | |
Fields | |
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
| Enum PreemptionBound Source # | |
| Eq PreemptionBound Source # | |
| Integral PreemptionBound Source # | |
| Num PreemptionBound Source # | |
| Ord PreemptionBound Source # | |
| Read PreemptionBound Source # | |
| Real PreemptionBound Source # | |
| Show PreemptionBound Source # | |
| Generic PreemptionBound Source # | Since: 1.3.1.0 |
| NFData PreemptionBound Source # | Since: 0.5.1.0 |
| type Rep PreemptionBound Source # | |
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
| Enum FairBound Source # | |
| Eq FairBound Source # | |
| Integral FairBound Source # | |
| Num FairBound Source # | |
| Ord FairBound Source # | |
| Read FairBound Source # | |
| Real FairBound Source # | |
| Show FairBound Source # | |
| Generic FairBound Source # | Since: 1.3.1.0 |
| NFData FairBound Source # | Since: 0.5.1.0 |
| type Rep FairBound Source # | |
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
| Enum LengthBound Source # | |
| Eq LengthBound Source # | |
| Integral LengthBound Source # | |
| Num LengthBound Source # | |
| Ord LengthBound Source # | |
| Read LengthBound Source # | |
| Real LengthBound Source # | |
| Show LengthBound Source # | |
| Generic LengthBound Source # | Since: 1.3.1.0 |
| NFData LengthBound Source # | Since: 0.5.1.0 |
| type Rep LengthBound Source # | |
defaultBounds :: Bounds Source #
All bounds enabled, using their default values.
Since: 0.2.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
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
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
The MemType
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:
>>> :{
let 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---
FalseIt'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 |
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 Failure 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 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. |
ldiscard :: Lens' (Settings n a) (Maybe (Either Failure 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 Failure 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 Failure 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.
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
Lens helpers
Deprecated
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 |
Deprecated: Use randomly instead. If you have a case where swarmy works better, please comment on issue #237.
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