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 |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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.
Synopsis
- runConcurrent :: MonadDejaFu n => Scheduler s -> MemType -> s -> Program pty n a -> n (Either Condition a, s, Trace)
- recordSnapshot :: MonadDejaFu n => Program pty n a -> n (Maybe (Either Condition (Snapshot pty n a), Trace))
- runSnapshot :: MonadDejaFu n => Scheduler s -> MemType -> s -> Snapshot pty n a -> n (Either Condition a, s, Trace)
- 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 {
- snapContext :: Context n ()
- snapRestore :: Threads n -> n ()
- snapNext :: ModelConc n a
- contextFromSnapshot :: Snapshot p n a -> Context n ()
- threadsFromSnapshot :: Snapshot p n a -> ([ThreadId], [ThreadId])
- defaultRecordSnapshot :: MonadDejaFu n => (SimpleSnapshot n a -> x -> snap) -> ModelConc n x -> (x -> ModelConc n a) -> n (Maybe (Either Condition snap, Trace))
- simpleRunConcurrency :: (MonadDejaFu n, HasCallStack) => Bool -> IdSource -> ModelConc n a -> n (CResult n () a)
- fromSnapContext :: g -> Context n s -> Context n g
- wrap :: (((a -> Action n) -> Action n) -> (a -> Action n) -> Action n) -> ModelConc n a -> ModelConc n a
Documentation
runConcurrent :: MonadDejaFu n => Scheduler s -> MemType -> s -> Program pty n a -> n (Either Condition a, s, Trace) Source #
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)) Source #
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
runSnapshot :: MonadDejaFu n => Scheduler s -> MemType -> s -> Snapshot pty n a -> n (Either Condition a, s, Trace) Source #
Runs a program with snapshotted setup to completion.
Since: 2.1.0.0
data Snapshot pty n a where Source #
A record of the state of a concurrent program immediately after completing the setup action.
Since: 2.0.0.0
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 Source #
SimpleSnapshot | |
|
threadsFromSnapshot :: Snapshot p n a -> ([ThreadId], [ThreadId]) Source #
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)) Source #
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) Source #
Run a concurrent program with a deterministic scheduler in snapshotting or non-snapshotting mode.
fromSnapContext :: g -> Context n s -> Context n g Source #
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 Source #
Orphan instances
pty ~ Basic => MonadTrans (Program pty) Source # | |
(pty ~ Basic, MonadIO n) => MonadIO (Program pty n) Source # | |
(pty ~ Basic, Monad n) => MonadConc (Program pty n) Source # | |
type STM (Program pty n) :: Type -> Type # type MVar (Program pty n) :: Type -> Type # type IORef (Program pty n) :: Type -> Type # 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)) # 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 () # getMaskingState :: Program pty n MaskingState # unsafeUnmask :: Program pty n a -> Program pty n a # | |
pty ~ Basic => MonadCatch (Program pty n) Source # | |
pty ~ Basic => MonadMask (Program pty n) Source # | |
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) # | |
pty ~ Basic => MonadThrow (Program pty n) Source # | |