dejafu-1.4.0.0: A library for unit-testing concurrent programs.

Copyright(c) 2018 Michael Walker
LicenseMIT
MaintainerMichael Walker <mike@barrucadu.co.uk>
Stabilityexperimental
PortabilityRankNTypes
Safe HaskellNone
LanguageHaskell2010

Test.DejaFu.Settings

Contents

Description

Configuration for the SCT functions.

Synopsis

SCT configuration

data Settings n a Source #

SCT configuration record.

Since: 1.2.0.0

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 #

Construct a Settings record from a Way and a MemType.

All other settings take on their default values.

Since: 1.2.0.0

The Way

data Way Source #

How to explore the possible executions of a concurrent program.

Since: 0.7.0.0

Instances

Show Way Source # 

Methods

showsPrec :: Int -> Way -> ShowS #

show :: Way -> String #

showList :: [Way] -> ShowS #

defaultWay :: Way Source #

A default way to execute concurrent programs: systematically using defaultBounds.

Since: 0.6.0.0

lway :: Lens' (Settings n a) Way Source #

A lens into the Way.

Since: 1.2.0.0

systematically Source #

Arguments

:: Bounds

The bounds to constrain the exploration.

-> Way 

Systematically execute a program, trying all distinct executions within the bounds.

Since: 0.7.0.0

randomly Source #

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

uniformly Source #

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

data Bounds Source #

Since: 0.2.0.0

Instances

Eq Bounds Source # 

Methods

(==) :: Bounds -> Bounds -> Bool #

(/=) :: Bounds -> Bounds -> Bool #

Ord Bounds Source # 
Read Bounds Source # 
Show Bounds Source # 
Generic Bounds Source #

Since: 1.3.1.0

Associated Types

type Rep Bounds :: * -> * #

Methods

from :: Bounds -> Rep Bounds x #

to :: Rep Bounds x -> Bounds #

NFData Bounds Source #

Since: 0.5.1.0

Methods

rnf :: Bounds -> () #

type Rep Bounds Source # 

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

Methods

rnf :: PreemptionBound -> () #

type Rep PreemptionBound Source # 
type Rep PreemptionBound = D1 * (MetaData "PreemptionBound" "Test.DejaFu.Types" "dejafu-1.4.0.0-AFpoiFtiimYFdg7zahVYCS" True) (C1 * (MetaCons "PreemptionBound" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)))

newtype FairBound 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

Constructors

FairBound Int 

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

Associated Types

type Rep FairBound :: * -> * #

NFData FairBound Source #

Since: 0.5.1.0

Methods

rnf :: FairBound -> () #

type Rep FairBound Source # 
type Rep FairBound = D1 * (MetaData "FairBound" "Test.DejaFu.Types" "dejafu-1.4.0.0-AFpoiFtiimYFdg7zahVYCS" True) (C1 * (MetaCons "FairBound" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)))

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

Associated Types

type Rep LengthBound :: * -> * #

NFData LengthBound Source #

Since: 0.5.1.0

Methods

rnf :: LengthBound -> () #

type Rep LengthBound Source # 
type Rep LengthBound = D1 * (MetaData "LengthBound" "Test.DejaFu.Types" "dejafu-1.4.0.0-AFpoiFtiimYFdg7zahVYCS" True) (C1 * (MetaCons "LengthBound" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int)))

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

noBounds :: Bounds Source #

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

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.

data MemType Source #

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 CRef is written to, that write is immediately visible to all threads.

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 CRef 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 to different CRefs are not necessarily committed in the same order that they are created.

Instances

Bounded MemType Source # 
Enum MemType Source # 
Eq MemType Source # 

Methods

(==) :: MemType -> MemType -> Bool #

(/=) :: MemType -> MemType -> Bool #

Ord MemType Source # 
Read MemType Source # 
Show MemType Source # 
Generic MemType Source #

Since: 1.3.1.0

Associated Types

type Rep MemType :: * -> * #

Methods

from :: MemType -> Rep MemType x #

to :: Rep MemType x -> MemType #

NFData MemType Source #

Since: 0.5.1.0

Methods

rnf :: MemType -> () #

type Rep MemType Source # 
type Rep MemType = D1 * (MetaData "MemType" "Test.DejaFu.Types" "dejafu-1.4.0.0-AFpoiFtiimYFdg7zahVYCS" False) ((:+:) * (C1 * (MetaCons "SequentialConsistency" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "TotalStoreOrder" PrefixI False) (U1 *)) (C1 * (MetaCons "PartialStoreOrder" PrefixI False) (U1 *))))

defaultMemType :: MemType Source #

The default memory model: TotalStoreOrder

Since: 0.2.0.0

lmemtype :: Lens' (Settings n a) MemType Source #

A lens into the MemType.

Since: 1.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.

data Discard Source #

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.

Instances

Bounded Discard Source # 
Enum Discard Source # 
Eq Discard Source # 

Methods

(==) :: Discard -> Discard -> Bool #

(/=) :: Discard -> Discard -> Bool #

Ord Discard Source # 
Read Discard Source # 
Show Discard Source # 
Generic Discard Source #

Since: 1.3.1.0

Associated Types

type Rep Discard :: * -> * #

Methods

from :: Discard -> Rep Discard x #

to :: Rep Discard x -> Discard #

NFData Discard Source # 

Methods

rnf :: Discard -> () #

type Rep Discard Source # 
type Rep Discard = D1 * (MetaData "Discard" "Test.DejaFu.Types" "dejafu-1.4.0.0-AFpoiFtiimYFdg7zahVYCS" False) ((:+:) * (C1 * (MetaCons "DiscardTrace" PrefixI False) (U1 *)) (C1 * (MetaCons "DiscardResultAndTrace" PrefixI False) (U1 *)))

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.

lsimplify :: Lens' (Settings n a) Bool Source #

A lens into the simplify flag.

Since: 1.3.2.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

Lens helpers

get :: Lens' s a -> s -> a Source #

Get a value from a lens.

Since: 1.2.0.0

set :: Lens' s a -> a -> s -> s Source #

Set a value in a lens.

Since: 1.2.0.0

Deprecated

swarmy Source #

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