Test.DejaFu.Conc.Internal.Program

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.

Documentation

runConcurrent :: MonadDejaFu n => Scheduler s -> MemType -> s -> Program pty n a -> n (Either Condition a, s, Trace)

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

recordSnapshot :: MonadDejaFu n => Program pty n a -> n (Maybe (Either Condition (Snapshot pty n a), Trace))

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 IORefs, MVars, and TVars, 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

runSnapshot :: MonadDejaFu n => Scheduler s -> MemType -> s -> Snapshot pty n a -> n (Either Condition a, s, Trace)

Runs a program with snapshotted setup to completion.

Since: 2.1.0.0

data Snapshot pty n a where

A record of the state of a concurrent program immediately after completing the setup action.

Since: 2.0.0.0

Constructors

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

Constructors

SimpleSnapshot

Fields

• snapContext :: Context n ()
• snapRestore :: Threads n -> n ()
• snapNext :: ModelConc n a

contextFromSnapshot :: Snapshot p n a -> Context n ()

Get the Context from a Snapshot.

threadsFromSnapshot :: Snapshot p n a -> ([ThreadId], [ThreadId])

Get the threads which exist in a snapshot, partitioned into runnable and not runnable.

defaultRecordSnapshot :: MonadDejaFu n => (SimpleSnapshot n a -> x -> snap) -> ModelConc n x -> (x -> ModelConc n a) -> n (Maybe (Either Condition snap, Trace))

recordSnapshot implemented generically.

Throws an error if the snapshot could not be produced.

simpleRunConcurrency :: (MonadDejaFu n, HasCallStack) => Bool -> IdSource -> ModelConc n a -> n (CResult n () a)

Run a concurrent program with a deterministic scheduler in snapshotting or non-snapshotting mode.

fromSnapContext :: g -> Context n s -> Context n g

Make a new context from a snapshot context.

wrap :: (((a -> Action n) -> Action n) -> (a -> Action n) -> Action n) -> ModelConc n a -> ModelConc n a

Orphan instances

pty ~ Basic => MonadTrans (Program pty)

Methods

lift :: Monad m => m a -> Program pty m a

(pty ~ Basic, MonadIO n) => MonadIO (Program pty n)

Methods

liftIO :: IO a -> Program pty n a

(pty ~ Basic, Monad n) => MonadConc (Program pty n)

Associated Types

type STM (Program pty n) :: Type -> Type

type MVar (Program pty n) :: Type -> Type

type IORef (Program pty n) :: Type -> Type

type Ticket (Program pty n) :: Type -> Type

type ThreadId (Program pty n) :: Type

Methods

forkWithUnmask :: ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

forkWithUnmaskN :: String -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

forkOnWithUnmask :: Int -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

forkOnWithUnmaskN :: String -> Int -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

forkOSWithUnmask :: ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

forkOSWithUnmaskN :: String -> ((forall a. Program pty n a -> Program pty n a) -> Program pty n ()) -> Program pty n (ThreadId (Program pty n))

supportsBoundThreads :: Program pty n Bool

isCurrentThreadBound :: Program pty n Bool

getNumCapabilities :: Program pty n Int

setNumCapabilities :: Int -> Program pty n ()

myThreadId :: Program pty n (ThreadId (Program pty n))

yield :: Program pty n ()

threadDelay :: Int -> Program pty n ()

newEmptyMVar :: Program pty n (MVar (Program pty n) a)

newEmptyMVarN :: String -> Program pty n (MVar (Program pty n) a)

putMVar :: MVar (Program pty n) a -> a -> Program pty n ()

tryPutMVar :: MVar (Program pty n) a -> a -> Program pty n Bool

readMVar :: MVar (Program pty n) a -> Program pty n a

tryReadMVar :: MVar (Program pty n) a -> Program pty n (Maybe a)

takeMVar :: MVar (Program pty n) a -> Program pty n a

tryTakeMVar :: MVar (Program pty n) a -> Program pty n (Maybe a)

newIORef :: a -> Program pty n (IORef (Program pty n) a)

newIORefN :: String -> a -> Program pty n (IORef (Program pty n) a)

readIORef :: IORef (Program pty n) a -> Program pty n a

atomicModifyIORef :: IORef (Program pty n) a -> (a -> (a, b)) -> Program pty n b

writeIORef :: IORef (Program pty n) a -> a -> Program pty n ()

atomicWriteIORef :: IORef (Program pty n) a -> a -> Program pty n ()

readForCAS :: IORef (Program pty n) a -> Program pty n (Ticket (Program pty n) a)

peekTicket' :: Proxy (Program pty n) -> Ticket (Program pty n) a -> a

casIORef :: IORef (Program pty n) a -> Ticket (Program pty n) a -> a -> Program pty n (Bool, Ticket (Program pty n) a)

modifyIORefCAS :: IORef (Program pty n) a -> (a -> (a, b)) -> Program pty n b

modifyIORefCAS_ :: IORef (Program pty n) a -> (a -> a) -> Program pty n ()

atomically :: STM (Program pty n) a -> Program pty n a

newTVarConc :: a -> Program pty n (TVar (STM (Program pty n)) a)

readTVarConc :: TVar (STM (Program pty n)) a -> Program pty n a

throwTo :: Exception e => ThreadId (Program pty n) -> e -> Program pty n ()

pty ~ Basic => MonadThrow (Program pty n)

Methods

throwM :: Exception e => e -> Program pty n a

pty ~ Basic => MonadCatch (Program pty n)

Methods

catch :: Exception e => Program pty n a -> (e -> Program pty n a) -> Program pty n a

pty ~ Basic => MonadMask (Program pty n)

Methods

mask :: ((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) -> Program pty n b

generalBracket :: Program pty n a -> (a -> ExitCase b -> Program pty n c) -> (a -> Program pty n b) -> Program pty n (b, c)