{-# OPTIONS_GHC -Wno-orphans #-}

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

-- 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 = ((a -> Action n) -> Action n) -> Program Basic n a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\a -> Action n
c -> n (Action n) -> Action n
forall (n :: * -> *). n (Action n) -> Action n
ALift ((a -> Action n) -> n a -> n (Action n)
forall a b. (a -> b) -> n a -> n b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Action n
c (IO a -> n a
forall a. IO a -> n a
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 = ((a -> Action m) -> Action m) -> Program Basic m a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\a -> Action m
c -> m (Action m) -> Action m
forall (n :: * -> *). n (Action n) -> Action n
ALift ((a -> Action m) -> m a -> m (Action m)
forall a b. (a -> b) -> m a -> m b
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.
(HasCallStack, 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 = ((a -> Action n) -> Action n) -> Program Basic n a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc ((e -> Program Basic n a)
-> Program Basic n a -> (a -> Action n) -> Action n
forall (n :: * -> *) a e.
Exception e =>
(e -> ModelConc n a)
-> ModelConc n a -> (a -> Action n) -> Action n
ACatching e -> Program pty n a
e -> Program Basic n a
h Program pty n a
Program Basic n a
ma)

instance (pty ~ Basic) => Ca.MonadThrow (Program pty n) where
  throwM :: forall e a. (HasCallStack, Exception e) => e -> Program pty n a
throwM e
e = ((a -> Action n) -> Action n) -> Program Basic n a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\a -> Action n
_ -> e -> 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.
HasCallStack =>
((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 = ((b -> Action n) -> Action n) -> Program Basic n b
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (MaskingState
-> ((forall b. ModelConc n b -> ModelConc n b)
    -> Program Basic n b)
-> (b -> Action n)
-> Action n
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 Program pty n a -> Program pty n a
ModelConc n a -> ModelConc n a
forall a. Program pty n a -> Program pty n a
forall b. ModelConc n b -> ModelConc n b
f))
  uninterruptibleMask :: forall b.
HasCallStack =>
((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 = ((b -> Action n) -> Action n) -> Program Basic n b
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (MaskingState
-> ((forall b. ModelConc n b -> ModelConc n b)
    -> Program Basic n b)
-> (b -> Action n)
-> Action n
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 Program pty n a -> Program pty n a
ModelConc n a -> ModelConc n a
forall a. Program pty n a -> Program pty n a
forall b. ModelConc n b -> ModelConc n b
f))

#if MIN_VERSION_exceptions(0,10,0)
  generalBracket :: forall a b c.
HasCallStack =>
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 a. Program pty n a -> Program pty n a)
 -> Program pty n (b, c))
-> Program pty n (b, c)
forall b.
HasCallStack =>
((forall a. Program pty n a -> Program pty n a) -> Program pty n b)
-> Program pty n b
forall (m :: * -> *) b.
(MonadMask m, HasCallStack) =>
((forall a. m a -> m a) -> m b) -> m b
Ca.mask (((forall a. Program pty n a -> Program pty n a)
  -> Program pty n (b, c))
 -> Program pty n (b, c))
-> ((forall a. Program pty n a -> Program pty n a)
    -> Program pty n (b, c))
-> Program pty n (b, c)
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 <- Program pty n b -> Program pty n b
forall a. Program pty n a -> Program pty n a
unmasked (a -> Program pty n b
use a
resource) Program pty n b
-> (SomeException -> Program pty n b) -> Program pty n b
forall e a.
(HasCallStack, Exception e) =>
Program pty n a -> (e -> Program pty n a) -> Program pty n a
forall (m :: * -> *) e a.
(MonadCatch m, HasCallStack, Exception e) =>
m a -> (e -> m a) -> m a
`Ca.catch` (\SomeException
e -> a -> ExitCase b -> Program pty n c
release a
resource (SomeException -> ExitCase b
forall a. SomeException -> ExitCase a
Ca.ExitCaseException SomeException
e) Program pty n c -> Program pty n b -> Program pty n b
forall a b. Program pty n a -> Program pty n b -> Program pty n b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SomeException -> Program pty n b
forall e a. (HasCallStack, Exception e) => e -> Program pty n a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
Ca.throwM SomeException
e)
    c
c <- a -> ExitCase b -> Program pty n c
release a
resource (b -> ExitCase b
forall a. a -> ExitCase a
Ca.ExitCaseSuccess b
b)
    (b, c) -> Program pty n (b, c)
forall a. a -> Program pty n a
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 = ((ThreadId -> Action n) -> Action n) -> Program Basic n ThreadId
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (String
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> (ThreadId -> Action n)
-> Action n
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 -> Program Basic n () -> (() -> Action n) -> Action n
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 Program pty n a -> Program pty n a
ModelConc n a -> ModelConc n a
forall a. Program pty n a -> Program pty n a
forall b. ModelConc n b -> ModelConc n b
umask) (\()
_ -> n () -> Action n
forall (n :: * -> *). n () -> Action n
AStop (() -> n ()
forall a. a -> n a
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
_  = String
-> ((forall a. Program pty n a -> Program pty n a)
    -> Program pty n ())
-> Program pty n (ThreadId (Program pty n))
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 = ((ThreadId -> Action n) -> Action n) -> Program Basic n ThreadId
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (String
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> (ThreadId -> Action n)
-> Action n
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 -> Program Basic n () -> (() -> Action n) -> Action n
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 Program pty n a -> Program pty n a
ModelConc n a -> ModelConc n a
forall a. Program pty n a -> Program pty n a
forall b. ModelConc n b -> ModelConc n b
umask) (\()
_ -> n () -> Action n
forall (n :: * -> *). n () -> Action n
AStop (() -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()))))

  supportsBoundThreads :: Program pty n Bool
supportsBoundThreads = ((Bool -> Action n) -> Action n) -> Program Basic n Bool
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (Bool -> Action n) -> Action n
forall (n :: * -> *). (Bool -> Action n) -> Action n
ASupportsBoundThreads
  isCurrentThreadBound :: Program pty n Bool
isCurrentThreadBound = ((Bool -> Action n) -> Action n) -> Program Basic n Bool
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (Bool -> Action n) -> Action n
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      = ((Int -> Action n) -> Action n) -> Program Basic n Int
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (Int -> Action n) -> Action n
forall (n :: * -> *). (Int -> Action n) -> Action n
AGetNumCapabilities
  setNumCapabilities :: Int -> Program pty n ()
setNumCapabilities Int
caps = ((() -> Action n) -> Action n) -> Program Basic n ()
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> Int -> Action n -> Action n
forall (n :: * -> *). Int -> Action n -> Action n
ASetNumCapabilities Int
caps (() -> Action n
c ()))

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

  yield :: Program pty n ()
yield = ((() -> Action n) -> Action n) -> Program Basic n ()
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> Action n -> Action n
forall (n :: * -> *). Action n -> Action n
AYield (() -> Action n
c ()))
  threadDelay :: Int -> Program pty n ()
threadDelay Int
n = ((() -> Action n) -> Action n) -> Program Basic n ()
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> Int -> Action n -> Action n
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 = ((ModelIORef n a -> Action n) -> Action n)
-> Program Basic n (ModelIORef n a)
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (String -> a -> (ModelIORef n a -> Action n) -> Action n
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 = ((a -> Action n) -> Action n) -> Program Basic n a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (ModelIORef n a -> (a -> Action n) -> Action n
forall (n :: * -> *) a.
ModelIORef n a -> (a -> Action n) -> Action n
AReadIORef    IORef (Program pty n) a
ModelIORef 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 = ((ModelTicket a -> Action n) -> Action n)
-> Program Basic n (ModelTicket a)
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (ModelIORef n a -> (ModelTicket a -> Action n) -> Action n
forall (n :: * -> *) a.
ModelIORef n a -> (ModelTicket a -> Action n) -> Action n
AReadIORefCas IORef (Program pty n) a
ModelIORef n a
ref)

  peekTicket' :: forall a. Proxy (Program pty n) -> Ticket (Program pty n) a -> a
peekTicket' Proxy (Program pty n)
_ = Ticket (Program pty n) a -> a
ModelTicket a -> a
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 = ((() -> Action n) -> Action n) -> Program Basic n ()
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> ModelIORef n a -> a -> Action n -> Action n
forall (n :: * -> *) a. ModelIORef n a -> a -> Action n -> Action n
AWriteIORef IORef (Program pty n) a
ModelIORef 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 = (((Bool, ModelTicket a) -> Action n) -> Action n)
-> Program Basic n (Bool, ModelTicket a)
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (ModelIORef n a
-> ModelTicket a
-> a
-> ((Bool, ModelTicket a) -> Action n)
-> Action n
forall (n :: * -> *) a.
ModelIORef n a
-> ModelTicket a
-> a
-> ((Bool, ModelTicket a) -> Action n)
-> Action n
ACasIORef IORef (Program pty n) a
ModelIORef n a
ref Ticket (Program pty n) a
ModelTicket 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 = ((b -> Action n) -> Action n) -> Program Basic n b
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (ModelIORef n a -> (a -> (a, b)) -> (b -> Action n) -> Action n
forall (n :: * -> *) a b.
ModelIORef n a -> (a -> (a, b)) -> (b -> Action n) -> Action n
AModIORef    IORef (Program pty n) a
ModelIORef 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 = ((b -> Action n) -> Action n) -> Program Basic n b
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (ModelIORef n a -> (a -> (a, b)) -> (b -> Action n) -> Action n
forall (n :: * -> *) a b.
ModelIORef n a -> (a -> (a, b)) -> (b -> Action n) -> Action n
AModIORefCas IORef (Program pty n) a
ModelIORef n a
ref a -> (a, b)
f)

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

  newEmptyMVarN :: forall a. String -> Program pty n (MVar (Program pty n) a)
newEmptyMVarN String
n = ((ModelMVar n a -> Action n) -> Action n)
-> Program Basic n (ModelMVar n a)
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (String -> (ModelMVar n a -> Action n) -> Action n
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 = ((() -> Action n) -> Action n) -> Program Basic n ()
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\() -> Action n
c -> ModelMVar n a -> a -> Action n -> Action n
forall (n :: * -> *) a. ModelMVar n a -> a -> Action n -> Action n
APutMVar MVar (Program pty n) a
ModelMVar 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   = ((a -> Action n) -> Action n) -> Program Basic n a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (ModelMVar n a -> (a -> Action n) -> Action n
forall (n :: * -> *) a.
ModelMVar n a -> (a -> Action n) -> Action n
AReadMVar MVar (Program pty n) a
ModelMVar n a
var)
  takeMVar :: forall a. MVar (Program pty n) a -> Program pty n a
takeMVar MVar (Program pty n) a
var   = ((a -> Action n) -> Action n) -> Program Basic n a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (ModelMVar n a -> (a -> Action n) -> Action n
forall (n :: * -> *) a.
ModelMVar n a -> (a -> Action n) -> Action n
ATakeMVar MVar (Program pty n) a
ModelMVar 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 = ((Bool -> Action n) -> Action n) -> Program Basic n Bool
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (ModelMVar n a -> a -> (Bool -> Action n) -> Action n
forall (n :: * -> *) a.
ModelMVar n a -> a -> (Bool -> Action n) -> Action n
ATryPutMVar  MVar (Program pty n) a
ModelMVar 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   = ((Maybe a -> Action n) -> Action n) -> Program Basic n (Maybe a)
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (ModelMVar n a -> (Maybe a -> Action n) -> Action n
forall (n :: * -> *) a.
ModelMVar n a -> (Maybe a -> Action n) -> Action n
ATryReadMVar MVar (Program pty n) a
ModelMVar n a
var)
  tryTakeMVar :: forall a. MVar (Program pty n) a -> Program pty n (Maybe a)
tryTakeMVar MVar (Program pty n) a
var   = ((Maybe a -> Action n) -> Action n) -> Program Basic n (Maybe a)
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (ModelMVar n a -> (Maybe a -> Action n) -> Action n
forall (n :: * -> *) a.
ModelMVar n a -> (Maybe a -> Action n) -> Action n
ATryTakeMVar MVar (Program pty n) a
ModelMVar n a
var)

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

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

  getMaskingState :: Program pty n MaskingState
getMaskingState = ((MaskingState -> Action n) -> Action n)
-> Program Basic n MaskingState
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (\MaskingState -> Action n
c -> (MaskingState -> Action n) -> Action n
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 = ((a -> Action n) -> Action n) -> Program Basic n a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (MaskingState
-> ((forall b. ModelConc n b -> ModelConc n b)
    -> Program Basic n a)
-> (a -> Action n)
-> Action n
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
Program Basic n a
ma))

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

  atomically :: forall a. STM (Program pty n) a -> Program pty n a
atomically = ((a -> Action n) -> Action n) -> Program pty n a
((a -> Action n) -> Action n) -> Program Basic n a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (((a -> Action n) -> Action n) -> Program pty n a)
-> (ModelSTM n a -> (a -> Action n) -> Action n)
-> ModelSTM n a
-> Program pty n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelSTM n a -> (a -> Action n) -> Action n
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 <- [Invariant n ()]
-> Bool
-> Scheduler s
-> MemType
-> s
-> IdSource
-> Int
-> ModelConc n a
-> n (CResult n s a)
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
ModelConc n a
ma
  Either Condition a
out <- Maybe (Either Condition a) -> Either Condition a
forall a. HasCallStack => Maybe a -> a
efromJust (Maybe (Either Condition a) -> Either Condition a)
-> n (Maybe (Either Condition a)) -> n (Either Condition a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ref n (Maybe (Either Condition a))
-> n (Maybe (Either Condition a))
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef (CResult n s a -> Ref n (Maybe (Either Condition a))
forall (n :: * -> *) g a.
CResult n g a -> Ref n (Maybe (Either Condition a))
finalRef CResult n s a
res)
  (Either Condition a, s, Trace) -> n (Either Condition a, s, Trace)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Either Condition a
out
       , Context n s -> s
forall (n :: * -> *) g. Context n g -> g
cSchedState (CResult n s a -> Context n s
forall (n :: * -> *) g a. CResult n g a -> Context n g
finalContext CResult n s a
res)
       , Seq (Decision, [(ThreadId, Lookahead)], ThreadAction) -> Trace
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (CResult n s a
-> Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
forall (n :: * -> *) g a.
CResult n g a
-> Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
finalTrace CResult n s a
res)
       )
runConcurrent Scheduler s
sched MemType
memtype s
s Program pty n a
ma = Program pty n a
-> n (Maybe (Either Condition (Snapshot pty n a), Trace))
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 n (Maybe (Either Condition (Snapshot pty n a), Trace))
-> (Maybe (Either Condition (Snapshot pty n a), Trace)
    -> n (Either Condition a, s, Trace))
-> n (Either Condition a, s, Trace)
forall a b. n a -> (a -> n b) -> n b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Just (Left Condition
cond, Trace
trc) -> (Either Condition a, s, Trace) -> n (Either Condition a, s, Trace)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Condition -> Either Condition a
forall a b. a -> Either a b
Left Condition
cond, s
s, Trace
trc)
  Just (Right Snapshot pty n a
snap, Trace
_)  -> Scheduler s
-> MemType
-> s
-> Snapshot pty n a
-> n (Either Condition a, s, 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 -> String -> n (Either Condition a, s, Trace)
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{} = Maybe (Either Condition (Snapshot pty n a), Trace)
-> n (Maybe (Either Condition (Snapshot pty n a), Trace))
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Either Condition (Snapshot pty n a), Trace)
forall a. Maybe a
Nothing
recordSnapshot WithSetup{ModelConc n x
x -> ModelConc n a
wsSetup :: ModelConc n x
wsProgram :: x -> ModelConc n a
wsProgram :: forall (n :: * -> *) x a.
Program (WithSetup x) n a -> x -> ModelConc n a
wsSetup :: forall (n :: * -> *) x a.
Program (WithSetup x) n a -> ModelConc n x
..} =
  let mkSnapshot :: SimpleSnapshot n a -> p -> Snapshot (WithSetup x) n a
mkSnapshot SimpleSnapshot n a
snap p
_ = SimpleSnapshot n a -> Snapshot (WithSetup x) n a
forall (n :: * -> *) a a.
SimpleSnapshot n a -> Snapshot (WithSetup a) n a
WS SimpleSnapshot n a
snap
  in (SimpleSnapshot n a -> x -> Snapshot pty n a)
-> ModelConc n x
-> (x -> ModelConc n a)
-> n (Maybe (Either Condition (Snapshot pty n a), Trace))
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 -> Snapshot pty n a
SimpleSnapshot n a -> x -> Snapshot (WithSetup x) n a
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
wstSetup :: ModelConc n x
wstProgram :: x -> ModelConc n y
wstTeardown :: x -> Either Condition y -> ModelConc n a
wstTeardown :: forall (n :: * -> *) x y a.
Program (WithSetupAndTeardown x y) n a
-> x -> Either Condition y -> ModelConc n a
wstProgram :: forall (n :: * -> *) x y a.
Program (WithSetupAndTeardown x y) n a -> x -> ModelConc n y
wstSetup :: forall (n :: * -> *) x y a.
Program (WithSetupAndTeardown x y) n a -> ModelConc n x
..} =
  let mkSnapshot :: SimpleSnapshot n y -> x -> Snapshot (WithSetupAndTeardown x y) n a
mkSnapshot SimpleSnapshot n y
snap = SimpleSnapshot n y
-> (Either Condition y -> ModelConc n a)
-> Snapshot (WithSetupAndTeardown x y) n a
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 ((Either Condition y -> ModelConc n a)
 -> Snapshot (WithSetupAndTeardown x y) n a)
-> (x -> Either Condition y -> ModelConc n a)
-> x
-> Snapshot (WithSetupAndTeardown x y) n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either Condition y -> ModelConc n a
wstTeardown
  in (SimpleSnapshot n y -> x -> Snapshot pty n a)
-> ModelConc n x
-> (x -> ModelConc n y)
-> n (Maybe (Either Condition (Snapshot pty n a), Trace))
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 pty n a
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 ()
snapContext :: Context n ()
snapRestore :: Threads n -> n ()
snapNext :: ModelConc n a
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 ()
..}) = do
  let context :: Context n s
context = s -> Context n () -> Context n s
forall g (n :: * -> *) s. g -> Context n s -> Context n g
fromSnapContext s
s Context n ()
snapContext
  CResult{Maybe (ThreadId, ThreadAction)
Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
Ref n (Maybe (Either Condition a))
Context n s
Threads n -> n ()
finalRef :: forall (n :: * -> *) g a.
CResult n g a -> Ref n (Maybe (Either Condition a))
finalContext :: forall (n :: * -> *) g a. CResult n g a -> Context n g
finalTrace :: forall (n :: * -> *) g a.
CResult n g a
-> Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
finalContext :: Context n s
finalRef :: Ref n (Maybe (Either Condition a))
finalRestore :: Threads n -> n ()
finalTrace :: Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
finalDecision :: Maybe (ThreadId, ThreadAction)
finalDecision :: forall (n :: * -> *) g a.
CResult n g a -> Maybe (ThreadId, ThreadAction)
finalRestore :: forall (n :: * -> *) g a. CResult n g a -> Threads n -> n ()
..} <- Scheduler s
-> MemType
-> Context n s
-> (Threads n -> n ())
-> ModelConc n a
-> n (CResult n s 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 <- Maybe (Either Condition a) -> Either Condition a
forall a. HasCallStack => Maybe a -> a
efromJust (Maybe (Either Condition a) -> Either Condition a)
-> n (Maybe (Either Condition a)) -> n (Either Condition a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ref n (Maybe (Either Condition a))
-> n (Maybe (Either Condition a))
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe (Either Condition a))
finalRef
  (Either Condition a, s, Trace) -> n (Either Condition a, s, Trace)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Either Condition a
out
       , Context n s -> s
forall (n :: * -> *) g. Context n g -> g
cSchedState Context n s
finalContext
       , Seq (Decision, [(ThreadId, Lookahead)], ThreadAction) -> Trace
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
finalTrace
       )
runSnapshot Scheduler s
sched MemType
memtype s
s (WSAT 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 ()
snapContext :: Context n ()
snapRestore :: Threads n -> n ()
snapNext :: ModelConc n a
..} Either Condition a -> ModelConc n a
teardown) = do
  let context :: Context n s
context = s -> Context n () -> Context n s
forall g (n :: * -> *) s. g -> Context n s -> Context n g
fromSnapContext s
s Context n ()
snapContext
  CResult n s a
intermediateResult <- Scheduler s
-> MemType
-> Context n s
-> (Threads n -> n ())
-> ModelConc n a
-> n (CResult n s 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
  let idsrc :: IdSource
idsrc = Context n s -> IdSource
forall (n :: * -> *) g. Context n g -> IdSource
cIdSource (CResult n s a -> Context n s
forall (n :: * -> *) g a. CResult n g a -> Context n g
finalContext CResult n s a
intermediateResult)
  Either Condition a
out1 <- Maybe (Either Condition a) -> Either Condition a
forall a. HasCallStack => Maybe a -> a
efromJust (Maybe (Either Condition a) -> Either Condition a)
-> n (Maybe (Either Condition a)) -> n (Either Condition a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ref n (Maybe (Either Condition a))
-> n (Maybe (Either Condition a))
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef (CResult n s a -> Ref n (Maybe (Either Condition a))
forall (n :: * -> *) g a.
CResult n g a -> Ref n (Maybe (Either Condition a))
finalRef CResult n s a
intermediateResult)
  CResult n () a
teardownResult <- Bool -> IdSource -> ModelConc n a -> n (CResult n () a)
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 <- Maybe (Either Condition a) -> Either Condition a
forall a. HasCallStack => Maybe a -> a
efromJust (Maybe (Either Condition a) -> Either Condition a)
-> n (Maybe (Either Condition a)) -> n (Either Condition a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ref n (Maybe (Either Condition a))
-> n (Maybe (Either Condition a))
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef (CResult n () a -> Ref n (Maybe (Either Condition a))
forall (n :: * -> *) g a.
CResult n g a -> Ref n (Maybe (Either Condition a))
finalRef CResult n () a
teardownResult)
  (Either Condition a, s, Trace) -> n (Either Condition a, s, Trace)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Either Condition a
out2
       , Context n s -> s
forall (n :: * -> *) g. Context n g -> g
cSchedState (CResult n s a -> Context n s
forall (n :: * -> *) g a. CResult n g a -> Context n g
finalContext CResult n s a
intermediateResult)
       , Seq (Decision, [(ThreadId, Lookahead)], ThreadAction) -> Trace
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (CResult n s a
-> Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
forall (n :: * -> *) g a.
CResult n g a
-> Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
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 :: 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 ()
snapContext :: Context n ()
snapRestore :: Threads n -> n ()
snapNext :: ModelConc n a
..})     = Context n ()
snapContext
contextFromSnapshot (WSAT 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 ()
snapContext :: Context n ()
snapRestore :: Threads n -> n ()
snapNext :: ModelConc n a
..} 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 ThreadId -> [ThreadId] -> [ThreadId]
forall a. a -> [a] -> [a]
: [ThreadId]
runnable, [ThreadId]
blocked) where
  ([ThreadId]
runnable, [ThreadId]
blocked) = (ThreadId -> Bool) -> [ThreadId] -> ([ThreadId], [ThreadId])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ThreadId -> Bool
isRunnable (Map ThreadId (Thread n) -> [ThreadId]
forall k a. Map k a -> [k]
M.keys Map ThreadId (Thread n)
threads)
  threads :: Map ThreadId (Thread n)
threads = Context n () -> Map ThreadId (Thread n)
forall (n :: * -> *) g. Context n g -> Threads n
cThreads (Snapshot p n a -> Context n ()
forall p (n :: * -> *) a. Snapshot p n a -> Context n ()
contextFromSnapshot Snapshot p n a
snap)
  isRunnable :: ThreadId -> Bool
isRunnable ThreadId
tid = Maybe BlockedOn -> Bool
forall a. Maybe a -> Bool
isNothing (Thread n -> Maybe BlockedOn
forall (n :: * -> *). Thread n -> Maybe BlockedOn
_blocking (Thread n -> Maybe BlockedOn)
-> Maybe (Thread n) -> Maybe BlockedOn
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ThreadId -> Map ThreadId (Thread n) -> Maybe (Thread n)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ThreadId
tid Map ThreadId (Thread 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)
Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
Ref n (Maybe (Either Condition x))
Context n ()
Threads n -> n ()
finalRef :: forall (n :: * -> *) g a.
CResult n g a -> Ref n (Maybe (Either Condition a))
finalContext :: forall (n :: * -> *) g a. CResult n g a -> Context n g
finalTrace :: forall (n :: * -> *) g a.
CResult n g a
-> Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
finalDecision :: forall (n :: * -> *) g a.
CResult n g a -> Maybe (ThreadId, ThreadAction)
finalRestore :: forall (n :: * -> *) g a. CResult n g a -> Threads n -> n ()
finalContext :: Context n ()
finalRef :: Ref n (Maybe (Either Condition x))
finalRestore :: Threads n -> n ()
finalTrace :: Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
finalDecision :: Maybe (ThreadId, ThreadAction)
..} <- Bool -> IdSource -> ModelConc n x -> n (CResult n () x)
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 = Seq (Decision, [(ThreadId, Lookahead)], ThreadAction) -> Trace
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)
finalTrace
  Maybe (Either Condition x)
out <- Ref n (Maybe (Either Condition x))
-> n (Maybe (Either Condition x))
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe (Either Condition x))
finalRef
  Maybe (Either Condition snap, Trace)
-> n (Maybe (Either Condition snap, Trace))
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Either Condition snap, Trace)
 -> n (Maybe (Either Condition snap, Trace)))
-> ((Either Condition snap, Trace)
    -> Maybe (Either Condition snap, Trace))
-> (Either Condition snap, Trace)
-> n (Maybe (Either Condition snap, Trace))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either Condition snap, Trace)
-> Maybe (Either Condition snap, Trace)
forall a. a -> Maybe a
Just ((Either Condition snap, Trace)
 -> n (Maybe (Either Condition snap, Trace)))
-> (Either Condition snap, Trace)
-> n (Maybe (Either Condition snap, Trace))
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 (Context n ()
-> (Threads n -> n ()) -> ModelConc n a -> SimpleSnapshot n a
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 (snap -> Either Condition snap
forall a b. b -> Either a b
Right snap
snap, Trace
trc)
    Just (Left Condition
f) -> (Condition -> Either Condition snap
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 -> String -> (Either Condition snap, Trace)
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 =
  [Invariant n ()]
-> Bool
-> Scheduler ()
-> MemType
-> ()
-> IdSource
-> Int
-> ModelConc n a
-> n (CResult n () a)
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cSchedState :: s
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
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
..} = Context n s
ctx
  { cSchedState = g
  , cInvariants = InvariantContext
    { icActive  = cNewInvariants
    , icBlocked = []
    }
  , 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 = ((a -> Action n) -> Action n) -> Program Basic n a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (((a -> Action n) -> Action n) -> Program Basic n a)
-> (Program Basic n a -> (a -> Action n) -> Action n)
-> Program Basic n a
-> Program Basic n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> Action n) -> Action n) -> (a -> Action n) -> Action n
f (((a -> Action n) -> Action n) -> (a -> Action n) -> Action n)
-> (Program Basic n a -> (a -> Action n) -> Action n)
-> Program Basic n a
-> (a -> Action n)
-> Action n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Program Basic n a -> (a -> Action n) -> Action n
forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc