-- |
-- Module      : Test.DejaFu.Conc
-- Copyright   : (c) 2016--2019 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : portable
--
-- Deterministic traced execution of concurrent computations.
--
-- This works by executing the computation on a single thread, calling
-- out to the supplied scheduler after each step to determine which
-- thread runs next.
module Test.DejaFu.Conc
  ( -- * Expressing concurrent programs
    Program
  , Basic
  , ConcT
  , ConcIO

  -- ** Setup and teardown
  , WithSetup
  , WithSetupAndTeardown
  , withSetup
  , withTeardown
  , withSetupAndTeardown

  -- ** Invariants
  , Invariant
  , registerInvariant
  , inspectIORef
  , inspectMVar
  , inspectTVar

  -- * Executing concurrent programs
  , Snapshot
  , MemType(..)
  , runConcurrent
  , recordSnapshot
  , runSnapshot

  -- ** Scheduling
  , module Test.DejaFu.Schedule

  -- * Results
  , Condition(..)
  , Trace
  , Decision(..)
  , ThreadId(..)
  , ThreadAction(..)
  , Lookahead(..)
  , MVarId
  , IORefId
  , MaskingState(..)
  , showTrace
  , showCondition
  ) where

import           Control.Exception                 (MaskingState(..))
import           Control.Monad                     (void)

import           Test.DejaFu.Conc.Internal.Common
import           Test.DejaFu.Conc.Internal.Program
import           Test.DejaFu.Conc.Internal.STM     (ModelTVar)
import           Test.DejaFu.Schedule
import           Test.DejaFu.Types
import           Test.DejaFu.Utils

-------------------------------------------------------------------------------
-- Expressing concurrent programs

-- | @since 1.4.0.0
type ConcT = Program Basic

-- | A 'MonadConc' implementation using @IO@.
--
-- @since 0.4.0.0
type ConcIO = ConcT IO

-------------------------------------------------------------------------------
-- Setup & teardown

-- | A concurrent program with some set-up action.
--
-- In terms of results, this is the same as @setup >>= program@.
-- However, the setup action will be __snapshotted__ (see
-- 'recordSnapshot' and 'runSnapshot') by the testing functions.  This
-- means that even if dejafu runs this program many many times, the
-- setup action will only be run the first time, and its effects
-- remembered for subsequent executions.
--
-- @since 2.0.0.0
withSetup
  :: Program Basic n x
  -- ^ Setup action
  -> (x -> Program Basic n a)
  -- ^ Main program
  -> Program (WithSetup x) n a
withSetup :: forall (n :: * -> *) x a.
Program Basic n x
-> (x -> Program Basic n a) -> Program (WithSetup x) n a
withSetup Program Basic n x
setup x -> Program Basic n a
p = WithSetup
  { wsSetup :: Program Basic n x
wsSetup   = Program Basic n x
setup
  , wsProgram :: x -> Program Basic n a
wsProgram = x -> Program Basic n a
p
  }

-- | A concurrent program with some set-up and teardown actions.
--
-- This is similar to
--
-- @
-- do
--   x <- setup
--   y <- program x
--   teardown x y
-- @
--
-- But with two differences:
--
--   * The setup action can be __snapshotted__, as described for
--     'withSetup'
--
--   * The teardown action will be executed even if the main action
--     fails to produce a value.
--
-- @since 2.0.0.0
withTeardown
  :: (x -> Either Condition y -> Program Basic n a)
  -- ^ Teardown action
  -> Program (WithSetup x) n y
  -- ^ Main program
  -> Program (WithSetupAndTeardown x y) n a
withTeardown :: forall x y (n :: * -> *) a.
(x -> Either Condition y -> Program Basic n a)
-> Program (WithSetup x) n y
-> Program (WithSetupAndTeardown x y) n a
withTeardown x -> Either Condition y -> Program Basic n a
teardown Program (WithSetup x) n y
ws = WithSetupAndTeardown
  { wstSetup :: ModelConc n x
wstSetup    = Program (WithSetup x) n y -> ModelConc n x
forall (n :: * -> *) x a.
Program (WithSetup x) n a -> ModelConc n x
wsSetup Program (WithSetup x) n y
ws
  , wstProgram :: x -> ModelConc n y
wstProgram  = Program (WithSetup x) n y -> x -> ModelConc n y
forall (n :: * -> *) x a.
Program (WithSetup x) n a -> x -> ModelConc n a
wsProgram Program (WithSetup x) n y
ws
  , wstTeardown :: x -> Either Condition y -> Program Basic n a
wstTeardown = x -> Either Condition y -> Program Basic n a
teardown
  }

-- | A combination of 'withSetup' and 'withTeardown' for convenience.
--
-- @
-- withSetupAndTeardown setup teardown =
--   withTeardown teardown . withSetup setup
-- @
--
-- @since 2.0.0.0
withSetupAndTeardown
  :: Program Basic n x
  -- ^ Setup action
  -> (x -> Either Condition y -> Program Basic n a)
  -- ^ Teardown action
  -> (x -> Program Basic n y)
  -- ^ Main program
  -> Program (WithSetupAndTeardown x y) n a
withSetupAndTeardown :: forall (n :: * -> *) x y a.
Program Basic n x
-> (x -> Either Condition y -> Program Basic n a)
-> (x -> Program Basic n y)
-> Program (WithSetupAndTeardown x y) n a
withSetupAndTeardown Program Basic n x
setup x -> Either Condition y -> Program Basic n a
teardown =
  (x -> Either Condition y -> Program Basic n a)
-> Program (WithSetup x) n y
-> Program (WithSetupAndTeardown x y) n a
forall x y (n :: * -> *) a.
(x -> Either Condition y -> Program Basic n a)
-> Program (WithSetup x) n y
-> Program (WithSetupAndTeardown x y) n a
withTeardown x -> Either Condition y -> Program Basic n a
teardown (Program (WithSetup x) n y
 -> Program (WithSetupAndTeardown x y) n a)
-> ((x -> Program Basic n y) -> Program (WithSetup x) n y)
-> (x -> Program Basic n y)
-> Program (WithSetupAndTeardown x y) n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Program Basic n x
-> (x -> Program Basic n y) -> Program (WithSetup x) n y
forall (n :: * -> *) x a.
Program Basic n x
-> (x -> Program Basic n a) -> Program (WithSetup x) n a
withSetup Program Basic n x
setup

-------------------------------------------------------------------------------
-- Invariants

-- | Call this in the setup phase to register new invariant which will
-- be checked after every scheduling point in the main phase.
-- Invariants are atomic actions which can inspect the shared state of
-- your computation.
--
-- If the invariant throws an exception, the execution will be aborted
-- with n @InvariantFailure@.  Any teardown action will still be run.
--
-- @since 2.0.0.0
registerInvariant :: Invariant n a -> Program Basic n ()
registerInvariant :: forall (n :: * -> *) a. Invariant n a -> Program Basic n ()
registerInvariant Invariant n a
inv = ((() -> Action n) -> Action n) -> Program Basic n ()
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> Invariant n () -> Action n -> Action n
forall (n :: * -> *). Invariant n () -> Action n -> Action n
ANewInvariant (Invariant n a -> Invariant n ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Invariant n a
inv) (() -> Action n
c ()))

-- | Read the content of an @IORef@.
--
-- This returns the globally visible value, which may not be the same
-- as the value visible to any particular thread when using a memory
-- model other than 'SequentialConsistency'.
--
-- @since 2.0.0.0
inspectIORef :: ModelIORef n a -> Invariant n a
inspectIORef :: forall (n :: * -> *) a. ModelIORef n a -> Invariant n a
inspectIORef = ((a -> IAction n) -> IAction n) -> Invariant n a
forall (n :: * -> *) a.
((a -> IAction n) -> IAction n) -> Invariant n a
Invariant (((a -> IAction n) -> IAction n) -> Invariant n a)
-> (ModelIORef n a -> (a -> IAction n) -> IAction n)
-> ModelIORef n a
-> Invariant n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelIORef n a -> (a -> IAction n) -> IAction n
forall (n :: * -> *) a.
ModelIORef n a -> (a -> IAction n) -> IAction n
IInspectIORef

-- | Read the content of an @MVar@.
--
-- This is essentially @tryReadMVar@.
--
-- @since 2.0.0.0
inspectMVar :: ModelMVar n a -> Invariant n (Maybe a)
inspectMVar :: forall (n :: * -> *) a. ModelMVar n a -> Invariant n (Maybe a)
inspectMVar = ((Maybe a -> IAction n) -> IAction n) -> Invariant n (Maybe a)
forall (n :: * -> *) a.
((a -> IAction n) -> IAction n) -> Invariant n a
Invariant (((Maybe a -> IAction n) -> IAction n) -> Invariant n (Maybe a))
-> (ModelMVar n a -> (Maybe a -> IAction n) -> IAction n)
-> ModelMVar n a
-> Invariant n (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelMVar n a -> (Maybe a -> IAction n) -> IAction n
forall (n :: * -> *) a.
ModelMVar n a -> (Maybe a -> IAction n) -> IAction n
IInspectMVar

-- | Read the content of a @TVar@.
--
-- This is essentially @readTVar@.
--
-- @since 2.0.0.0
inspectTVar :: ModelTVar n a -> Invariant n a
inspectTVar :: forall (n :: * -> *) a. ModelTVar n a -> Invariant n a
inspectTVar = ((a -> IAction n) -> IAction n) -> Invariant n a
forall (n :: * -> *) a.
((a -> IAction n) -> IAction n) -> Invariant n a
Invariant (((a -> IAction n) -> IAction n) -> Invariant n a)
-> (ModelTVar n a -> (a -> IAction n) -> IAction n)
-> ModelTVar n a
-> Invariant n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelTVar n a -> (a -> IAction n) -> IAction n
forall (n :: * -> *) a.
ModelTVar n a -> (a -> IAction n) -> IAction n
IInspectTVar