A representation of a concurrent program for testing.

To construct these, use the MonadConc instance, or see withSetup, withTeardown, and withSetupAndTeardown.

Since: 2.0.0.0

A type used to constrain Program: a Program Basic is a "basic" program with no set-up or teardown.

Construct with the MonadConc instance.

Since: 2.0.0.0

Since: 1.4.0.0

A MonadConc implementation using IO.

Since: 0.4.0.0

A type used to constrain Program: a Program (WithSetup x) is a program with some set-up action producing a value of type x.

Construct with withSetup.

Since: 2.0.0.0

A type used to constrain Program: a Program (WithSetupAndTeardown x y) is a program producing a value of type y with some set-up action producing a value of type x and a teardown action producing the final result.

Construct with withTeardown or withSetupAndTeardown.

Since: 2.0.0.0

A concurrent program with some set-up action.

In terms of results, this is the same as setup >>= program. However, the setup action will be snapshotted (see recordSnapshot and runSnapshot) by the testing functions. This means that even if dejafu runs this program many many times, the setup action will only be run the first time, and its effects remembered for subsequent executions.

Since: 2.0.0.0

A concurrent program with some set-up and teardown actions.

This is similar to

do
  x <- setup
  y <- program x
  teardown x y

But with two differences:

• The setup action can be snapshotted, as described for withSetup
• The teardown action will be executed even if the main action fails to produce a value.

Since: 2.0.0.0

A combination of withSetup and withTeardown for convenience.

withSetupAndTeardown setup teardown =
  withTeardown teardown . withSetup setup

Since: 2.0.0.0

Invariants are atomic actions which can inspect the shared state of your computation, and terminate it on failure. Invariants have no visible effects, and are checked after each scheduling point.

To be checked, an invariant must be created during the setup phase of your Program, using registerInvariant. The invariant will then be checked in the main phase (but not in the setup or teardown phase). As a consequence of this, any shared state you want your invariant to check must also be created in the setup phase, and passed into the main phase as a parameter.

Since: 2.0.0.0

Call this in the setup phase to register new invariant which will be checked after every scheduling point in the main phase. Invariants are atomic actions which can inspect the shared state of your computation.

If the invariant throws an exception, the execution will be aborted with n InvariantFailure. Any teardown action will still be run.

Since: 2.0.0.0

Read the content of an IORef.

This returns the globally visible value, which may not be the same as the value visible to any particular thread when using a memory model other than SequentialConsistency.

Since: 2.0.0.0

Read the content of an MVar.

This is essentially tryReadMVar.

Since: 2.0.0.0

Read the content of a TVar.

This is essentially readTVar.

Since: 2.0.0.0

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

Since: 2.0.0.0

The memory model to use for non-synchronised IORef operations.

Since: 0.4.0.0

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

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

Runs a program with snapshotted setup to completion.

Since: 2.1.0.0

An indication of how a concurrent computation terminated, if it didn't produce a value.

The Eq, Ord, and NFData instances compare/evaluate the exception with show in the UncaughtException and InvariantFailure cases.

Since: 2.0.0.0

One of the outputs of the runner is a Trace, which is a log of decisions made, all the alternative unblocked threads and what they would do, and the action a thread took in its step.

Since: 0.8.0.0

Scheduling decisions are based on the state of the running program, and so we can capture some of that state in recording what specific decision we made.

Since: 0.5.0.0

Every thread has a unique identitifer.

Since: 1.0.0.0

All the actions that a thread can perform.

Since: 2.2.0.0

A one-step look-ahead at what a thread will do next.

Since: 2.2.0.0

Every MVar has a unique identifier.

Since: 1.0.0.0

Every IORef has a unique identifier.

Since: 1.11.0.0

Describes the behaviour of a thread when an asynchronous exception is received.

Pretty-print a trace, including a key of the thread IDs (not including thread 0). Each line of the key is indented by two spaces.

Since: 0.5.0.0

Pretty-print a condition

Since: 1.12.0.0