"take" steals a name from the Prelude, meaning that to use Control.Monad.Conc either requires hiding take, which is uses quite often, or importing qualified, which is annoying.

Control.Concurrent.MVar uses "takeMVar", could something similar be done? (yes)

For consistency with dejafu' et al.

Relaxed memory is needed for accurately testing primitives like compare-and-swap and modifyIORef (NOT atomicModifyIORef).

As relaxed memory only shows itself in reads, it seems that the best way to do this would be to record a set of possible values for fields, and return one of them on a read. The value returned would also need to be recorded in the trace. When a barrier is encountered, all of these sets would need to be resolved to a consistent state.

Multiple memory models could be available, and affect how these sets change when loads and stores are performed. This would allow keeping the current behaviour by specifying a sequentially-consistent model. Other interesting models are TSO and PSO (and perhaps others?).

POR for exceptions is really bad, as throwing an exception to a thread conflicts with everything. This is definitely the worst case, but surely this can be improved upon with knowledge of what types of exceptions a thread is prepared to catch, and its masking state.

For example, throwing an exception to a thread with an uninterruptible mask: it doesn't matter where exactly inside the masked chunk it gets delivered, as the same thing will happen in every case, the throwing thread is blocked and the receiving thread continues as normal.

Type synonyms which could result in breakage should be newtypes.

Global deadlock is detected when all threads are blocked, but more generally a collection of threads are deadlocked when they are all blocked on the same CVar which no thread outside of the collection has a reference to. This is probably impossible to solve at the level of Haskell, as it's a GC problem.

• Add warning to documentation
• Maybe have a deadlock-timeout as a parameter to the runner, where if a collection of threads are blocked on the same CVar for longer than it deadlock is assumed?

This allows a potentially huge shortcut to be taken when determining outcome of testing: if an execution with n pre-emptions exhibits a bug, we can skip all child executions of that one on the assumption that they will exhibit the same bug.

Need to see how this behaves in practice, but I expect it will vastly speed up testing where a bug is present.

One of the major design motivators has been keeping the interface similar to what already exists, so it would definitely be good to implement some sort of automated instrumentation of existing code, with warnings printed where automated translation is not possible.

Two changes:

• Don't pick the first "todo" in findSchedulePrefix, instead take an index and interpret that modulo the size of the (partitioned) possibilities.
• Take an optional execution limit. Terminate when this is reached, or when there are no "todo"s remaining.

Like PCT, but worse. However, implementing this with the dpor machinery will at least prevent duplicate schedules from being tried.

Combination of bug and enhancement because there are two issues involved here:

• cBacktrack (https://github.com/barrucadu/dejafu/blob/master/dejafu/Test/DejaFu/SCT.hs#L176) doesn't work if there are no bounds set; it won't add backtracking points
• Need to write a new backtracking function for unbounded DPOR

Can probably also factor out the backtrack-adding code from pbBacktrack, fBacktrack, and lBacktrack to achieve this.

Currently the only not-immediately-trivial example is the logger, it would be nice to have more (and maybe rename "tests" to "examples", and drop the trivial ones).

Avoid making decisions which would exceed the bound.

As stack test dejafu and cabal test dejafu don't work becasue Cabal-the-library is naff (commercialhaskell/stack#1122), there should really be a separate dejafu-tests package to avoid confusing people.

As I'm now pulling that in for the test suite so that QuickCheck can be used, it might be nice to provide a test-framework-dejafu package as a first-class citizen, rather than go via HUnit.

Add an equivalent of IORef: non-blocking, always-full, mutable state.

Unfortunately, the documentation states that IORef operations can appear out-of-order on some processor architectures (eg, x86), and testing this would be rather tricky. There are a few solutions:

• Ignore the problem completely, and add a warning to the documentation that out-of-order cases just aren't tested for.
• Test up to some number of actions offset, and add a warning to the documentation that out-of-order cases may be found (makes testing of IORef-intensive things slower).
• Test with full generality, only constraining things by the barrier imposed by atomicModifyIORef (makes testing of IORef-intensive things much slower).

(note: talk to Mike Dodds about this)

CTMVars can be used to implement CVars if the transactions are small enough, so given that the MonadSTM machinery is now in place and working, it seems silly to have a separate CVar implementation. Unfortunately, they can't be dropped entirely, as otherwise we lose the ability to distinguish between CVar deadlock and CTVar deadlock, but that should be able to be resolved by slightly extending the STM blocking code.

MVars can be equated, CVars can't (necessarily). It would be nice to make this possible.

Sadly, this doesn't work:

class (Monad m, Eq (CVar m a)) => MonadConc m where
  type CVar m :: * -> *

Because the a isn't in scope. Is there some way to have universally-quantified type variables in constraints?

Citing from http://hydra.cryp.to/build/1128096/log/raw:

Preprocessing test suite 'tests' for dejafu-0.1.0.0...

tests/Tests.hs:6:18:
    Could not find module ‘Tests.Cases’
    Use -v to see a list of the files searched for.

tests/Tests.hs:7:18:
    Could not find module ‘Tests.Logger’
    Use -v to see a list of the files searched for.

The STM constructor in ThreadAction could include a trace of what the transaction did. This would probably be very useful for debugging transaction-heavy applications.

The _concMessage action is purely for adding information to the test execution trace and cannot influence the actual results in any way, so we can probably make use of that fact to improve the POR somehow.

It's not a great solution to the problem, clutters execution traces, and I've not actually had a case where it was essential yet. It was more useful when I only did schedule bounding, as then anything to prune extra schedules was good, but the current partial-order reduction is good enough to render it unnecessary.

Every module in the Control.Concurrent hierarchy in base and stm should be available in classy form.

This only has one execution:

{-# LANGUAGE FlexibleContexts #-}

module Terminal where

import Control.Monad.Monitor
import Control.Monad.Monitor.Property
import Control.Concurrent.Classy
import Control.Monad

data Event = Waiting Int | Trying Int deriving (Eq, Ord, Show)

prop :: Int -> Property Event
prop i = Exists (globally waiting) `SAnd`
         Exists (finally trying)   `SAnd`
         All (globally waiting `POr` finally trying)
  where
    waiting = Event (Waiting i)
    trying  = Event (Trying i)

server :: (MonadConc m, MonadMonitor Event m) => MVar m Char -> Lock m -> Int -> m ()
server charVar lock i = do
  addProperty (show i) (prop i)
  forever $ do
    -- Wait for input
    char <- withEvent (Waiting i) (takeMVar charVar)

    -- Wait for the lock
    withEvent (Trying i) (takeLock lock)

    -- Print the output
    -- liftIO (putChar char)

    -- Release the lock
    releaseLock lock

testCase :: (MonadConc m, MonadMonitor Event m) => m ()
testCase = do
  charVar <- newEmptyMVar
  lock    <- newLock

  -- Start some servers
  mapM_ (fork . server charVar lock) [0]

  -- Send some input
  mapM_ (putMVar charVar) "a"

type Lock m = MVar m ()

newLock :: MonadConc m => m (Lock m)
newLock = newMVar ()

takeLock :: MonadConc m => Lock m -> m ()
takeLock = takeMVar

releaseLock :: MonadConc m => Lock m -> m ()
releaseLock lock = putMVar lock ()

Surely there are more: the main thread stopping should be preemptable by the server thread. That doesn't exceed any bounds, so it should show up. Need to add tests to dpor to see if the breakage is there, or somewhere in dejafu.

A nice tutorial in the README, showing how to write a thing with (or port a thing to) MonadConc and test with DejaFu.

Now that I'm using a typeclass abstraction for mutable references, all the code to actually run things should be polymorphic over the monad.

This also fixes an issue where I keep needing unsafeCoerce to work around the universal quantification in ST t because I am already doing the runST elsewhere. Everything should be in ST t with the caller doing runST where necessary.

This is just a fanciful idea, floating in a nice blue sky, but it would be rather nice.

• A MonadSTM class and CTVar type.
• Every MonadConc has an associated MonadSTM, and can run transactions atomically.
• Testing handles getting blocked on STM actions, rolling them back, and reports STM deadlock differently to CVar deadlock.

Why? Well, STM is probably the main go-to for new concurrent Haskell stuff now. It's just so much more convenient and easy than using IORefs or MVars directly, so the natural complaint about DejaFu is "well, this is nice, but what if I'm using atomic transactions in the STM monad instead?"

This is just a wart.

Gives rise to a slight complication when doing pre-emption bounding, as yield lets you have one free pre-emption.

This one is tricky, as it requires changes to atomic-primops to make this possible. Specifically, a type-class abstraction. @rrnewton seems ok with this, and I have a preliminary implementation here, although I'm sure things could be improved.

Ties into #15 very intimately.

We should have this operation, and have it return false.

forkIO returns the ID of the thread produced, and there are a few actions on thread IDs (eg, throwing an exception to a thread). So, the MonadConc interface should support this.

This would require adding a ThreadId type to the MonadConc typeclass. Unfortunately, GHC-ThreadIds support Eq, Ord, and Show, but there isn't a way to add constraints to type families. Would this require the use of MPTCs and FunDeps? Seems a bit of a shame as I got rid of those.

Currently, for ease of implementation, a context switch after a commit is not counted as a preemption in any circumstances. This is bad, because it means in very relaxed test cases, threads get lots of free preemptions, which is defeating the point of preemption bounding. More seriously, I wonder if this is what introduces the extra results seen in f3457b2 and 29150d0.

The fix is to count the context switch as a preemption if it is not a switch back to the thread which was executing before the commit.

Currently POR doesn't take blocking into account. For example, if we have the situation where two actions are dependent, but the thread which performs the later action is blocked, then there is no point adding a backtracking point if the former thread is the one which unblocks it, I think.

1. Rename everything to be more in line with the IO variants. This is mostly the case for functions, but the type families could do with some renaming.
2. Remodularise everything so it's easier to change existing imports.

An uncaught exception only kills its thread, and exceptions can be thrown to a thread, killing it. Furthermore, actions can be registered which are called when a thread is killed.

In DejaFu, however, an exception during testing would kill everything. This should be fixed, and the missing thread operations should be added to MonadConc.

Depends on #3.

(note: read Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell - SPJ)

dejafus runs the computation for every test, if it's expensive this takes some time. It should instead run the computation once, producing a lazy list of all results up to the bound, which the predicates are then applied to.

E.g., this straightforward dining philosophers implementation: https://github.com/jwaldmann/dejafu/blob/master/dejafu/examples/Diner.hs has

 forM [1..n] $ \ p ->
    (if p < n then void . forkIO else id ) $ forever $ do

and when I run it under dejavu, nothing happens for a long time (for n >= 2), while I would hope the deadlock is detected.

No other runnable threads with a reference to the thing blocked on is too loose. The condition should be: no other threads with a reference to the thing which are not blocked on (a) the same variable, or (b) a thread blocked on the same variable (eg, in throwTo)

The probabilistic concurrency testing (PCT) algorithm [Burckhardt et al. 2010] is an-
other controlled scheduling technique that repeatedly executes a multithreaded pro-
gram using a randomized priority-based scheduler, where the highest priority thread
that is enabled is scheduled. The initial thread priorities are chosen randomly, as are
d − 1 priority change points. Importantly, the depth of each change point (the number
of execution steps before the change point causing the currently executed thread to be
lowered) is chosen uniformly over the length of the execution. Given a program with
n threads, at most k execution steps and a bug that requires d ordering constraints to
manifest, PCT guarantees that it will find the bug in a single execution with proba-
bility 1/nk d−1 [Burckhardt et al. 2010]. We refer to PCT as being non-systematic (i.e.
non-exhaustive), because the same schedule could be explored more than once and
schedules are not exhaustively enumerated in some order. However, PCT is still a con-
trolled technique: because all scheduling nondeterminism is controlled, the schedule to
be executed is precisely determined by the PCT algorithm and not by the OS scheduler.
Thus, buggy schedules can still be recorded and replayed precisely, as with SCT.

Two tricky aspects:

• dpor library currently has no facility for randomness.
• The threads aren't known up-front (maybe the paper covers this), so priorities would need to be assigned at fork time.

This way the MonadConc and MonadSTM stuff will be in "Test.DejaFu.{Conc,STM}", and "Test.DejaFu.Common" (or whatever) will have all the common things.

The current SCT implementation is fairly tightly coupled with the rest of dejafu, but this doesn't need to be the case. Given execution/dependency functions, the actual algorithm can be (should be able to be) fairly generic and suitable for re-use in other cases. This would make it possible to re-use this machinery in other contexts: like the execution of distributed systems.

It would also allow for more experimentation on the SCT front (eg: adding optional randomness) without either (a) sacrificing completeness even more in dejafu or (b) adding yet more variants of the dejafu/autocheck functions to Test.DejaFu.

• setNumCapabilities
• threadCapability

threadCapability might be tricky, as it introduces another source of nondeterminism. Might be best to not support that one.

Basically done, but filing an issue so I remember to check documentation and READMEs

One big disadvantage of dejafu is the additional load of dependencies. Control.Concurrent is in base, it's hard to get more lightweight than that. And yet, if you want to use MonadConc, and not even do any testing, you incur the following additional dependencies:

1. dejafu
2. array
3. atomic-primops
4. containers
5. deepseq
6. dpor
7. exceptions
8. monad-control
9. monad-loops
10. mtl
11. semigroups
12. stm
13. template-haskell
14. transformers
15. transformers-base

And all of their dependencies (some of which are massive, like text for semigroups). Some of these are used in the typeclass modules, but a lot of this is only used by the testing code. It's unreasonably heavyweight. It's fine for a testsuite to opt in to additional dependencies, but this is a bit much for everyday library and executable use.

So, should I make a separate "concurrency" module which (in addition to claiming a very sweet name on hackage) would have a far lighter load of dependencies?

Basically done, but filing an issue to remember to check docs and README.

To include in docs: differences from async and why.

This will always return Right ():

test :: MonadConc m => m (Either SomeException ())
test = do
  v <- newEmptyCVar
  t <- mask $ \restore -> fork $ try (restore $ return ()) >>= putCVar v
  killThread t
  readCVar v

This is because return is invisible as far as dejafu is concerned, there isn't a corresponding primitive action, as the monad instances for Conc and ConcIO are built on that of Cont.

In order to be able to pre-empt a return, a new primitive action is needed and the monad instance must be changed.

Kind of essential with #16

No point using a memory model which is less accurate!