Configuration for the SCT functions.

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 suggests 2 is 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.

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.

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---
False

It'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.

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.

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.

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.

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.

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!

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.

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.

The debugging output includes both recoverable errors and informative messages. Those recoverable errors can be made fatal instead.