dejafu-2.4.0.0: A library for unit-testing concurrent programs.

Copyright (c) 2019 Michael Walker MIT Michael Walker experimental CPP, FlexibleContexts, FlexibleInstances, GADTs, LambdaCase, RecordWildCards, TypeFamilies None Haskell2010

Test.DejaFu.Conc.Internal.Program

Contents

Description

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

# 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 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)


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)

good_snapshot2 = withSetup
(do r <- liftIO (newIORef 0)
liftIO (writeIORef r 0)
liftIO (modifyIORef r (+1))
pure r)


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

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 Source #

Constructors

 SimpleSnapshot FieldssnapContext :: Context n () snapRestore :: Threads n -> n () snapNext :: ModelConc n a

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

Get the Context from a Snapshot.

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 #