{-# LANGUAGE RankNTypes #-}

-- |
-- Module      : Test.DejaFu.Settings
-- Copyright   : (c) 2018 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : RankNTypes
--
-- Configuration for the SCT functions.
module Test.DejaFu.Settings
  ( -- * SCT configuration
    Settings
  , defaultSettings
  , fromWayAndMemType

  -- ** The @Way@
  , Way
  , defaultWay
  , lway
  , systematically
  , randomly
  , uniformly

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

  , Bounds(..)
  , PreemptionBound(..)
  , FairBound(..)
  , defaultBounds
  , defaultPreemptionBound
  , defaultFairBound
  , noBounds

  -- *** 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 'Way's use the length bound.

  , LengthBound(..)
  , llengthBound

  -- ** 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 @IORef@s
  -- containing @False@, and forks two threads.  Each thread writes
  -- @True@ to one of the @IORef@s 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.

  , MemType(..)
  , defaultMemType
  , lmemtype

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

  , Discard(..)
  , ldiscard

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

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

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

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

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

  -- ** 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
  , ldebugPrint

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

  , ldebugFatal

  -- * Lens helpers
  , get
  , set
  ) where

import           Control.Applicative   (Const(..))
import           Data.Functor.Identity (Identity(..))
import           System.Random         (RandomGen, randomR)

import           Test.DejaFu.Internal  (Settings(..), Way(..))
import           Test.DejaFu.Types

-------------------------------------------------------------------------------
-- SCT configuration

-- | Default SCT settings: just combine all the other defaults.
--
-- @since 1.2.0.0
defaultSettings :: Applicative n => Settings n a
defaultSettings :: forall (n :: * -> *) a. Applicative n => Settings n a
defaultSettings = forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
defaultWay MemType
defaultMemType

-- | Construct a 'Settings' record from a 'Way' and a 'MemType'.
--
-- All other settings take on their default values.
--
-- @since 1.2.0.0
fromWayAndMemType :: Applicative n => Way -> MemType -> Settings n a
fromWayAndMemType :: forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way MemType
memtype = Settings
  { _way :: Way
_way = Way
way
  , _lengthBound :: Maybe LengthBound
_lengthBound = forall a. Maybe a
Nothing
  , _memtype :: MemType
_memtype = MemType
memtype
  , _discard :: Maybe (Either Condition a -> Maybe Discard)
_discard = forall a. Maybe a
Nothing
  , _debugShow :: Maybe (a -> String)
_debugShow = forall a. Maybe a
Nothing
  , _debugPrint :: Maybe (String -> n ())
_debugPrint = forall a. Maybe a
Nothing
  , _debugFatal :: Bool
_debugFatal = Bool
False
  , _earlyExit :: Maybe (Either Condition a -> Bool)
_earlyExit = forall a. Maybe a
Nothing
  , _equality :: Maybe (a -> a -> Bool)
_equality = forall a. Maybe a
Nothing
  , _simplify :: Bool
_simplify = Bool
False
  , _safeIO :: Bool
_safeIO = Bool
False
  , _showAborts :: Bool
_showAborts = Bool
False
  }

-------------------------------------------------------------------------------
-- The @Way@

-- | A default way to execute concurrent programs: systematically
-- using 'defaultBounds'.
--
-- @since 0.6.0.0
defaultWay :: Way
defaultWay :: Way
defaultWay = Bounds -> Way
systematically Bounds
defaultBounds

-- | A lens into the 'Way'.
--
-- @since 1.2.0.0
lway :: Lens' (Settings n a) Way
lway :: forall (n :: * -> *) a. Lens' (Settings n a) Way
lway Way -> f Way
afb Settings n a
s = (\Way
b -> Settings n a
s {_way :: Way
_way = Way
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Way -> f Way
afb (forall (n :: * -> *) a. Settings n a -> Way
_way Settings n a
s)

-- | Systematically execute a program, trying all distinct executions
-- within the bounds.
--
-- @since 0.7.0.0
systematically
  :: Bounds
  -- ^ The bounds to constrain the exploration.
  -> Way
systematically :: Bounds -> Way
systematically = Bounds -> Way
Systematic

-- | 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
randomly :: RandomGen g
  => g
  -- ^ The random generator to drive the scheduling.
  -> Int
  -- ^ The number of executions to try.
  -> Way
randomly :: forall g. RandomGen g => g -> Int -> Way
randomly = forall g. RandomGen g => (g -> (Int, g)) -> g -> Int -> Way
Randomly forall a b. (a -> b) -> a -> b
$ forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Int
1, Int
50)

-- | 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
uniformly :: RandomGen g
  => g
  -- ^ The random generator to drive the scheduling.
  -> Int
  -- ^ The number of executions to try.
  -> Way
uniformly :: forall g. RandomGen g => g -> Int -> Way
uniformly = forall g. RandomGen g => (g -> (Int, g)) -> g -> Int -> Way
Randomly forall a b. (a -> b) -> a -> b
$ \g
g -> (Int
1, g
g)

-------------------------------------------------------------------------------
-- Schedule bounding

-- | 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
defaultBounds :: Bounds
defaultBounds :: Bounds
defaultBounds = Bounds
  { boundPreemp :: Maybe PreemptionBound
boundPreemp = forall a. a -> Maybe a
Just PreemptionBound
defaultPreemptionBound
  , boundFair :: Maybe FairBound
boundFair   = forall a. a -> Maybe a
Just FairBound
defaultFairBound
  }

-- | 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
defaultPreemptionBound :: PreemptionBound
defaultPreemptionBound :: PreemptionBound
defaultPreemptionBound = PreemptionBound
2

-- | A sensible default fair bound: 5.
--
-- This comes from playing around myself, but there is probably a
-- better default.
--
-- @since 0.2.0.0
defaultFairBound :: FairBound
defaultFairBound :: FairBound
defaultFairBound = FairBound
5

-- | 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
noBounds :: Bounds
noBounds :: Bounds
noBounds = Bounds
  { boundPreemp :: Maybe PreemptionBound
boundPreemp = forall a. Maybe a
Nothing
  , boundFair :: Maybe FairBound
boundFair   = forall a. Maybe a
Nothing
  }

-------------------------------------------------------------------------------
-- Length bounding

-- | A lens into the length bound.
--
-- @since 2.0.0.0
llengthBound :: Lens' (Settings n a) (Maybe LengthBound)
llengthBound :: forall (n :: * -> *) a. Lens' (Settings n a) (Maybe LengthBound)
llengthBound Maybe LengthBound -> f (Maybe LengthBound)
afb Settings n a
s = (\Maybe LengthBound
b -> Settings n a
s {_lengthBound :: Maybe LengthBound
_lengthBound = Maybe LengthBound
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe LengthBound -> f (Maybe LengthBound)
afb (forall (n :: * -> *) a. Settings n a -> Maybe LengthBound
_lengthBound Settings n a
s)

-------------------------------------------------------------------------------
-- The @MemType@

-- | The default memory model: @TotalStoreOrder@
--
-- @since 0.2.0.0
defaultMemType :: MemType
defaultMemType :: MemType
defaultMemType = MemType
TotalStoreOrder

-- | A lens into the 'MemType'.
--
-- @since 1.2.0.0
lmemtype :: Lens' (Settings n a) MemType
lmemtype :: forall (n :: * -> *) a. Lens' (Settings n a) MemType
lmemtype MemType -> f MemType
afb Settings n a
s = (\MemType
b -> Settings n a
s {_memtype :: MemType
_memtype = MemType
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MemType -> f MemType
afb (forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
s)

-------------------------------------------------------------------------------
-- Discard functions

-- | A lens into the discard function.
--
-- @since 1.2.0.0
ldiscard :: Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
ldiscard :: forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
ldiscard Maybe (Either Condition a -> Maybe Discard)
-> f (Maybe (Either Condition a -> Maybe Discard))
afb Settings n a
s = (\Maybe (Either Condition a -> Maybe Discard)
b -> Settings n a
s {_discard :: Maybe (Either Condition a -> Maybe Discard)
_discard = Maybe (Either Condition a -> Maybe Discard)
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Either Condition a -> Maybe Discard)
-> f (Maybe (Either Condition a -> Maybe Discard))
afb (forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Maybe Discard)
_discard Settings n a
s)

-------------------------------------------------------------------------------
-- Early exit

-- | A lens into the early-exit predicate.
--
-- @since 1.2.0.0
learlyExit :: Lens' (Settings n a) (Maybe (Either Condition a -> Bool))
learlyExit :: forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (Either Condition a -> Bool))
learlyExit Maybe (Either Condition a -> Bool)
-> f (Maybe (Either Condition a -> Bool))
afb Settings n a
s = (\Maybe (Either Condition a -> Bool)
b -> Settings n a
s {_earlyExit :: Maybe (Either Condition a -> Bool)
_earlyExit = Maybe (Either Condition a -> Bool)
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Either Condition a -> Bool)
-> f (Maybe (Either Condition a -> Bool))
afb (forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Bool)
_earlyExit Settings n a
s)

-------------------------------------------------------------------------------
-- Representative traces

-- | A lens into the equality predicate.
--
-- @since 1.3.2.0
lequality :: Lens' (Settings n a) (Maybe (a -> a -> Bool))
lequality :: forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (a -> a -> Bool))
lequality Maybe (a -> a -> Bool) -> f (Maybe (a -> a -> Bool))
afb Settings n a
s = (\Maybe (a -> a -> Bool)
b -> Settings n a
s {_equality :: Maybe (a -> a -> Bool)
_equality = Maybe (a -> a -> Bool)
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (a -> a -> Bool) -> f (Maybe (a -> a -> Bool))
afb (forall (n :: * -> *) a. Settings n a -> Maybe (a -> a -> Bool)
_equality Settings n a
s)

-------------------------------------------------------------------------------
-- Simplification

-- | A lens into the simplify flag.
--
-- @since 1.3.2.0
lsimplify :: Lens' (Settings n a) Bool
lsimplify :: forall (n :: * -> *) a. Lens' (Settings n a) Bool
lsimplify Bool -> f Bool
afb Settings n a
s = (\Bool
b -> Settings n a
s {_simplify :: Bool
_simplify = Bool
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> f Bool
afb (forall (n :: * -> *) a. Settings n a -> Bool
_simplify Settings n a
s)

-------------------------------------------------------------------------------
-- Safe IO

-- | A lens into the safe IO flag.
--
-- @since 1.10.1.0
lsafeIO :: Lens' (Settings n a) Bool
lsafeIO :: forall (n :: * -> *) a. Lens' (Settings n a) Bool
lsafeIO Bool -> f Bool
afb Settings n a
s = (\Bool
b -> Settings n a
s {_safeIO :: Bool
_safeIO = Bool
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> f Bool
afb (forall (n :: * -> *) a. Settings n a -> Bool
_safeIO Settings n a
s)

-------------------------------------------------------------------------------
-- Abort conditions

-- | A lens into the show-aborts flag.
--
-- @since 1.12.0.0
lshowAborts :: Lens' (Settings n a) Bool
lshowAborts :: forall (n :: * -> *) a. Lens' (Settings n a) Bool
lshowAborts Bool -> f Bool
afb Settings n a
s = (\Bool
b -> Settings n a
s {_showAborts :: Bool
_showAborts = Bool
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> f Bool
afb (forall (n :: * -> *) a. Settings n a -> Bool
_showAborts Settings n a
s)

-------------------------------------------------------------------------------
-- Debug output

-- | A lens into the debug 'show' function.
--
-- @since 1.2.0.0
ldebugShow :: Lens' (Settings n a) (Maybe (a -> String))
ldebugShow :: forall (n :: * -> *) a. Lens' (Settings n a) (Maybe (a -> String))
ldebugShow Maybe (a -> String) -> f (Maybe (a -> String))
afb Settings n a
s = (\Maybe (a -> String)
b -> Settings n a
s {_debugShow :: Maybe (a -> String)
_debugShow = Maybe (a -> String)
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (a -> String) -> f (Maybe (a -> String))
afb (forall (n :: * -> *) a. Settings n a -> Maybe (a -> String)
_debugShow Settings n a
s)

-- | A lens into the debug 'print' function.
--
-- @since 1.2.0.0
ldebugPrint :: Lens' (Settings n a) (Maybe (String -> n ()))
ldebugPrint :: forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (String -> n ()))
ldebugPrint Maybe (String -> n ()) -> f (Maybe (String -> n ()))
afb Settings n a
s = (\Maybe (String -> n ())
b -> Settings n a
s {_debugPrint :: Maybe (String -> n ())
_debugPrint = Maybe (String -> n ())
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (String -> n ()) -> f (Maybe (String -> n ()))
afb (forall (n :: * -> *) a. Settings n a -> Maybe (String -> n ())
_debugPrint Settings n a
s)

-- | A lens into the make-recoverable-errors-fatal flag.
--
-- @since 1.3.2.0
ldebugFatal :: Lens' (Settings n a) Bool
ldebugFatal :: forall (n :: * -> *) a. Lens' (Settings n a) Bool
ldebugFatal Bool -> f Bool
afb Settings n a
s = (\Bool
b -> Settings n a
s {_debugFatal :: Bool
_debugFatal = Bool
b}) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> f Bool
afb (forall (n :: * -> *) a. Settings n a -> Bool
_debugFatal Settings n a
s)

-------------------------------------------------------------------------------
-- Lens helpers

-- lens type synonyms, unexported
type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
type Lens' s a = Lens s s a a

-- | Get a value from a lens.
--
-- @since 1.2.0.0
get :: Lens' s a -> s -> a
get :: forall s a. Lens' s a -> s -> a
get Lens' s a
lens = forall {k} a (b :: k). Const a b -> a
getConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' s a
lens forall {k} a (b :: k). a -> Const a b
Const

-- | Set a value in a lens.
--
-- @since 1.2.0.0
set :: Lens' s a -> a -> s -> s
set :: forall s a. Lens' s a -> a -> s -> s
set Lens' s a
lens a
a = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' s a
lens (\a
_ -> forall a. a -> Identity a
Identity a
a)