dejafu-2.4.0.5: A library for unit-testing concurrent programs.
Copyright(c) 2018 Michael Walker
LicenseMIT
MaintainerMichael Walker <mike@barrucadu.co.uk>
Stabilityexperimental
PortabilityRankNTypes
Safe HaskellSafe-Inferred
LanguageHaskell2010

Test.DejaFu.Settings

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

Instances details
Show Way Source # 
Instance details

Defined in Test.DejaFu.Internal

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 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 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: 2.0.0.0

Instances

Instances details
Generic Bounds Source # 
Instance details

Defined in Test.DejaFu.Types

Associated Types

type Rep Bounds :: Type -> Type #

Methods

from :: Bounds -> Rep Bounds x #

to :: Rep Bounds x -> Bounds #

Read Bounds Source # 
Instance details

Defined in Test.DejaFu.Types

Show Bounds Source # 
Instance details

Defined in Test.DejaFu.Types

NFData Bounds Source # 
Instance details

Defined in Test.DejaFu.Types

Methods

rnf :: Bounds -> () #

Eq Bounds Source # 
Instance details

Defined in Test.DejaFu.Types

Methods

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

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

Ord Bounds Source # 
Instance details

Defined in Test.DejaFu.Types

type Rep Bounds Source # 
Instance details

Defined in Test.DejaFu.Types

type Rep Bounds = D1 ('MetaData "Bounds" "Test.DejaFu.Types" "dejafu-2.4.0.5-G4EEj1kXZBX5wEYbPUnAst" '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

Instances details
Enum PreemptionBound Source # 
Instance details

Defined in Test.DejaFu.Types

Generic PreemptionBound Source # 
Instance details

Defined in Test.DejaFu.Types

Associated Types

type Rep PreemptionBound :: Type -> Type #

Num PreemptionBound Source # 
Instance details

Defined in Test.DejaFu.Types

Read PreemptionBound Source # 
Instance details

Defined in Test.DejaFu.Types

Integral PreemptionBound Source # 
Instance details

Defined in Test.DejaFu.Types

Real PreemptionBound Source # 
Instance details

Defined in Test.DejaFu.Types

Show PreemptionBound Source # 
Instance details

Defined in Test.DejaFu.Types

NFData PreemptionBound Source #

Since: 0.5.1.0

Instance details

Defined in Test.DejaFu.Types

Methods

rnf :: PreemptionBound -> () #

Eq PreemptionBound Source # 
Instance details

Defined in Test.DejaFu.Types

Ord PreemptionBound Source # 
Instance details

Defined in Test.DejaFu.Types

type Rep PreemptionBound Source #

Since: 1.3.1.0

Instance details

Defined in Test.DejaFu.Types

type Rep PreemptionBound = D1 ('MetaData "PreemptionBound" "Test.DejaFu.Types" "dejafu-2.4.0.5-G4EEj1kXZBX5wEYbPUnAst" 'True) (C1 ('MetaCons "PreemptionBound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe 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

Instances details
Enum FairBound Source # 
Instance details

Defined in Test.DejaFu.Types

Generic FairBound Source # 
Instance details

Defined in Test.DejaFu.Types

Associated Types

type Rep FairBound :: Type -> Type #

Num FairBound Source # 
Instance details

Defined in Test.DejaFu.Types

Read FairBound Source # 
Instance details

Defined in Test.DejaFu.Types

Integral FairBound Source # 
Instance details

Defined in Test.DejaFu.Types

Real FairBound Source # 
Instance details

Defined in Test.DejaFu.Types

Show FairBound Source # 
Instance details

Defined in Test.DejaFu.Types

NFData FairBound Source #

Since: 0.5.1.0

Instance details

Defined in Test.DejaFu.Types

Methods

rnf :: FairBound -> () #

Eq FairBound Source # 
Instance details

Defined in Test.DejaFu.Types

Ord FairBound Source # 
Instance details

Defined in Test.DejaFu.Types

type Rep FairBound Source #

Since: 1.3.1.0

Instance details

Defined in Test.DejaFu.Types

type Rep FairBound = D1 ('MetaData "FairBound" "Test.DejaFu.Types" "dejafu-2.4.0.5-G4EEj1kXZBX5wEYbPUnAst" 'True) (C1 ('MetaCons "FairBound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

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

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

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

Instances details
Enum LengthBound Source # 
Instance details

Defined in Test.DejaFu.Types

Generic LengthBound Source # 
Instance details

Defined in Test.DejaFu.Types

Associated Types

type Rep LengthBound :: Type -> Type #

Num LengthBound Source # 
Instance details

Defined in Test.DejaFu.Types

Read LengthBound Source # 
Instance details

Defined in Test.DejaFu.Types

Integral LengthBound Source # 
Instance details

Defined in Test.DejaFu.Types

Real LengthBound Source # 
Instance details

Defined in Test.DejaFu.Types

Show LengthBound Source # 
Instance details

Defined in Test.DejaFu.Types

NFData LengthBound Source #

Since: 0.5.1.0

Instance details

Defined in Test.DejaFu.Types

Methods

rnf :: LengthBound -> () #

Eq LengthBound Source # 
Instance details

Defined in Test.DejaFu.Types

Ord LengthBound Source # 
Instance details

Defined in Test.DejaFu.Types

type Rep LengthBound Source #

Since: 1.3.1.0

Instance details

Defined in Test.DejaFu.Types

type Rep LengthBound = D1 ('MetaData "LengthBound" "Test.DejaFu.Types" "dejafu-2.4.0.5-G4EEj1kXZBX5wEYbPUnAst" 'True) (C1 ('MetaCons "LengthBound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

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

data MemType Source #

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 IORef 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 IORef 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 IORefs are not necessarily committed in the same order that they are created.

Instances

Instances details
Bounded MemType Source # 
Instance details

Defined in Test.DejaFu.Types

Enum MemType Source # 
Instance details

Defined in Test.DejaFu.Types

Generic MemType Source # 
Instance details

Defined in Test.DejaFu.Types

Associated Types

type Rep MemType :: Type -> Type #

Methods

from :: MemType -> Rep MemType x #

to :: Rep MemType x -> MemType #

Read MemType Source # 
Instance details

Defined in Test.DejaFu.Types

Show MemType Source # 
Instance details

Defined in Test.DejaFu.Types

NFData MemType Source #

Since: 0.5.1.0

Instance details

Defined in Test.DejaFu.Types

Methods

rnf :: MemType -> () #

Eq MemType Source # 
Instance details

Defined in Test.DejaFu.Types

Methods

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

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

Ord MemType Source # 
Instance details

Defined in Test.DejaFu.Types

type Rep MemType Source #

Since: 1.3.1.0

Instance details

Defined in Test.DejaFu.Types

type Rep MemType = D1 ('MetaData "MemType" "Test.DejaFu.Types" "dejafu-2.4.0.5-G4EEj1kXZBX5wEYbPUnAst" '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

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

data Discard Source #

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

Instances details
Bounded Discard Source # 
Instance details

Defined in Test.DejaFu.Types

Enum Discard Source # 
Instance details

Defined in Test.DejaFu.Types

Generic Discard Source # 
Instance details

Defined in Test.DejaFu.Types

Associated Types

type Rep Discard :: Type -> Type #

Methods

from :: Discard -> Rep Discard x #

to :: Rep Discard x -> Discard #

Read Discard Source # 
Instance details

Defined in Test.DejaFu.Types

Show Discard Source # 
Instance details

Defined in Test.DejaFu.Types

NFData Discard Source # 
Instance details

Defined in Test.DejaFu.Types

Methods

rnf :: Discard -> () #

Eq Discard Source # 
Instance details

Defined in Test.DejaFu.Types

Methods

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

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

Ord Discard Source # 
Instance details

Defined in Test.DejaFu.Types

type Rep Discard Source #

Since: 1.3.1.0

Instance details

Defined in Test.DejaFu.Types

type Rep Discard = D1 ('MetaData "Discard" "Test.DejaFu.Types" "dejafu-2.4.0.5-G4EEj1kXZBX5wEYbPUnAst" 'False) (C1 ('MetaCons "DiscardTrace" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DiscardResultAndTrace" 'PrefixI 'False) (U1 :: Type -> Type))

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.

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

A lens into the simplify flag.

Since: 1.3.2.0

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!

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

A lens into the safe IO flag.

Since: 1.10.1.0

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

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