{-# 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 = fromWayAndMemType defaultWay 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 way memtype = Settings
  { _way = way
  , _lengthBound = Nothing
  , _memtype = memtype
  , _discard = Nothing
  , _debugShow = Nothing
  , _debugPrint = Nothing
  , _debugFatal = False
  , _earlyExit = Nothing
  , _equality = Nothing
  , _simplify = False
  , _safeIO = False
  , _showAborts = False
  }

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

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

-- | A lens into the 'Way'.
--
-- @since 1.2.0.0
lway :: Lens' (Settings n a) Way
lway afb s = (\b -> s {_way = b}) <$> afb (_way 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 = 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 = Randomly $ randomR (1, 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 = Randomly $ \g -> (1, 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
  { boundPreemp = Just defaultPreemptionBound
  , boundFair   = Just 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 = 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 = 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
  { boundPreemp = Nothing
  , boundFair   = Nothing
  }

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

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

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

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

-- | A lens into the 'MemType'.
--
-- @since 1.2.0.0
lmemtype :: Lens' (Settings n a) MemType
lmemtype afb s = (\b -> s {_memtype = b}) <$> afb (_memtype 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 afb s = (\b -> s {_discard = b}) <$> afb (_discard 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 afb s = (\b -> s {_earlyExit = b}) <$> afb (_earlyExit s)

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

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

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

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

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

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

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

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

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

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

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

-- | A lens into the make-recoverable-errors-fatal flag.
--
-- @since 1.3.2.0
ldebugFatal :: Lens' (Settings n a) Bool
ldebugFatal afb s = (\b -> s {_debugFatal = b}) <$> afb (_debugFatal 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 lens = getConst . lens Const

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