{-# OPTIONS_GHC -Wno-orphans #-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}

-- GHC doesn't need this to compile the module, but stylish-haskell
-- does to format it.
{-# LANGUAGE FlexibleContexts #-}

-- |
-- Module      : Test.DejaFu.Conc.Internal.Program
-- Copyright   : (c) 2019--2021 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : CPP, FlexibleContexts, FlexibleInstances, GADTs, LambdaCase, RecordWildCards, TypeFamilies
--
-- Representations of concurrent programs with setup, teardown, and
-- snapshotting.  This module is NOT considered to form part of the
-- public interface of this library.
--
-- This module defines orphan instances for the 'Program' type which
-- lives in "Test.DejaFu.Conc.Internal.Common", to avoid needing to
-- pull a bunch more stuff into that module.
module Test.DejaFu.Conc.Internal.Program where

import           Control.Applicative                 (Applicative(..))
import           Control.Exception                   (MaskingState(..))
import qualified Control.Monad.Catch                 as Ca
import qualified Control.Monad.IO.Class              as IO
import           Control.Monad.Trans.Class           (MonadTrans(..))
import qualified Data.Foldable                       as F
import           Data.List                           (partition)
import qualified Data.Map.Strict                     as M
import           Data.Maybe                          (isNothing)
import           GHC.Stack                           (HasCallStack)

import qualified Control.Monad.Conc.Class            as C
import           Test.DejaFu.Conc.Internal
import           Test.DejaFu.Conc.Internal.Common
import           Test.DejaFu.Conc.Internal.STM       (ModelSTM)
import           Test.DejaFu.Conc.Internal.Threading (Threads, _blocking)
import           Test.DejaFu.Internal
import           Test.DejaFu.Schedule
import           Test.DejaFu.Types

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

instance (pty ~ Basic, IO.MonadIO n) => IO.MonadIO (Program pty n) where
  liftIO :: forall a. IO a -> Program pty n a
liftIO IO a
ma = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\a -> Action n
c -> forall (n :: * -> *). n (Action n) -> Action n
ALift (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Action n
c (forall (m :: * -> *) a. MonadIO m => IO a -> m a
IO.liftIO IO a
ma)))

instance (pty ~ Basic) => MonadTrans (Program pty) where
  lift :: forall (m :: * -> *) a. Monad m => m a -> Program pty m a
lift m a
ma = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\a -> Action m
c -> forall (n :: * -> *). n (Action n) -> Action n
ALift (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Action m
c m a
ma))

instance (pty ~ Basic) =>  Ca.MonadCatch (Program pty n) where
  catch :: forall e a.
Exception e =>
Program pty n a -> (e -> Program pty n a) -> Program pty n a
catch Program pty n a
ma e -> Program pty n a
h = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a e.
Exception e =>
(e -> ModelConc n a)
-> ModelConc n a -> (a -> Action n) -> Action n
ACatching e -> Program pty n a
h Program pty n a
ma)

instance (pty ~ Basic) => Ca.MonadThrow (Program pty n) where
  throwM :: forall e a. Exception e => e -> Program pty n a
throwM e
e = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\a -> Action n
_ -> forall (n :: * -> *) e. Exception e => e -> Action n
AThrow e
e)

instance (pty ~ Basic) => Ca.MonadMask (Program pty n) where
  mask :: forall b.
((forall a. Program pty n a -> Program pty n a) -> Program pty n b)
-> Program pty n b
mask                (forall a. Program pty n a -> Program pty n a) -> Program pty n b
mb = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
MaskingState
-> ((forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a)
-> (a -> Action n)
-> Action n
AMasking MaskingState
MaskedInterruptible   (\forall b. ModelConc n b -> ModelConc n b
f -> (forall a. Program pty n a -> Program pty n a) -> Program pty n b
mb forall b. ModelConc n b -> ModelConc n b
f))
  uninterruptibleMask :: forall b.
((forall a. Program pty n a -> Program pty n a) -> Program pty n b)
-> Program pty n b
uninterruptibleMask (forall a. Program pty n a -> Program pty n a) -> Program pty n b
mb = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
MaskingState
-> ((forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a)
-> (a -> Action n)
-> Action n
AMasking MaskingState
MaskedUninterruptible (\forall b. ModelConc n b -> ModelConc n b
f -> (forall a. Program pty n a -> Program pty n a) -> Program pty n b
mb forall b. ModelConc n b -> ModelConc n b
f))

#if MIN_VERSION_exceptions(0,10,0)
  generalBracket :: forall a b c.
Program pty n a
-> (a -> ExitCase b -> Program pty n c)
-> (a -> Program pty n b)
-> Program pty n (b, c)
generalBracket Program pty n a
acquire a -> ExitCase b -> Program pty n c
release a -> Program pty n b
use = forall (m :: * -> *) b.
MonadMask m =>
((forall a. m a -> m a) -> m b) -> m b
Ca.mask forall a b. (a -> b) -> a -> b
$ \forall a. Program pty n a -> Program pty n a
unmasked -> do
    a
resource <- Program pty n a
acquire
    b
b <- forall a. Program pty n a -> Program pty n a
unmasked (a -> Program pty n b
use a
resource) forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`Ca.catch` (\SomeException
e -> a -> ExitCase b -> Program pty n c
release a
resource (forall a. SomeException -> ExitCase a
Ca.ExitCaseException SomeException
e) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
Ca.throwM SomeException
e)
    c
c <- a -> ExitCase b -> Program pty n c
release a
resource (forall a. a -> ExitCase a
Ca.ExitCaseSuccess b
b)
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (b
b, c
c)
#elif MIN_VERSION_exceptions(0,9,0)
  -- from https://github.com/fpco/stackage/issues/3315#issuecomment-368583481
  generalBracket acquire release cleanup use = Ca.mask $ \unmasked -> do
    resource <- acquire
    result <- unmasked (use resource) `Ca.catch` (\e -> cleanup resource e >> Ca.throwM e)
    _ <- release resource
    pure result
#endif

instance (pty ~ Basic, Monad n) => C.MonadConc (Program pty n) where
  type MVar     (Program pty n) = ModelMVar n
  type IORef    (Program pty n) = ModelIORef n
  type Ticket   (Program pty n) = ModelTicket
  type STM      (Program pty n) = ModelSTM n
  type ThreadId (Program pty n) = ThreadId

  -- ----------

  forkWithUnmaskN :: String
-> ((forall a. Program pty n a -> Program pty n a)
    -> Program pty n ())
-> Program pty n (ThreadId (Program pty n))
forkWithUnmaskN   String
n (forall a. Program pty n a -> Program pty n a) -> Program pty n ()
ma = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *).
String
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> (ThreadId -> Action n)
-> Action n
AFork String
n (\forall b. ModelConc n b -> ModelConc n b
umask -> forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()
ma forall b. ModelConc n b -> ModelConc n b
umask) (\()
_ -> forall (n :: * -> *). n () -> Action n
AStop (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()))))
  forkOnWithUnmaskN :: String
-> Int
-> ((forall a. Program pty n a -> Program pty n a)
    -> Program pty n ())
-> Program pty n (ThreadId (Program pty n))
forkOnWithUnmaskN String
n Int
_  = forall (m :: * -> *).
MonadConc m =>
String -> ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)
C.forkWithUnmaskN String
n
  forkOSWithUnmaskN :: String
-> ((forall a. Program pty n a -> Program pty n a)
    -> Program pty n ())
-> Program pty n (ThreadId (Program pty n))
forkOSWithUnmaskN String
n (forall a. Program pty n a -> Program pty n a) -> Program pty n ()
ma = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *).
String
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> (ThreadId -> Action n)
-> Action n
AForkOS String
n (\forall b. ModelConc n b -> ModelConc n b
umask -> forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()
ma forall b. ModelConc n b -> ModelConc n b
umask) (\()
_ -> forall (n :: * -> *). n () -> Action n
AStop (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()))))

  supportsBoundThreads :: Program pty n Bool
supportsBoundThreads = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc forall (n :: * -> *). (Bool -> Action n) -> Action n
ASupportsBoundThreads
  isCurrentThreadBound :: Program pty n Bool
isCurrentThreadBound = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc forall (n :: * -> *). (Bool -> Action n) -> Action n
AIsBound

  -- This implementation lies and returns 2 until a value is set. This
  -- will potentially avoid special-case behaviour for 1 capability,
  -- so it seems a sane choice.
  getNumCapabilities :: Program pty n Int
getNumCapabilities      = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc forall (n :: * -> *). (Int -> Action n) -> Action n
AGetNumCapabilities
  setNumCapabilities :: Int -> Program pty n ()
setNumCapabilities Int
caps = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> forall (n :: * -> *). Int -> Action n -> Action n
ASetNumCapabilities Int
caps (() -> Action n
c ()))

  myThreadId :: Program pty n (ThreadId (Program pty n))
myThreadId = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc forall (n :: * -> *). (ThreadId -> Action n) -> Action n
AMyTId

  yield :: Program pty n ()
yield = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> forall (n :: * -> *). Action n -> Action n
AYield (() -> Action n
c ()))
  threadDelay :: Int -> Program pty n ()
threadDelay Int
n = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> forall (n :: * -> *). Int -> Action n -> Action n
ADelay Int
n (() -> Action n
c ()))

  -- ----------

  newIORefN :: forall a. String -> a -> Program pty n (IORef (Program pty n) a)
newIORefN String
n a
a = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
String -> a -> (ModelIORef n a -> Action n) -> Action n
ANewIORef String
n a
a)

  readIORef :: forall a. IORef (Program pty n) a -> Program pty n a
readIORef   IORef (Program pty n) a
ref = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
ModelIORef n a -> (a -> Action n) -> Action n
AReadIORef    IORef (Program pty n) a
ref)
  readForCAS :: forall a.
IORef (Program pty n) a -> Program pty n (Ticket (Program pty n) a)
readForCAS IORef (Program pty n) a
ref = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
ModelIORef n a -> (ModelTicket a -> Action n) -> Action n
AReadIORefCas IORef (Program pty n) a
ref)

  peekTicket' :: forall a. Proxy (Program pty n) -> Ticket (Program pty n) a -> a
peekTicket' Proxy (Program pty n)
_ = forall a. ModelTicket a -> a
ticketVal

  writeIORef :: forall a. IORef (Program pty n) a -> a -> Program pty n ()
writeIORef IORef (Program pty n) a
ref      a
a = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> forall (n :: * -> *) a. ModelIORef n a -> a -> Action n -> Action n
AWriteIORef IORef (Program pty n) a
ref a
a (() -> Action n
c ()))
  casIORef :: forall a.
IORef (Program pty n) a
-> Ticket (Program pty n) a
-> a
-> Program pty n (Bool, Ticket (Program pty n) a)
casIORef   IORef (Program pty n) a
ref Ticket (Program pty n) a
tick a
a = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
ModelIORef n a
-> ModelTicket a
-> a
-> ((Bool, ModelTicket a) -> Action n)
-> Action n
ACasIORef IORef (Program pty n) a
ref Ticket (Program pty n) a
tick a
a)

  atomicModifyIORef :: forall a b.
IORef (Program pty n) a -> (a -> (a, b)) -> Program pty n b
atomicModifyIORef IORef (Program pty n) a
ref a -> (a, b)
f = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a b.
ModelIORef n a -> (a -> (a, b)) -> (b -> Action n) -> Action n
AModIORef    IORef (Program pty n) a
ref a -> (a, b)
f)
  modifyIORefCAS :: forall a b.
IORef (Program pty n) a -> (a -> (a, b)) -> Program pty n b
modifyIORefCAS    IORef (Program pty n) a
ref a -> (a, b)
f = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a b.
ModelIORef n a -> (a -> (a, b)) -> (b -> Action n) -> Action n
AModIORefCas IORef (Program pty n) a
ref a -> (a, b)
f)

  -- ----------

  newEmptyMVarN :: forall a. String -> Program pty n (MVar (Program pty n) a)
newEmptyMVarN String
n = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
String -> (ModelMVar n a -> Action n) -> Action n
ANewMVar String
n)

  putMVar :: forall a. MVar (Program pty n) a -> a -> Program pty n ()
putMVar  MVar (Program pty n) a
var a
a = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> forall (n :: * -> *) a. ModelMVar n a -> a -> Action n -> Action n
APutMVar MVar (Program pty n) a
var a
a (() -> Action n
c ()))
  readMVar :: forall a. MVar (Program pty n) a -> Program pty n a
readMVar MVar (Program pty n) a
var   = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
ModelMVar n a -> (a -> Action n) -> Action n
AReadMVar MVar (Program pty n) a
var)
  takeMVar :: forall a. MVar (Program pty n) a -> Program pty n a
takeMVar MVar (Program pty n) a
var   = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
ModelMVar n a -> (a -> Action n) -> Action n
ATakeMVar MVar (Program pty n) a
var)

  tryPutMVar :: forall a. MVar (Program pty n) a -> a -> Program pty n Bool
tryPutMVar  MVar (Program pty n) a
var a
a = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
ModelMVar n a -> a -> (Bool -> Action n) -> Action n
ATryPutMVar  MVar (Program pty n) a
var a
a)
  tryReadMVar :: forall a. MVar (Program pty n) a -> Program pty n (Maybe a)
tryReadMVar MVar (Program pty n) a
var   = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
ModelMVar n a -> (Maybe a -> Action n) -> Action n
ATryReadMVar MVar (Program pty n) a
var)
  tryTakeMVar :: forall a. MVar (Program pty n) a -> Program pty n (Maybe a)
tryTakeMVar MVar (Program pty n) a
var   = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
ModelMVar n a -> (Maybe a -> Action n) -> Action n
ATryTakeMVar MVar (Program pty n) a
var)

  -- ----------

  throwTo :: forall e.
Exception e =>
ThreadId (Program pty n) -> e -> Program pty n ()
throwTo ThreadId (Program pty n)
tid e
e = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> forall (n :: * -> *) e.
Exception e =>
ThreadId -> e -> Action n -> Action n
AThrowTo ThreadId (Program pty n)
tid e
e (() -> Action n
c ()))

  getMaskingState :: Program pty n MaskingState
getMaskingState = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\MaskingState -> Action n
c -> forall (n :: * -> *). (MaskingState -> Action n) -> Action n
AGetMasking MaskingState -> Action n
c)

  unsafeUnmask :: forall a. Program pty n a -> Program pty n a
unsafeUnmask Program pty n a
ma = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (forall (n :: * -> *) a.
MaskingState
-> ((forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a)
-> (a -> Action n)
-> Action n
AMasking MaskingState
Unmasked (\forall b. ModelConc n b -> ModelConc n b
_ -> Program pty n a
ma))

  -- ----------

  atomically :: forall a. STM (Program pty n) a -> Program pty n a
atomically = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a. ModelSTM n a -> (a -> Action n) -> Action n
AAtom

-------------------------------------------------------------------------------
-- Executing concurrent programs

-- | Run a concurrent computation with a given 'Scheduler' and initial
-- state, returning either the final result or the condition which
-- prevented that. Also returned is the final state of the scheduler,
-- and an execution trace.
--
-- If the RTS supports bound threads (ghc -threaded when linking) then
-- the main thread of the concurrent computation will be bound, and
-- @forkOS@ / @forkOSN@ will work during execution.  If not, then the
-- main thread will not be found, and attempting to fork a bound
-- thread will raise an error.
--
-- __Warning:__ Blocking on the action of another thread in 'liftIO'
-- cannot be detected! So if you perform some potentially blocking
-- action in a 'liftIO' the entire collection of threads may deadlock!
-- You should therefore keep @IO@ blocks small, and only perform
-- blocking operations with the supplied primitives, insofar as
-- possible.
--
-- __Note:__ In order to prevent computation from hanging, the runtime
-- will assume that a deadlock situation has arisen if the scheduler
-- attempts to (a) schedule a blocked thread, or (b) schedule a
-- nonexistent thread. In either of those cases, the computation will
-- be halted.
--
-- @since 2.1.0.0
runConcurrent :: MonadDejaFu n
  => Scheduler s
  -> MemType
  -> s
  -> Program pty n a
  -> n (Either Condition a, s, Trace)
runConcurrent :: forall (n :: * -> *) s pty a.
MonadDejaFu n =>
Scheduler s
-> MemType
-> s
-> Program pty n a
-> n (Either Condition a, s, Trace)
runConcurrent Scheduler s
sched MemType
memtype s
s ma :: Program pty n a
ma@(ModelConc (a -> Action n) -> Action n
_) = do
  CResult n s a
res <- forall (n :: * -> *) g a.
(MonadDejaFu n, HasCallStack) =>
[Invariant n ()]
-> Bool
-> Scheduler g
-> MemType
-> g
-> IdSource
-> Int
-> ModelConc n a
-> n (CResult n g a)
runConcurrency [] Bool
False Scheduler s
sched MemType
memtype s
s IdSource
initialIdSource Int
2 Program pty n a
ma
  Either Condition a
out <- forall a. HasCallStack => Maybe a -> a
efromJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef (forall (n :: * -> *) g a.
CResult n g a -> Ref n (Maybe (Either Condition a))
finalRef CResult n s a
res)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Either Condition a
out
       , forall (n :: * -> *) g. Context n g -> g
cSchedState (forall (n :: * -> *) g a. CResult n g a -> Context n g
finalContext CResult n s a
res)
       , forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (forall (n :: * -> *) g a. CResult n g a -> SeqTrace
finalTrace CResult n s a
res)
       )
runConcurrent Scheduler s
sched MemType
memtype s
s Program pty n a
ma = forall (n :: * -> *) pty a.
MonadDejaFu n =>
Program pty n a
-> n (Maybe (Either Condition (Snapshot pty n a), Trace))
recordSnapshot Program pty n a
ma forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Just (Left Condition
cond, Trace
trc) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left Condition
cond, s
s, Trace
trc)
  Just (Right Snapshot pty n a
snap, Trace
_)  -> forall (n :: * -> *) s pty a.
MonadDejaFu n =>
Scheduler s
-> MemType
-> s
-> Snapshot pty n a
-> n (Either Condition a, s, Trace)
runSnapshot Scheduler s
sched MemType
memtype s
s Snapshot pty n a
snap
  Maybe (Either Condition (Snapshot pty n a), Trace)
Nothing -> forall a. HasCallStack => String -> a
fatal String
"failed to record snapshot!"

-- | Runs any setup action and returns a 'Snapshot' which can be
-- passed to 'runSnapshot'.  If there is no setup action (this is a
-- @Program Basic@, then @Nothing@ is returned.  The snapshot captures
-- the state at the end of the setup, so the full program can be run
-- multiple times without repeating the setup.
--
-- The setup action is executed atomically with a deterministic
-- scheduler under sequential consistency.  Any forked threads
-- continue to exist in the main program.
--
-- If the setup action does not successfully produce a value
-- (deadlock, uncaught exception, etc), no snapshot is produced.
--
-- __Snapshotting @IO@:__ A snapshot captures entire state of your
-- concurrent program: the state of every thread, the number of
-- capabilities, the values of any @IORef@s, @MVar@s, and @TVar@s, and
-- records any @IO@ that you performed.
--
-- When restoring a snapshot this @IO@ is replayed, in order.  But the
-- whole snapshotted computation is not.  So the effects of the @IO@
-- take place again, but any return values are ignored.  For example,
-- this program will not do what you want:
--
-- @
-- bad_snapshot = withSetup
--   (do r <- liftIO (newIORef 0)
--       liftIO (modifyIORef r (+1))
--       pure r)
--   (liftIO . readIORef)
-- @
--
-- When the snapshot is taken, the value in the @IORef@ will be 1.
-- When the snapshot is restored for the first time, those @IO@
-- actions will be run again, /but their return values will be
-- discarded/.  The value in the @IORef@ will be 2.  When the snapshot
-- is restored for the second time, the value in the @IORef@ will be
-- 3.  And so on.
--
-- To safely use @IO@ in a snapshotted computation, __the combined
-- effect must be idempotent__.  You should either use actions which
-- set the state to the final value directly, rather than modifying it
-- (eg, using a combination of @liftIO . readIORef@ and @liftIO
-- . writeIORef@ here), or reset the state to a known value.  Both of
-- these approaches will work:
--
-- @
-- good_snapshot1 = withSetup
--   (do let modify r f = liftIO (readIORef r) >>= liftIO . writeIORef r . f
--        r <- liftIO (newIORef 0)
--        modify r (+1)
--        pure r)
--   (liftIO . readIORef)
--
-- good_snapshot2 = withSetup
--   (do r <- liftIO (newIORef 0)
--       liftIO (writeIORef r 0)
--       liftIO (modifyIORef r (+1))
--       pure r)
--   (liftIO . readIORef)
-- @
--
-- @since 2.1.0.0
recordSnapshot
  :: MonadDejaFu n
  => Program pty n a
  -> n (Maybe (Either Condition (Snapshot pty n a), Trace))
recordSnapshot :: forall (n :: * -> *) pty a.
MonadDejaFu n =>
Program pty n a
-> n (Maybe (Either Condition (Snapshot pty n a), Trace))
recordSnapshot ModelConc{} = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
recordSnapshot WithSetup{ModelConc n x
x -> ModelConc n a
wsProgram :: forall (n :: * -> *) a a.
Program (WithSetup a) n a -> a -> ModelConc n a
wsSetup :: forall (n :: * -> *) a a.
Program (WithSetup a) n a -> ModelConc n a
wsProgram :: x -> ModelConc n a
wsSetup :: ModelConc n x
..} =
  let mkSnapshot :: SimpleSnapshot n a -> p -> Snapshot (WithSetup x) n a
mkSnapshot SimpleSnapshot n a
snap p
_ = forall (n :: * -> *) a a.
SimpleSnapshot n a -> Snapshot (WithSetup a) n a
WS SimpleSnapshot n a
snap
  in forall (n :: * -> *) a x snap.
MonadDejaFu n =>
(SimpleSnapshot n a -> x -> snap)
-> ModelConc n x
-> (x -> ModelConc n a)
-> n (Maybe (Either Condition snap, Trace))
defaultRecordSnapshot forall {n :: * -> *} {a} {p} {x}.
SimpleSnapshot n a -> p -> Snapshot (WithSetup x) n a
mkSnapshot ModelConc n x
wsSetup x -> ModelConc n a
wsProgram
recordSnapshot WithSetupAndTeardown{ModelConc n x
x -> ModelConc n y
x -> Either Condition y -> ModelConc n a
wstTeardown :: forall (n :: * -> *) a x a.
Program (WithSetupAndTeardown a x) n a
-> a -> Either Condition x -> ModelConc n a
wstProgram :: forall (n :: * -> *) a x a.
Program (WithSetupAndTeardown a x) n a -> a -> ModelConc n x
wstSetup :: forall (n :: * -> *) a x a.
Program (WithSetupAndTeardown a x) n a -> ModelConc n a
wstTeardown :: x -> Either Condition y -> ModelConc n a
wstProgram :: x -> ModelConc n y
wstSetup :: ModelConc n x
..} =
  let mkSnapshot :: SimpleSnapshot n y -> x -> Snapshot (WithSetupAndTeardown x y) n a
mkSnapshot SimpleSnapshot n y
snap = forall (n :: * -> *) a y x.
SimpleSnapshot n a
-> (Either Condition a -> ModelConc n y)
-> Snapshot (WithSetupAndTeardown x a) n y
WSAT SimpleSnapshot n y
snap forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either Condition y -> ModelConc n a
wstTeardown
  in forall (n :: * -> *) a x snap.
MonadDejaFu n =>
(SimpleSnapshot n a -> x -> snap)
-> ModelConc n x
-> (x -> ModelConc n a)
-> n (Maybe (Either Condition snap, Trace))
defaultRecordSnapshot SimpleSnapshot n y -> x -> Snapshot (WithSetupAndTeardown x y) n a
mkSnapshot ModelConc n x
wstSetup x -> ModelConc n y
wstProgram

-- | Runs a program with snapshotted setup to completion.
--
-- @since 2.1.0.0
runSnapshot
  :: MonadDejaFu n
  => Scheduler s
  -> MemType
  -> s
  -> Snapshot pty n a
  -> n (Either Condition a, s, Trace)
runSnapshot :: forall (n :: * -> *) s pty a.
MonadDejaFu n =>
Scheduler s
-> MemType
-> s
-> Snapshot pty n a
-> n (Either Condition a, s, Trace)
runSnapshot Scheduler s
sched MemType
memtype s
s (WS SimpleSnapshot{ModelConc n a
Context n ()
Threads n -> n ()
snapNext :: forall (n :: * -> *) a. SimpleSnapshot n a -> ModelConc n a
snapRestore :: forall (n :: * -> *) a. SimpleSnapshot n a -> Threads n -> n ()
snapContext :: forall (n :: * -> *) a. SimpleSnapshot n a -> Context n ()
snapNext :: ModelConc n a
snapRestore :: Threads n -> n ()
snapContext :: Context n ()
..}) = do
  let context :: Context n s
context = forall g (n :: * -> *) s. g -> Context n s -> Context n g
fromSnapContext s
s Context n ()
snapContext
  CResult{Maybe (ThreadId, ThreadAction)
SeqTrace
Ref n (Maybe (Either Condition a))
Context n s
Threads n -> n ()
finalDecision :: forall (n :: * -> *) g a.
CResult n g a -> Maybe (ThreadId, ThreadAction)
finalRestore :: forall (n :: * -> *) g a. CResult n g a -> Threads n -> n ()
finalDecision :: Maybe (ThreadId, ThreadAction)
finalTrace :: SeqTrace
finalRestore :: Threads n -> n ()
finalRef :: Ref n (Maybe (Either Condition a))
finalContext :: Context n s
finalTrace :: forall (n :: * -> *) g a. CResult n g a -> SeqTrace
finalContext :: forall (n :: * -> *) g a. CResult n g a -> Context n g
finalRef :: forall (n :: * -> *) g a.
CResult n g a -> Ref n (Maybe (Either Condition a))
..} <- forall (n :: * -> *) g a.
(MonadDejaFu n, HasCallStack) =>
Scheduler g
-> MemType
-> Context n g
-> (Threads n -> n ())
-> ModelConc n a
-> n (CResult n g a)
runConcurrencyWithSnapshot Scheduler s
sched MemType
memtype Context n s
context Threads n -> n ()
snapRestore ModelConc n a
snapNext
  Either Condition a
out <- forall a. HasCallStack => Maybe a -> a
efromJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe (Either Condition a))
finalRef
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Either Condition a
out
       , forall (n :: * -> *) g. Context n g -> g
cSchedState Context n s
finalContext
       , forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList SeqTrace
finalTrace
       )
runSnapshot Scheduler s
sched MemType
memtype s
s (WSAT SimpleSnapshot{ModelConc n a
Context n ()
Threads n -> n ()
snapNext :: ModelConc n a
snapRestore :: Threads n -> n ()
snapContext :: Context n ()
snapNext :: forall (n :: * -> *) a. SimpleSnapshot n a -> ModelConc n a
snapRestore :: forall (n :: * -> *) a. SimpleSnapshot n a -> Threads n -> n ()
snapContext :: forall (n :: * -> *) a. SimpleSnapshot n a -> Context n ()
..} Either Condition a -> ModelConc n a
teardown) = do
  let context :: Context n s
context = forall g (n :: * -> *) s. g -> Context n s -> Context n g
fromSnapContext s
s Context n ()
snapContext
  CResult n s a
intermediateResult <- forall (n :: * -> *) g a.
(MonadDejaFu n, HasCallStack) =>
Scheduler g
-> MemType
-> Context n g
-> (Threads n -> n ())
-> ModelConc n a
-> n (CResult n g a)
runConcurrencyWithSnapshot Scheduler s
sched MemType
memtype Context n s
context Threads n -> n ()
snapRestore ModelConc n a
snapNext
  let idsrc :: IdSource
idsrc = forall (n :: * -> *) g. Context n g -> IdSource
cIdSource (forall (n :: * -> *) g a. CResult n g a -> Context n g
finalContext CResult n s a
intermediateResult)
  Either Condition a
out1 <- forall a. HasCallStack => Maybe a -> a
efromJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef (forall (n :: * -> *) g a.
CResult n g a -> Ref n (Maybe (Either Condition a))
finalRef CResult n s a
intermediateResult)
  CResult n () a
teardownResult <- forall (n :: * -> *) a.
(MonadDejaFu n, HasCallStack) =>
Bool -> IdSource -> ModelConc n a -> n (CResult n () a)
simpleRunConcurrency Bool
False IdSource
idsrc (Either Condition a -> ModelConc n a
teardown Either Condition a
out1)
  Either Condition a
out2 <- forall a. HasCallStack => Maybe a -> a
efromJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef (forall (n :: * -> *) g a.
CResult n g a -> Ref n (Maybe (Either Condition a))
finalRef CResult n () a
teardownResult)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Either Condition a
out2
       , forall (n :: * -> *) g. Context n g -> g
cSchedState (forall (n :: * -> *) g a. CResult n g a -> Context n g
finalContext CResult n s a
intermediateResult)
       , forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (forall (n :: * -> *) g a. CResult n g a -> SeqTrace
finalTrace CResult n s a
intermediateResult)
       )

-------------------------------------------------------------------------------
-- Snapshotting

-- | A record of the state of a concurrent program immediately after
-- completing the setup action.
--
-- @since 2.0.0.0
data Snapshot pty n a where
  WS   :: SimpleSnapshot n a -> Snapshot (WithSetup x) n a
  WSAT :: SimpleSnapshot n a -> (Either Condition a -> ModelConc n y) -> Snapshot (WithSetupAndTeardown x a) n y

data SimpleSnapshot n a = SimpleSnapshot
  { forall (n :: * -> *) a. SimpleSnapshot n a -> Context n ()
snapContext :: Context n ()
  , forall (n :: * -> *) a. SimpleSnapshot n a -> Threads n -> n ()
snapRestore :: Threads n -> n ()
  , forall (n :: * -> *) a. SimpleSnapshot n a -> ModelConc n a
snapNext    :: ModelConc n a
  }

-- | Get the 'Context' from a 'Snapshot'.
contextFromSnapshot :: Snapshot p n a -> Context n ()
contextFromSnapshot :: forall p (n :: * -> *) a. Snapshot p n a -> Context n ()
contextFromSnapshot (WS SimpleSnapshot{ModelConc n a
Context n ()
Threads n -> n ()
snapNext :: ModelConc n a
snapRestore :: Threads n -> n ()
snapContext :: Context n ()
snapNext :: forall (n :: * -> *) a. SimpleSnapshot n a -> ModelConc n a
snapRestore :: forall (n :: * -> *) a. SimpleSnapshot n a -> Threads n -> n ()
snapContext :: forall (n :: * -> *) a. SimpleSnapshot n a -> Context n ()
..})     = Context n ()
snapContext
contextFromSnapshot (WSAT SimpleSnapshot{ModelConc n a
Context n ()
Threads n -> n ()
snapNext :: ModelConc n a
snapRestore :: Threads n -> n ()
snapContext :: Context n ()
snapNext :: forall (n :: * -> *) a. SimpleSnapshot n a -> ModelConc n a
snapRestore :: forall (n :: * -> *) a. SimpleSnapshot n a -> Threads n -> n ()
snapContext :: forall (n :: * -> *) a. SimpleSnapshot n a -> Context n ()
..} Either Condition a -> ModelConc n a
_) = Context n ()
snapContext

-- | Get the threads which exist in a snapshot, partitioned into
-- runnable and not runnable.
threadsFromSnapshot :: Snapshot p n a -> ([ThreadId], [ThreadId])
threadsFromSnapshot :: forall p (n :: * -> *) a.
Snapshot p n a -> ([ThreadId], [ThreadId])
threadsFromSnapshot Snapshot p n a
snap = (ThreadId
initialThread forall a. a -> [a] -> [a]
: [ThreadId]
runnable, [ThreadId]
blocked) where
  ([ThreadId]
runnable, [ThreadId]
blocked) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ThreadId -> Bool
isRunnable (forall k a. Map k a -> [k]
M.keys Threads n
threads)
  threads :: Threads n
threads = forall (n :: * -> *) g. Context n g -> Threads n
cThreads (forall p (n :: * -> *) a. Snapshot p n a -> Context n ()
contextFromSnapshot Snapshot p n a
snap)
  isRunnable :: ThreadId -> Bool
isRunnable ThreadId
tid = forall a. Maybe a -> Bool
isNothing (forall (n :: * -> *). Thread n -> Maybe BlockedOn
_blocking forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ThreadId
tid Threads n
threads)

-- | 'recordSnapshot' implemented generically.
--
-- Throws an error if the snapshot could not be produced.
defaultRecordSnapshot :: MonadDejaFu n
  => (SimpleSnapshot n a -> x -> snap)
  -> ModelConc n x
  -> (x -> ModelConc n a)
  -> n (Maybe (Either Condition snap, Trace))
defaultRecordSnapshot :: forall (n :: * -> *) a x snap.
MonadDejaFu n =>
(SimpleSnapshot n a -> x -> snap)
-> ModelConc n x
-> (x -> ModelConc n a)
-> n (Maybe (Either Condition snap, Trace))
defaultRecordSnapshot SimpleSnapshot n a -> x -> snap
mkSnapshot ModelConc n x
setup x -> ModelConc n a
program = do
  CResult{Maybe (ThreadId, ThreadAction)
SeqTrace
Ref n (Maybe (Either Condition x))
Context n ()
Threads n -> n ()
finalDecision :: Maybe (ThreadId, ThreadAction)
finalTrace :: SeqTrace
finalRestore :: Threads n -> n ()
finalRef :: Ref n (Maybe (Either Condition x))
finalContext :: Context n ()
finalDecision :: forall (n :: * -> *) g a.
CResult n g a -> Maybe (ThreadId, ThreadAction)
finalRestore :: forall (n :: * -> *) g a. CResult n g a -> Threads n -> n ()
finalTrace :: forall (n :: * -> *) g a. CResult n g a -> SeqTrace
finalContext :: forall (n :: * -> *) g a. CResult n g a -> Context n g
finalRef :: forall (n :: * -> *) g a.
CResult n g a -> Ref n (Maybe (Either Condition a))
..} <- forall (n :: * -> *) a.
(MonadDejaFu n, HasCallStack) =>
Bool -> IdSource -> ModelConc n a -> n (CResult n () a)
simpleRunConcurrency Bool
True IdSource
initialIdSource ModelConc n x
setup
  let trc :: Trace
trc = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList SeqTrace
finalTrace
  Maybe (Either Condition x)
out <- forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe (Either Condition x))
finalRef
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ case Maybe (Either Condition x)
out of
    Just (Right x
a) ->
      let snap :: snap
snap = SimpleSnapshot n a -> x -> snap
mkSnapshot (forall (n :: * -> *) a.
Context n ()
-> (Threads n -> n ()) -> ModelConc n a -> SimpleSnapshot n a
SimpleSnapshot Context n ()
finalContext Threads n -> n ()
finalRestore (x -> ModelConc n a
program x
a)) x
a
      in (forall a b. b -> Either a b
Right snap
snap, Trace
trc)
    Just (Left Condition
f) -> (forall a b. a -> Either a b
Left Condition
f, Trace
trc)
    -- alternative behaviour: return @Nothing@ here.  but this should
    -- never fail, so it should be an error if it does.
    Maybe (Either Condition x)
Nothing -> forall a. HasCallStack => String -> a
fatal String
"failed to produce snapshot"

-------------------------------------------------------------------------------
-- Utilities

-- | Run a concurrent program with a deterministic scheduler in
-- snapshotting or non-snapshotting mode.
simpleRunConcurrency ::(MonadDejaFu n, HasCallStack)
  => Bool
  -> IdSource
  -> ModelConc n a
  -> n (CResult n () a)
simpleRunConcurrency :: forall (n :: * -> *) a.
(MonadDejaFu n, HasCallStack) =>
Bool -> IdSource -> ModelConc n a -> n (CResult n () a)
simpleRunConcurrency Bool
forSnapshot IdSource
idsrc =
  forall (n :: * -> *) g a.
(MonadDejaFu n, HasCallStack) =>
[Invariant n ()]
-> Bool
-> Scheduler g
-> MemType
-> g
-> IdSource
-> Int
-> ModelConc n a
-> n (CResult n g a)
runConcurrency [] Bool
forSnapshot Scheduler ()
roundRobinSchedNP MemType
SequentialConsistency () IdSource
idsrc Int
2

-- | Make a new context from a snapshot context.
fromSnapContext :: g -> Context n s -> Context n g
fromSnapContext :: forall g (n :: * -> *) s. g -> Context n s -> Context n g
fromSnapContext g
g ctx :: Context n s
ctx@Context{s
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: s
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} = Context n s
ctx
  { cSchedState :: g
cSchedState = g
g
  , cInvariants :: InvariantContext n
cInvariants = InvariantContext
    { icActive :: [Invariant n ()]
icActive  = [Invariant n ()]
cNewInvariants
    , icBlocked :: [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
icBlocked = []
    }
  , cNewInvariants :: [Invariant n ()]
cNewInvariants = []
  }

wrap :: (((a -> Action n) -> Action n) -> ((a -> Action n) -> Action n)) -> ModelConc n a -> ModelConc n a
wrap :: forall a (n :: * -> *).
(((a -> Action n) -> Action n) -> (a -> Action n) -> Action n)
-> ModelConc n a -> ModelConc n a
wrap ((a -> Action n) -> Action n) -> (a -> Action n) -> Action n
f = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> Action n) -> Action n) -> (a -> Action n) -> Action n
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc