Merge pull request #157 from barrucadu/next-supermajor

The Big 1.0

.weeder.yaml

@@ -109,7 +109,7 @@
       - module:
         - name: Examples.ClassLaws
         - identifier:
-          - CST
+          - C
           - Concurrently
           - concurrently
           - concurrently'

CONTRIBUTING.markdown

@@ -164,6 +164,7 @@ dejafusIO = dejafusWayIO defaultWay defaultMemType
 - moving a definition to a different module is an API change
 - version numbers will be filled in when a release is made, using
   "@since unreleased" makes it easy to find the necessary places
+- internal things don't need an `@since` comment
 
 **If the change is visible to end-users** add an entry to the relevant
 change log in the "unreleased" section. if there is no "unreleased"

README.markdown

@@ -45,10 +45,10 @@ There are a few different packages under the Déjà Fu umbrella:
 
 |   | Version | Summary |
 | - | ------- | ------- |
-| [concurrency][h:conc]    | 1.2.3.0 | Typeclasses, functions, and data types for concurrency and STM. |
-| [dejafu][h:dejafu]       | 0.9.1.2 | Systematic testing for Haskell concurrency. |
-| [hunit-dejafu][h:hunit]  | 0.7.1.1 | Deja Fu support for the HUnit test framework. |
-| [tasty-dejafu][h:tasty]  | 0.7.1.1 | Deja Fu support for the Tasty test framework. |
+| [concurrency][h:conc]    | 1.3.0.0 | Typeclasses, functions, and data types for concurrency and STM. |
+| [dejafu][h:dejafu]       | 1.0.0.0 | Systematic testing for Haskell concurrency. |
+| [hunit-dejafu][h:hunit]  | 1.0.0.0 | Deja Fu support for the HUnit test framework. |
+| [tasty-dejafu][h:tasty]  | 1.0.0.0 | Deja Fu support for the Tasty test framework. |
 
 Each package has its own README and CHANGELOG in its subdirectory.
 
@@ -71,7 +71,7 @@ Installation
 Install from Hackage globally:
 
 ```
-$ cabal-install dejafu
+$ cabal install dejafu
 ```
 
 Or add it to your cabal file:
@@ -112,12 +112,12 @@ we'll get onto that shortly.  First, the result of testing:
 
 ```
 > autocheck myFunction
-[pass] Never Deadlocks (checked: 12)
-[pass] No Exceptions (checked: 12)
-[fail] Consistent Result (checked: 11)
-        "hello" S0----S1-P2-S0--
+[pass] Never Deadlocks
+[pass] No Exceptions
+[fail] Consistent Result
+        "hello" S0----S1--S0--
 
-        "world" S0----S2--S0-P1-S0-
+        "world" S0----S2--S0--
 False
 ```
 
@@ -145,10 +145,10 @@ These approaches are inadequate for a few reasons:
 - **How do you know if you've fixed a bug you saw previously?**
   Because the scheduler is a black box, you don't know if the
   previously buggy schedule has been re-run.
-- **You won't actually get that much scheduling variety!** Operating
-  systems and language runtimes like to run threads for long periods
-  of time, which reduces the variety you get (and so drives up the
-  number of runs you need).
+- **You won't get that much scheduling variety!** Operating systems
+  and language runtimes like to run threads for long periods of time,
+  which reduces the variety you get (and so drives up the number of
+  runs you need).
 
 Déjà Fu addresses these points by offering *complete* testing.  You
 can run a test case and be guaranteed to find all results with some

concurrency/CHANGELOG.markdown

@@ -7,6 +7,36 @@ This project is versioned according to the [Package Versioning Policy](https://p
 *de facto* standard Haskell versioning scheme.
 
 
+1.3.0.0
+-------
+
+- **Date**    unreleased
+- **Git tag** [concurrency-1.3.0.0][]
+- **Hackage** https://hackage.haskell.org/package/concurrency-1.3.0.0
+
+### Control.Concurrent.Classy.Async
+
+- New `asyncBound`, `asyncBoundN`, `withAsyncBound`, and `withAsyncBoundN` functions for doing
+  asynchronous actions on bound threads. (#126)
+
+### Control.Monad.Conc.Class
+
+- `MonadConc` now supports bound threads with new `forkOS`, `forkOSN`, and `isCurrentThreadBound`
+  functions. (#126)
+
+- New `runInBoundThread` and `runInUnboundThread` functions. (#126)
+
+- The `rtsSupportsBoundThreads` definition is now the definition from Control.Concurrent
+  re-exported, not just `False`. (#126)
+
+Note that bound threads are only supported if you compile with GHC and link with -threaded.
+
+[concurrency-1.3.0.0]: https://github.com/barrucadu/dejafu/releases/tag/concurrency-1.3.0.0
+
+
+---------------------------------------------------------------------------------------------------
+
+
 1.2.3.0
 -------
 

concurrency/Control/Concurrent/Classy/Async.hs

@@ -1,7 +1,15 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE RankNTypes #-}
 
--- | This module is a version of the
+-- |
+-- Module      : Control.Concurrent.Classy.Async
+-- Copyright   : (c) 2016--2017 Michael Walker
+-- License     : MIT
+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
+-- Stability   : stable
+-- Portability : CPP, RankNTypes
+--
+-- This module is a version of the
 -- <https://hackage.haskell.org/package/async async> package. It
 -- provides a set of operations for running @MonadConc@ operations
 -- asynchronously and waiting for their results.
@@ -18,14 +26,9 @@
 -- The 'withAsync' function starts an operation in a separate thread,
 -- and kills it if the inner action finishes before it completes.
 --
--- There are a few deviations from the regular async package:
---
---   * 'asyncBound' and 'withAsyncBound' are missing as @MonadConc@
---   does not support bound threads.
---
---   * The @Alternative@ instance for 'Concurrently' uses @forever
---   yield@ in the definition of @empty@, rather than @forever
---   (threadDelay maxBound)@.
+-- Unlike the regular async package, the @Alternative@ instance for
+-- 'Concurrently' uses @forever yield@ in the definition of @empty@,
+-- rather than @forever (threadDelay maxBound)@.
 module Control.Concurrent.Classy.Async
   ( -- * Asynchronous actions
     Async
@@ -33,6 +36,8 @@ module Control.Concurrent.Classy.Async
   -- * Spawning
   , async
   , asyncN
+  , asyncBound
+  , asyncBoundN
   , asyncOn
   , asyncOnN
   , asyncWithUnmask
@@ -43,6 +48,8 @@ module Control.Concurrent.Classy.Async
   -- * Spawning with automatic 'cancel'ation
   , withAsync
   , withAsyncN
+  , withAsyncBound
+  , withAsyncBoundN
   , withAsyncOn
   , withAsyncOnN
   , withAsyncWithUnmask
@@ -192,6 +199,19 @@ async = asyncUsing fork
 asyncN :: MonadConc m => String -> m a -> m (Async m a)
 asyncN name = asyncUsing (forkN name)
 
+-- | Like 'async' but uses 'forkOS' internally.
+--
+-- @since 1.3.0.0
+asyncBound :: MonadConc m => m a -> m (Async m a)
+asyncBound = asyncUsing forkOS
+
+-- | Like 'asyncBound', but using a named thread for better debugging
+-- information.
+--
+-- @since 1.3.0.0
+asyncBoundN :: MonadConc m => String -> m a -> m (Async m a)
+asyncBoundN name = asyncUsing (forkOSN name)
+
 -- | Like 'async' but using 'forkOn' internally.
 --
 -- @since 1.1.1.0
@@ -266,6 +286,19 @@ withAsync = withAsyncUsing fork
 withAsyncN :: MonadConc m => String -> m a -> (Async m a -> m b) -> m b
 withAsyncN name = withAsyncUsing (forkN name)
 
+-- | Like 'withAsync' but uses 'forkOS' internally.
+--
+-- @since 1.3.0.0
+withAsyncBound :: MonadConc m => m a -> (Async m a -> m b) -> m b
+withAsyncBound = withAsyncUsing forkOS
+
+-- | Like 'withAsyncBound' but using a named thread for better
+-- debugging information.
+--
+-- @since 1.3.0.0
+withAsyncBoundN :: MonadConc m => String -> m a -> (Async m a -> m b) -> m b
+withAsyncBoundN name = withAsyncUsing (forkOSN name)
+
 -- | Like 'withAsync' but uses 'forkOn' internally.
 --
 -- @since 1.1.1.0

concurrency/Control/Concurrent/Classy/CRef.hs

@@ -48,28 +48,28 @@ module Control.Concurrent.Classy.CRef
   --
   -- We can see this by testing with different memory models:
   --
-  -- > > autocheck' SequentialConsistency crefs
-  -- > [pass] Never Deadlocks (checked: 6)
-  -- > [pass] No Exceptions (checked: 6)
-  -- > [fail] Consistent Result (checked: 5)
-  -- >         (False,True) S0-------S1-----S0--S2-----S0---
-  -- >         (True,False) S0-------S1-P2-----S1----S0----
-  -- >         (True,True) S0-------S1--P2-----S1---S0----
-  -- >         (False,True) S0-------S1---P2-----S1--S0----
-  -- >         (True,False) S0-------S2-----S1-----S0----
-  -- >         ...
+  -- > > autocheckWay defaultWay SequentialConsistency relaxed
+  -- > [pass] Never Deadlocks
+  -- > [pass] No Exceptions
+  -- > [fail] Consistent Result
+  -- >        (False,True) S0---------S1----S0--S2----S0--
+  -- >
+  -- >        (True,True) S0---------S1-P2----S1---S0---
+  -- >
+  -- >        (True,False) S0---------S2----S1----S0---
   -- > False
   --
-  -- > > autocheck' TotalStoreOrder crefs
-  -- > [pass] Never Deadlocks (checked: 303)
-  -- > [pass] No Exceptions (checked: 303)
-  -- > [fail] Consistent Result (checked: 302)
-  -- >         (False,True) S0-------S1-----C-S0--S2-----C-S0---
-  -- >         (True,False) S0-------S1-P2-----C-S1----S0----
-  -- >         (True,True) S0-------S1-P2--C-S1----C-S0--S2---S0---
-  -- >         (False,True) S0-------S1-P2--P1--C-C-S1--S0--S2---S0---
-  -- >         (False,False) S0-------S1-P2--P1----S2---C-C-S0----
-  -- >         ...
+  -- > > autocheckWay defaultWay TotalStoreOrder  relaxed
+  -- > [pass] Never Deadlocks
+  -- > [pass] No Exceptions
+  -- > [fail] Consistent Result
+  -- >         (False,True) S0---------S1----S0--S2----S0--
+  -- >
+  -- >         (False,False) S0---------S1--P2----S1--S0---
+  -- >
+  -- >         (True,False) S0---------S2----S1----S0---
+  -- >
+  -- >         (True,True) S0---------S1-C-S2----S1---S0---
   -- > False
   --
   -- Traces for non-sequentially-consistent memory models show where

concurrency/Control/Monad/Conc/Class.hs

@@ -8,7 +8,7 @@
 
 -- |
 -- Module      : Control.Monad.Conc.Class
--- Copyright   : (c) 2016 Michael Walker
+-- Copyright   : (c) 2016--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
@@ -17,16 +17,16 @@
 -- This module captures in a typeclass the interface of concurrency
 -- monads.
 --
--- __Deviations:__ An instance of @MonadConc@ is not required to be
--- an instance of @MonadFix@, unlike @IO@. The @CRef@, @MVar@, and
+-- __Deviations:__ An instance of @MonadConc@ is not required to be an
+-- instance of @MonadFix@, unlike @IO@. The @CRef@, @MVar@, and
 -- @Ticket@ types are not required to be instances of @Show@ or @Eq@,
 -- unlike their normal counterparts. The @threadCapability@,
 -- @threadWaitRead@, @threadWaitWrite@, @threadWaitReadSTM@,
 -- @threadWaitWriteSTM@, and @mkWeakThreadId@ functions are not
 -- provided. The @threadDelay@ function is not required to delay the
--- thread, merely to yield it. Bound threads are not supported. The
--- @BlockedIndefinitelyOnMVar@ (and similar) exceptions are /not/
--- thrown during testing, so do not rely on them at all.
+-- thread, merely to yield it. The @BlockedIndefinitelyOnMVar@ (and
+-- similar) exceptions are /not/ thrown during testing, so do not rely
+-- on them at all.
 module Control.Monad.Conc.Class
   ( MonadConc(..)
 
@@ -35,18 +35,31 @@ module Control.Monad.Conc.Class
   , forkFinally
   , killThread
 
+  -- ** Bound threads
+
+  -- | Support for multiple operating system threads and bound threads
+  -- as described below is currently only available in the GHC runtime
+  -- system if you use the -threaded option when linking.
+  --
+  -- Other Haskell systems do not currently support multiple operating
+  -- system threads.
+  --
+  -- A bound thread is a haskell thread that is bound to an operating
+  -- system thread. While the bound thread is still scheduled by the
+  -- Haskell run-time system, the operating system thread takes care
+  -- of all the foreign calls made by the bound thread.
+  --
+  -- To a foreign library, the bound thread will look exactly like an
+  -- ordinary operating system thread created using OS functions like
+  -- pthread_create or CreateThread.
+  , IO.rtsSupportsBoundThreads
+  , runInBoundThread
+  , runInUnboundThread
+
   -- ** Named Threads
   , forkN
   , forkOnN
 
-  -- ** Bound Threads
-
-  -- | @MonadConc@ does not support bound threads, if you need that
-  -- sort of thing you will have to use regular @IO@.
-
-  , rtsSupportsBoundThreads
-  , isCurrentThreadBound
-
   -- * Exceptions
   , throw
   , catch
@@ -109,7 +122,7 @@ import qualified Control.Monad.Writer.Strict  as WS
 -- Every @MonadConc@ has an associated 'MonadSTM', transactions of
 -- which can be run atomically.
 --
--- @since 1.0.0.0
+-- @since 1.3.0.0
 class ( Applicative m, Monad m
       , MonadCatch m, MonadThrow m, MonadMask m
       , MonadSTM (STM m)
@@ -118,6 +131,8 @@ class ( Applicative m, Monad m
   {-# MINIMAL
         (forkWithUnmask | forkWithUnmaskN)
       , (forkOnWithUnmask | forkOnWithUnmaskN)
+      , (forkOS | forkOSN)
+      , isCurrentThreadBound
       , getNumCapabilities
       , setNumCapabilities
       , myThreadId
@@ -194,10 +209,6 @@ class ( Applicative m, Monad m
   -- | Like 'forkWithUnmask', but the thread is given a name which may
   -- be used to present more useful debugging information.
   --
-  -- If an empty name is given, the @ThreadId@ is used. If names
-  -- conflict, successive threads with the same name are given a
-  -- numeric suffix, counting up from 1.
-  --
   -- > forkWithUnmaskN _ = forkWithUnmask
   --
   -- @since 1.0.0.0
@@ -234,6 +245,35 @@ class ( Applicative m, Monad m
   forkOnWithUnmaskN :: String -> Int -> ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)
   forkOnWithUnmaskN _ = forkOnWithUnmask
 
+  -- | Fork a computation to happen in a /bound thread/, which is
+  -- necessary if you need to call foreign (non-Haskell) libraries
+  -- that make use of thread-local state, such as OpenGL.
+  --
+  -- > forkOS = forkOSN ""
+  --
+  -- @since 1.3.0.0
+  forkOS :: m () -> m (ThreadId m)
+  forkOS = forkOSN ""
+
+  -- | Like 'forkOS', but the thread is given a name which may be used
+  -- to present more useful debugging information.
+  --
+  -- > forkOSN _ = forkOS
+  --
+  -- @since 1.3.0.0
+  forkOSN :: String -> m () -> m (ThreadId m)
+  forkOSN _ = forkOS
+
+  -- | Returns 'True' if the calling thread is bound, that is, if it
+  -- is safe to use foreign libraries that rely on thread-local state
+  -- from the calling thread.
+  --
+  -- This will always be false if your program is not compiled with
+  -- the threaded runtime.
+  --
+  -- @since 1.3.0.0
+  isCurrentThreadBound :: m Bool
+
   -- | Get the number of Haskell threads that can run simultaneously.
   --
   -- @since 1.0.0.0
@@ -249,8 +289,7 @@ class ( Applicative m, Monad m
   -- @since 1.0.0.0
   myThreadId :: m (ThreadId m)
 
-  -- | Allows a context-switch to any other currently runnable thread
-  -- (if any).
+  -- | Allows a context-switch to any other unblocked thread (if any).
   --
   -- @since 1.0.0.0
   yield :: m ()
@@ -279,10 +318,6 @@ class ( Applicative m, Monad m
   -- | Create a new empty @MVar@, but it is given a name which may be
   -- used to present more useful debugging information.
   --
-  -- If an empty name is given, a counter starting from 0 is used. If
-  -- names conflict, successive @MVar@s with the same name are given a
-  -- numeric suffix, counting up from 1.
-  --
   -- > newEmptyMVarN _ = newEmptyMVar
   --
   -- @since 1.0.0.0
@@ -343,10 +378,6 @@ class ( Applicative m, Monad m
   -- | Create a new reference, but it is given a name which may be
   -- used to present more useful debugging information.
   --
-  -- If an empty name is given, a counter starting from 0 is used. If
-  -- names conflict, successive @CRef@s with the same name are given a
-  -- numeric suffix, counting up from 1.
-  --
   -- > newCRefN _ = newCRef
   --
   -- @since 1.0.0.0
@@ -479,10 +510,6 @@ killThread tid = throwTo tid ThreadKilled
 -- | Like 'fork', but the thread is given a name which may be used to
 -- present more useful debugging information.
 --
--- If no name is given, the @ThreadId@ is used. If names conflict,
--- successive threads with the same name are given a numeric suffix,
--- counting up from 1.
---
 -- @since 1.0.0.0
 forkN :: MonadConc m => String -> m () -> m (ThreadId m)
 forkN name ma = forkWithUnmaskN name (const ma)
@@ -490,27 +517,57 @@ forkN name ma = forkWithUnmaskN name (const ma)
 -- | Like 'forkOn', but the thread is given a name which may be used
 -- to present more useful debugging information.
 --
--- If no name is given, the @ThreadId@ is used. If names conflict,
--- successive threads with the same name are given a numeric suffix,
--- counting up from 1.
---
 -- @since 1.0.0.0
 forkOnN :: MonadConc m => String -> Int -> m () -> m (ThreadId m)
 forkOnN name i ma = forkOnWithUnmaskN name i (const ma)
 
--- Bound Threads
-
--- | Provided for compatibility, always returns 'False'.
+-- | Run the computation passed as the first argument.  If the calling
+-- thread is not /bound/, a bound thread is created temporarily.
+-- @runInBoundThread@ doesn't finish until the inner computation
+-- finishes.
 --
--- @since 1.0.0.0
-rtsSupportsBoundThreads :: Bool
-rtsSupportsBoundThreads = False
-
--- | Provided for compatibility, always returns 'False'.
+-- You can wrap a series of foreign function calls that rely on
+-- thread-local state with @runInBoundThread@ so that you can use them
+-- without knowing whether the current thread is /bound/.
 --
--- @since 1.0.0.0
-isCurrentThreadBound :: MonadConc m => m Bool
-isCurrentThreadBound = pure False
+-- @since 1.3.0.0
+runInBoundThread :: MonadConc m => m a -> m a
+runInBoundThread =
+  runInThread (not <$> isCurrentThreadBound) (forkOSN "runInBoundThread")
+
+-- | Run the computation passed as the first argument. If the calling
+-- thread is /bound/, an unbound thread is created temporarily using
+-- @fork@.  @runInBoundThread@ doesn't finish until the inner
+-- computation finishes.
+--
+-- Use this function /only/ in the rare case that you have actually
+-- observed a performance loss due to the use of bound threads. A
+-- program that doesn't need its main thread to be bound and makes
+-- /heavy/ use of concurrency (e.g. a web server), might want to wrap
+-- its @main@ action in @runInUnboundThread@.
+--
+-- Note that exceptions which are thrown to the current thread are
+-- thrown in turn to the thread that is executing the given
+-- computation. This ensures there's always a way of killing the
+-- forked thread.
+--
+-- @since 1.3.0.0
+runInUnboundThread :: MonadConc m => m a -> m a
+runInUnboundThread =
+  runInThread isCurrentThreadBound (forkN "runInUnboundThread")
+
+-- | Helper for 'runInBoundThread' and 'runInUnboundThread'
+runInThread :: MonadConc m => m Bool -> (m () -> m (ThreadId m)) -> m a -> m a
+runInThread check dofork action = do
+  flag <- check
+  if flag
+    then do
+      mv <- newEmptyMVar
+      mask $ \restore -> do
+        tid <- dofork $ Ca.try (restore action) >>= putMVar mv
+        let wait = takeMVar mv `catch` \(e :: SomeException) -> throwTo tid e >> wait
+        wait >>= either (\(e :: SomeException) -> throw e) pure
+    else action
 
 -- Exceptions
 
@@ -575,10 +632,6 @@ newMVar a = do
 -- | Create a new @MVar@ containing a value, but it is given a name
 -- which may be used to present more useful debugging information.
 --
--- If no name is given, a counter starting from 0 is used. If names
--- conflict, successive @MVar@s with the same name are given a numeric
--- suffix, counting up from 1.
---
 -- @since 1.0.0.0
 newMVarN :: MonadConc m => String -> a -> m (MVar m a)
 newMVarN n a = do
@@ -620,10 +673,15 @@ instance MonadConc IO where
 
   fork   = IO.forkIO
   forkOn = IO.forkOn
+  forkOS = IO.forkOS
 
   forkWithUnmask   = IO.forkIOWithUnmask
   forkOnWithUnmask = IO.forkOnWithUnmask
 
+  forkOSN n ma = forkOS $ do
+    labelMe n
+    ma
+
   forkWithUnmaskN n ma = forkWithUnmask $ \umask -> do
     labelMe n
     ma umask
@@ -632,6 +690,8 @@ instance MonadConc IO where
     labelMe n
     ma umask
 
+  isCurrentThreadBound = IO.isCurrentThreadBound
+
   getNumCapabilities = IO.getNumCapabilities
   setNumCapabilities = IO.setNumCapabilities
   readMVar           = IO.readMVar
@@ -698,11 +758,16 @@ instance MonadConc m => MonadConc (IsConc m) where
   fork     ma = toIsConc (fork     $ unIsConc ma)
   forkOn i ma = toIsConc (forkOn i $ unIsConc ma)
 
+  forkOS    ma = toIsConc (forkOS    $ unIsConc ma)
+  forkOSN n ma = toIsConc (forkOSN n $ unIsConc ma)
+
   forkWithUnmask        ma = toIsConc (forkWithUnmask        (\umask -> unIsConc $ ma (\mx -> toIsConc (umask $ unIsConc mx))))
   forkWithUnmaskN   n   ma = toIsConc (forkWithUnmaskN   n   (\umask -> unIsConc $ ma (\mx -> toIsConc (umask $ unIsConc mx))))
   forkOnWithUnmask    i ma = toIsConc (forkOnWithUnmask    i (\umask -> unIsConc $ ma (\mx -> toIsConc (umask $ unIsConc mx))))
   forkOnWithUnmaskN n i ma = toIsConc (forkOnWithUnmaskN n i (\umask -> unIsConc $ ma (\mx -> toIsConc (umask $ unIsConc mx))))
 
+  isCurrentThreadBound = toIsConc isCurrentThreadBound
+
   getNumCapabilities = toIsConc getNumCapabilities
   setNumCapabilities = toIsConc . setNumCapabilities
   myThreadId         = toIsConc myThreadId
@@ -744,12 +809,17 @@ instance C => MonadConc (T m) where                            { \
                                                                  \
   fork   = liftedF F fork                                      ; \
   forkOn = liftedF F . forkOn                                  ; \
+  forkOS = liftedF F forkOS                                    ; \
+                                                                 \
+  forkOSN = liftedF F . forkOSN                                ; \
                                                                  \
   forkWithUnmask        = liftedFork F forkWithUnmask          ; \
   forkWithUnmaskN   n   = liftedFork F (forkWithUnmaskN   n  ) ; \
   forkOnWithUnmask    i = liftedFork F (forkOnWithUnmask    i) ; \
   forkOnWithUnmaskN n i = liftedFork F (forkOnWithUnmaskN n i) ; \
                                                                  \
+  isCurrentThreadBound = lift isCurrentThreadBound             ; \
+                                                                 \
   getNumCapabilities = lift getNumCapabilities                 ; \
   setNumCapabilities = lift . setNumCapabilities               ; \
   myThreadId         = lift myThreadId                         ; \

concurrency/Control/Monad/STM/Class.hs

@@ -5,7 +5,7 @@
 
 -- |
 -- Module      : Control.Monad.STM.Class
--- Copyright   : (c) 2016 Michael Walker
+-- Copyright   : (c) 2016--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental

concurrency/LICENSE

@@ -1,4 +1,4 @@
-Copyright (c) 2015, Michael Walker <mike@barrucadu.co.uk>
+Copyright (c) 2016--2017, Michael Walker <mike@barrucadu.co.uk>
 
 Permission is hereby granted, free of charge, to any person obtaining
 a copy of this software and associated documentation files (the

concurrency/README.markdown

@@ -3,16 +3,15 @@ concurrency
 
 A typeclass abstraction over much of Control.Concurrent (and some
 extras!). If you're looking for a general introduction to Haskell
-concurrency, you should check out the excellent
-[Parallel and Concurrent Programming in Haskell][parconc], by Simon
-Marlow. If you are already familiar with concurrent Haskell, just
-change all the imports from Control.Concurrent.* to
-Control.Concurrent.Classy.* and fix the type errors.
+concurrency, you should check out the excellent [Parallel and
+Concurrent Programming in Haskell][parconc], by Simon Marlow. If you
+are already familiar with concurrent Haskell, just change all the
+imports from Control.Concurrent.* to Control.Concurrent.Classy.* and
+fix the type errors.
 
 A brief list of supported functionality:
 
-- Threads: the `forkIO*` and `forkOn*` functions, although bound
-  threads are not supported.
+- Threads: both unbound and bound.
 - Getting and setting capablities.
 - Yielding and delaying.
 - Mutable state: STM, `MVar`, and `IORef`.

concurrency/concurrency.cabal

@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                concurrency
-version:             1.2.3.0
+version:             1.3.0.0
 synopsis:            Typeclasses, functions, and data types for concurrency and STM.
 
 description:
@@ -19,7 +19,7 @@ license:             MIT
 license-file:        LICENSE
 author:              Michael Walker
 maintainer:          mike@barrucadu.co.uk
--- copyright:           
+copyright:           (c) 2016--2017 Michael Walker
 category:            Concurrency
 build-type:          Simple
 extra-source-files:  README.markdown CHANGELOG.markdown
@@ -32,7 +32,7 @@ source-repository head
 source-repository this
   type:     git
   location: https://github.com/barrucadu/dejafu.git
-  tag:      concurrency-1.2.3.0
+  tag:      concurrency-1.3.0.0
 
 library
   exposed-modules:     Control.Monad.Conc.Class

dejafu-tests/Cases/Async.hs

@@ -1,6 +1,5 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE RankNTypes #-}
 
 module Cases.Async where
 
@@ -15,7 +14,7 @@ import Data.List (sort)
 import Data.Maybe (isJust, isNothing)
 import Data.Typeable (Typeable)
 import Test.DejaFu (alwaysTrue)
-import Test.DejaFu.Conc (ConcST)
+import Test.DejaFu.Conc (ConcIO)
 
 import Common
 
@@ -180,7 +179,7 @@ assertEqual err a1 a2
   | a1 == a2  = pure ()
   | otherwise = assertFailure err
 
-testCase :: String -> (forall t. ConcST t ()) -> Test
+testCase :: String -> ConcIO () -> Test
 testCase name c = djfu name (alwaysTrue p) (try c) where
   p (Right (Left (e::SomeException))) = False
   p (Right _) = True

dejafu-tests/Cases/Discard.hs

@@ -16,12 +16,9 @@ tests = toTestList
       \x -> if x == Right 3 then Just DiscardResultAndTrace else Nothing
   ]
   where
-    check name xs f = testDejafuDiscard f defaultWay defaultMemType nondet name (gives' xs)
-
-nondet :: MonadConc m => m Int
-nondet = do
-  mvar <- newEmptyMVar
-  _ <- fork $ putMVar mvar 1
-  _ <- fork $ putMVar mvar 2
-  _ <- fork $ putMVar mvar 3
-  readMVar mvar
+    check name xs f = testDejafuDiscard f defaultWay defaultMemType name (gives' xs) $ do
+      mvar <- newEmptyMVar
+      _ <- fork $ putMVar mvar 1
+      _ <- fork $ putMVar mvar 2
+      _ <- fork $ putMVar mvar 3
+      readMVar mvar

dejafu-tests/Cases/Litmus.hs

@@ -6,7 +6,7 @@ import Control.Monad (replicateM)
 import Control.Monad.ST (runST)
 import Data.List (nub, sort)
 import Test.DejaFu (MemType(..), defaultWay, gives')
-import Test.DejaFu.Conc (ConcST)
+import Test.DejaFu.Conc (ConcIO)
 import Test.DejaFu.SCT (runSCT)
 import Test.Framework (Test, testGroup)
 import Test.Framework.Providers.HUnit (hUnitTestToTests)
@@ -46,11 +46,11 @@ tests =
     in litmusTest "Independent Read Independent Write" intelWP28 out out out
   ]
 
-litmusTest :: (Eq a, Show a) => String -> (forall t. ConcST t a) -> [a] -> [a] -> [a] -> Test
+litmusTest :: (Eq a, Show a) => String -> ConcIO a -> [a] -> [a] -> [a] -> Test
 litmusTest name act sq tso pso = testGroup name . hUnitTestToTests $ test
-  [ testDejafuWay defaultWay SequentialConsistency act "SQ"  (gives' sq)
-  , testDejafuWay defaultWay TotalStoreOrder       act "TSO" (gives' tso)
-  , testDejafuWay defaultWay PartialStoreOrder     act "PSO" (gives' pso)
+  [ testDejafuWay defaultWay SequentialConsistency "SQ"  (gives' sq)  act
+  , testDejafuWay defaultWay TotalStoreOrder       "TSO" (gives' tso) act
+  , testDejafuWay defaultWay PartialStoreOrder     "PSO" (gives' pso) act
   ]
 
 -- | Run a litmus test against the three different memory models, and
@@ -62,14 +62,14 @@ litmusTest name act sq tso pso = testGroup name . hUnitTestToTests $ test
 -- possible results. This is why dejafu is good!
 compareTest :: forall a. (Ord a, Show a) => (forall m. MonadConc m => m a) -> IO ()
 compareTest act = do
-  putStrLn $ "DejaFu-SQ:  " ++ results SequentialConsistency
-  putStrLn $ "DejaFu-TSO: " ++ results TotalStoreOrder
-  putStrLn $ "DejaFu-PSO: " ++ results PartialStoreOrder
-  putStr     "IO:         " >> ioResults >>= putStrLn
+  putStr "DejaFu-SQ:  " >> results SequentialConsistency
+  putStr "DejaFu-TSO: " >> results TotalStoreOrder
+  putStr "DejaFu-PSO: " >> results PartialStoreOrder
+  putStr "IO:         " >> ioResults >>= putStrLn
 
   where
-    results memtype = show . nub . sort . map (\(Right a,_) -> a) $
-      runST (runSCT defaultWay memtype act)
+    results memtype = show . nub . sort . map (\(Right a,_) -> a) <$>
+      runSCT defaultWay memtype act
 
     ioResults = show . nub . sort <$> replicateM 99999 act
 

dejafu-tests/Cases/MultiThreaded.hs

@@ -1,6 +1,8 @@
 module Cases.MultiThreaded where
 
 import Control.Exception (ArithException(..))
+import Control.Monad.IO.Class (liftIO)
+import qualified Control.Concurrent as C
 import Test.DejaFu (Failure(..), gives, gives', isUncaughtException)
 import Test.Framework (Test)
 
@@ -36,6 +38,41 @@ threadingTests = toTestList
       x <- newCRef Nothing
       _ <- fork . writeCRef x $ Just ()
       readCRef x
+
+  , djfuT "The main thread is bound" (gives' [(True, True)]) $ do
+      b1 <- isCurrentThreadBound
+      -- check the thread is *really* bound
+      b2 <- liftIO C.isCurrentThreadBound
+      pure (b1, b2)
+
+  , djfuT "A thread started with forkOS is bound" (gives' [(True, True)]) $ do
+      v <- newEmptyMVar
+      forkOS $ do
+        b1 <- isCurrentThreadBound
+        b2 <- liftIO C.isCurrentThreadBound
+        putMVar v (b1, b2)
+      readMVar v
+
+  , djfuT "A thread started with fork is not bound" (gives' [False]) $ do
+      v <- newEmptyMVar
+      fork $ putMVar v =<< isCurrentThreadBound
+      readMVar v
+
+  , djfuT "An action can be run in an unbound thread" (gives' [(True, False)]) $ do
+      v <- newEmptyMVar
+      forkOS $ do
+        b1 <- isCurrentThreadBound
+        b2 <- runInUnboundThread isCurrentThreadBound
+        putMVar v (b1, b2)
+      readMVar v
+
+  , djfuT "An action can be run in a bound thread" (gives' [(False, True)]) $ do
+      v <- newEmptyMVar
+      fork $ do
+        b1 <- isCurrentThreadBound
+        b2 <- runInBoundThread isCurrentThreadBound
+        putMVar v (b1, b2)
+      readMVar v
   ]
 
 --------------------------------------------------------------------------------

dejafu-tests/Cases/Properties.hs

@@ -12,11 +12,14 @@ import qualified Data.Map as M
 import Data.Maybe (fromJust, isJust)
 import Data.Proxy (Proxy(..))
 import qualified Data.Sequence as S
-import Test.DejaFu.Common (ThreadAction, Lookahead)
-import qualified Test.DejaFu.Common as D
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Test.DejaFu.Types (ThreadAction, Lookahead)
+import qualified Test.DejaFu.Types as D
+import qualified Test.DejaFu.Internal as D
 import qualified Test.DejaFu.Conc.Internal.Common as D
 import qualified Test.DejaFu.Conc.Internal.Memory as Mem
-import qualified Test.DejaFu.SCT.Internal as SCT
+import qualified Test.DejaFu.SCT.Internal.DPOR as SCT
 import Test.Framework (Test)
 import Test.LeanCheck (Listable(..), (\/), (><), (==>), cons0, cons1, cons2, cons3, mapT)
 
@@ -25,11 +28,8 @@ import Common
 tests :: [Test]
 tests =
   [ testGroup "Class Laws"
-    [ testGroup "ThreadId" (eqord (Proxy :: Proxy D.ThreadId))
-    , testGroup "CRefId"   (eqord (Proxy :: Proxy D.CRefId))
-    , testGroup "MVarId"   (eqord (Proxy :: Proxy D.MVarId))
-    , testGroup "TVarId"   (eqord (Proxy :: Proxy D.TVarId))
-    , testGroup "Failure"  (eqord (Proxy :: Proxy D.Failure))
+    [ testGroup "Id"      (eqord (Proxy :: Proxy D.Id))
+    , testGroup "Failure" (eqord (Proxy :: Proxy D.Failure))
     ]
 
   , testGroup "Common"
@@ -162,16 +162,19 @@ eq_wb (Mem.WriteBuffer wb1) (Mem.WriteBuffer wb2) = andM (pure (ks1 == ks2) :
 -- Typeclass instances
 
 instance Listable D.ThreadId where
-  tiers = mapT (D.ThreadId Nothing) tiers
+  tiers = mapT D.ThreadId tiers
 
 instance Listable D.CRefId where
-  tiers = mapT (D.CRefId Nothing) tiers
+  tiers = mapT D.CRefId tiers
 
 instance Listable D.MVarId where
-  tiers = mapT (D.MVarId Nothing) tiers
+  tiers = mapT D.MVarId tiers
 
 instance Listable D.TVarId where
-  tiers = mapT (D.TVarId Nothing) tiers
+  tiers = mapT D.TVarId tiers
+
+instance Listable D.Id where
+  tiers = mapT (D.Id Nothing) tiers
 
 instance Listable D.ThreadAction where
   tiers =
@@ -247,11 +250,14 @@ instance Listable D.ActionType where
     \/ cons0 D.SynchronisedOther
 
 instance Listable SCT.DepState where
-  tiers = mapT (uncurry SCT.DepState) (tiers >< tiers)
+  tiers = mapT (\(a,(b,c)) -> SCT.DepState a b c) (tiers >< tiers >< tiers)
 
 instance (Ord k, Listable k, Listable v) => Listable (Map k v) where
   tiers = mapT M.fromList tiers
 
+instance (Ord v, Listable v) => Listable (Set v) where
+  tiers = mapT Set.fromList tiers
+
 instance Listable D.Failure where
   list =
     [ D.InternalError

dejafu-tests/Common.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE RankNTypes #-}
 
 module Common
   ( module Common
@@ -12,8 +11,8 @@ import qualified Control.Monad.Catch as C
 import Control.Monad.Conc.Class
 import Control.Monad.STM.Class
 import System.Random (mkStdGen)
-import Test.DejaFu (Predicate, Failure, Result(..), alwaysTrue)
-import Test.DejaFu.Conc (ConcST)
+import Test.DejaFu (Predicate, ProPredicate(..), Failure, Result(..), alwaysTrue)
+import Test.DejaFu.Conc (ConcIO)
 import qualified Test.Framework as TF
 import Test.Framework.Providers.HUnit (hUnitTestToTests)
 import qualified Test.HUnit as TH
@@ -35,7 +34,7 @@ instance IsTest TH.Test where
 instance IsTest T where
   toTestList (T n c p) = toTestList (BT n c p defaultBounds)
   toTestList (BT n c p b) = toTestList . testGroup n $
-    let mk way name = testDejafuWay way defaultMemType c name p
+    let mk way name = testDejafuWay way defaultMemType name p c
         g = mkStdGen 0
     in [ mk (systematically b) "systematically"
        , mk (uniformly g 100) "uniformly"
@@ -47,16 +46,16 @@ instance IsTest t => IsTest [t] where
   toTestList = concatMap toTestList
 
 data T where
-  T  :: Show a => String -> (forall t. ConcST t a) -> Predicate a -> T
-  BT :: Show a => String -> (forall t. ConcST t a) -> Predicate a -> Bounds -> T
+  T  :: Show a => String -> ConcIO a -> Predicate a -> T
+  BT :: Show a => String -> ConcIO a -> Predicate a -> Bounds -> T
 
 testGroup :: IsTest t => String -> t -> TF.Test
 testGroup name = TF.testGroup name . toTestList
 
-djfu :: Show a => String -> Predicate a -> (forall t. ConcST t a) -> TF.Test
-djfu name p c = hunitTest $ testDejafu c name p
+djfu :: Show a => String -> Predicate a -> ConcIO a -> TF.Test
+djfu name p c = hunitTest $ testDejafu name p c
 
-djfuT :: Show a => String -> Predicate a -> (forall t. ConcST t a) -> [TF.Test]
+djfuT :: Show a => String -> Predicate a -> ConcIO a -> [TF.Test]
 djfuT name p c = toTestList $ T name c p
 
 alwaysFailsWith :: (Failure -> Bool) -> Predicate a
@@ -109,6 +108,8 @@ newTVarInt = newTVar
 
 -- | A test which should fail.
 failing :: Predicate a -> Predicate a
-failing p as =
-  let result = p as
-  in result { _pass = not (_pass result) }
+failing p = p
+  { peval = \xs ->
+      let result = peval p xs
+      in result { _pass = not (_pass result) }
+  }

dejafu-tests/Examples/ClassLaws.hs

@@ -1,5 +1,3 @@
-{-# LANGUAGE CPP                 #-}
-{-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell     #-}
 {-# LANGUAGE ViewPatterns        #-}
@@ -15,14 +13,13 @@ import Control.Monad.Conc.Class
 import Data.Maybe (isJust)
 import Data.Set (fromList)
 import Test.DejaFu (defaultBounds, defaultMemType)
-import Test.DejaFu.Conc (ConcST)
+import Test.DejaFu.Conc (ConcIO)
 import Test.DejaFu.SCT (sctBound)
 import Test.Framework (Test, testGroup)
 import Test.Framework.Providers.QuickCheck2 (testProperty)
-import Test.QuickCheck (Arbitrary(..), expectFailure, monomorphic)
+import Test.QuickCheck (Arbitrary(..), Property, expectFailure, monomorphic)
 import Test.QuickCheck.Function (Fun, apply)
-
-import Examples.ClassLaws.Impredicative
+import Test.QuickCheck.Monadic (assert, monadicIO, run)
 
 -- Tests at bottom of file due to Template Haskell silliness.
 
@@ -37,7 +34,7 @@ import Examples.ClassLaws.Impredicative
 -- before delivering the result of type @a@.
 newtype Concurrently m a = Concurrently { runConcurrently :: m a }
 
-type CST t = Concurrently (ConcST t)
+type C = Concurrently ConcIO
 
 --------------------------------------------------------------------------------
 -- Functor
@@ -46,11 +43,11 @@ instance MonadConc m => Functor (Concurrently m) where
   fmap f (Concurrently a) = Concurrently $ f <$> a
 
 -- fmap id a = a
-prop_functor_id :: Ord a => CST t a -> Bool
+prop_functor_id :: Ord a => C a -> Property
 prop_functor_id ca = ca `eq` (fmap id ca)
 
 -- fmap f . fmap g = fmap (f . g)
-prop_functor_comp :: Ord c => CST t a -> Fun a b -> Fun b c -> Bool
+prop_functor_comp :: Ord c => C a -> Fun a b -> Fun b c -> Property
 prop_functor_comp ca (apply -> f) (apply -> g) = (g . f <$> ca) `eq` (g <$> (f <$> ca))
 
 --------------------------------------------------------------------------------
@@ -62,26 +59,26 @@ instance MonadConc m => Applicative (Concurrently m) where
   Concurrently fs <*> Concurrently as = Concurrently $ (\(f, a) -> f a) <$> concurrently fs as
 
 -- pure id <*> a = a
-prop_applicative_id :: Ord a => CST t a -> Bool
+prop_applicative_id :: Ord a => C a -> Property
 prop_applicative_id ca = ca `eq` (pure id <*> ca)
 
 -- pure f <*> pure x = pure (f x)
-prop_applicative_homo :: Ord b => a -> Fun a b -> Bool
+prop_applicative_homo :: Ord b => a -> Fun a b -> Property
 prop_applicative_homo a (apply -> f) = (pure $ f a) `eq` (pure f <*> pure a)
 
 -- u <*> pure y = pure ($ y) <*> u
-prop_applicative_inter :: Ord b => CST t (Fun a b) -> a -> Bool
+prop_applicative_inter :: Ord b => C (Fun a b) -> a -> Property
 prop_applicative_inter u y = (u' <*> pure y) `eq` (pure ($ y) <*> u') where
   u' = apply <$> u
 
 -- u <*> (v <*> w) = pure (.) <*> u <*> v <*> w
-prop_applicative_comp :: Ord c => CST t (Fun b c) -> CST t (Fun a b) -> CST t a -> Bool
+prop_applicative_comp :: Ord c => C (Fun b c) -> C (Fun a b) -> C a -> Property
 prop_applicative_comp u v w = (u' <*> (v' <*> w)) `eq` (pure (.) <*> u' <*> v' <*> w) where
   u' = apply <$> u
   v' = apply <$> v
 
 -- f <$> x = pure f <*> x
-prop_applicative_fmap :: Ord b => Fun a b -> CST t a -> Bool
+prop_applicative_fmap :: Ord b => Fun a b -> C a -> Property
 prop_applicative_fmap (apply -> f) a = (f <$> a) `eq` (pure f <*> a)
 
 --------------------------------------------------------------------------------
@@ -93,33 +90,33 @@ instance MonadConc m => Monad (Concurrently m) where
   Concurrently a >>= f = Concurrently $ a >>= runConcurrently . f
 
 -- return >=> f = f
-prop_monad_left_id :: Ord b => Fun a (CST t b) -> a -> Bool
+prop_monad_left_id :: Ord b => Fun a (C b) -> a -> Property
 prop_monad_left_id (apply -> f) = f `eqf` (return >=> f)
 
 -- f >=> return = f
-prop_monad_right_id :: Ord b => Fun a (CST t b) -> a -> Bool
+prop_monad_right_id :: Ord b => Fun a (C b) -> a -> Property
 prop_monad_right_id (apply -> f) = f `eqf` (f >=> return)
 
 -- (f >=> g) >=> h = f >=> (g >=> h)
-prop_monad_assoc :: Ord d => Fun a (CST t b) -> Fun b (CST t c) -> Fun c (CST t d) -> a -> Bool
+prop_monad_assoc :: Ord d => Fun a (C b) -> Fun b (C c) -> Fun c (C d) -> a -> Property
 prop_monad_assoc (apply -> f) (apply -> g) (apply -> h) = ((f >=> g) >=> h) `eqf` (f >=> (g >=> h))
 
 -- f <$> a = f `liftM` a
-prop_monad_fmap :: Ord b => Fun a b -> CST t a -> Bool
+prop_monad_fmap :: Ord b => Fun a b -> C a -> Property
 prop_monad_fmap (apply -> f) a = (f <$> a) `eq` (f `liftM` a)
 
 -- return = pure
-prop_monad_pure :: Ord a => a -> Bool
+prop_monad_pure :: Ord a => a -> Property
 prop_monad_pure = pure `eqf` return
 
 -- (<*>) = ap
-prop_monad_ap :: Ord b => Fun a b -> a -> Bool
+prop_monad_ap :: Ord b => Fun a b -> a -> Property
 prop_monad_ap (apply -> f) a = (pure f <*> pure a) `eq` (return f `ap` return a)
 
 -- (<*>) = ap, side-effect-testing version
-prop_monad_ap' :: forall a b. Ord b => Fun a b -> Fun a b -> a -> Bool
+prop_monad_ap' :: forall a b. Ord b => Fun a b -> Fun a b -> a -> Property
 prop_monad_ap' (apply -> f) (apply -> g) a = go (<*>) `eq'` go ap where
-  go :: (CST t (a -> b) -> CST t a -> CST t b) -> ConcST t b
+  go :: (C (a -> b) -> C a -> C b) -> ConcIO b
   go combine = do
     var <- newEmptyMVar
     let cf = do { res <- tryTakeMVar var; pure $ if isJust res then f else g }
@@ -136,15 +133,15 @@ instance MonadConc m => Alternative (Concurrently m) where
     Concurrently $ either id id <$> race as bs
 
 -- x <|> (y <|> z) = (x <|> y) <|> z
-prop_alternative_assoc :: Ord a => CST t a -> CST t a -> CST t a -> Bool
+prop_alternative_assoc :: Ord a => C a -> C a -> C a -> Property
 prop_alternative_assoc x y z = (x <|> (y <|> z)) `eq` ((x <|> y) <|> z)
 
 -- x = x <|> empty
-prop_alternative_right_id :: Ord a => CST t a -> Bool
+prop_alternative_right_id :: Ord a => C a -> Property
 prop_alternative_right_id x = x `eq` (x <|> empty)
 
 -- x = empty <|> x
-prop_alternative_left_id :: Ord a => CST t a -> Bool
+prop_alternative_left_id :: Ord a => C a -> Property
 prop_alternative_left_id x = x `eq` (empty <|> x)
 
 --------------------------------------------------------------------------------
@@ -160,17 +157,17 @@ instance Monoid Integer where
   mempty  = 0
   mappend = (+)
 
-eq :: Ord a => CST t a -> CST t a -> Bool
+eq :: Ord a => C a -> C a -> Property
 eq left right = runConcurrently left `eq'` runConcurrently right
 
-eq' :: forall t a. Ord a => ConcST t a -> ConcST t a -> Bool
-eq' left right = runST' $ do
-  leftTraces  <- sctBound defaultMemType defaultBounds left
-  rightTraces <- sctBound defaultMemType defaultBounds right
+eq' :: forall t a. Ord a => ConcIO a -> ConcIO a -> Property
+eq' left right = monadicIO $ do
+  leftTraces  <- run $ sctBound defaultMemType defaultBounds left
+  rightTraces <- run $ sctBound defaultMemType defaultBounds right
   let toSet = fromList . map fst
-  pure (toSet leftTraces == toSet rightTraces)
+  assert (toSet leftTraces == toSet rightTraces)
 
-eqf :: Ord b => (a -> CST t b) -> (a -> CST t b) -> a -> Bool
+eqf :: Ord b => (a -> C b) -> (a -> C b) -> a -> Property
 eqf left right a = left a `eq` right a
 
 --------------------------------------------------------------------------------

dejafu-tests/Examples/ClassLaws/Impredicative.hs

@@ -1,12 +0,0 @@
-{-# LANGUAGE ImpredicativeTypes #-}
-
--- | This is a separate module because of the need for
--- ImpredicativeTypes, which breaks things elsewhere in the main
--- SearchParty module.
-module Examples.ClassLaws.Impredicative where
-
-import Control.Monad.ST (ST, runST)
-import Unsafe.Coerce (unsafeCoerce)
-
-runST' :: ST t Bool -> Bool
-runST' = unsafeCoerce runST

dejafu-tests/Examples/Philosophers.hs

@@ -12,8 +12,8 @@ import Test.HUnit.DejaFu
 
 tests :: [Test]
 tests = hUnitTestToTests $ test
-  [ testDejafuWay way defaultMemType (philosophers 3) "deadlocks" deadlocksSometimes
-  , testDejafuWay way defaultMemType (philosophers 3) "loops"     abortsSometimes
+  [ testDejafuWay way defaultMemType "deadlocks" deadlocksSometimes (philosophers 3)
+  , testDejafuWay way defaultMemType "loops"     abortsSometimes    (philosophers 3)
   ]
 
 -- | Shorter execution length bound

dejafu-tests/Examples/SearchParty.hs

@@ -21,34 +21,29 @@ import Data.Functor (void)
 import Data.Maybe (fromJust, isNothing)
 
 -- test imports
-import Data.List (permutations)
-import Test.DejaFu (Predicate, Result(..), alwaysTrue2)
+import Data.List (sort)
+import Test.DejaFu (Predicate, Result(..), alwaysSameOn)
 import Test.Framework (Test)
 import Test.Framework.Providers.HUnit (hUnitTestToTests)
 import Test.HUnit (test)
 import Test.HUnit.DejaFu (testDejafu)
 
+import Common
+
 import Examples.SearchParty.Impredicative
 
 tests :: [Test]
 tests = hUnitTestToTests $ test
-  [ testDejafu concFilter "concurrent filter" (invPred checkResultLists)
+  [ testDejafu "concurrent filter" (failing checkResultLists) concFilter
   ]
 
 -- | Filter a list concurrently.
 concFilter :: MonadConc m => m [Int]
 concFilter = unsafeRunFind $ [0..5] @! const True
 
--- | Invert the result of a predicate.
-invPred :: Predicate a -> Predicate a
-invPred p xs = let r = p xs in r { _pass = not (_pass r) }
-
 -- | Check that two lists of results are equal, modulo order.
-checkResultLists :: Eq a => Predicate [a]
-checkResultLists = alwaysTrue2 checkLists where
-  checkLists (Right as) (Right bs) =
-    as `elem` permutations bs
-  checkLists a b = a == b
+checkResultLists :: Ord a => Predicate [a]
+checkResultLists = alwaysSameOn (fmap sort)
 
 -------------------------------------------------------------------------------
 

dejafu-tests/dejafu-tests.cabal

@@ -32,7 +32,6 @@ executable dejafu-tests
                      , Examples
                      , Examples.AutoUpdate
                      , Examples.ClassLaws
-                     , Examples.ClassLaws.Impredicative
                      , Examples.Logger
                      , Examples.Philosophers
                      , Examples.SearchParty
@@ -56,5 +55,8 @@ executable dejafu-tests
                      , test-framework
                      , test-framework-hunit
                      , test-framework-quickcheck2
+  if impl(ghc < 8.0.1)
+    build-depends: transformers
   -- hs-source-dirs:      
   default-language:    Haskell2010
+  ghc-options: -threaded

dejafu/CHANGELOG.markdown

@@ -7,6 +7,118 @@ This project is versioned according to the [Package Versioning Policy](https://p
 *de facto* standard Haskell versioning scheme.
 
 
+1.0.0.0
+-------
+
+- **Date**    unreleased
+- **Git tag** [dejafu-1.0.0.0][]
+- **Hackage** https://hackage.haskell.org/package/dejafu-1.0.0.0
+
+### Test.DejaFu
+
+- All testing functions now require a `MonadConc`, `MonadRef`, and `MonadIO` constraint:
+
+    It is no longer possible to test things in `ST`.
+
+- All testing functions now take the action to test as the last parameter.
+
+- The `autocheckIO`, `dejafuIO`, `dejafusIO`, `autocheckWayIO`, `dejafuWayIO`, `dejafusWayIO`,
+  `dejafuDiscardIO`, `runTestM`, and `runTestWayM` functions are now gone.
+
+- The `Predicate` type has been replaced with a more general `ProPredicate` type which is a
+  profunctor and (b) can discard results not needed to determine if the predicate passes. (#124)
+
+    All testing functions have been generalised to take a `ProPredicate` instead.  The `Predicate a`
+    type remains as an alias for `ProPredicate a a`.  Passing tests have their resident memory usage
+    significantly decreased.
+
+- The `Result` type no longer includes a number of cases checked, as this is not meaningful with
+  predicates including discard functions.
+
+- New `alwaysNothing` and `somewhereNothing` functions, like `alwaysTrue` and `somewhereTrue`, to
+  lift functions to `ProPredicate`s.
+
+- The `alwaysTrue2` function is gone, as its behaviour was unintuitive and easy to get wrong, and
+  has been replaced with new `alwaysSameOn` and `alwaysSameBy` predicates, which generalise
+  `alwaysSame`.
+
+- The `alwaysSame`, `alwaysSameOn`, and `alwaysSameBy` predicates now gives the simplest execution
+  trace leading to each distinct result.
+
+### Test.DejaFu.Common
+
+- This module has been split up into new Test.DejaFu.Internal, Types, and Utils modules. (#155)
+
+- New `ForkOS` and `IsCurrentThreadBound` thread actions. (#126)
+
+- New `WillForkOS` and `WillIsCurrentThreadBound` lookaheads. (#126)
+
+- The `TTrace` type synonym for `[TAction]` has been removed.
+
+- The `preEmpCount` function has been removed.
+
+- New functions `strengthenDiscard` and `weakenDiscard` to combine discard functions.
+
+- The `Discard` type is now defined here and re-exported from Test.DejaFu.SCT.
+
+- The `ThreadId`, `CRefId`, `MVarId`, and `TVarId` types are now newtypes over a common `Id`
+  type. (#137)
+
+### Test.DejaFu.Conc
+
+- The `ConcST` type alias is gone.
+
+- The `MonadBase IO ConcIO` instance is gone.
+
+- The `MonadIO ConcIO` instance is replaces with a more general `MonadIO n => MonadIO (ConcT r n)`
+  instance.
+
+- The `runConcurrent` function now has a `MonadConc` constraint.
+
+- If bound threads are supported, the main thread when testing is bound. (#126)
+
+- Each entry in an execution trace is now in the form `(decision, alternatives, action)`.  The
+  chosen thread is no longer in the list of alternatives, which makes raw traces easier to
+  read. (#121)
+
+- Due to changes in Test.DejaFu.Schedule, no longer re-exports `Decision`, `NonEmpty`, `tidOf`, or
+  `decisionOf`.
+
+### Test.DejaFu.Refinement
+
+- A blocking interference function is no longer reported as a deadlocking execution.
+
+### Test.DejaFu.Schedule
+
+- No longer re-exports `Decision` or `NonEmpty`.
+
+- The `tidOf` and `decisionOf` functions have moved to Test.DejaFu.Utils.
+
+### Test.DejaFu.SCT
+
+- All testing functions now require a `MonadConc` constraint:
+
+    It is no longer possible to test things in `ST`.
+
+### Test.DejaFu.STM
+
+- This is now an internal module. (#155)
+
+### Performance
+
+- Significant resident memory reduction for most passing tests.
+- Improved dependency detection for `MVar` actions, leading to fewer executions.
+
+### Miscellaneous
+
+- The minimum supported version of concurrency is now 1.3.0.0.
+
+[dejafu-1.0.0.0]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-1.0.0.0
+
+
+---------------------------------------------------------------------------------------------------
+
+
 0.9.1.2
 -------
 

dejafu/LICENSE

@@ -1,4 +1,4 @@
-Copyright (c) 2015, Michael Walker <mike@barrucadu.co.uk>
+Copyright (c) 2015--2017, Michael Walker <mike@barrucadu.co.uk>
 
 Permission is hereby granted, free of charge, to any person obtaining
 a copy of this software and associated documentation files (the

dejafu/README.markdown

@@ -7,57 +7,124 @@ dejafu
 >
 > -- Terry Pratchett, Thief of Time
 
-Concurrency is nice, deadlocks and race conditions not so much. The
-`Par` monad family, as defined in [abstract-par][] provides
-deterministic parallelism, but sometimes we can tolerate a bit of
-nondeterminism.
+- [Installation](#installation)
+- [Quick start guide](#quick-start-guide)
+- [Why Déjà Fu?](#why-déjà-fu)
+- [Contributing](#contributing)
+- [Release notes](#release-notes)
+- [Questions, feedback, discussion](#questions-feedback-discussion)
+- [Bibliography](#bibliography)
+- **[The website!](http://dejafu.readthedocs.io/)**
 
-This package builds on the concurrency package (also in this
-repository) by enabling you to systematically and deterministically
-test your concurrent programs.
+Déjà Fu is a unit-testing library for concurrent Haskell programs.
+Tests are deterministic and expressive, making it easy and convenient
+to test your threaded code.  Available on [GitHub][], [Hackage][], and
+[Stackage][].
 
-The documentation of the latest developmental version is
-[available online][docs]. Examples can be found in the test suite.
+[GitHub]:   https://github.com/barrucadu/dejafu
+[Hackage]:  https://hackage.haskell.org/package/dejafu
+[Stackage]: https://www.stackage.org/package/dejafu
 
-**Note on the test suite:** This is in a separate project
-(dejafu-tests) because Cabal-the-library is a bit naff. See this
-[issue][].
 
-Déjà Fu and `IO`
-----------------
-
-The core assumption underlying Déjà Fu is that any apparent
-nondeterminism arises purely from the scheduling behaviour. To put it
-another way, a given computation, parametrised with a fixed set of
-scheduling decisions, is deterministic.
-
-Whilst this assumption may not hold in general when `IO` is involved,
-you should strive to produce test cases where it does.
-
-Memory Model
+Installation
 ------------
 
-The testing functionality supports a few different memory models, for
-computations which use non-synchronised `CRef` operations. The
-supported models are:
+Install from Hackage globally:
 
-- **Sequential Consistency:** A program behaves as a simple
-    interleaving of the actions in different threads. When a CRef is
-    written to, that write is immediately visible to all threads.
+```
+$ cabal install dejafu
+```
 
-- **Total Store Order (TSO):** Each thread has a write buffer. A
-    thread sees its writes immediately, but other threads will only
-    see writes when they are committed, which may happen later. Writes
-    are committed in the same order that they are created.
+Or add it to your cabal file:
 
-- **Partial Store Order (PSO):** Each CRef has a write buffer. A
-    thread sees its writes immediately, but other threads will only
-    see writes when they are committed, which may happen later. Writes
-    to different CRefs are not necessarily committed in the same order
-    that they are created.
+```
+build-depends: ...
+             , dejafu
+```
+
+Or to your package.yaml:
+
+```
+dependencies:
+  ...
+  - dejafu
+```
+
+
+Quick start guide
+-----------------
+
+Déjà Fu supports unit testing, and comes with a helper function called
+`autocheck` to look for some common issues.  Let's see it in action:
+
+```haskell
+import Control.Concurrent.Classy
+
+myFunction :: MonadConc m => m String
+myFunction = do
+  var <- newEmptyMVar
+  fork (putMVar var "hello")
+  fork (putMVar var "world")
+  readMVar var
+```
+
+That `MonadConc` is a typeclass abstraction over concurrency, but
+we'll get onto that shortly.  First, the result of testing:
+
+```
+> autocheck myFunction
+[pass] Never Deadlocks
+[pass] No Exceptions
+[fail] Consistent Result
+        "hello" S0----S1--S0--
+
+        "world" S0----S2--S0--
+False
+```
+
+There are no deadlocks or uncaught exceptions, which is good; but the
+program is (as you probably spotted) nondeterministic!
+
+Along with each result, Déjà Fu gives us a representative execution
+trace in an abbreviated form.  `Sn` means that thread `n` started
+executing, and `Pn` means that thread `n` pre-empted the previously
+running thread.
+
+
+Why Déjà Fu?
+------------
+
+Testing concurrent programs is difficult, because in general they are
+nondeterministic.  This leads to people using work-arounds like
+running their testsuite many thousands of times; or running their
+testsuite while putting their machine under heavy load.
+
+These approaches are inadequate for a few reasons:
+
+- **How many runs is enough?** When you are just hopping to spot a bug
+  by coincidence, how do you know to stop?
+- **How do you know if you've fixed a bug you saw previously?**
+  Because the scheduler is a black box, you don't know if the
+  previously buggy schedule has been re-run.
+- **You won't get that much scheduling variety!** Operating systems
+  and language runtimes like to run threads for long periods of time,
+  which reduces the variety you get (and so drives up the number of
+  runs you need).
+
+Déjà Fu addresses these points by offering *complete* testing.  You
+can run a test case and be guaranteed to find all results with some
+bounds.  These bounds can be configured, or even disabled!  The
+underlying approach used is smarter than merely trying all possible
+executions, and will in general explore the state-space quickly.
+
+If your test case is just too big for complete testing, there is also
+a random scheduling mode, which is necessarily *incomplete*.  However,
+Déjà Fu will tend to produce much more schedule variety than just
+running your test case in `IO` the same number of times, and so bugs
+will tend to crop up sooner.  Furthermore, as you get execution traces
+out, you can be certain that a bug has been fixed by simply following
+the trace by eye.
 
-If a testing function does not take the memory model as a parameter,
-it uses TSO.
 
 Contributing
 ------------
@@ -66,7 +133,3 @@ Bug reports, pull requests, and comments are very welcome!
 
 Feel free to contact me on GitHub, through IRC (#haskell on freenode),
 or email (mike@barrucadu.co.uk).
-
-[docs]:         https://docs.barrucadu.co.uk/dejafu
-[abstract-par]: https://hackage.haskell.org/package/abstract-par/docs/Control-Monad-Par-Class.html
-[issue]:        https://github.com/commercialhaskell/stack/issues/1122

dejafu/Test/DejaFu/Conc.hs

@@ -4,15 +4,14 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeSynonymInstances #-}
 
 -- |
 -- Module      : Test.DejaFu.Conc
--- Copyright   : (c) 2016 Michael Walker
+-- Copyright   : (c) 2016--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
--- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, RankNTypes, TypeFamilies, TypeSynonymInstances
+-- Portability : CPP, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, TypeFamilies
 --
 -- Deterministic traced execution of concurrent computations.
 --
@@ -22,7 +21,6 @@
 module Test.DejaFu.Conc
   ( -- * The @ConcT@ monad transformer
     ConcT
-  , ConcST
   , ConcIO
 
   -- * Executing computations
@@ -48,23 +46,22 @@ module Test.DejaFu.Conc
   ) where
 
 import           Control.Exception                (MaskingState(..))
-import qualified Control.Monad.Base               as Ba
 import qualified Control.Monad.Catch              as Ca
 import qualified Control.Monad.IO.Class           as IO
 import           Control.Monad.Ref                (MonadRef)
 import qualified Control.Monad.Ref                as Re
-import           Control.Monad.ST                 (ST)
 import           Control.Monad.Trans.Class        (MonadTrans(..))
 import qualified Data.Foldable                    as F
 import           Data.IORef                       (IORef)
-import           Data.STRef                       (STRef)
 import           Test.DejaFu.Schedule
 
 import qualified Control.Monad.Conc.Class         as C
-import           Test.DejaFu.Common
 import           Test.DejaFu.Conc.Internal
 import           Test.DejaFu.Conc.Internal.Common
-import           Test.DejaFu.STM
+import           Test.DejaFu.Conc.Internal.STM
+import           Test.DejaFu.Internal
+import           Test.DejaFu.Types
+import           Test.DejaFu.Utils
 
 #if MIN_VERSION_base(4,9,0)
 import qualified Control.Monad.Fail               as Fail
@@ -79,12 +76,6 @@ instance Fail.MonadFail (ConcT r n) where
   fail = C . fail
 #endif
 
--- | A 'MonadConc' implementation using @ST@, this should be preferred
--- if you do not need 'liftIO'.
---
--- @since 0.4.0.0
-type ConcST t = ConcT (STRef t) (ST t)
-
 -- | A 'MonadConc' implementation using @IO@.
 --
 -- @since 0.4.0.0
@@ -96,11 +87,9 @@ toConc = C . cont
 wrap :: (M n r a -> M n r a) -> ConcT r n a -> ConcT r n a
 wrap f = C . f . unC
 
-instance IO.MonadIO ConcIO where
-  liftIO ma = toConc (\c -> ALift (fmap c ma))
-
-instance Ba.MonadBase IO ConcIO where
-  liftBase = IO.liftIO
+-- | @since 1.0.0.0
+instance IO.MonadIO n => IO.MonadIO (ConcT r n) where
+  liftIO ma = toConc (\c -> ALift (fmap c (IO.liftIO ma)))
 
 instance Re.MonadRef (CRef r) (ConcT r n) where
   newRef a = toConc (ANewCRef "" a)
@@ -131,13 +120,16 @@ instance Monad n => C.MonadConc (ConcT r n) where
   type MVar     (ConcT r n) = MVar r
   type CRef     (ConcT r n) = CRef r
   type Ticket   (ConcT r n) = Ticket
-  type STM      (ConcT r n) = STMLike n r
+  type STM      (ConcT r n) = S n r
   type ThreadId (ConcT r n) = ThreadId
 
   -- ----------
 
-  forkWithUnmaskN   n ma = toConc (AFork n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop (pure ()))))
+  forkWithUnmaskN   n ma = toConc (AFork   n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop (pure ()))))
   forkOnWithUnmaskN n _  = C.forkWithUnmaskN n
+  forkOSN n ma = forkOSWithUnmaskN n (const ma)
+
+  isCurrentThreadBound = toConc AIsBound
 
   -- This implementation lies and returns 2 until a value is set. This
   -- will potentially avoid special-case behaviour for 1 capability,
@@ -185,10 +177,22 @@ instance Monad n => C.MonadConc (ConcT r n) where
 
   atomically = toConc . AAtom
 
+-- move this into the instance defn when forkOSWithUnmaskN is added to MonadConc in 2018
+forkOSWithUnmaskN :: Applicative n => String -> ((forall a. ConcT r n a -> ConcT r n a) -> ConcT r n ()) -> ConcT r n ThreadId
+forkOSWithUnmaskN n ma
+  | C.rtsSupportsBoundThreads = toConc (AForkOS n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop (pure ()))))
+  | otherwise = fail "RTS doesn't support multiple OS threads (use ghc -threaded when linking)"
+
 -- | Run a concurrent computation with a given 'Scheduler' and initial
 -- state, returning a failure reason on error. 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!
@@ -202,8 +206,8 @@ instance Monad n => C.MonadConc (ConcT r n) where
 -- nonexistent thread. In either of those cases, the computation will
 -- be halted.
 --
--- @since 0.8.0.0
-runConcurrent :: MonadRef r n
+-- @since 1.0.0.0
+runConcurrent :: (C.MonadConc n, MonadRef r n)
   => Scheduler s
   -> MemType
   -> s

dejafu/Test/DejaFu/Conc/Internal.hs

@@ -4,7 +4,7 @@
 
 -- |
 -- Module      : Test.DejaFu.Conc.Internal
--- Copyright   : (c) 2016 Michael Walker
+-- Copyright   : (c) 2016--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
@@ -17,6 +17,8 @@ module Test.DejaFu.Conc.Internal where
 
 import           Control.Exception                   (MaskingState(..),
                                                       toException)
+import           Control.Monad.Conc.Class            (MonadConc,
+                                                      rtsSupportsBoundThreads)
 import           Control.Monad.Ref                   (MonadRef, newRef, readRef,
                                                       writeRef)
 import           Data.Functor                        (void)
@@ -27,13 +29,13 @@ import           Data.Monoid                         ((<>))
 import           Data.Sequence                       (Seq, (<|))
 import qualified Data.Sequence                       as Seq
 
-import           Test.DejaFu.Common
 import           Test.DejaFu.Conc.Internal.Common
 import           Test.DejaFu.Conc.Internal.Memory
+import           Test.DejaFu.Conc.Internal.STM
 import           Test.DejaFu.Conc.Internal.Threading
+import           Test.DejaFu.Internal
 import           Test.DejaFu.Schedule
-import           Test.DejaFu.STM                     (Result(..),
-                                                      runTransaction)
+import           Test.DejaFu.Types
 
 --------------------------------------------------------------------------------
 -- * Execution
@@ -45,23 +47,27 @@ type SeqTrace
 -- | Run a concurrent computation with a given 'Scheduler' and initial
 -- state, returning a failure reason on error. Also returned is the
 -- final state of the scheduler, and an execution trace.
-runConcurrency :: MonadRef r n
-               => Scheduler g
-               -> MemType
-               -> g
-               -> IdSource
-               -> Int
-               -> M n r a
-               -> n (Either Failure a, Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction))
+runConcurrency :: (MonadConc n, MonadRef r n)
+  => Scheduler g
+  -> MemType
+  -> g
+  -> IdSource
+  -> Int
+  -> M n r a
+  -> n (Either Failure a, Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction))
 runConcurrency sched memtype g idsrc caps ma = do
   (c, ref) <- runRefCont AStop (Just . Right) (runM ma)
+  let threads0 = launch' Unmasked initialThread (const c) M.empty
+  threads <- (if rtsSupportsBoundThreads then makeBound initialThread else pure) threads0
   let ctx = Context { cSchedState = g
                     , cIdSource   = idsrc
-                    , cThreads    = launch' Unmasked initialThread (const c) M.empty
+                    , cThreads    = threads
                     , cWriteBuf   = emptyBuffer
                     , cCaps       = caps
                     }
   (finalCtx, trace, finalAction) <- runThreads sched memtype ref ctx
+  let finalThreads = cThreads finalCtx
+  mapM_ (`kill` finalThreads) (M.keys finalThreads)
   out <- readRef ref
   pure (efromJust "runConcurrency" out, finalCtx, trace, finalAction)
 
@@ -75,7 +81,7 @@ data Context n r g = Context
   }
 
 -- | Run a collection of threads, until there are no threads left.
-runThreads :: MonadRef r n
+runThreads :: (MonadConc n, MonadRef r n)
   => Scheduler g
   -> MemType
   -> r (Maybe (Either Failure a))
@@ -140,8 +146,10 @@ runThreads sched memtype ref = go Seq.empty Nothing where
             | (fst <$> prior) `notElem` map (Just . fst) runnable' = Start chosen
             | otherwise = SwitchTo chosen
 
-          getTrc (Single a)    = Seq.singleton (decision, runnable', a)
-          getTrc (SubC   as _) = (decision, runnable', Subconcurrency) <| as
+          getTrc (Single a)    = Seq.singleton (decision, alternatives, a)
+          getTrc (SubC   as _) = (decision, alternatives, Subconcurrency) <| as
+
+          alternatives = filter (\(t, _) -> t /= chosen) runnable'
 
           getPrior (Single a)      = Just (chosen, a)
           getPrior (SubC _ finalD) = finalD
@@ -159,7 +167,7 @@ data Act
 
 -- | Run a single thread one step, by dispatching on the type of
 -- 'Action'.
-stepThread :: forall n r g. MonadRef r n
+stepThread :: forall n r g. (MonadConc n, MonadRef r n)
   => Scheduler g
   -- ^ The scheduler.
   -> MemType
@@ -174,9 +182,21 @@ stepThread :: forall n r g. MonadRef r n
 stepThread sched memtype tid action ctx = case action of
     -- start a new thread, assigning it the next 'ThreadId'
     AFork n a b -> pure $
-        let threads' = launch tid newtid a (cThreads ctx)
-            (idSource', newtid) = nextTId n (cIdSource ctx)
-        in (Right ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }, Single (Fork newtid))
+      let threads' = launch tid newtid a (cThreads ctx)
+          (idSource', newtid) = nextTId n (cIdSource ctx)
+      in (Right ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }, Single (Fork newtid))
+
+    -- start a new bound thread, assigning it the next 'ThreadId'
+    AForkOS n a b -> do
+      let (idSource', newtid) = nextTId n (cIdSource ctx)
+      let threads' = launch tid newtid a (cThreads ctx)
+      threads'' <- makeBound newtid threads'
+      pure (Right ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }, Single (Fork newtid))
+
+    -- check if the current thread is bound
+    AIsBound c ->
+      let isBound = isJust (_bound =<< M.lookup tid (cThreads ctx))
+      in simple (goto (c isBound) tid (cThreads ctx)) (IsCurrentThreadBound isBound)
 
     -- get the 'ThreadId' of the current thread
     AMyTId c -> simple (goto (c tid) tid (cThreads ctx)) MyThreadId
@@ -316,7 +336,7 @@ stepThread sched memtype tid action ctx = case action of
     -- lift an action from the underlying monad into the @Conc@
     -- computation.
     ALift na -> do
-      a <- na
+      a <- runLiftedAct tid (cThreads ctx) na
       simple (goto a tid (cThreads ctx)) LiftIO
 
     -- throw an exception, and propagate it to the appropriate
@@ -367,7 +387,10 @@ stepThread sched memtype tid action ctx = case action of
     AReturn c -> simple (goto c tid (cThreads ctx)) Return
 
     -- kill the current thread.
-    AStop na -> na >> simple (kill tid (cThreads ctx)) Stop
+    AStop na -> do
+      na
+      threads' <- kill tid (cThreads ctx)
+      simple threads' Stop
 
     -- run a subconcurrent computation.
     ASub ma c
@@ -394,7 +417,9 @@ stepThread sched memtype tid action ctx = case action of
            Just ts' -> simple ts' act
            Nothing
              | t == initialThread -> pure (Left (UncaughtException some), Single act)
-             | otherwise -> simple (kill t ts) act
+             | otherwise -> do
+                 ts' <- kill t ts
+                 simple ts' act
 
     -- helper for actions which only change the threads.
     simple threads' act = pure (Right ctx { cThreads = threads' }, Single act)

dejafu/Test/DejaFu/Conc/Internal/Common.hs

@@ -4,7 +4,7 @@
 
 -- |
 -- Module      : Test.DejaFu.Conc.Internal.Common
--- Copyright   : (c) 2016 Michael Walker
+-- Copyright   : (c) 2016--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
@@ -12,15 +12,16 @@
 --
 -- Common types and utility functions for deterministic execution of
 -- 'MonadConc' implementations. This module is NOT considered to form
+-- part of the public interface of this library.
 module Test.DejaFu.Conc.Internal.Common where
 
-import           Control.Exception  (Exception, MaskingState(..))
-import           Data.Map.Strict    (Map)
-import           Test.DejaFu.Common
-import           Test.DejaFu.STM    (STMLike)
+import           Control.Exception             (Exception, MaskingState(..))
+import           Data.Map.Strict               (Map)
+import           Test.DejaFu.Conc.Internal.STM (S)
+import           Test.DejaFu.Types
 
 #if MIN_VERSION_base(4,9,0)
-import qualified Control.Monad.Fail as Fail
+import qualified Control.Monad.Fail            as Fail
 #endif
 
 --------------------------------------------------------------------------------
@@ -109,7 +110,9 @@ runCont = runM
 -- primitives of the concurrency. 'spawn' is absent as it is
 -- implemented in terms of 'newEmptyMVar', 'fork', and 'putMVar'.
 data Action n r =
-    AFork  String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r)
+    AFork   String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r)
+  | AForkOS String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r)
+  | AIsBound (Bool -> Action n r)
   | AMyTId (ThreadId -> Action n r)
 
   | AGetNumCapabilities (Int -> Action n r)
@@ -138,7 +141,7 @@ data Action n r =
   | forall a. AMasking MaskingState ((forall b. M n r b -> M n r b) -> M n r a) (a -> Action n r)
   | AResetMask Bool Bool MaskingState (Action n r)
 
-  | forall a. AAtom (STMLike n r a) (a -> Action n r)
+  | forall a. AAtom (S n r a) (a -> Action n r)
   | ALift (n (Action n r))
   | AYield  (Action n r)
   | ADelay Int (Action n r)
@@ -155,6 +158,8 @@ data Action n r =
 -- | Look as far ahead in the given continuation as possible.
 lookahead :: Action n r -> Lookahead
 lookahead (AFork _ _ _) = WillFork
+lookahead (AForkOS _ _ _) = WillForkOS
+lookahead (AIsBound _) = WillIsCurrentThreadBound
 lookahead (AMyTId _) = WillMyThreadId
 lookahead (AGetNumCapabilities _) = WillGetNumCapabilities
 lookahead (ASetNumCapabilities i _) = WillSetNumCapabilities i

dejafu/Test/DejaFu/Conc/Internal/Memory.hs

@@ -4,7 +4,7 @@
 
 -- |
 -- Module      : Test.DejaFu.Conc.Internal.Memory
--- Copyright   : (c) 2016 Michael Walker
+-- Copyright   : (c) 2016--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
@@ -26,16 +26,16 @@ module Test.DejaFu.Conc.Internal.Memory where
 import           Control.Monad.Ref                   (MonadRef, readRef,
                                                       writeRef)
 import           Data.Map.Strict                     (Map)
+import qualified Data.Map.Strict                     as M
 import           Data.Maybe                          (maybeToList)
 import           Data.Monoid                         ((<>))
 import           Data.Sequence                       (Seq, ViewL(..), singleton,
                                                       viewl, (><))
 
-import           Test.DejaFu.Common
 import           Test.DejaFu.Conc.Internal.Common
 import           Test.DejaFu.Conc.Internal.Threading
-
-import qualified Data.Map.Strict                     as M
+import           Test.DejaFu.Internal
+import           Test.DejaFu.Types
 
 --------------------------------------------------------------------------------
 -- * Manipulating @CRef@s
@@ -129,7 +129,7 @@ writeBarrier (WriteBuffer wb) = mapM_ flush $ M.elems wb where
 -- | Add phantom threads to the thread list to commit pending writes.
 addCommitThreads :: WriteBuffer r -> Threads n r -> Threads n r
 addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where
-  phantoms = [ (ThreadId Nothing $ negate tid, mkthread c)
+  phantoms = [ (ThreadId (Id Nothing $ negate tid), mkthread c)
              | ((_, b), tid) <- zip (M.toList wb) [1..]
              , c <- maybeToList (go $ viewl b)
              ]

dejafu/Test/DejaFu/Conc/Internal/STM.hs

@@ -1,69 +1,88 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+
+-- Must come after TypeFamilies
+{-# LANGUAGE NoMonoLocalBinds #-}
 
 -- |
--- Module      : Test.DejaFu.STM.Internal
--- Copyright   : (c) 2016 Michael Walker
+-- Module      : Test.DejaFu.Conc.Internal.STM
+-- Copyright   : (c) 2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
--- Portability : CPP, ExistentialQuantification, MultiParamTypeClasses, RankNTypes
+-- Portability : CPP, ExistentialQuantification, MultiParamTypeClasses, NoMonoLocalBinds, TypeFamilies
 --
--- 'MonadSTM' testing implementation, internal types and
--- definitions. This module is NOT considered to form part of the
--- public interface of this library.
-module Test.DejaFu.STM.Internal where
+-- 'MonadSTM' testing implementation, internal types and definitions.
+-- This module is NOT considered to form part of the public interface
+-- of this library.
+module Test.DejaFu.Conc.Internal.STM where
 
-import           Control.DeepSeq    (NFData(..))
-import           Control.Exception  (Exception, SomeException, fromException,
-                                     toException)
-import           Control.Monad.Ref  (MonadRef, newRef, readRef, writeRef)
-import           Data.List          (nub)
+import           Control.Applicative     (Alternative(..))
+import           Control.Exception       (Exception, SomeException,
+                                          fromException, toException)
+import           Control.Monad           (MonadPlus(..))
+import           Control.Monad.Catch     (MonadCatch(..), MonadThrow(..))
+import           Control.Monad.Ref       (MonadRef, newRef, readRef, writeRef)
+import           Data.List               (nub)
 
-import           Test.DejaFu.Common
+import qualified Control.Monad.STM.Class as C
+import           Test.DejaFu.Internal
+import           Test.DejaFu.Types
 
 #if MIN_VERSION_base(4,9,0)
-import qualified Control.Monad.Fail as Fail
+import qualified Control.Monad.Fail      as Fail
 #endif
 
 --------------------------------------------------------------------------------
--- The @STMLike@ monad
+-- * The @S@ monad
 
 -- | The underlying monad is based on continuations over primitive
 -- actions.
 --
 -- This is not @Cont@ because we want to give it a custom @MonadFail@
 -- instance.
-newtype M n r a = M { runM :: (a -> STMAction n r) -> STMAction n r }
+newtype S n r a = S { runSTM :: (a -> STMAction n r) -> STMAction n r }
 
-instance Functor (M n r) where
-    fmap f m = M $ \ c -> runM m (c . f)
+instance Functor (S n r) where
+    fmap f m = S $ \c -> runSTM m (c . f)
 
-instance Applicative (M n r) where
-    pure x  = M $ \c -> c x
-    f <*> v = M $ \c -> runM f (\g -> runM v (c . g))
+instance Applicative (S n r) where
+    pure x  = S $ \c -> c x
+    f <*> v = S $ \c -> runSTM f (\g -> runSTM v (c . g))
 
-instance Monad (M n r) where
+instance Monad (S n r) where
     return  = pure
-    m >>= k = M $ \c -> runM m (\x -> runM (k x) c)
+    m >>= k = S $ \c -> runSTM m (\x -> runSTM (k x) c)
 
 #if MIN_VERSION_base(4,9,0)
     fail = Fail.fail
 
--- | @since 0.7.1.2
-instance Fail.MonadFail (M n r) where
+instance Fail.MonadFail (S n r) where
 #endif
-    fail e = cont (\_ -> SThrow (MonadFailException e))
+    fail e = S $ \_ -> SThrow (MonadFailException e)
 
--- | Construct a continuation-passing operation from a function.
-cont :: ((a -> STMAction n r) -> STMAction n r) -> M n r a
-cont = M
+instance MonadThrow (S n r) where
+  throwM e = S $ \_ -> SThrow e
 
--- | Run a CPS computation with the given final computation.
-runCont :: M n r a -> (a -> STMAction n r) -> STMAction n r
-runCont = runM
+instance MonadCatch (S n r) where
+  catch stm handler = S $ SCatch handler stm
+
+instance Alternative (S n r) where
+  a <|> b = S $ SOrElse a b
+  empty = S $ const SRetry
+
+instance MonadPlus (S n r)
+
+instance C.MonadSTM (S n r) where
+  type TVar (S n r) = TVar r
+
+  newTVarN n = S . SNew n
+
+  readTVar = S . SRead
+
+  writeTVar tvar a = S $ \c -> SWrite tvar a (c ())
 
 --------------------------------------------------------------------------------
 -- * Primitive actions
@@ -71,10 +90,10 @@ runCont = runM
 -- | STM transactions are represented as a sequence of primitive
 -- actions.
 data STMAction n r
-  = forall a e. Exception e => SCatch (e -> M n r a) (M n r a) (a -> STMAction n r)
+  = forall a e. Exception e => SCatch (e -> S n r a) (S n r a) (a -> STMAction n r)
   | forall a. SRead  (TVar r a) (a -> STMAction n r)
   | forall a. SWrite (TVar r a) a (STMAction n r)
-  | forall a. SOrElse (M n r a) (M n r a) (a -> STMAction n r)
+  | forall a. SOrElse (S n r a) (S n r a) (a -> STMAction n r)
   | forall a. SNew String a (TVar r a -> STMAction n r)
   | forall e. Exception e => SThrow e
   | SRetry
@@ -93,8 +112,6 @@ newtype TVar r a = TVar (TVarId, r a)
 
 -- | The result of an STM transaction, along with which 'TVar's it
 -- touched whilst executing.
---
--- @since 0.1.0.0
 data Result a =
     Success [TVarId] [TVarId] a
   -- ^ The transaction completed successfully, reading the first list
@@ -107,41 +124,35 @@ data Result a =
   -- ^ The transaction aborted by throwing an exception.
   deriving Show
 
--- | This only reduces a 'SomeException' to WHNF.
---
--- @since 0.5.1.0
-instance NFData a => NFData (Result a) where
-  rnf (Success tr1 tr2 a) = rnf (tr1, tr2, a)
-  rnf (Retry tr) = rnf tr
-  rnf (Exception e) = e `seq` ()
-
--- | Check if a 'Result' is a @Success@.
-isSTMSuccess :: Result a -> Bool
-isSTMSuccess (Success _ _ _) = True
-isSTMSuccess _ = False
-
-instance Functor Result where
-  fmap f (Success rs ws a) = Success rs ws $ f a
-  fmap _ (Retry rs)    = Retry rs
-  fmap _ (Exception e) = Exception e
-
-instance Foldable Result where
-  foldMap f (Success _ _ a) = f a
-  foldMap _ _ = mempty
 
 --------------------------------------------------------------------------------
 -- * Execution
 
+-- | Run a transaction, returning the result and new initial 'TVarId'.
+-- If the transaction failed, any effects are undone.
+runTransaction :: MonadRef r n
+  => S n r a
+  -> IdSource
+  -> n (Result a, IdSource, [TAction])
+runTransaction ma tvid = do
+  (res, _, tvid', trace) <- doTransaction ma tvid
+  pure (res, tvid', trace)
+
 -- | Run a STM transaction, returning an action to undo its effects.
-doTransaction :: MonadRef r n => M n r a -> IdSource -> n (Result a, n (), IdSource, TTrace)
+--
+-- If the transaction fails, its effects will automatically be undone,
+-- so the undo action returned will be @pure ()@.
+doTransaction :: MonadRef r n
+  => S n r a
+  -> IdSource
+  -> n (Result a, n (), IdSource, [TAction])
 doTransaction ma idsource = do
-  (c, ref) <- runRefCont SStop (Just . Right) (runCont ma)
+  (c, ref) <- runRefCont SStop (Just . Right) (runSTM ma)
   (idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] []
   res <- readRef ref
 
   case res of
     Just (Right val) -> pure (Success (nub readen) (nub written) val, undo, idsource', reverse trace)
-
     Just (Left  exc) -> undo >> pure (Exception exc,      pure (), idsource, reverse trace)
     Nothing          -> undo >> pure (Retry $ nub readen, pure (), idsource, reverse trace)
 
@@ -167,7 +178,10 @@ doTransaction ma idsource = do
         _ -> go ref newAct newUndo newIDSource newReaden newWritten newSofar
 
 -- | Run a transaction for one step.
-stepTrans :: MonadRef r n => STMAction n r -> IdSource -> n (STMAction n r, n (), IdSource, [TVarId], [TVarId], TAction)
+stepTrans :: MonadRef r n
+  => STMAction n r
+  -> IdSource
+  -> n (STMAction n r, n (), IdSource, [TVarId], [TVarId], TAction)
 stepTrans act idsource = case act of
   SCatch  h stm c -> stepCatch h stm c
   SRead   ref c   -> stepRead ref c

dejafu/Test/DejaFu/Conc/Internal/Threading.hs

@@ -3,7 +3,7 @@
 
 -- |
 -- Module      : Test.DejaFu.Conc.Internal.Threading
--- Copyright   : (c) 2016 Michael Walker
+-- Copyright   : (c) 2016--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
@@ -13,14 +13,16 @@
 -- form part of the public interface of this library.
 module Test.DejaFu.Conc.Internal.Threading where
 
+import qualified Control.Concurrent.Classy        as C
 import           Control.Exception                (Exception, MaskingState(..),
                                                    SomeException, fromException)
 import           Data.List                        (intersect)
 import           Data.Map.Strict                  (Map)
 import           Data.Maybe                       (isJust)
 
-import           Test.DejaFu.Common
 import           Test.DejaFu.Conc.Internal.Common
+import           Test.DejaFu.Internal
+import           Test.DejaFu.Types
 
 import qualified Data.Map.Strict                  as M
 
@@ -40,11 +42,23 @@ data Thread n r = Thread
   -- ^ Stack of exception handlers
   , _masking      :: MaskingState
   -- ^ The exception masking state.
+  , _bound        :: Maybe (BoundThread n r)
+  -- ^ State for the associated bound thread, if it exists.
+  }
+
+-- | The state of a bound thread.
+data BoundThread n r = BoundThread
+  { _runboundIO :: C.MVar n (n (Action n r))
+  -- ^ Run an @IO@ action in the bound thread by writing to this.
+  , _getboundIO :: C.MVar n (Action n r)
+  -- ^ Get the result of the above by reading from this.
+  , _boundTId   :: C.ThreadId n
+  -- ^ Thread ID
   }
 
 -- | Construct a thread with just one action
 mkthread :: Action n r -> Thread n r
-mkthread c = Thread c Nothing [] Unmasked
+mkthread c = Thread c Nothing [] Unmasked Nothing
 
 --------------------------------------------------------------------------------
 -- * Blocking
@@ -122,15 +136,11 @@ launch parent tid a threads = launch' ms tid a threads where
 -- | Start a thread with the given ID and masking state. This must not already be in use!
 launch' :: MaskingState -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r
 launch' ms tid a = M.insert tid thread where
-  thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = ms }
+  thread = Thread (a umask) Nothing [] ms Nothing
 
   umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False ms >> pure b
   resetMask typ m = cont $ \k -> AResetMask typ True m $ k ()
 
--- | Kill a thread.
-kill :: ThreadId -> Threads n r -> Threads n r
-kill = M.delete
-
 -- | Block a thread.
 block :: BlockedOn -> ThreadId -> Threads n r -> Threads n r
 block blockedOn = M.adjust $ \thread -> thread { _blocking = Just blockedOn }
@@ -147,3 +157,44 @@ wake blockedOn threads = (unblock <$> threads, M.keys $ M.filter isBlocked threa
   isBlocked thread = case (_blocking thread, blockedOn) of
     (Just (OnTVar tvids), OnTVar blockedOn') -> tvids `intersect` blockedOn' /= []
     (theblock, _) -> theblock == Just blockedOn
+
+-------------------------------------------------------------------------------
+-- ** Bound threads
+
+-- | Turn a thread into a bound thread.
+makeBound :: C.MonadConc n => ThreadId -> Threads n r -> n (Threads n r)
+makeBound tid threads = do
+    runboundIO <- C.newEmptyMVar
+    getboundIO <- C.newEmptyMVar
+    btid <- C.forkOSN ("bound worker for '" ++ show tid ++ "'") (go runboundIO getboundIO)
+    let bt = BoundThread runboundIO getboundIO btid
+    pure (M.adjust (\t -> t { _bound = Just bt }) tid threads)
+  where
+    go runboundIO getboundIO =
+      let loop = do
+            na <- C.takeMVar runboundIO
+            C.putMVar getboundIO =<< na
+            loop
+      in loop
+
+-- | Kill a thread and remove it from the thread map.
+--
+-- If the thread is bound, the worker thread is cleaned up.
+kill :: C.MonadConc n => ThreadId -> Threads n r -> n (Threads n r)
+kill tid threads = case M.lookup tid threads of
+  Just thread -> case _bound thread of
+    Just bt -> do
+      C.killThread (_boundTId bt)
+      pure (M.delete tid threads)
+    Nothing -> pure (M.delete tid threads)
+  Nothing -> pure threads
+
+-- | Run an action.
+--
+-- If the thread is bound, the action is run in the worker thread.
+runLiftedAct :: C.MonadConc n => ThreadId -> Threads n r -> n (Action n r) -> n (Action n r)
+runLiftedAct tid threads ma = case _bound =<< M.lookup tid threads of
+  Just bt -> do
+    C.putMVar (_runboundIO bt) ma
+    C.takeMVar (_getboundIO bt)
+  Nothing -> ma

dejafu/Test/DejaFu/Defaults.hs

@@ -9,8 +9,8 @@
 -- Default parameters for test execution.
 module Test.DejaFu.Defaults where
 
-import           Test.DejaFu.Common
 import           Test.DejaFu.SCT
+import           Test.DejaFu.Types
 
 -- | A default way to execute concurrent programs: systematically
 -- using 'defaultBounds'.

dejafu/Test/DejaFu/Internal.hs

@@ -0,0 +1,338 @@
+-- |
+-- Module      : Test.DejaFu.Internal
+-- Copyright   : (c) 2017 Michael Walker
+-- License     : MIT
+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
+-- Stability   : experimental
+-- Portability : portable
+--
+-- Internal types and functions used throughout DejaFu.  This module
+-- is NOT considered to form part of the public interface of this
+-- library.
+module Test.DejaFu.Internal where
+
+import           Control.DeepSeq    (NFData(..))
+import           Control.Monad.Ref  (MonadRef(..))
+import           Data.List.NonEmpty (NonEmpty(..))
+import           Data.Maybe         (fromMaybe)
+import           Data.Set           (Set)
+import qualified Data.Set           as S
+
+import           Test.DejaFu.Types
+
+-------------------------------------------------------------------------------
+-- * Identifiers
+
+-- | The number of ID parameters was getting a bit unwieldy, so this
+-- hides them all away.
+data IdSource = IdSource
+  { _crids :: (Int, [String])
+  , _mvids :: (Int, [String])
+  , _tvids :: (Int, [String])
+  , _tids  :: (Int, [String])
+  } deriving (Eq, Ord, Show)
+
+instance NFData IdSource where
+  rnf idsource = rnf ( _crids idsource
+                     , _mvids idsource
+                     , _tvids idsource
+                     , _tids  idsource
+                     )
+
+-- | Get the next free 'CRefId'.
+nextCRId :: String -> IdSource -> (IdSource, CRefId)
+nextCRId name idsource =
+  let (crid, crids') = nextId name (_crids idsource)
+  in (idsource { _crids = crids' }, CRefId crid)
+
+-- | Get the next free 'MVarId'.
+nextMVId :: String -> IdSource -> (IdSource, MVarId)
+nextMVId name idsource =
+  let (mvid, mvids') = nextId name (_mvids idsource)
+  in (idsource { _mvids = mvids' }, MVarId mvid)
+
+-- | Get the next free 'TVarId'.
+nextTVId :: String -> IdSource -> (IdSource, TVarId)
+nextTVId name idsource =
+  let (tvid, tvids') = nextId name (_tvids idsource)
+  in (idsource { _tvids = tvids' }, TVarId tvid)
+
+-- | Get the next free 'ThreadId'.
+nextTId :: String -> IdSource -> (IdSource, ThreadId)
+nextTId name idsource =
+  let (tid, tids') = nextId name (_tids idsource)
+  in (idsource { _tids = tids' }, ThreadId tid)
+
+-- | Helper for @next*@
+nextId :: String -> (Int, [String]) -> (Id, (Int, [String]))
+nextId name (num, used) = (Id newName (num+1), (num+1, newUsed)) where
+  newName
+    | null name = Nothing
+    | occurrences > 0 = Just (name ++ "-" ++ show occurrences)
+    | otherwise = Just name
+  newUsed
+    | null name = used
+    | otherwise = name : used
+  occurrences = length (filter (==name) used)
+
+-- | The initial ID source.
+initialIdSource :: IdSource
+initialIdSource = IdSource (0, []) (0, []) (0, []) (0, [])
+
+-------------------------------------------------------------------------------
+-- * Actions
+
+-- | Check if a @ThreadAction@ immediately blocks.
+isBlock :: ThreadAction -> Bool
+isBlock (BlockedThrowTo  _) = True
+isBlock (BlockedTakeMVar _) = True
+isBlock (BlockedReadMVar _) = True
+isBlock (BlockedPutMVar  _) = True
+isBlock (BlockedSTM _) = True
+isBlock _ = False
+
+-- | Get the @TVar@s affected by a @ThreadAction@.
+tvarsOf :: ThreadAction -> Set TVarId
+tvarsOf act = tvarsRead act `S.union` tvarsWritten act
+
+-- | Get the @TVar@s a transaction wrote to (or would have, if it
+-- didn't @retry@).
+tvarsWritten :: ThreadAction -> Set TVarId
+tvarsWritten act = S.fromList $ case act of
+  STM trc _ -> concatMap tvarsOf' trc
+  BlockedSTM trc -> concatMap tvarsOf' trc
+  _ -> []
+
+  where
+    tvarsOf' (TWrite tv) = [tv]
+    tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
+    tvarsOf' (TCatch  ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
+    tvarsOf' _ = []
+
+-- | Get the @TVar@s a transaction read from.
+tvarsRead :: ThreadAction -> Set TVarId
+tvarsRead act = S.fromList $ case act of
+  STM trc _ -> concatMap tvarsOf' trc
+  BlockedSTM trc -> concatMap tvarsOf' trc
+  _ -> []
+
+  where
+    tvarsOf' (TRead tv) = [tv]
+    tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
+    tvarsOf' (TCatch  ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)
+    tvarsOf' _ = []
+
+-- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has
+-- happened. 'Killed' has no 'Lookahead' counterpart.
+rewind :: ThreadAction -> Maybe Lookahead
+rewind (Fork _) = Just WillFork
+rewind (ForkOS _) = Just WillForkOS
+rewind (IsCurrentThreadBound _) = Just WillIsCurrentThreadBound
+rewind MyThreadId = Just WillMyThreadId
+rewind (GetNumCapabilities _) = Just WillGetNumCapabilities
+rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i)
+rewind Yield = Just WillYield
+rewind (ThreadDelay n) = Just (WillThreadDelay n)
+rewind (NewMVar _) = Just WillNewMVar
+rewind (PutMVar c _) = Just (WillPutMVar c)
+rewind (BlockedPutMVar c) = Just (WillPutMVar c)
+rewind (TryPutMVar c _ _) = Just (WillTryPutMVar c)
+rewind (ReadMVar c) = Just (WillReadMVar c)
+rewind (BlockedReadMVar c) = Just (WillReadMVar c)
+rewind (TryReadMVar c _) = Just (WillTryReadMVar c)
+rewind (TakeMVar c _) = Just (WillTakeMVar c)
+rewind (BlockedTakeMVar c) = Just (WillTakeMVar c)
+rewind (TryTakeMVar c _ _) = Just (WillTryTakeMVar c)
+rewind (NewCRef _) = Just WillNewCRef
+rewind (ReadCRef c) = Just (WillReadCRef c)
+rewind (ReadCRefCas c) = Just (WillReadCRefCas c)
+rewind (ModCRef c) = Just (WillModCRef c)
+rewind (ModCRefCas c) = Just (WillModCRefCas c)
+rewind (WriteCRef c) = Just (WillWriteCRef c)
+rewind (CasCRef c _) = Just (WillCasCRef c)
+rewind (CommitCRef t c) = Just (WillCommitCRef t c)
+rewind (STM _ _) = Just WillSTM
+rewind (BlockedSTM _) = Just WillSTM
+rewind Catching = Just WillCatching
+rewind PopCatching = Just WillPopCatching
+rewind Throw = Just WillThrow
+rewind (ThrowTo t) = Just (WillThrowTo t)
+rewind (BlockedThrowTo t) = Just (WillThrowTo t)
+rewind Killed = Nothing
+rewind (SetMasking b m) = Just (WillSetMasking b m)
+rewind (ResetMasking b m) = Just (WillResetMasking b m)
+rewind LiftIO = Just WillLiftIO
+rewind Return = Just WillReturn
+rewind Stop = Just WillStop
+rewind Subconcurrency = Just WillSubconcurrency
+rewind StopSubconcurrency = Just WillStopSubconcurrency
+
+-- | Check if an operation could enable another thread.
+willRelease :: Lookahead -> Bool
+willRelease WillFork = True
+willRelease WillForkOS = True
+willRelease WillYield = True
+willRelease (WillThreadDelay _) = True
+willRelease (WillPutMVar _) = True
+willRelease (WillTryPutMVar _) = True
+willRelease (WillReadMVar _) = True
+willRelease (WillTakeMVar _) = True
+willRelease (WillTryTakeMVar _) = True
+willRelease WillSTM = True
+willRelease WillThrow = True
+willRelease (WillSetMasking _ _) = True
+willRelease (WillResetMasking _ _) = True
+willRelease WillStop = True
+willRelease _ = False
+
+-------------------------------------------------------------------------------
+-- * Simplified actions
+
+-- | A simplified view of the possible actions a thread can perform.
+data ActionType =
+    UnsynchronisedRead  CRefId
+  -- ^ A 'readCRef' or a 'readForCAS'.
+  | UnsynchronisedWrite CRefId
+  -- ^ A 'writeCRef'.
+  | UnsynchronisedOther
+  -- ^ Some other action which doesn't require cross-thread
+  -- communication.
+  | PartiallySynchronisedCommit CRefId
+  -- ^ A commit.
+  | PartiallySynchronisedWrite  CRefId
+  -- ^ A 'casCRef'
+  | PartiallySynchronisedModify CRefId
+  -- ^ A 'modifyCRefCAS'
+  | SynchronisedModify  CRefId
+  -- ^ An 'atomicModifyCRef'.
+  | SynchronisedRead    MVarId
+  -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants).
+  | SynchronisedWrite   MVarId
+  -- ^ A 'putMVar' (or @try@/@blocked@ variant).
+  | SynchronisedOther
+  -- ^ Some other action which does require cross-thread
+  -- communication.
+  deriving (Eq, Show)
+
+instance NFData ActionType where
+  rnf (UnsynchronisedRead c) = rnf c
+  rnf (UnsynchronisedWrite c) = rnf c
+  rnf (PartiallySynchronisedCommit c) = rnf c
+  rnf (PartiallySynchronisedWrite c) = rnf c
+  rnf (PartiallySynchronisedModify c) = rnf c
+  rnf (SynchronisedModify c) = rnf c
+  rnf (SynchronisedRead m) = rnf m
+  rnf (SynchronisedWrite m) = rnf m
+  rnf a = a `seq` ()
+
+-- | Check if an action imposes a write barrier.
+isBarrier :: ActionType -> Bool
+isBarrier (SynchronisedModify _) = True
+isBarrier (SynchronisedRead   _) = True
+isBarrier (SynchronisedWrite  _) = True
+isBarrier SynchronisedOther = True
+isBarrier _ = False
+
+-- | Check if an action commits a given 'CRef'.
+isCommit :: ActionType -> CRefId -> Bool
+isCommit (PartiallySynchronisedCommit c) r = c == r
+isCommit (PartiallySynchronisedWrite  c) r = c == r
+isCommit (PartiallySynchronisedModify c) r = c == r
+isCommit _ _ = False
+
+-- | Check if an action synchronises a given 'CRef'.
+synchronises :: ActionType -> CRefId -> Bool
+synchronises a r = isCommit a r || isBarrier a
+
+-- | Get the 'CRef' affected.
+crefOf :: ActionType -> Maybe CRefId
+crefOf (UnsynchronisedRead  r) = Just r
+crefOf (UnsynchronisedWrite r) = Just r
+crefOf (SynchronisedModify  r) = Just r
+crefOf (PartiallySynchronisedCommit r) = Just r
+crefOf (PartiallySynchronisedWrite  r) = Just r
+crefOf (PartiallySynchronisedModify r) = Just r
+crefOf _ = Nothing
+
+-- | Get the 'MVar' affected.
+mvarOf :: ActionType -> Maybe MVarId
+mvarOf (SynchronisedRead  c) = Just c
+mvarOf (SynchronisedWrite c) = Just c
+mvarOf _ = Nothing
+
+-- | Throw away information from a 'ThreadAction' and give a
+-- simplified view of what is happening.
+--
+-- This is used in the SCT code to help determine interesting
+-- alternative scheduling decisions.
+simplifyAction :: ThreadAction -> ActionType
+simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind
+
+-- | Variant of 'simplifyAction' that takes a 'Lookahead'.
+simplifyLookahead :: Lookahead -> ActionType
+simplifyLookahead (WillPutMVar c)     = SynchronisedWrite c
+simplifyLookahead (WillTryPutMVar c)  = SynchronisedWrite c
+simplifyLookahead (WillReadMVar c)    = SynchronisedRead c
+simplifyLookahead (WillTryReadMVar c) = SynchronisedRead c
+simplifyLookahead (WillTakeMVar c)    = SynchronisedRead c
+simplifyLookahead (WillTryTakeMVar c)  = SynchronisedRead c
+simplifyLookahead (WillReadCRef r)     = UnsynchronisedRead r
+simplifyLookahead (WillReadCRefCas r)  = UnsynchronisedRead r
+simplifyLookahead (WillModCRef r)      = SynchronisedModify r
+simplifyLookahead (WillModCRefCas r)   = PartiallySynchronisedModify r
+simplifyLookahead (WillWriteCRef r)    = UnsynchronisedWrite r
+simplifyLookahead (WillCasCRef r)      = PartiallySynchronisedWrite r
+simplifyLookahead (WillCommitCRef _ r) = PartiallySynchronisedCommit r
+simplifyLookahead WillSTM         = SynchronisedOther
+simplifyLookahead (WillThrowTo _) = SynchronisedOther
+simplifyLookahead _ = UnsynchronisedOther
+
+-------------------------------------------------------------------------------
+-- * Error reporting
+
+-- | 'head' but with a better error message if it fails.  Use this
+-- only where it shouldn't fail!
+ehead :: String -> [a] -> a
+ehead _ (x:_) = x
+ehead src _ = fatal src "head: empty list"
+
+-- | 'tail' but with a better error message if it fails.  Use this
+-- only where it shouldn't fail!
+etail :: String -> [a] -> [a]
+etail _ (_:xs) = xs
+etail src _ = fatal src "tail: empty list"
+
+-- | '(!!)' but with a better error message if it fails.  Use this
+-- only where it shouldn't fail!
+eidx :: String -> [a] -> Int -> a
+eidx src xs i
+  | i < length xs = xs !! i
+  | otherwise = fatal src "(!!): index too large"
+
+-- | 'fromJust' but with a better error message if it fails.  Use this
+-- only where it shouldn't fail!
+efromJust :: String -> Maybe a -> a
+efromJust _ (Just x) = x
+efromJust src _ = fatal src "fromJust: Nothing"
+
+-- | 'fromList' but with a better error message if it fails.  Use this
+-- only where it shouldn't fail!
+efromList :: String -> [a] -> NonEmpty a
+efromList _ (x:xs) = x:|xs
+efromList src _ = fatal src "fromList: empty list"
+
+-- | 'error' but saying where it came from
+fatal :: String -> String -> a
+fatal src msg = error ("(dejafu: " ++ src ++ ") " ++ msg)
+
+-------------------------------------------------------------------------------
+-- * Miscellaneous
+
+-- | Run with a continuation that writes its value into a reference,
+-- returning the computation and the reference.  Using the reference
+-- is non-blocking, it is up to you to ensure you wait sufficiently.
+runRefCont :: MonadRef r n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, r (Maybe b))
+runRefCont act f k = do
+  ref <- newRef Nothing
+  let c = k (act . writeRef ref . f)
+  pure (c, ref)

dejafu/Test/DejaFu/Refinement.hs

@@ -106,8 +106,7 @@ module Test.DejaFu.Refinement
   ) where
 
 import           Control.Arrow            (first)
-import           Control.Monad            (void)
-import           Control.Monad.Conc.Class (readMVar, spawn)
+import           Control.Monad.Conc.Class (fork)
 import           Data.Maybe               (isNothing)
 import           Data.Set                 (Set)
 import qualified Data.Set                 as S
@@ -410,9 +409,9 @@ evalSigWithSeed sig x = do
   results <- runSCT defaultWay defaultMemType $ do
     s <- initialise sig x
     r <- subconcurrency $ do
-      j <- spawn (interfere sig s x)
-      void (expression sig s)
-      void (readMVar j)
+      _ <- fork (interfere sig s x)
+      _ <- expression sig s
+      pure ()
     o <- observe sig s x
     pure (either Just (const Nothing) r, o)
   pure . S.fromList $ map (\(Right a, _) -> a) results

dejafu/Test/DejaFu/SCT.hs

@@ -4,7 +4,7 @@
 
 -- |
 -- Module      : Test.DejaFu.SCT
--- Copyright   : (c) 2016 Michael Walker
+-- Copyright   : (c) 2015--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
@@ -59,38 +59,13 @@ module Test.DejaFu.SCT
   -- K. McKinley for more details.
 
   , Bounds(..)
+  , PreemptionBound(..)
+  , FairBound(..)
+  , LengthBound(..)
   , noBounds
   , sctBound
   , sctBoundDiscard
 
-  -- ** Pre-emption Bounding
-
-  -- | BPOR using pre-emption bounding. This adds conservative
-  -- backtracking points at the prior context switch whenever a
-  -- non-conervative backtracking point is added, as alternative
-  -- decisions can influence the reachability of different states.
-  --
-  -- See the BPOR paper for more details.
-
-  , PreemptionBound(..)
-
-  -- ** Fair Bounding
-
-  -- | BPOR using fair bounding. This bounds the maximum difference
-  -- between the number of yield operations different threads have
-  -- performed.
-  --
-  -- See the BPOR paper for more details.
-
-  , FairBound(..)
-
-  -- ** Length Bounding
-
-  -- | BPOR using length bounding. This bounds the maximum length (in
-  -- terms of primitive actions) of an execution.
-
-  , LengthBound(..)
-
   -- * Random Scheduling
 
   -- | By greatly sacrificing completeness, testing of a large
@@ -106,19 +81,23 @@ module Test.DejaFu.SCT
   , sctWeightedRandomDiscard
   ) where
 
-import           Control.Applicative      ((<|>))
-import           Control.DeepSeq          (NFData(..), force)
-import           Control.Monad.Ref        (MonadRef)
-import           Data.List                (foldl')
-import qualified Data.Map.Strict          as M
-import           Data.Maybe               (fromMaybe)
-import           Data.Set                 (Set)
-import qualified Data.Set                 as S
-import           System.Random            (RandomGen, randomR)
+import           Control.Applicative               ((<|>))
+import           Control.DeepSeq                   (NFData(..), force)
+import           Control.Monad.Conc.Class          (MonadConc)
+import           Control.Monad.Ref                 (MonadRef)
+import           Data.List                         (foldl')
+import qualified Data.Map.Strict                   as M
+import           Data.Maybe                        (fromMaybe)
+import           Data.Set                          (Set)
+import qualified Data.Set                          as S
+import           System.Random                     (RandomGen, randomR)
 
-import           Test.DejaFu.Common
 import           Test.DejaFu.Conc
-import           Test.DejaFu.SCT.Internal
+import           Test.DejaFu.Internal
+import           Test.DejaFu.SCT.Internal.DPOR
+import           Test.DejaFu.SCT.Internal.Weighted
+import           Test.DejaFu.Types
+import           Test.DejaFu.Utils
 
 -------------------------------------------------------------------------------
 -- Running Concurrent Programs
@@ -207,8 +186,11 @@ swarmy = Weighted
 -- | Explore possible executions of a concurrent program according to
 -- the given 'Way'.
 --
--- @since 0.6.0.0
-runSCT :: MonadRef r n
+-- The exact executions tried, and the order in which results are
+-- found, is unspecified and may change between releases.
+--
+-- @since 1.0.0.0
+runSCT :: (MonadConc n, MonadRef r n)
   => Way
   -- ^ How to run the concurrent program.
   -> MemType
@@ -220,8 +202,8 @@ runSCT = runSCTDiscard (const Nothing)
 
 -- | Return the set of results of a concurrent program.
 --
--- @since 0.6.0.0
-resultsSet :: (MonadRef r n, Ord a)
+-- @since 1.0.0.0
+resultsSet :: (MonadConc n, MonadRef r n, Ord a)
   => Way
   -- ^ How to run the concurrent program.
   -> MemType
@@ -231,26 +213,13 @@ resultsSet :: (MonadRef r n, Ord a)
   -> n (Set (Either Failure a))
 resultsSet = resultsSetDiscard (const Nothing)
 
--- | An @Either Failure a -> Maybe Discard@ value can be used to
--- selectively discard results.
---
--- @since 0.7.1.0
-data Discard
-  = DiscardTrace
-  -- ^ Discard the trace but keep the result.  The result will appear
-  -- to have an empty trace.
-  | DiscardResultAndTrace
-  -- ^ Discard the result and the trace.  It will simply not be
-  -- reported as a possible behaviour of the program.
-  deriving (Eq, Show, Read, Ord, Enum, Bounded)
-
-instance NFData Discard where
-  rnf d = d `seq` ()
-
 -- | A variant of 'runSCT' which can selectively discard results.
 --
--- @since 0.7.1.0
-runSCTDiscard :: MonadRef r n
+-- The exact executions tried, and the order in which results are
+-- found, is unspecified and may change between releases.
+--
+-- @since 1.0.0.0
+runSCTDiscard :: (MonadConc n, MonadRef r n)
   => (Either Failure a -> Maybe Discard)
   -- ^ Selectively discard results.
   -> Way
@@ -266,8 +235,8 @@ runSCTDiscard discard (Uniform  g lim)     memtype = sctUniformRandomDiscard  di
 
 -- | A variant of 'resultsSet' which can selectively discard results.
 --
--- @since 0.7.1.0
-resultsSetDiscard :: (MonadRef r n, Ord a)
+-- @since 1.0.0.0
+resultsSetDiscard :: (MonadConc n, MonadRef r n, Ord a)
   => (Either Failure a -> Maybe Discard)
   -- ^ Selectively discard results.  Traces are always discarded.
   -> Way
@@ -286,8 +255,11 @@ resultsSetDiscard discard way memtype conc =
 -- Demanding the result of this will force it to normal form, which
 -- may be more efficient in some situations.
 --
--- @since 0.6.0.0
-runSCT' :: (MonadRef r n, NFData a)
+-- The exact executions tried, and the order in which results are
+-- found, is unspecified and may change between releases.
+--
+-- @since 1.0.0.0
+runSCT' :: (MonadConc n, MonadRef r n, NFData a)
   => Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)]
 runSCT' = runSCTDiscard' (const Nothing)
 
@@ -296,8 +268,8 @@ runSCT' = runSCTDiscard' (const Nothing)
 -- Demanding the result of this will force it to normal form, which
 -- may be more efficient in some situations.
 --
--- @since 0.6.0.0
-resultsSet' :: (MonadRef r n, Ord a, NFData a)
+-- @since 1.0.0.0
+resultsSet' :: (MonadConc n, MonadRef r n, Ord a, NFData a)
   => Way -> MemType -> ConcT r n a -> n (Set (Either Failure a))
 resultsSet' = resultsSetDiscard' (const Nothing)
 
@@ -306,8 +278,11 @@ resultsSet' = resultsSetDiscard' (const Nothing)
 -- Demanding the result of this will force it to normal form, which
 -- may be more efficient in some situations.
 --
--- @since 0.7.1.0
-runSCTDiscard' :: (MonadRef r n, NFData a)
+-- The exact executions tried, and the order in which results are
+-- found, is unspecified and may change between releases.
+--
+-- @since 1.0.0.0
+runSCTDiscard' :: (MonadConc n, MonadRef r n, NFData a)
   => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)]
 runSCTDiscard' discard way memtype conc = do
   res <- runSCTDiscard discard way memtype conc
@@ -318,8 +293,8 @@ runSCTDiscard' discard way memtype conc = do
 -- Demanding the result of this will force it to normal form, which
 -- may be more efficient in some situations.
 --
--- @since 0.7.1.0
-resultsSetDiscard' :: (MonadRef r n, Ord a, NFData a)
+-- @since 1.0.0.0
+resultsSetDiscard' :: (MonadConc n, MonadRef r n, Ord a, NFData a)
   => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT r n a -> n (Set (Either Failure a))
 resultsSetDiscard' discard way memtype conc = do
   res <- resultsSetDiscard discard way memtype conc
@@ -376,7 +351,14 @@ cBacktrack _ = backtrackAt (\_ _ -> False)
 -------------------------------------------------------------------------------
 -- Pre-emption bounding
 
--- | @since 0.2.0.0
+-- | BPOR using pre-emption bounding. This adds conservative
+-- backtracking points at the prior context switch whenever a
+-- non-conervative backtracking point is added, as alternative
+-- decisions can influence the reachability of different states.
+--
+-- See the BPOR paper for more details.
+--
+-- @since 0.2.0.0
 newtype PreemptionBound = PreemptionBound Int
   deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
 
@@ -415,7 +397,13 @@ pBacktrack bs = backtrackAt (\_ _ -> False) bs . concatMap addConservative where
 -------------------------------------------------------------------------------
 -- Fair bounding
 
--- | @since 0.2.0.0
+-- | BPOR using fair bounding. This bounds the maximum difference
+-- between the number of yield operations different threads have
+-- performed.
+--
+-- See the BPOR paper for more details.
+--
+-- @since 0.2.0.0
 newtype FairBound = FairBound Int
   deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
 
@@ -432,8 +420,8 @@ fBound (FairBound fb) k prior lhead =
      then Just k'
      else Nothing
 
--- | Add a backtrack point. If the thread isn't runnable, or performs
--- a release operation, add all runnable threads.
+-- | Add a backtrack point. If the thread doesn't exist or is blocked,
+-- or performs a release operation, add all unblocked threads.
 fBacktrack :: BacktrackFunc
 fBacktrack = backtrackAt check where
   -- True if a release operation is performed.
@@ -442,7 +430,10 @@ fBacktrack = backtrackAt check where
 -------------------------------------------------------------------------------
 -- Length bounding
 
--- | @since 0.2.0.0
+-- | BPOR using length bounding. This bounds the maximum length (in
+-- terms of primitive actions) of an execution.
+--
+-- @since 0.2.0.0
 newtype LengthBound = LengthBound Int
   deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)
 
@@ -457,8 +448,8 @@ lBound (LengthBound lb) len _ _ =
   let len' = maybe 1 (+1) len
   in if len' < lb then Just len' else Nothing
 
--- | Add a backtrack point. If the thread isn't runnable, add all
--- runnable threads.
+-- | Add a backtrack point. If the thread doesn't exist or is blocked,
+-- add all unblocked threads.
 lBacktrack :: BacktrackFunc
 lBacktrack = backtrackAt (\_ _ -> False)
 
@@ -477,8 +468,11 @@ lBacktrack = backtrackAt (\_ _ -> False)
 -- do some redundant work as the introduction of a bound can make
 -- previously non-interfering events interfere with each other.
 --
--- @since 0.5.0.0
-sctBound :: MonadRef r n
+-- The exact executions tried, and the order in which results are
+-- found, is unspecified and may change between releases.
+--
+-- @since 1.0.0.0
+sctBound :: (MonadConc n, MonadRef r n)
   => MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
   -> Bounds
@@ -490,8 +484,11 @@ sctBound = sctBoundDiscard (const Nothing)
 
 -- | A variant of 'sctBound' which can selectively discard results.
 --
--- @since 0.7.1.0
-sctBoundDiscard :: MonadRef r n
+-- The exact executions tried, and the order in which results are
+-- found, is unspecified and may change between releases.
+--
+-- @since 1.0.0.0
+sctBoundDiscard :: (MonadConc n, MonadRef r n)
   => (Either Failure a -> Maybe Discard)
   -- ^ Selectively discard results.
   -> MemType
@@ -533,8 +530,8 @@ sctBoundDiscard discard memtype cb conc = go initialState where
 --
 -- This is not guaranteed to find all distinct results.
 --
--- @since 0.7.0.0
-sctUniformRandom :: (MonadRef r n, RandomGen g)
+-- @since 1.0.0.0
+sctUniformRandom :: (MonadConc n, MonadRef r n, RandomGen g)
   => MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
   -> g
@@ -549,8 +546,10 @@ sctUniformRandom = sctUniformRandomDiscard (const Nothing)
 -- | A variant of 'sctUniformRandom' which can selectively discard
 -- results.
 --
--- @since 0.7.1.0
-sctUniformRandomDiscard :: (MonadRef r n, RandomGen g)
+-- This is not guaranteed to find all distinct results.
+--
+-- @since 1.0.0.0
+sctUniformRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g)
   => (Either Failure a -> Maybe Discard)
   -- ^ Selectively discard results.
   -> MemType
@@ -578,8 +577,8 @@ sctUniformRandomDiscard discard memtype g0 lim0 conc = go g0 (max 0 lim0) where
 --
 -- This is not guaranteed to find all distinct results.
 --
--- @since 0.7.0.0
-sctWeightedRandom :: (MonadRef r n, RandomGen g)
+-- @since 1.0.0.0
+sctWeightedRandom :: (MonadConc n, MonadRef r n, RandomGen g)
   => MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
   -> g
@@ -596,8 +595,10 @@ sctWeightedRandom = sctWeightedRandomDiscard (const Nothing)
 -- | A variant of 'sctWeightedRandom' which can selectively discard
 -- results.
 --
--- @since 0.7.1.0
-sctWeightedRandomDiscard :: (MonadRef r n, RandomGen g)
+-- This is not guaranteed to find all distinct results.
+--
+-- @since 1.0.0.0
+sctWeightedRandomDiscard :: (MonadConc n, MonadRef r n, RandomGen g)
   => (Either Failure a -> Maybe Discard)
   -- ^ Selectively discard results.
   -> MemType

dejafu/Test/DejaFu/SCT/Internal/DPOR.hs

@@ -1,17 +1,15 @@
-{-# LANGUAGE TupleSections #-}
-
 -- |
--- Module      : Test.DejaFu.SCT.Internal
--- Copyright   : (c) 2016 Michael Walker
+-- Module      : Test.DejaFu.SCT.Internal.DPOR
+-- Copyright   : (c) 2015--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
--- Portability : TupleSections
+-- Portability : portable
 --
--- Internal types and functions for dynamic partial-order
--- reduction. This module is NOT considered to form part of the public
--- interface of this library.
-module Test.DejaFu.SCT.Internal where
+-- Internal types and functions for SCT via dynamic partial-order
+-- reduction.  This module is NOT considered to form part of the
+-- public interface of this library.
+module Test.DejaFu.SCT.Internal.DPOR where
 
 import           Control.Applicative  ((<|>))
 import           Control.DeepSeq      (NFData(..))
@@ -22,16 +20,16 @@ import           Data.List            (nubBy, partition, sortOn)
 import           Data.List.NonEmpty   (toList)
 import           Data.Map.Strict      (Map)
 import qualified Data.Map.Strict      as M
-import           Data.Maybe           (fromMaybe, isJust, isNothing,
-                                       listToMaybe)
+import           Data.Maybe           (isJust, isNothing, listToMaybe)
 import           Data.Sequence        (Seq, (|>))
 import qualified Data.Sequence        as Sq
 import           Data.Set             (Set)
 import qualified Data.Set             as S
-import           System.Random        (RandomGen, randomR)
 
-import           Test.DejaFu.Common
-import           Test.DejaFu.Schedule (Scheduler(..), decisionOf, tidOf)
+import           Test.DejaFu.Internal
+import           Test.DejaFu.Schedule (Scheduler(..))
+import           Test.DejaFu.Types
+import           Test.DejaFu.Utils    (decisionOf, tidOf)
 
 -------------------------------------------------------------------------------
 -- * Dynamic partial-order reduction
@@ -529,51 +527,7 @@ dporSched boundf = Scheduler $ \prior threads s ->
           (Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill', schedBState = Nothing })
 
 -------------------------------------------------------------------------------
--- Weighted random scheduler
-
--- | The scheduler state
-data RandSchedState g = RandSchedState
-  { schedWeights :: Map ThreadId Int
-  -- ^ The thread weights: used in determining which to run.
-  , schedGen     :: g
-  -- ^ The random number generator.
-  } deriving (Eq, Show)
-
-instance NFData g => NFData (RandSchedState g) where
-  rnf s = rnf ( schedWeights s
-              , schedGen     s
-              )
-
--- | Initial weighted random scheduler state.
-initialRandSchedState :: Maybe (Map ThreadId Int) -> g -> RandSchedState g
-initialRandSchedState = RandSchedState . fromMaybe M.empty
-
--- | Weighted random scheduler: assigns to each new thread a weight,
--- and makes a weighted random choice out of the runnable threads at
--- every step.
-randSched :: RandomGen g => (g -> (Int, g)) -> Scheduler (RandSchedState g)
-randSched weightf = Scheduler $ \_ threads s ->
-  let
-    -- Select a thread
-    pick idx ((x, f):xs)
-      | idx < f = Just x
-      | otherwise = pick (idx - f) xs
-    pick _ [] = Nothing
-    (choice, g'') = randomR (0, sum (map snd enabled) - 1) g'
-    enabled = M.toList $ M.filterWithKey (\tid _ -> tid `elem` tids) weights'
-
-    -- The weights, with any new threads added.
-    (weights', g') = foldr assignWeight (M.empty, schedGen s) tids
-    assignWeight tid ~(ws, g0) =
-      let (w, g) = maybe (weightf g0) (,g0) (M.lookup tid (schedWeights s))
-      in (M.insert tid w ws, g)
-
-    -- The runnable threads.
-    tids = map fst (toList threads)
-  in (pick choice enabled, RandSchedState weights' g'')
-
--------------------------------------------------------------------------------
--- Dependency function
+-- * Dependency function
 
 -- | Check if an action is dependent on another.
 --
@@ -678,6 +632,12 @@ dependentActions ds a1 a2 = case (a1, a2) of
   (PartiallySynchronisedCommit _, _) | isBarrier a2 -> True
   (_, PartiallySynchronisedCommit _) | isBarrier a1 -> True
 
+  -- Two @MVar@ puts are dependent if they're to the same empty
+  -- @MVar@, and two takes are dependent if they're to the same full
+  -- @MVar@.
+  (SynchronisedWrite v1, SynchronisedWrite v2) -> v1 == v2 && not (isFull ds v1)
+  (SynchronisedRead  v1, SynchronisedRead  v2) -> v1 == v2 && isFull ds v1
+
   (_, _) -> case getSame crefOf of
     -- Two actions on the same CRef where at least one is synchronised
     Just r -> synchronises a1 r || synchronises a2 r
@@ -695,11 +655,13 @@ dependentActions ds a1 a2 = case (a1, a2) of
       in if f1 == f2 then f1 else Nothing
 
 -------------------------------------------------------------------------------
--- Dependency function state
+-- ** Dependency function state
 
 data DepState = DepState
   { depCRState :: Map CRefId Bool
   -- ^ Keep track of which @CRef@s have buffered writes.
+  , depMVState :: Set MVarId
+  -- ^ Keep track of which @MVar@s are full.
   , depMaskState :: Map ThreadId MaskingState
   -- ^ Keep track of thread masking states. If a thread isn't present,
   -- the masking state is assumed to be @Unmasked@. This nicely
@@ -709,22 +671,24 @@ data DepState = DepState
 
 instance NFData DepState where
   rnf depstate = rnf ( depCRState depstate
+                     , depMVState depstate
                      , [(t, m `seq` ()) | (t, m) <- M.toList (depMaskState depstate)]
                      )
 
 -- | Initial dependency state.
 initialDepState :: DepState
-initialDepState = DepState M.empty M.empty
+initialDepState = DepState M.empty S.empty M.empty
 
--- | Update the 'CRef' buffer state with the action that has just
+-- | Update the dependency state with the action that has just
 -- happened.
 updateDepState :: DepState -> ThreadId -> ThreadAction -> DepState
 updateDepState depstate tid act = DepState
   { depCRState   = updateCRState       act $ depCRState   depstate
+  , depMVState   = updateMVState       act $ depMVState   depstate
   , depMaskState = updateMaskState tid act $ depMaskState depstate
   }
 
--- | Update the 'CRef' buffer state with the action that has just
+-- | Update the @CRef@ buffer state with the action that has just
 -- happened.
 updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool
 updateCRState (CommitCRef _ r) = M.delete r
@@ -733,6 +697,15 @@ updateCRState ta
   | isBarrier $ simplifyAction ta = const M.empty
   | otherwise = id
 
+-- | Update the @MVar@ full/empty state with the action that has just
+-- happened.
+updateMVState :: ThreadAction -> Set MVarId -> Set MVarId
+updateMVState (PutMVar mvid _) = S.insert mvid
+updateMVState (TryPutMVar mvid True _) = S.insert mvid
+updateMVState (TakeMVar mvid _) = S.delete mvid
+updateMVState (TryTakeMVar mvid True _) = S.delete mvid
+updateMVState _ = id
+
 -- | Update the thread masking state with the action that has just
 -- happened.
 updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState
@@ -744,10 +717,14 @@ updateMaskState tid (SetMasking   _ ms) = M.insert tid ms
 updateMaskState tid (ResetMasking _ ms) = M.insert tid ms
 updateMaskState _ _ = id
 
--- | Check if a 'CRef' has a buffered write pending.
+-- | Check if a @CRef@ has a buffered write pending.
 isBuffered :: DepState -> CRefId -> Bool
 isBuffered depstate r = M.findWithDefault False r (depCRState depstate)
 
+-- | Check if an @MVar@ is full.
+isFull :: DepState -> MVarId -> Bool
+isFull depstate v = S.member v (depMVState depstate)
+
 -- | Check if an exception can interrupt a thread (action).
 canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool
 canInterrupt depstate tid act

dejafu/Test/DejaFu/SCT/Internal/Weighted.hs

@@ -0,0 +1,66 @@
+-- |
+-- Module      : Test.DejaFu.SCT.Internal.Weighted
+-- Copyright   : (c) 2015--2017 Michael Walker
+-- License     : MIT
+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
+-- Stability   : experimental
+-- Portability : portable
+--
+-- Internal types and functions for SCT via weighted random
+-- scheduling.  This module is NOT considered to form part of the
+-- public interface of this library.
+module Test.DejaFu.SCT.Internal.Weighted where
+
+import           Control.DeepSeq      (NFData(..))
+import           Data.List.NonEmpty   (toList)
+import           Data.Map.Strict      (Map)
+import qualified Data.Map.Strict      as M
+import           Data.Maybe           (fromMaybe)
+import           System.Random        (RandomGen, randomR)
+
+import           Test.DejaFu.Schedule (Scheduler(..))
+import           Test.DejaFu.Types
+
+-------------------------------------------------------------------------------
+-- * Weighted random scheduler
+
+-- | The scheduler state
+data RandSchedState g = RandSchedState
+  { schedWeights :: Map ThreadId Int
+  -- ^ The thread weights: used in determining which to run.
+  , schedGen     :: g
+  -- ^ The random number generator.
+  } deriving (Eq, Show)
+
+instance NFData g => NFData (RandSchedState g) where
+  rnf s = rnf ( schedWeights s
+              , schedGen     s
+              )
+
+-- | Initial weighted random scheduler state.
+initialRandSchedState :: Maybe (Map ThreadId Int) -> g -> RandSchedState g
+initialRandSchedState = RandSchedState . fromMaybe M.empty
+
+-- | Weighted random scheduler: assigns to each new thread a weight,
+-- and makes a weighted random choice out of the runnable threads at
+-- every step.
+randSched :: RandomGen g => (g -> (Int, g)) -> Scheduler (RandSchedState g)
+randSched weightf = Scheduler $ \_ threads s ->
+  let
+    -- Select a thread
+    pick idx ((x, f):xs)
+      | idx < f = Just x
+      | otherwise = pick (idx - f) xs
+    pick _ [] = Nothing
+    (choice, g'') = randomR (0, sum (map snd enabled) - 1) g'
+    enabled = M.toList $ M.filterWithKey (\tid _ -> tid `elem` tids) weights'
+
+    -- The weights, with any new threads added.
+    (weights', g') = foldr assignWeight (M.empty, schedGen s) tids
+    assignWeight tid ~(ws, g0) =
+      let (w, g) = maybe (weightf g0) (\w0 -> (w0, g0)) (M.lookup tid (schedWeights s))
+      in (M.insert tid w ws, g)
+
+    -- The runnable threads.
+    tids = map fst (toList threads)
+  in (pick choice enabled, RandSchedState weights' g'')

dejafu/Test/DejaFu/STM.hs

@@ -1,122 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeFamilies #-}
-
--- |
--- Module      : Test.DejaFu.STM
--- Copyright   : (c) 2016 Michael Walker
--- License     : MIT
--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
--- Stability   : experimental
--- Portability : CPP, GeneralizedNewtypeDeriving, RankNTypes, TypeFamilies
---
--- A 'MonadSTM' implementation, which can be run on top of 'IO' or
--- 'ST'.
-module Test.DejaFu.STM
-  ( -- * The @STMLike@ Monad
-    STMLike
-  , STMST
-  , STMIO
-
-  -- * Executing Transactions
-  , Result(..)
-  , TTrace
-  , TAction(..)
-  , TVarId
-  , runTransaction
-  ) where
-
-import           Control.Applicative      (Alternative(..))
-import           Control.Monad            (MonadPlus(..), unless)
-import           Control.Monad.Catch      (MonadCatch(..), MonadThrow(..))
-import           Control.Monad.Ref        (MonadRef)
-import           Control.Monad.ST         (ST)
-import           Data.IORef               (IORef)
-import           Data.STRef               (STRef)
-
-import qualified Control.Monad.STM.Class  as C
-import           Test.DejaFu.Common
-import           Test.DejaFu.STM.Internal
-
-#if MIN_VERSION_base(4,9,0)
-import qualified Control.Monad.Fail       as Fail
-#endif
-
--- | @since 0.3.0.0
-newtype STMLike n r a = S { runSTM :: M n r a } deriving (Functor, Applicative, Monad)
-
-#if MIN_VERSION_base(4,9,0)
--- | @since 0.9.1.0
-instance Fail.MonadFail (STMLike r n) where
-  fail = S . fail
-#endif
-
--- | Create a new STM continuation.
-toSTM :: ((a -> STMAction n r) -> STMAction n r) -> STMLike n r a
-toSTM = S . cont
-
--- | A 'MonadSTM' implementation using @ST@, it encapsulates a single
--- atomic transaction. The environment, that is, the collection of
--- defined 'TVar's is implicit, there is no list of them, they exist
--- purely as references. This makes the types simpler, but means you
--- can't really get an aggregate of them (if you ever wanted to for
--- some reason).
---
--- @since 0.3.0.0
-type STMST t = STMLike (ST t) (STRef t)
-
--- | A 'MonadSTM' implementation using @ST@, it encapsulates a single
--- atomic transaction. The environment, that is, the collection of
--- defined 'TVar's is implicit, there is no list of them, they exist
--- purely as references. This makes the types simpler, but means you
--- can't really get an aggregate of them (if you ever wanted to for
--- some reason).
---
--- @since 0.3.0.0
-type STMIO = STMLike IO IORef
-
-instance MonadThrow (STMLike n r) where
-  throwM = toSTM . const . SThrow
-
-instance MonadCatch (STMLike n r) where
-  catch (S stm) handler = toSTM (SCatch (runSTM . handler) stm)
-
--- | @since 0.7.2.0
-instance Alternative (STMLike n r) where
-  S a <|> S b = toSTM (SOrElse a b)
-  empty = toSTM (const SRetry)
-
--- | @since 0.7.2.0
-instance MonadPlus (STMLike n r)
-
-instance C.MonadSTM (STMLike n r) where
-  type TVar (STMLike n r) = TVar r
-
-#if MIN_VERSION_concurrency(1,2,0)
-  -- retry and orElse are top-level definitions in
-  -- Control.Monad.STM.Class in 1.2 and up
-#else
-  retry = empty
-  orElse = (<|>)
-#endif
-
-  newTVarN n = toSTM . SNew n
-
-  readTVar = toSTM . SRead
-
-  writeTVar tvar a = toSTM (\c -> SWrite tvar a (c ()))
-
--- | Run a transaction, returning the result and new initial
--- 'TVarId'. If the transaction ended by calling 'retry', any 'TVar'
--- modifications are undone.
---
--- @since 0.4.0.0
-runTransaction :: MonadRef r n
-               => STMLike n r a -> IdSource -> n (Result a, IdSource, TTrace)
-runTransaction ma tvid = do
-  (res, undo, tvid', trace) <- doTransaction (runSTM ma) tvid
-
-  unless (isSTMSuccess res) undo
-
-  pure (res, tvid', trace)

dejafu/Test/DejaFu/Schedule.hs

@@ -1,6 +1,6 @@
 -- |
 -- Module      : Test.DejaFu.Schedule
--- Copyright   : (c) 2016 Michael Walker
+-- Copyright   : (c) 2016--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
@@ -11,12 +11,6 @@ module Test.DejaFu.Schedule
   ( -- * Scheduling
     Scheduler(..)
 
-  , Decision(..)
-  , tidOf
-  , decisionOf
-
-  , NonEmpty(..)
-
   -- ** Preemptive
   , randomSched
   , roundRobinSched
@@ -29,10 +23,11 @@ module Test.DejaFu.Schedule
   , makeNonPreemptive
   ) where
 
-import           Data.List.NonEmpty (NonEmpty(..), toList)
-import           System.Random      (RandomGen, randomR)
+import           Data.List.NonEmpty   (NonEmpty(..), toList)
+import           System.Random        (RandomGen, randomR)
 
-import           Test.DejaFu.Common
+import           Test.DejaFu.Internal
+import           Test.DejaFu.Types
 
 -- | A @Scheduler@ drives the execution of a concurrent program. The
 -- parameters it takes are:
@@ -40,7 +35,7 @@ import           Test.DejaFu.Common
 -- 1. The last thread executed (if this is the first invocation, this
 --    is @Nothing@).
 --
--- 2. The runnable threads at this point.
+-- 2. The unblocked threads.
 --
 -- 3. The state.
 --
@@ -56,36 +51,6 @@ newtype Scheduler state = Scheduler
     -> (Maybe ThreadId, state)
   }
 
--------------------------------------------------------------------------------
--- Scheduling decisions
-
--- | Get the resultant thread identifier of a 'Decision', with a default case
--- for 'Continue'.
---
--- @since 0.5.0.0
-tidOf :: ThreadId -> Decision -> ThreadId
-tidOf _ (Start t)    = t
-tidOf _ (SwitchTo t) = t
-tidOf tid _          = tid
-
--- | Get the 'Decision' that would have resulted in this thread identifier,
--- given a prior thread (if any) and list of runnable threads.
---
--- @since 0.5.0.0
-decisionOf :: Foldable f
-  => Maybe ThreadId
-  -- ^ The prior thread.
-  -> f ThreadId
-  -- ^ The runnable threads.
-  -> ThreadId
-  -- ^ The current thread.
-  -> Decision
-decisionOf Nothing _ chosen = Start chosen
-decisionOf (Just prior) runnable chosen
-  | prior == chosen = Continue
-  | prior `elem` runnable = SwitchTo chosen
-  | otherwise = Start chosen
-
 -------------------------------------------------------------------------------
 -- Preemptive
 
@@ -118,16 +83,18 @@ roundRobinSched = Scheduler go where
 -------------------------------------------------------------------------------
 -- Non-preemptive
 
--- | A random scheduler which doesn't preempt the running
--- thread. That is, if the last thread scheduled is still runnable,
--- run that, otherwise schedule randomly.
+-- | A random scheduler which doesn't preempt the running thread. That
+-- is, if the previously scheduled thread is not blocked, it is picked
+-- again, otherwise schedule randomly.
 --
 -- @since 0.8.0.0
 randomSchedNP :: RandomGen g => Scheduler g
 randomSchedNP = makeNonPreemptive randomSched
 
 -- | A round-robin scheduler which doesn't preempt the running
--- thread.
+-- thread. That is, if the previously scheduled thread is not blocked,
+-- it is picked again, otherwise schedule the thread with the next
+-- 'ThreadId'.
 --
 -- @since 0.8.0.0
 roundRobinSchedNP :: Scheduler ()

dejafu/Test/DejaFu/Types.hs

@@ -0,0 +1,566 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+-- |
+-- Module      : Test.DejaFu.Types
+-- Copyright   : (c) 2017 Michael Walker
+-- License     : MIT
+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
+-- Stability   : experimental
+-- Portability : GeneralizedNewtypeDeriving
+--
+-- Common types and functions used throughout DejaFu.
+module Test.DejaFu.Types where
+
+import           Control.DeepSeq   (NFData(..))
+import           Control.Exception (Exception(..), MaskingState(..),
+                                    SomeException)
+import           Data.Function     (on)
+
+-------------------------------------------------------------------------------
+-- * Identifiers
+
+-- | Every thread has a unique identitifer.
+--
+-- @since 1.0.0.0
+newtype ThreadId = ThreadId Id
+  deriving (Eq, Ord, NFData)
+
+instance Show ThreadId where
+  show (ThreadId id_) = show id_
+
+-- | Every @CRef@ has a unique identifier.
+--
+-- @since 1.0.0.0
+newtype CRefId = CRefId Id
+  deriving (Eq, Ord, NFData)
+
+instance Show CRefId where
+  show (CRefId id_) = show id_
+
+-- | Every @MVar@ has a unique identifier.
+--
+-- @since 1.0.0.0
+newtype MVarId = MVarId Id
+  deriving (Eq, Ord, NFData)
+
+instance Show MVarId where
+  show (MVarId id_) = show id_
+
+-- | Every @TVar@ has a unique identifier.
+--
+-- @since 1.0.0.0
+newtype TVarId = TVarId Id
+  deriving (Eq, Ord, NFData)
+
+instance Show TVarId where
+  show (TVarId id_) = show id_
+
+-- | An identifier for a thread, @MVar@, @CRef@, or @TVar@.
+--
+-- The number is the important bit.  The string is to make execution
+-- traces easier to read, but is meaningless.
+data Id = Id (Maybe String) {-# UNPACK #-} !Int
+
+instance Eq Id where
+  (Id _ i) == (Id _ j) = i == j
+
+instance Ord Id where
+  compare (Id _ i) (Id _ j) = compare i j
+
+instance Show Id where
+  show (Id (Just n) _) = n
+  show (Id _ i) = show i
+
+instance NFData Id where
+  rnf (Id n i) = rnf (n, i)
+
+-- | The ID of the initial thread.
+--
+-- @since 0.4.0.0
+initialThread :: ThreadId
+initialThread = ThreadId (Id (Just "main") 0)
+
+-------------------------------------------------------------------------------
+-- * Actions
+
+-- | All the actions that a thread can perform.
+--
+-- @since 1.0.0.0
+data ThreadAction =
+    Fork ThreadId
+  -- ^ Start a new thread.
+  | ForkOS ThreadId
+  -- ^ Start a new bound thread.
+  | IsCurrentThreadBound Bool
+  -- ^ Check if the current thread is bound.
+  | MyThreadId
+  -- ^ Get the 'ThreadId' of the current thread.
+  | GetNumCapabilities Int
+  -- ^ Get the number of Haskell threads that can run simultaneously.
+  | SetNumCapabilities Int
+  -- ^ Set the number of Haskell threads that can run simultaneously.
+  | Yield
+  -- ^ Yield the current thread.
+  | ThreadDelay Int
+  -- ^ Yield/delay the current thread.
+  | NewMVar MVarId
+  -- ^ Create a new 'MVar'.
+  | PutMVar MVarId [ThreadId]
+  -- ^ Put into a 'MVar', possibly waking up some threads.
+  | BlockedPutMVar MVarId
+  -- ^ Get blocked on a put.
+  | TryPutMVar MVarId Bool [ThreadId]
+  -- ^ Try to put into a 'MVar', possibly waking up some threads.
+  | ReadMVar MVarId
+  -- ^ Read from a 'MVar'.
+  | TryReadMVar MVarId Bool
+  -- ^ Try to read from a 'MVar'.
+  | BlockedReadMVar MVarId
+  -- ^ Get blocked on a read.
+  | TakeMVar MVarId [ThreadId]
+  -- ^ Take from a 'MVar', possibly waking up some threads.
+  | BlockedTakeMVar MVarId
+  -- ^ Get blocked on a take.
+  | TryTakeMVar MVarId Bool [ThreadId]
+  -- ^ Try to take from a 'MVar', possibly waking up some threads.
+  | NewCRef CRefId
+  -- ^ Create a new 'CRef'.
+  | ReadCRef CRefId
+  -- ^ Read from a 'CRef'.
+  | ReadCRefCas CRefId
+  -- ^ Read from a 'CRef' for a future compare-and-swap.
+  | ModCRef CRefId
+  -- ^ Modify a 'CRef'.
+  | ModCRefCas CRefId
+  -- ^ Modify a 'CRef' using a compare-and-swap.
+  | WriteCRef CRefId
+  -- ^ Write to a 'CRef' without synchronising.
+  | CasCRef CRefId Bool
+  -- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising
+  -- it.
+  | CommitCRef ThreadId CRefId
+  -- ^ Commit the last write to the given 'CRef' by the given thread,
+  -- so that all threads can see the updated value.
+  | STM [TAction] [ThreadId]
+  -- ^ An STM transaction was executed, possibly waking up some
+  -- threads.
+  | BlockedSTM [TAction]
+  -- ^ Got blocked in an STM transaction.
+  | Catching
+  -- ^ Register a new exception handler
+  | PopCatching
+  -- ^ Pop the innermost exception handler from the stack.
+  | Throw
+  -- ^ Throw an exception.
+  | ThrowTo ThreadId
+  -- ^ Throw an exception to a thread.
+  | BlockedThrowTo ThreadId
+  -- ^ Get blocked on a 'throwTo'.
+  | Killed
+  -- ^ Killed by an uncaught exception.
+  | SetMasking Bool MaskingState
+  -- ^ Set the masking state. If 'True', this is being used to set the
+  -- masking state to the original state in the argument passed to a
+  -- 'mask'ed function.
+  | ResetMasking Bool MaskingState
+  -- ^ Return to an earlier masking state.  If 'True', this is being
+  -- used to return to the state of the masked block in the argument
+  -- passed to a 'mask'ed function.
+  | LiftIO
+  -- ^ Lift an IO action. Note that this can only happen with
+  -- 'ConcIO'.
+  | Return
+  -- ^ A 'return' or 'pure' action was executed.
+  | Stop
+  -- ^ Cease execution and terminate.
+  | Subconcurrency
+  -- ^ Start executing an action with @subconcurrency@.
+  | StopSubconcurrency
+  -- ^ Stop executing an action with @subconcurrency@.
+  deriving (Eq, Show)
+
+instance NFData ThreadAction where
+  rnf (Fork t) = rnf t
+  rnf (ForkOS t) = rnf t
+  rnf (ThreadDelay n) = rnf n
+  rnf (GetNumCapabilities c) = rnf c
+  rnf (SetNumCapabilities c) = rnf c
+  rnf (NewMVar m) = rnf m
+  rnf (PutMVar m ts) = rnf (m, ts)
+  rnf (BlockedPutMVar m) = rnf m
+  rnf (TryPutMVar m b ts) = rnf (m, b, ts)
+  rnf (ReadMVar m) = rnf m
+  rnf (TryReadMVar m b) = rnf (m, b)
+  rnf (BlockedReadMVar m) = rnf m
+  rnf (TakeMVar m ts) = rnf (m, ts)
+  rnf (BlockedTakeMVar m) = rnf m
+  rnf (TryTakeMVar m b ts) = rnf (m, b, ts)
+  rnf (NewCRef c) = rnf c
+  rnf (ReadCRef c) = rnf c
+  rnf (ReadCRefCas c) = rnf c
+  rnf (ModCRef c) = rnf c
+  rnf (ModCRefCas c) = rnf c
+  rnf (WriteCRef c) = rnf c
+  rnf (CasCRef c b) = rnf (c, b)
+  rnf (CommitCRef t c) = rnf (t, c)
+  rnf (STM tr ts) = rnf (tr, ts)
+  rnf (BlockedSTM tr) = rnf tr
+  rnf (ThrowTo t) = rnf t
+  rnf (BlockedThrowTo t) = rnf t
+  rnf (SetMasking b m) = b `seq` m `seq` ()
+  rnf (ResetMasking b m) = b `seq` m `seq` ()
+  rnf a = a `seq` ()
+
+-- | A one-step look-ahead at what a thread will do next.
+--
+-- @since 1.0.0.0
+data Lookahead =
+    WillFork
+  -- ^ Will start a new thread.
+  | WillForkOS
+  -- ^ Will start a new bound thread.
+  | WillIsCurrentThreadBound
+  -- ^ Will check if the current thread is bound.
+  | WillMyThreadId
+  -- ^ Will get the 'ThreadId'.
+  | WillGetNumCapabilities
+  -- ^ Will get the number of Haskell threads that can run
+  -- simultaneously.
+  | WillSetNumCapabilities Int
+  -- ^ Will set the number of Haskell threads that can run
+  -- simultaneously.
+  | WillYield
+  -- ^ Will yield the current thread.
+  | WillThreadDelay Int
+  -- ^ Will yield/delay the current thread.
+  | WillNewMVar
+  -- ^ Will create a new 'MVar'.
+  | WillPutMVar MVarId
+  -- ^ Will put into a 'MVar', possibly waking up some threads.
+  | WillTryPutMVar MVarId
+  -- ^ Will try to put into a 'MVar', possibly waking up some threads.
+  | WillReadMVar MVarId
+  -- ^ Will read from a 'MVar'.
+  | WillTryReadMVar MVarId
+  -- ^ Will try to read from a 'MVar'.
+  | WillTakeMVar MVarId
+  -- ^ Will take from a 'MVar', possibly waking up some threads.
+  | WillTryTakeMVar MVarId
+  -- ^ Will try to take from a 'MVar', possibly waking up some threads.
+  | WillNewCRef
+  -- ^ Will create a new 'CRef'.
+  | WillReadCRef CRefId
+  -- ^ Will read from a 'CRef'.
+  | WillReadCRefCas CRefId
+  -- ^ Will read from a 'CRef' for a future compare-and-swap.
+  | WillModCRef CRefId
+  -- ^ Will modify a 'CRef'.
+  | WillModCRefCas CRefId
+  -- ^ Will modify a 'CRef' using a compare-and-swap.
+  | WillWriteCRef CRefId
+  -- ^ Will write to a 'CRef' without synchronising.
+  | WillCasCRef CRefId
+  -- ^ Will attempt to to a 'CRef' using a compare-and-swap,
+  -- synchronising it.
+  | WillCommitCRef ThreadId CRefId
+  -- ^ Will commit the last write by the given thread to the 'CRef'.
+  | WillSTM
+  -- ^ Will execute an STM transaction, possibly waking up some
+  -- threads.
+  | WillCatching
+  -- ^ Will register a new exception handler
+  | WillPopCatching
+  -- ^ Will pop the innermost exception handler from the stack.
+  | WillThrow
+  -- ^ Will throw an exception.
+  | WillThrowTo ThreadId
+  -- ^ Will throw an exception to a thread.
+  | WillSetMasking Bool MaskingState
+  -- ^ Will set the masking state. If 'True', this is being used to
+  -- set the masking state to the original state in the argument
+  -- passed to a 'mask'ed function.
+  | WillResetMasking Bool MaskingState
+  -- ^ Will return to an earlier masking state.  If 'True', this is
+  -- being used to return to the state of the masked block in the
+  -- argument passed to a 'mask'ed function.
+  | WillLiftIO
+  -- ^ Will lift an IO action. Note that this can only happen with
+  -- 'ConcIO'.
+  | WillReturn
+  -- ^ Will execute a 'return' or 'pure' action.
+  | WillStop
+  -- ^ Will cease execution and terminate.
+  | WillSubconcurrency
+  -- ^ Will execute an action with @subconcurrency@.
+  | WillStopSubconcurrency
+  -- ^ Will stop executing an extion with @subconcurrency@.
+  deriving (Eq, Show)
+
+instance NFData Lookahead where
+  rnf (WillThreadDelay n) = rnf n
+  rnf (WillSetNumCapabilities c) = rnf c
+  rnf (WillPutMVar m) = rnf m
+  rnf (WillTryPutMVar m) = rnf m
+  rnf (WillReadMVar m) = rnf m
+  rnf (WillTryReadMVar m) = rnf m
+  rnf (WillTakeMVar m) = rnf m
+  rnf (WillTryTakeMVar m) = rnf m
+  rnf (WillReadCRef c) = rnf c
+  rnf (WillReadCRefCas c) = rnf c
+  rnf (WillModCRef c) = rnf c
+  rnf (WillModCRefCas c) = rnf c
+  rnf (WillWriteCRef c) = rnf c
+  rnf (WillCasCRef c) = rnf c
+  rnf (WillCommitCRef t c) = rnf (t, c)
+  rnf (WillThrowTo t) = rnf t
+  rnf (WillSetMasking b m) = b `seq` m `seq` ()
+  rnf (WillResetMasking b m) = b `seq` m `seq` ()
+  rnf l = l `seq` ()
+
+-- | All the actions that an STM transaction can perform.
+--
+-- @since 0.8.0.0
+data TAction =
+    TNew TVarId
+  -- ^ Create a new @TVar@
+  | TRead  TVarId
+  -- ^ Read from a @TVar@.
+  | TWrite TVarId
+  -- ^ Write to a @TVar@.
+  | TRetry
+  -- ^ Abort and discard effects.
+  | TOrElse [TAction] (Maybe [TAction])
+  -- ^ Execute a transaction.  If the transaction aborts by calling
+  -- @retry@, execute the other transaction.
+  | TThrow
+  -- ^ Throw an exception, abort, and discard effects.
+  | TCatch [TAction] (Maybe [TAction])
+  -- ^ Execute a transaction.  If the transaction aborts by throwing
+  -- an exception of the appropriate type, it is handled and execution
+  -- continues; otherwise aborts, propagating the exception upwards.
+  | TStop
+  -- ^ Terminate successfully and commit effects.
+  deriving (Eq, Show)
+
+-- | @since 0.5.1.0
+instance NFData TAction where
+  rnf (TRead t) = rnf t
+  rnf (TWrite t) = rnf t
+  rnf (TOrElse tr mtr) = rnf (tr, mtr)
+  rnf (TCatch tr mtr) = rnf (tr, mtr)
+  rnf ta = ta `seq` ()
+
+-------------------------------------------------------------------------------
+-- * Traces
+
+-- | 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
+type Trace
+  = [(Decision, [(ThreadId, Lookahead)], ThreadAction)]
+
+-- | 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
+data Decision =
+    Start ThreadId
+  -- ^ Start a new thread, because the last was blocked (or it's the
+  -- start of computation).
+  | Continue
+  -- ^ Continue running the last thread for another step.
+  | SwitchTo ThreadId
+  -- ^ Pre-empt the running thread, and switch to another.
+  deriving (Eq, Show)
+
+-- | @since 0.5.1.0
+instance NFData Decision where
+  rnf (Start t) = rnf t
+  rnf (SwitchTo t) = rnf t
+  rnf d = d `seq` ()
+
+-------------------------------------------------------------------------------
+-- * Failures
+
+-- | An indication of how a concurrent computation failed.
+--
+-- The @Eq@, @Ord@, and @NFData@ instances compare/evaluate the
+-- exception with @show@ in the @UncaughtException@ case.
+--
+-- @since 0.9.0.0
+data Failure
+  = InternalError
+  -- ^ Will be raised if the scheduler does something bad. This should
+  -- never arise unless you write your own, faulty, scheduler! If it
+  -- does, please file a bug report.
+  | Abort
+  -- ^ The scheduler chose to abort execution. This will be produced
+  -- if, for example, all possible decisions exceed the specified
+  -- bounds (there have been too many pre-emptions, the computation
+  -- has executed for too long, or there have been too many yields).
+  | Deadlock
+  -- ^ Every thread is blocked, and the main thread is /not/ blocked
+  -- in an STM transaction.
+  | STMDeadlock
+  -- ^ Every thread is blocked, and the main thread is blocked in an
+  -- STM transaction.
+  | UncaughtException SomeException
+  -- ^ An uncaught exception bubbled to the top of the computation.
+  | IllegalSubconcurrency
+  -- ^ Calls to @subconcurrency@ were nested, or attempted when
+  -- multiple threads existed.
+  deriving Show
+
+instance Eq Failure where
+  InternalError          == InternalError          = True
+  Abort                  == Abort                  = True
+  Deadlock               == Deadlock               = True
+  STMDeadlock            == STMDeadlock            = True
+  (UncaughtException e1) == (UncaughtException e2) = show e1 == show e2
+  IllegalSubconcurrency  == IllegalSubconcurrency  = True
+  _ == _ = False
+
+instance Ord Failure where
+  compare = compare `on` transform where
+    transform :: Failure -> (Int, Maybe String)
+    transform InternalError = (0, Nothing)
+    transform Abort = (1, Nothing)
+    transform Deadlock = (2, Nothing)
+    transform STMDeadlock = (3, Nothing)
+    transform (UncaughtException e) = (4, Just (show e))
+    transform IllegalSubconcurrency = (5, Nothing)
+
+instance NFData Failure where
+  rnf (UncaughtException e) = rnf (show e)
+  rnf f = f `seq` ()
+
+-- | Check if a failure is an @InternalError@.
+--
+-- @since 0.9.0.0
+isInternalError :: Failure -> Bool
+isInternalError InternalError = True
+isInternalError _ = False
+
+-- | Check if a failure is an @Abort@.
+--
+-- @since 0.9.0.0
+isAbort :: Failure -> Bool
+isAbort Abort = True
+isAbort _ = False
+
+-- | Check if a failure is a @Deadlock@ or an @STMDeadlock@.
+--
+-- @since 0.9.0.0
+isDeadlock :: Failure -> Bool
+isDeadlock Deadlock = True
+isDeadlock STMDeadlock = True
+isDeadlock _ = False
+
+-- | Check if a failure is an @UncaughtException@
+--
+-- @since 0.9.0.0
+isUncaughtException :: Failure -> Bool
+isUncaughtException (UncaughtException _) = True
+isUncaughtException _ = False
+
+-- | Check if a failure is an @IllegalSubconcurrency@
+--
+-- @since 0.9.0.0
+isIllegalSubconcurrency :: Failure -> Bool
+isIllegalSubconcurrency IllegalSubconcurrency = True
+isIllegalSubconcurrency _ = False
+
+-------------------------------------------------------------------------------
+-- * Discarding results and traces
+
+-- | An @Either Failure a -> Maybe Discard@ value can be used to
+-- selectively discard results.
+--
+-- @since 0.7.1.0
+data Discard
+  = DiscardTrace
+  -- ^ Discard the trace but keep the result.  The result will appear
+  -- to have an empty trace.
+  | DiscardResultAndTrace
+  -- ^ Discard the result and the trace.  It will simply not be
+  -- reported as a possible behaviour of the program.
+  deriving (Eq, Show, Read, Ord, Enum, Bounded)
+
+instance NFData Discard where
+  rnf d = d `seq` ()
+
+-- | Combine two discard values, keeping the weaker.
+--
+-- @Nothing@ is weaker than @Just DiscardTrace@, which is weaker than
+-- @Just DiscardResultAndTrace@.  This forms a commutative monoid
+-- where the unit is @const (Just DiscardResultAndTrace)@.
+--
+-- @since 1.0.0.0
+weakenDiscard ::
+     (Either Failure a -> Maybe Discard)
+  -> (Either Failure a -> Maybe Discard)
+  -> Either Failure a -> Maybe Discard
+weakenDiscard d1 d2 efa = case (d1 efa, d2 efa) of
+  (Nothing, _) -> Nothing
+  (_, Nothing) -> Nothing
+  (Just DiscardTrace, _) -> Just DiscardTrace
+  (_, Just DiscardTrace) -> Just DiscardTrace
+  _ -> Just DiscardResultAndTrace
+
+-- | Combine two discard functions, keeping the stronger.
+--
+-- @Just DiscardResultAndTrace@ is stronger than @Just DiscardTrace@,
+-- which is stronger than @Nothing@.  This forms a commutative monoid
+-- where the unit is @const Nothing@.
+--
+-- @since 1.0.0.0
+strengthenDiscard ::
+     (Either Failure a -> Maybe Discard)
+  -> (Either Failure a -> Maybe Discard)
+  -> Either Failure a -> Maybe Discard
+strengthenDiscard d1 d2 efa = case (d1 efa, d2 efa) of
+  (Just DiscardResultAndTrace, _) -> Just DiscardResultAndTrace
+  (_, Just DiscardResultAndTrace) -> Just DiscardResultAndTrace
+  (Just DiscardTrace, _) -> Just DiscardTrace
+  (_, Just DiscardTrace) -> Just DiscardTrace
+  _ -> Nothing
+
+-------------------------------------------------------------------------------
+-- * Memory Models
+
+-- | The memory model to use for non-synchronised 'CRef' operations.
+--
+-- @since 0.4.0.0
+data MemType =
+    SequentialConsistency
+  -- ^ The most intuitive model: a program behaves as a simple
+  -- interleaving of the actions in different threads. When a 'CRef'
+  -- is written to, that write is immediately visible to all threads.
+  | TotalStoreOrder
+  -- ^ Each thread has a write buffer. A thread sees its writes
+  -- immediately, but other threads will only see writes when they are
+  -- committed, which may happen later. Writes are committed in the
+  -- same order that they are created.
+  | PartialStoreOrder
+  -- ^ Each 'CRef' has a write buffer. A thread sees its writes
+  -- immediately, but other threads will only see writes when they are
+  -- committed, which may happen later. Writes to different 'CRef's
+  -- are not necessarily committed in the same order that they are
+  -- created.
+  deriving (Eq, Show, Read, Ord, Enum, Bounded)
+
+-- | @since 0.5.1.0
+instance NFData MemType where
+  rnf m = m `seq` ()
+
+-------------------------------------------------------------------------------
+-- * @MonadFail@
+
+-- | An exception for errors in testing caused by use of 'fail'.
+newtype MonadFailException = MonadFailException String
+  deriving Show
+
+instance Exception MonadFailException

dejafu/Test/DejaFu/Utils.hs

@@ -0,0 +1,114 @@
+-- |
+-- Module      : Test.DejaFu.utils
+-- Copyright   : (c) 2017 Michael Walker
+-- License     : MIT
+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
+-- Stability   : experimental
+-- Portability : portable
+--
+-- Utility functions for users of dejafu.
+module Test.DejaFu.Utils where
+
+import           Control.Exception (Exception(..), displayException)
+import           Data.List         (intercalate, minimumBy)
+import           Data.Maybe        (mapMaybe)
+import           Data.Ord          (comparing)
+
+import           Test.DejaFu.Types
+
+-------------------------------------------------------------------------------
+-- * Traces
+
+-- | 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
+showTrace :: Trace -> String
+showTrace []  = "<trace discarded>"
+showTrace trc = intercalate "\n" $ go False trc : strkey where
+  go _ ((_,_,CommitCRef _ _):rest) = "C-" ++ go False rest
+  go _ ((Start    (ThreadId (Id _ i)),_,a):rest) = "S" ++ show i ++ "-" ++ go (didYield a) rest
+  go y ((SwitchTo (ThreadId (Id _ i)),_,a):rest) = (if y then "p" else "P") ++ show i ++ "-" ++ go (didYield a) rest
+  go _ ((Continue,_,a):rest) = '-' : go (didYield a) rest
+  go _ _ = ""
+
+  strkey =
+    ["  " ++ show i ++ ": " ++ name | (i, name) <- threadNames trc]
+
+  didYield Yield = True
+  didYield (ThreadDelay _) = True
+  didYield _ = False
+
+-- | Get all named threads in the trace.
+--
+-- @since 0.7.3.0
+threadNames :: Trace -> [(Int, String)]
+threadNames = mapMaybe go where
+  go (_, _, Fork   (ThreadId (Id (Just name) i))) = Just (i, name)
+  go (_, _, ForkOS (ThreadId (Id (Just name) i))) = Just (i, name)
+  go _ = Nothing
+
+-- | Find the \"simplest\" trace leading to each result.
+simplestsBy :: (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)]
+simplestsBy f = map choose . collect where
+  collect = groupBy' [] (\(a,_) (b,_) -> f a b)
+  choose  = minimumBy . comparing $ \(_, trc) ->
+    let switchTos = length . filter (\(d,_,_) -> case d of SwitchTo _ -> True; _ -> False)
+        starts    = length . filter (\(d,_,_) -> case d of Start    _ -> True; _ -> False)
+        commits   = length . filter (\(_,_,a) -> case a of CommitCRef _ _ -> True; _ -> False)
+    in (switchTos trc, commits trc, length trc, starts trc)
+
+  groupBy' res _ [] = res
+  groupBy' res eq (y:ys) = groupBy' (insert' eq y res) eq ys
+
+  insert' _ x [] = [[x]]
+  insert' eq x (ys@(y:_):yss)
+    | x `eq` y  = (x:ys) : yss
+    | otherwise = ys : insert' eq x yss
+  insert' _ _ ([]:_) = undefined
+
+-------------------------------------------------------------------------------
+-- * Failures
+
+-- | Pretty-print a failure
+--
+-- @since 0.4.0.0
+showFail :: Failure -> String
+showFail Abort = "[abort]"
+showFail Deadlock = "[deadlock]"
+showFail STMDeadlock = "[stm-deadlock]"
+showFail InternalError = "[internal-error]"
+showFail (UncaughtException exc) = "[" ++ displayException exc ++ "]"
+showFail IllegalSubconcurrency = "[illegal-subconcurrency]"
+
+-------------------------------------------------------------------------------
+-- * Scheduling
+
+-- | Get the resultant thread identifier of a 'Decision', with a default case
+-- for 'Continue'.
+--
+-- @since 0.5.0.0
+tidOf :: ThreadId -> Decision -> ThreadId
+tidOf _ (Start t)    = t
+tidOf _ (SwitchTo t) = t
+tidOf tid _          = tid
+
+-- | Get the 'Decision' that would have resulted in this thread
+-- identifier, given a prior thread (if any) and collection of threads
+-- which are unblocked at this point.
+--
+-- @since 0.5.0.0
+decisionOf :: Foldable f
+  => Maybe ThreadId
+  -- ^ The prior thread.
+  -> f ThreadId
+  -- ^ The threads.
+  -> ThreadId
+  -- ^ The current thread.
+  -> Decision
+decisionOf Nothing _ chosen = Start chosen
+decisionOf (Just prior) runnable chosen
+  | prior == chosen = Continue
+  | prior `elem` runnable = SwitchTo chosen
+  | otherwise = Start chosen

dejafu/dejafu.cabal

@@ -2,29 +2,25 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                dejafu
-version:             0.9.1.2
-synopsis:            Systematic testing for Haskell concurrency.
+version:             1.0.0.0
+synopsis:            A library for unit-testing concurrent programs.
 
 description:
   /[Déjà Fu is] A martial art in which the user's limbs move in time as well as space, […] It is best described as "the feeling that you have been kicked in the head this way before"/ -- Terry Pratchett, Thief of Time
   .
-  Concurrency is nice, deadlocks and race conditions not so much. The
-  @Par@ monad family, as defined in
-  <https://hackage.haskell.org/package/abstract-par/docs/Control-Monad-Par-Class.html abstract-par>
-  provides deterministic parallelism, but sometimes we can tolerate a
-  bit of nondeterminism.
-  .
   This package builds on the
-  <https://hackage.haskell.org/package/concurrency concurrency>
-  package by enabling you to systematically and deterministically test
-  your concurrent programs.
+  [concurrency](https://hackage.haskell.org/package/concurrency)
+  package by enabling you to deterministically test your concurrent
+  programs.
+  .
+  See the [website](https://dejafu.readthedocs.io) or README for more.
 
 homepage:            https://github.com/barrucadu/dejafu
 license:             MIT
 license-file:        LICENSE
 author:              Michael Walker
 maintainer:          mike@barrucadu.co.uk
--- copyright:           
+copyright:           (c) 2015--2017 Michael Walker
 category:            Concurrency
 build-type:          Simple
 extra-source-files:  README.markdown CHANGELOG.markdown
@@ -37,37 +33,39 @@ source-repository head
 source-repository this
   type:     git
   location: https://github.com/barrucadu/dejafu.git
-  tag:      dejafu-0.9.1.2
+  tag:      dejafu-1.0.0.0
 
 library
   exposed-modules:     Test.DejaFu
                      , Test.DejaFu.Conc
-                     , Test.DejaFu.Common
                      , Test.DejaFu.Defaults
                      , Test.DejaFu.Refinement
-                     , Test.DejaFu.Schedule
                      , Test.DejaFu.SCT
-                     , Test.DejaFu.STM
+                     , Test.DejaFu.Schedule
+                     , Test.DejaFu.Types
+                     , Test.DejaFu.Utils
 
                      , Test.DejaFu.Conc.Internal
                      , Test.DejaFu.Conc.Internal.Common
                      , Test.DejaFu.Conc.Internal.Memory
+                     , Test.DejaFu.Conc.Internal.STM
                      , Test.DejaFu.Conc.Internal.Threading
-                     , Test.DejaFu.SCT.Internal
-                     , Test.DejaFu.STM.Internal
+                     , Test.DejaFu.Internal
+                     , Test.DejaFu.SCT.Internal.DPOR
+                     , Test.DejaFu.SCT.Internal.Weighted
 
   -- other-modules:       
   -- other-extensions:    
   build-depends:       base              >=4.8 && <5
-                     , concurrency       >=1.1 && <1.3
+                     , concurrency       >=1.3 && <1.4
                      , containers        >=0.5 && <0.6
                      , deepseq           >=1.1 && <2
                      , exceptions        >=0.7 && <0.9
                      , leancheck         >=0.6 && <0.8
+                     , profunctors       >=4.0 && <6.0
                      , random            >=1.0 && <1.2
                      , ref-fd            >=0.4 && <0.5
-                     , transformers      >=0.4  && <0.6
-                     , transformers-base >=0.4  && <0.5
+                     , transformers      >=0.4 && <0.6
   -- hs-source-dirs:      
   default-language:    Haskell2010
   ghc-options:         -Wall

doc/adding_a_new_primitive.rst

@@ -34,14 +34,14 @@ Normally it's a bad idea to add primitives which only work when
 testing, as they can't be used in ``IO`` code.
 
 
-Trace elements
+Thread actions
 --------------
 
 Every primitive has a corresponding constructor in the
 ``ThreadAction`` and ``Lookahead`` types, which appear in execution
 traces.
 
-These types live in ``Test.DejaFu.Common``:
+These types live in ``Test.DejaFu.Types``:
 
 .. code-block:: haskell
 
@@ -150,7 +150,8 @@ We also need a ``Lookahead`` equivalent:
 Both ``ThreadAction`` and ``Lookahead`` have ``NFData`` instances,
 don't forget to add the extra cases in those.
 
-The ``rewind`` function converts between ``ThreadAction`` and
+Now we jump over to the ``Test.DejaFu.Internal`` module.  The
+``rewind`` function converts between ``ThreadAction`` and
 ``Lookahead`` values, so we need to add a case to that as well:
 
 .. code-block:: haskell
@@ -159,7 +160,7 @@ The ``rewind`` function converts between ``ThreadAction`` and
 
 Finally, we need to make sure the systematic testing will treat our
 new primitive correctly.  As setting the value of an ``MVar`` may
-cause previously blocked threads to become runnable, it is a *release*
+cause previously blocked threads to be unblocked, it is a *release*
 action.  Furthermore, as it writes to an ``MVar`` it is a
 *synchronised write*:
 
@@ -183,14 +184,14 @@ action.  Furthermore, as it writes to an ``MVar`` it is a
   ``simplifyLookahead``
 
 
-Actions
--------
+Primitive actions
+-----------------
 
-Now jump to the ``Test.DejaFu.Conc.Internal.Common`` module (yes,
-another "common").  The ``Action`` type defines the actual primitive
-actions which are used to implement all the concurrency primitives.
-An ``Action`` value contains the information needed to perform that
-action and a continuation to call when it is done:
+Now jump to the ``Test.DejaFu.Conc.Internal.Common`` module.  The
+``Action`` type defines the actual primitive actions which are used to
+implement all the concurrency primitives.  An ``Action`` value
+contains the information needed to perform that action and a
+continuation to call when it is done:
 
 .. code-block:: haskell
 

doc/advanced.rst

@@ -53,9 +53,9 @@ We can see this by testing with different memory models:
 .. code-block:: none
 
   > autocheckWay defaultWay SequentialConsistency example
-  [pass] Never Deadlocks (checked: 6)
-  [pass] No Exceptions (checked: 6)
-  [fail] Consistent Result (checked: 5)
+  [pass] Never Deadlocks
+  [pass] No Exceptions
+  [fail] Consistent Result
           (False,True) S0---------S1----S0--S2----S0--
 
           (True,True) S0---------S1-P2----S1---S0---
@@ -64,9 +64,9 @@ We can see this by testing with different memory models:
   False
 
   > autocheckWay defaultWay TotalStoreOrder example
-  [pass] Never Deadlocks (checked: 28)
-  [pass] No Exceptions (checked: 28)
-  [fail] Consistent Result (checked: 27)
+  [pass] Never Deadlocks
+  [pass] No Exceptions
+  [fail] Consistent Result
           (False,True) S0---------S1----S0--S2----S0--
 
           (False,False) S0---------S1--P2----S1--S0---
@@ -95,8 +95,8 @@ There are three supported types of bounds:
 
 Pre-emption bounding
   Restricts the number of pre-emptive context switches.  A context
-  switch is pre-emptive if the previously executing thread is still
-  runnable and did not explicitly yield.
+  switch is pre-emptive if the previously executing thread is not
+  blocked and did not explicitly yield.
 
 Fair bounding
   Restricts how many times each thread can yield, by bounding the
@@ -136,7 +136,7 @@ There are three variants:
   Perform the given number of executions using weighted random
   scheduling.  On creation, a thread is given a random weight, which
   is used to perform a nonuniform random selection amongst the
-  runnable threads at every scheduling point.
+  enabled (not blocked) threads at every scheduling point.
 
 ``uniformly randomGen numExecutions``
   Like ``randomly``, but rather than a weighted selection, it's a
@@ -189,19 +189,22 @@ Performance tuning
     and ``Test.{HUnit,Tasty}.DejaFu``.
 
 For example, let's say you want to know if your test case deadlocks,
-and are going to sacrifice completeness because your possible
-state-space is huge.  You could do it like this:
+but you don't care about the execution trace, and you are going to
+sacrifice completeness because your possible state-space is huge.  You
+could do it like this:
 
 .. code-block:: haskell
 
   dejafuDiscard
     -- "efa" == "either failure a", discard everything but deadlocks
-    (\efa -> if efa == Left Deadlock then Nothing else Just DiscardResultAndTrace)
+    (\efa -> Just (if either isDeadlock (const False) efa then DiscardTrace else DiscardResultAndTrace))
     -- try 10000 executions with random scheduling
     (randomly (mkStdGen 42) 10000)
     -- use the default memory model
     defaultMemType
+    -- the name of the test
+    "Never Deadlocks"
+    -- the predicate to check
+    deadlocksNever
     -- your test case
     testCase
-    -- the predicate to check (which is a bit redundant in this case)
-    ("Never Deadlocks", deadlocksNever)

doc/getting_started.rst

@@ -35,10 +35,10 @@ There are a few different packages under the Déjà Fu umbrella:
 .. csv-table::
    :header: "Package", "Version", "Summary"
 
-   "concurrency_",  "1.2.3.0", "Typeclasses, functions, and data types for concurrency and STM"
-   "dejafu_",       "0.9.1.2", "Systematic testing for Haskell concurrency"
-   "hunit-dejafu_", "0.7.1.1", "Déjà Fu support for the HUnit test framework"
-   "tasty-dejafu_", "0.7.1.1", "Déjà Fu support for the tasty test framework"
+   "concurrency_",  "1.3.0.0", "Typeclasses, functions, and data types for concurrency and STM"
+   "dejafu_",       "1.0.0.0", "Systematic testing for Haskell concurrency"
+   "hunit-dejafu_", "1.0.0.0", "Déjà Fu support for the HUnit test framework"
+   "tasty-dejafu_", "1.0.0.0", "Déjà Fu support for the tasty test framework"
 
 .. _concurrency:  https://hackage.haskell.org/package/concurrency
 .. _dejafu:       https://hackage.haskell.org/package/dejafu
@@ -56,7 +56,7 @@ Install from Hackage globally:
 
 .. code-block:: none
 
-  $ cabal-install dejafu
+  $ cabal install dejafu
 
 Or add it to your cabal file:
 
@@ -98,12 +98,12 @@ we'll get onto that shortly.  First, the result of testing:
 .. code-block:: none
 
   > autocheck myFunction
-  [pass] Never Deadlocks (checked: 12)
-  [pass] No Exceptions (checked: 12)
-  [fail] Consistent Result (checked: 11)
-          "hello" S0----S1-P2-S0--
+  [pass] Never Deadlocks
+  [pass] No Exceptions
+  [fail] Consistent Result
+          "hello" S0----S1--S0--
 
-          "world" S0----S2--S0-P1-S0-
+          "world" S0----S2--S0--
   False
 
 There are no deadlocks or uncaught exceptions, which is good; but the

doc/index.rst

@@ -26,6 +26,12 @@ This is Déjà Fu
    hunit-dejafu <changelog_hunit-dejafu>
    tasty-dejafu <changelog_tasty-dejafu>
 
+.. toctree::
+   :maxdepth: 2
+   :caption: Migration Guides
+
+   migration_0x_1x
+
 .. toctree::
    :maxdepth: 2
    :caption: Developer Documentation

doc/migration_0x_1x.rst

@@ -0,0 +1,130 @@
+0.x to 1.x
+==========
+
+`dejafu-1.0.0.0`__ is a super-major release which breaks compatibility
+with `dejafu-0.x`__ quite significantly, but brings with it support
+for bound threads, and significantly improves memory usage in the
+general case.
+
+.. __: https://hackage.haskell.org/package/dejafu-1.0.0.0
+.. __: https://hackage.haskell.org/package/dejafu-0.9.1.1
+
+Highlights reel:
+
+* Most predicates now only need to keep around the failures, rather
+  than all results.
+* Support for bound threads (with `concurrency-1.3.0.0`__).
+* The ``ST`` / ``IO`` interface duplication is gone, everything is now
+  monadic.
+* Function parameter order is closer to other testing libraries.
+* Much improved API documentation.
+
+.. __: https://hackage.haskell.org/package/concurrency-1.3.0.0
+
+See the changelogs for the full details.
+
+
+``ST`` and ``IO`` functions
+---------------------------
+
+There is only one set of functions now.  Testing bound threads
+requires being able to fork actual threads, so testing with ``ST`` is
+no longer possible.  The ``ConcST`` type is gone, there is only
+``ConcIO``.
+
+For dejafu_ change:
+
+* ``autocheckIO`` to ``autocheck``
+* ``dejafuIO`` to ``dejafu``
+* ``dejafusIO`` to ``dejafus``
+* ``autocheckWayIO`` to ``autocheckWay``
+* ``dejafuWayIO`` to ``dejafuWay``
+* ``dejafusWayIO`` to ``dejafusWay``
+* ``dejafuDiscardIO`` to ``dejafuDiscard``
+* ``runTestM`` to ``runTest``
+* ``runTestWayM`` to ``runTestWay``
+
+If you relied on being able to get a pure result from the ``ConcST``
+functions, you can no longer do this.
+
+For hunit-dejafu_ and tasty-dejafu_ change:
+
+* ``testAutoIO`` to ``testAuto``
+* ``testDejafuIO`` to ``testDejafu``
+* ``testDejafusIO`` to ``testDejafus``
+* ``testAutoWayIO`` to ``testAutoWay``
+* ``testDejafuWayIO`` to ``testDejafuWay``
+* ``testDejafusWayIO`` to ``testDejafusWay``
+* ``testDejafuDiscardIO`` to ``testDejafuDiscard``
+
+
+Function parameter order
+------------------------
+
+Like HUnit_, the monadic action to test is now the last parameter of
+the testing functions.  This makes it convenient to write tests
+without needing to define the action elsewhere.
+
+.. _HUnit: https://hackage.haskell.org/package/HUnit
+
+For dejafu_ change:
+
+* ``dejafu ma (s, p)`` to ``dejafu s p ma``
+* ``dejafus ma ps`` to ``dejafus ps ma``
+* ``dejafuWay way mem ma (s, p)`` to ``dejafuWay way mem s p ma``
+* ``dejafusWay way mem ma ps`` to ``dejafuWay way mem ps ma``
+* ``dejafuDiscard d way mem ma (s, p)`` to ``dejafuDiscard d way mem s p ma``
+
+For hunit-dejafu_ and tasty-dejafu_ change:
+
+* ``testDejafu ma s p`` to ``testDejafu s p ma``
+* ``testDejafus ma ps`` to ``testDejafus ps ma``
+* ``testDejafuWay way mem ma s p`` to ``testDejafuWay way mem s p ma``
+* ``testDejafusWay way mem ma ps`` to ``testDejafusWay way mem ps ma``
+* ``testDejafuDiscard d way mem ma s p`` to ``testDejafuDiscard d way mem s p ma``
+
+.. _dejafu: https://hackage.haskell.org/package/dejafu
+.. _hunit-dejafu: https://hackage.haskell.org/package/hunit-dejafu
+.. _tasty-dejafu: https://hackage.haskell.org/package/tasty-dejafu
+
+
+Predicates
+----------
+
+The ``Predicate a`` type is now an alias for ``ProPredicate a a``,
+defined like so:
+
+.. code-block:: haskell
+
+  data ProPredicate a b = ProPredicate
+    { pdiscard :: Either Failure a -> Maybe Discard
+    -- ^ Selectively discard results before computing the result.
+    , peval :: [(Either Failure a, Trace)] -> Result b
+    -- ^ Compute the result with the un-discarded results.
+    }
+
+If you use the predicate helper functions to construct a predicate,
+you do not need to change anything (and should get a nice reduction in
+your resident memory usage).  If you supply a function directly, you
+can recover the old behaviour like so:
+
+.. code-block:: haskell
+
+  old :: ([(Either Failure a, Trace)] -> Result a) -> ProPredicate a a
+  old p = ProPredicate
+    { pdiscard = const Nothing
+    , peval = p
+    }
+
+The ``alwaysTrue2`` helper function is gone.  If you use it, use
+``alwaysSameOn`` or ``alwaysSameBy`` instead.
+
+
+Need help?
+----------
+
+* For general help talk to me in IRC (barrucadu in #haskell) or shoot
+  me an email (mike@barrucadu.co.uk)
+* For bugs, issues, or requests, please `file an issue`__.
+
+.. __:  https://github.com/barrucadu/dejafu/issues

doc/unit_testing.rst

@@ -10,14 +10,14 @@ Most tests will look something like this:
 
 .. code-block:: haskell
 
-  dejafu myAction ("Assert the thing holds", myPredicate)
+  dejafu "Assert the thing holds" myPredicate myAction
 
 The ``dejafu`` function comes from ``Test.DejaFu``.  It can't deal
 with testcases which need ``MonadIO``, use ``dejafuIO`` for that.
 
 
 Actions
-----------
+-------
 
 An action is just something with the type ``MonadConc m => m a``, or
 ``(MonadConc m, MonadIO m) => m a`` for some ``a`` that your chosen
@@ -65,6 +65,13 @@ want to see the full code. [#]_
        predicates are checking that the bug is found, not that the
        code is correct.
 
+If the RTS supports bound threads (the ``-threaded`` flag was passed
+to GHC when linking), then the main thread of an action given to Déjà
+Fu will be bound, and further bound threads can be forked with the
+``forkOS`` functions.  If not, then attempting to fork a bound thread
+will raise an error.
+
+
 Predicates
 ----------
 
@@ -108,6 +115,8 @@ to it from a different thread).
   :widths: 25, 75
 
   ``alwaysSame``,"checks that the computation is deterministic"
+  ``alwaysSameOn f``,"is like ``alwaysSame``, but transforms the results with ``f`` first"
+  ``alwaysSameBy f``,"is like ``alwaysSame``, but uses ``f`` instead of ``(==)`` to compare"
   ``notAlwaysSame``,"checks that the computation is nondeterministic"
 
 Checking for **determinism** will also find nondeterministic failures:
@@ -117,7 +126,6 @@ deadlocking (for instance) is still a result of a test!
   :widths: 25, 75
 
   ``alwaysTrue p``,"checks that ``p`` is true for every result"
-  ``alwaysTrue2 p``,"checks that ``p`` is true for every pair of results"
   ``somewhereTrue p``,"checks that ``p`` is true for at least one result"
 
 These can be used to check custom predicates.  For example, you might
@@ -164,7 +172,7 @@ Our example from the start becomes:
 
 .. code-block:: haskell
 
-  testDejafu myAction "Assert the thing holds" myPredicate
+  testDejafu "Assert the thing holds" myPredicate myAction
 
 The ``autocheck`` and ``autocheckIO`` functions are exposed as
 ``testAuto`` and ``testAutoIO``.

hunit-dejafu/CHANGELOG.markdown

@@ -7,6 +7,30 @@ This project is versioned according to the [Package Versioning Policy](https://p
 *de facto* standard Haskell versioning scheme.
 
 
+1.0.0.0
+-------
+
+- **Date**    unreleased
+- **Git tag** [hunit-dejafu-1.0.0.0][]
+- **Hackage** https://hackage.haskell.org/package/hunit-dejafu-1.0.0.0
+
+### Test.HUnit.DejaFu
+
+- The `ConcST` functions have been removed and replaced by the `ConcIO` functions.
+- The `Testable` and `Assertable` instances for `ConcST t ()` are gone.
+- All test functions are generalised to take a `ProPredicate`.
+- All test functions now take the action to test as the last parameter.
+
+### Miscellaneous
+
+- The minimum supported version of dejafu is now 1.0.0.0.
+
+[hunit-dejafu-1.0.0.0]: https://github.com/barrucadu/dejafu/releases/tag/hunit-dejafu-1.0.0.0
+
+
+---------------------------------------------------------------------------------------------------
+
+
 0.7.1.1
 -------
 

hunit-dejafu/LICENSE

@@ -1,4 +1,4 @@
-Copyright (c) 2015, Michael Walker <mike@barrucadu.co.uk>
+Copyright (c) 2015--2017, Michael Walker <mike@barrucadu.co.uk>
 
 Permission is hereby granted, free of charge, to any person obtaining
 a copy of this software and associated documentation files (the

hunit-dejafu/Test/HUnit/DejaFu.hs

@@ -1,39 +1,27 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 
-#if MIN_TOOL_VERSION_ghc(8,0,0)
--- Impredicative polymorphism checks got stronger in GHC 8, breaking
--- the use of 'unsafeCoerce' below.
-{-# LANGUAGE ImpredicativeTypes #-}
-#endif
-
 -- |
 -- Module      : Test.HUnit.DejaFu
--- Copyright   : (c) 2017 Michael Walker
+-- Copyright   : (c) 2015--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : stable
--- Portability : CPP, FlexibleContexts, FlexibleInstances, ImpredicativeTypes, LambdaCase, RankNTypes, ScopedTypeVariables, TypeSynonymInstances
+-- Portability : FlexibleContexts, FlexibleInstances, LambdaCase, TypeSynonymInstances
 --
 -- This module allows using Deja Fu predicates with HUnit to test the
 -- behaviour of concurrent systems.
 module Test.HUnit.DejaFu
   ( -- * Unit testing
 
-  -- | This is supported by the 'Assertable' and 'Testable'
-  -- instances for 'ConcST' and 'ConcIO'. These instances try all
-  -- executions, reporting as failures the cases which throw an
-  -- 'HUnitFailure' exception.
+  -- | This is supported by the 'Assertable' and 'Testable' instances
+  -- for 'ConcIO'.  These instances try all executions, reporting as
+  -- failures the cases which throw an 'HUnitFailure' exception.
   --
-  -- @instance Testable   (ConcST t ())@
-  -- @instance Assertable (ConcST t ())@
-  -- @instance Testable   (ConcIO   ())@
-  -- @instance Assertable (ConcIO   ())@
+  -- @instance Testable   (ConcIO ())@
+  -- @instance Assertable (ConcIO ())@
   --
   -- These instances use 'defaultWay' and 'defaultMemType'.
 
@@ -48,18 +36,9 @@ module Test.HUnit.DejaFu
 
   , testDejafuDiscard
 
-  -- ** @IO@
-  , testAutoIO
-  , testDejafuIO
-  , testDejafusIO
-
-  , testAutoWayIO
-  , testDejafuWayIO
-  , testDejafusWayIO
-
-  , testDejafuDiscardIO
-
   -- ** Re-exports
+  , Predicate
+  , ProPredicate(..)
   , Way
   , defaultWay
   , systematically
@@ -89,56 +68,29 @@ module Test.HUnit.DejaFu
   ) where
 
 import           Control.Monad.Catch    (try)
-import           Control.Monad.ST       (runST)
 import qualified Data.Foldable          as F
 import           Data.List              (intercalate, intersperse)
 import           Test.DejaFu            hiding (Testable(..))
 import qualified Test.DejaFu.Conc       as Conc
 import qualified Test.DejaFu.Refinement as R
 import qualified Test.DejaFu.SCT        as SCT
+import qualified Test.DejaFu.Types      as D
 import           Test.HUnit             (Assertable(..), Test(..), Testable(..),
                                          assertFailure, assertString)
 import           Test.HUnit.Lang        (HUnitFailure(..))
 
--- Can't put the necessary forall in the @Assertable Conc.ConcST t@
--- instance :(
-import           Unsafe.Coerce          (unsafeCoerce)
-
-runSCTst :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> (forall t. Conc.ConcST t a) -> [(Either Failure a, Conc.Trace)]
-runSCTst discard way memtype conc = runST (SCT.runSCTDiscard discard way memtype conc)
-
-runSCTio :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> IO [(Either Failure a, Conc.Trace)]
-runSCTio = SCT.runSCTDiscard
-
 --------------------------------------------------------------------------------
 -- HUnit-style unit testing
 
--- | @since 0.3.0.0
-instance Testable (Conc.ConcST t ()) where
-  test conc = TestCase (assert conc)
-
 -- | @since 0.3.0.0
 instance Testable (Conc.ConcIO ()) where
   test conc = TestCase (assert conc)
 
--- | @since 0.3.0.0
-instance Assertable (Conc.ConcST t ()) where
-  assert conc = do
-    let traces = runSCTst' conc'
-    assertString . showErr $ assertableP traces
-
-    where
-      conc' :: Conc.ConcST t (Either HUnitFailure ())
-      conc' = try conc
-
-      runSCTst' :: Conc.ConcST t (Either HUnitFailure ()) -> [(Either Failure (Either HUnitFailure ()), Conc.Trace)]
-      runSCTst' = unsafeCoerce $ runSCTst (const Nothing) defaultWay defaultMemType
-
 -- | @since 0.3.0.0
 instance Assertable (Conc.ConcIO ()) where
   assert conc = do
-    traces <- runSCTio (const Nothing) defaultWay defaultMemType (try conc)
-    assertString . showErr $ assertableP traces
+    traces <- SCT.runSCTDiscard (pdiscard assertableP) defaultWay defaultMemType (try conc)
+    assertString . showErr $ peval assertableP traces
 
 assertableP :: Predicate (Either HUnitFailure ())
 assertableP = alwaysTrue $ \case
@@ -152,45 +104,26 @@ assertableP = alwaysTrue $ \case
 -- | Automatically test a computation. In particular, look for
 -- deadlocks, uncaught exceptions, and multiple return values.
 --
--- This uses the 'Conc' monad for testing, which is an instance of
--- 'MonadConc'. If you need to test something which also uses
--- 'MonadIO', use 'testAutoIO'.
---
--- @since 0.2.0.0
+-- @since 1.0.0.0
 testAuto :: (Eq a, Show a)
-  => (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
+  => Conc.ConcIO a
+  -- ^ The computation to test.
   -> Test
 testAuto = testAutoWay defaultWay defaultMemType
 
 -- | Variant of 'testAuto' which tests a computation under a given
 -- execution way and memory model.
 --
--- @since 0.5.0.0
+-- @since 1.0.0.0
 testAutoWay :: (Eq a, Show a)
   => Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> Test
-testAutoWay way memtype conc =
-  testDejafusWay way memtype conc autocheckCases
-
--- | Variant of 'testAuto' for computations which do 'IO'.
---
--- @since 0.2.0.0
-testAutoIO :: (Eq a, Show a) => Conc.ConcIO a -> Test
-testAutoIO = testAutoWayIO defaultWay defaultMemType
-
--- | Variant of 'testAutoWay' for computations which do 'IO'.
---
--- @since 0.5.0.0
-testAutoWayIO :: (Eq a, Show a)
-  => Way -> MemType -> Conc.ConcIO a -> Test
-testAutoWayIO way memtype concio =
-  testDejafusWayIO way memtype concio autocheckCases
+testAutoWay way memtype = testDejafusWay way memtype autocheckCases
 
 -- | Predicates for the various autocheck functions.
 autocheckCases :: Eq a => [(String, Predicate a)]
@@ -202,116 +135,83 @@ autocheckCases =
 
 -- | Check that a predicate holds.
 --
--- @since 0.2.0.0
-testDejafu :: Show a
-  => (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
-  -> String
+-- @since 1.0.0.0
+testDejafu :: Show b
+  => String
   -- ^ The name of the test.
-  -> Predicate a
-  -- ^ The predicate to check
+  -> ProPredicate a b
+  -- ^ The predicate to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> Test
 testDejafu = testDejafuWay defaultWay defaultMemType
 
 -- | Variant of 'testDejafu' which takes a way to execute the program
 -- and a memory model.
 --
--- @since 0.5.0.0
-testDejafuWay :: Show a
+-- @since 1.0.0.0
+testDejafuWay :: Show b
   => Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
   -> String
   -- ^ The name of the test.
-  -> Predicate a
-  -- ^ The predicate to check
+  -> ProPredicate a b
+  -- ^ The predicate to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> Test
 testDejafuWay = testDejafuDiscard (const Nothing)
 
 -- | Variant of 'testDejafuWay' which can selectively discard results.
 --
--- @since 0.7.0.0
-testDejafuDiscard :: Show a
+-- @since 1.0.0.0
+testDejafuDiscard :: Show b
   => (Either Failure a -> Maybe Discard)
   -- ^ Selectively discard results.
   -> Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
   -> String
   -- ^ The name of the test.
-  -> Predicate a
-  -- ^ The predicate to check
+  -> ProPredicate a b
+  -- ^ The predicate to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> Test
-testDejafuDiscard discard way memtype conc name test =
-  testst discard way memtype conc [(name, test)]
+testDejafuDiscard discard way memtype name test =
+  testconc discard way memtype [(name, test)]
 
 -- | Variant of 'testDejafu' which takes a collection of predicates to
 -- test. This will share work between the predicates, rather than
 -- running the concurrent computation many times for each predicate.
 --
--- @since 0.2.0.0
-testDejafus :: Show a
-  => (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
-  -> [(String, Predicate a)]
-  -- ^ The list of predicates (with names) to check
+-- @since 1.0.0.0
+testDejafus :: Show b
+  => [(String, ProPredicate a b)]
+  -- ^ The list of predicates (with names) to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> Test
 testDejafus = testDejafusWay defaultWay defaultMemType
 
 -- | Variant of 'testDejafus' which takes a way to execute the program
 -- and a memory model.
 --
--- @since 0.5.0.0
-testDejafusWay :: Show a
+-- @since 1.0.0.0
+testDejafusWay :: Show b
   => Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
-  -> [(String, Predicate a)]
-  -- ^ The list of predicates (with names) to check
+  -> [(String, ProPredicate a b)]
+  -- ^ The list of predicates (with names) to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> Test
-testDejafusWay = testst (const Nothing)
-
--- | Variant of 'testDejafu' for computations which do 'IO'.
---
--- @since 0.2.0.0
-testDejafuIO :: Show a => Conc.ConcIO a -> String -> Predicate a -> Test
-testDejafuIO = testDejafuWayIO defaultWay defaultMemType
-
--- | Variant of 'testDejafuWay' for computations which do 'IO'.
---
--- @since 0.5.0.0
-testDejafuWayIO :: Show a
-  => Way -> MemType -> Conc.ConcIO a -> String -> Predicate a -> Test
-testDejafuWayIO = testDejafuDiscardIO (const Nothing)
-
--- | Variant of 'testDejafuDiscard' for computations which do 'IO'.
---
--- @since 0.7.0.0
-testDejafuDiscardIO :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> String -> Predicate a -> Test
-testDejafuDiscardIO discard way memtype concio name test =
-  testio discard way memtype concio [(name, test)]
-
--- | Variant of 'testDejafus' for computations which do 'IO'.
---
--- @since 0.2.0.0
-testDejafusIO :: Show a => Conc.ConcIO a -> [(String, Predicate a)] -> Test
-testDejafusIO = testDejafusWayIO defaultWay defaultMemType
-
--- | Variant of 'dejafusWay' for computations which do 'IO'.
---
--- @since 0.5.0.0
-testDejafusWayIO :: Show a
-  => Way -> MemType -> Conc.ConcIO a -> [(String, Predicate a)] -> Test
-testDejafusWayIO = testio (const Nothing)
+testDejafusWay = testconc (const Nothing)
 
 
 -------------------------------------------------------------------------------
@@ -351,44 +251,23 @@ testPropertyFor = testprop
 --------------------------------------------------------------------------------
 -- HUnit integration
 
--- | Produce a HUnit 'Test' from a Deja Fu test.
-testst :: Show a
-  => (Either Failure a -> Maybe Discard)
-  -> Way
-  -> MemType
-  -> (forall t. Conc.ConcST t a)
-  -> [(String, Predicate a)]
-  -> Test
-testst discard way memtype conc tests = case map toTest tests of
-  [t] -> t
-  ts  -> TestList ts
-
-  where
-    toTest (name, p) = TestLabel name . TestCase $
-      assertString . showErr $ p traces
-
-    traces = runSCTst discard way memtype conc
-
--- | Produce a HUnit 'Test' from an IO-using Deja Fu test.
-testio :: Show a
+-- | Produce a HUnit 'Test' from a Deja Fu unit test.
+testconc :: Show b
   => (Either Failure a -> Maybe Discard)
   -> Way
   -> MemType
+  -> [(String, ProPredicate a b)]
   -> Conc.ConcIO a
-  -> [(String, Predicate a)]
   -> Test
-testio discard way memtype concio tests = case map toTest tests of
+testconc discard way memtype tests concio = case map toTest tests of
   [t] -> t
   ts  -> TestList ts
 
   where
     toTest (name, p) = TestLabel name . TestCase $ do
-      -- Sharing of traces probably not possible (without something
-      -- really unsafe) here, as 'test' doesn't allow side-effects
-      -- (eg, constructing an 'MVar' to share the traces after one
-      -- test computed them).
-      traces <- runSCTio discard way memtype concio
-      assertString . showErr $ p traces
+      let discarder = D.strengthenDiscard discard (pdiscard p)
+      traces <- SCT.runSCTDiscard discarder way memtype concio
+      assertString . showErr $ peval p traces
 
 -- | Produce a HUnit 'Test' from a Deja Fu refinement property test.
 testprop :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
@@ -414,7 +293,7 @@ testprop sn vn name p = TestLabel name . TestCase $ do
 showErr :: Show a => Result a -> String
 showErr res
   | _pass res = ""
-  | otherwise = "Failed after " ++ show (_casesChecked res) ++ " cases:\n" ++ msg ++ unlines failures ++ rest where
+  | otherwise = "Failed:\n" ++ msg ++ unlines failures ++ rest where
 
   msg = if null (_failureMsg res) then "" else _failureMsg res ++ "\n"
 

hunit-dejafu/hunit-dejafu.cabal

@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                hunit-dejafu
-version:             0.7.1.1
+version:             1.0.0.0
 synopsis:            Deja Fu support for the HUnit test framework.
 
 description:
@@ -17,7 +17,7 @@ license:             MIT
 license-file:        LICENSE
 author:              Michael Walker
 maintainer:          mike@barrucadu.co.uk
--- copyright:           
+copyright:           (c) 2015--2017 Michael Walker
 category:            Testing
 build-type:          Simple
 extra-source-files:  README.markdown CHANGELOG.markdown
@@ -30,7 +30,7 @@ source-repository head
 source-repository this
   type:     git
   location: https://github.com/barrucadu/dejafu.git
-  tag:      hunit-dejafu-0.7.1.1
+  tag:      hunit-dejafu-1.0.0.0
 
 library
   exposed-modules:     Test.HUnit.DejaFu
@@ -38,7 +38,7 @@ library
   -- other-extensions:    
   build-depends:       base       >=4.8 && <5
                      , exceptions >=0.7 && <0.9
-                     , dejafu     >=0.7.1 && <0.10
+                     , dejafu     >=1.0 && <1.1
                      , HUnit      >=1.2 && <1.7
   -- hs-source-dirs:      
   default-language:    Haskell2010

tasty-dejafu/CHANGELOG.markdown

@@ -7,6 +7,30 @@ This project is versioned according to the [Package Versioning Policy](https://p
 *de facto* standard Haskell versioning scheme.
 
 
+1.0.0.0
+-------
+
+- **Date**    unreleased
+- **Git tag** [tasty-dejafu-1.0.0.0][]
+- **Hackage** https://hackage.haskell.org/package/tasty-dejafu-1.0.0.0
+
+### Test.Tasty.DejaFu
+
+- The `ConcST` functions have been removed and replaced by the `ConcIO` functions.
+- The `IsTest` instance for `ConcST t (Maybe String)` is gone.
+- All test functions are generalised to take a `ProPredicate`.
+- All test functions now take the action to test as the last parameter.
+
+### Miscellaneous
+
+- The minimum supported version of dejafu is now 1.0.0.0.
+
+[tasty-dejafu-1.0.0.0]: https://github.com/barrucadu/dejafu/releases/tag/tasty-dejafu-1.0.0.0
+
+
+---------------------------------------------------------------------------------------------------
+
+
 0.7.1.1
 -------
 

tasty-dejafu/LICENSE

@@ -1,4 +1,4 @@
-Copyright (c) 2015, Michael Walker <mike@barrucadu.co.uk>
+Copyright (c) 2015--2017, Michael Walker <mike@barrucadu.co.uk>
 
 Permission is hereby granted, free of charge, to any person obtaining
 a copy of this software and associated documentation files (the

tasty-dejafu/Test/Tasty/DejaFu.hs

@@ -1,40 +1,31 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 
-#if MIN_TOOL_VERSION_ghc(8,0,0)
--- Impredicative polymorphism checks got stronger in GHC 8, breaking
--- the use of 'unsafeCoerce' below.
-{-# LANGUAGE ImpredicativeTypes #-}
-#endif
-
 -- |
 -- Module      : Test.Tasty.DejaFu
--- Copyright   : (c) 2016 Michael Walker
+-- Copyright   : (c) 2015--2017 Michael Walker
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : stable
--- Portability : CPP, FlexibleContexts, FlexibleInstances, GADTs, ImpredicativeTypes, LambdaCase, RankNTypes, TypeSynonymInstances
+-- Portability : FlexibleContexts, FlexibleInstances, GADTs, LambdaCase, TypeSynonymInstances
 --
 -- This module allows using Deja Fu predicates with Tasty to test the
 -- behaviour of concurrent systems.
 module Test.Tasty.DejaFu
   ( -- * Unit testing
 
-  -- | This is supported by the 'IsTest' instances for 'ConcST' and
-  -- 'ConcIO'. These instances try all executions, reporting as
-  -- failures the cases which return a 'Just' string.
+  -- | This is supported by an 'IsTest' instance for 'ConcIO'.  This
+  -- instance tries all executions, reporting as failures the cases
+  -- which return a 'Just' string.
   --
-  -- @instance Typeable t => IsTest (ConcST t (Maybe String))@
-  -- @instance               IsTest (ConcIO   (Maybe String))@
+  -- @instance IsTest (ConcIO (Maybe String))@
   -- @instance IsOption Bounds@
   -- @instance IsOption MemType@
 
-  -- * Property testing
+  -- * Unit testing
     testAuto
   , testDejafu
   , testDejafus
@@ -45,18 +36,9 @@ module Test.Tasty.DejaFu
 
   , testDejafuDiscard
 
-  -- ** @IO@
-  , testAutoIO
-  , testDejafuIO
-  , testDejafusIO
-
-  , testAutoWayIO
-  , testDejafuWayIO
-  , testDejafusWayIO
-
-  , testDejafuDiscardIO
-
   -- ** Re-exports
+  , Predicate
+  , ProPredicate(..)
   , Way
   , defaultWay
   , systematically
@@ -85,7 +67,6 @@ module Test.Tasty.DejaFu
   , R.equivalentTo, (R.===)
   ) where
 
-import           Control.Monad.ST       (runST)
 import           Data.Char              (toUpper)
 import qualified Data.Foldable          as F
 import           Data.List              (intercalate, intersperse)
@@ -97,37 +78,16 @@ import           Test.DejaFu            hiding (Testable(..))
 import qualified Test.DejaFu.Conc       as Conc
 import qualified Test.DejaFu.Refinement as R
 import qualified Test.DejaFu.SCT        as SCT
+import qualified Test.DejaFu.Types      as D
 import           Test.Tasty             (TestName, TestTree, testGroup)
 import           Test.Tasty.Options     (IsOption(..), OptionDescription(..),
                                          lookupOption)
 import           Test.Tasty.Providers   (IsTest(..), singleTest, testFailed,
                                          testPassed)
 
--- Can't put the necessary forall in the @IsTest ConcST t@
--- instance :(
-import           Unsafe.Coerce          (unsafeCoerce)
-
-runSCTst :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> (forall t. Conc.ConcST t a) -> [(Either Failure a, Conc.Trace)]
-runSCTst discard way memtype conc = runST (SCT.runSCTDiscard discard way memtype conc)
-
-runSCTio :: (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> IO [(Either Failure a, Conc.Trace)]
-runSCTio = SCT.runSCTDiscard
-
 --------------------------------------------------------------------------------
 -- Tasty-style unit testing
 
--- | @since 0.3.0.0
-instance Typeable t => IsTest (Conc.ConcST t (Maybe String)) where
-  testOptions = Tagged concOptions
-
-  run options conc callback = do
-    let memtype = lookupOption options :: MemType
-    let way     = lookupOption options :: Way
-    let runSCTst' :: Conc.ConcST t (Maybe String) -> [(Either Failure (Maybe String), Conc.Trace)]
-        runSCTst' = unsafeCoerce $ runSCTst (const Nothing) way memtype
-    let traces = runSCTst' conc
-    run options (ConcTest traces assertableP) callback
-
 -- | @since 0.3.0.0
 instance IsTest (Conc.ConcIO (Maybe String)) where
   testOptions = Tagged concOptions
@@ -135,8 +95,8 @@ instance IsTest (Conc.ConcIO (Maybe String)) where
   run options conc callback = do
     let memtype = lookupOption options
     let way     = lookupOption options
-    let traces  = runSCTio (const Nothing) way memtype conc
-    run options (ConcIOTest traces assertableP) callback
+    let traces  = SCT.runSCTDiscard (pdiscard assertableP) way memtype conc
+    run options (ConcTest traces (peval assertableP)) callback
 
 concOptions :: [OptionDescription]
 concOptions =
@@ -177,44 +137,26 @@ instance IsOption Way where
 -- | Automatically test a computation. In particular, look for
 -- deadlocks, uncaught exceptions, and multiple return values.
 --
--- This uses the 'Conc' monad for testing, which is an instance of
--- 'MonadConc'. If you need to test something which also uses
--- 'MonadIO', use 'testAutoIO'.
---
--- @since 0.2.0.0
+-- @since 1.0.0.0
 testAuto :: (Eq a, Show a)
-  => (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
+  => Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
 testAuto = testAutoWay defaultWay defaultMemType
 
 -- | Variant of 'testAuto' which tests a computation under a given
 -- execution way and memory model.
 --
--- @since 0.5.0.0
+-- @since 1.0.0.0
 testAutoWay :: (Eq a, Show a)
   => Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
-testAutoWay way memtype conc = testDejafusWay way memtype conc autocheckCases
-
--- | Variant of 'testAuto' for computations which do 'IO'.
---
--- @since 0.2.0.0
-testAutoIO :: (Eq a, Show a) => Conc.ConcIO a -> TestTree
-testAutoIO = testAutoWayIO defaultWay defaultMemType
-
--- | Variant of 'testAutoWay' for computations which do 'IO'.
---
--- @since 0.5.0.0
-testAutoWayIO :: (Eq a, Show a)
-  => Way -> MemType -> Conc.ConcIO a -> TestTree
-testAutoWayIO way memtype concio =
-  testDejafusWayIO way memtype  concio autocheckCases
+testAutoWay way memtype = testDejafusWay way memtype autocheckCases
 
 -- | Predicates for the various autocheck functions.
 autocheckCases :: Eq a => [(TestName, Predicate a)]
@@ -226,116 +168,83 @@ autocheckCases =
 
 -- | Check that a predicate holds.
 --
--- @since 0.2.0.0
-testDejafu :: Show a
-  => (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
-  -> TestName
+-- @since 1.0.0.0
+testDejafu :: Show b
+  => TestName
   -- ^ The name of the test.
-  -> Predicate a
-  -- ^ The predicate to check
+  -> ProPredicate a b
+  -- ^ The predicate to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
 testDejafu = testDejafuWay defaultWay defaultMemType
 
 -- | Variant of 'testDejafu' which takes a way to execute the program
 -- and a memory model.
 --
--- @since 0.5.0.0
-testDejafuWay :: Show a
+-- @since 1.0.0.0
+testDejafuWay :: Show b
   => Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
   -> TestName
   -- ^ The name of the test.
-  -> Predicate a
-  -- ^ The predicate to check
+  -> ProPredicate a b
+  -- ^ The predicate to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
 testDejafuWay = testDejafuDiscard (const Nothing)
 
 -- | Variant of 'testDejafuWay' which can selectively discard results.
 --
--- @since 0.7.0.0
-testDejafuDiscard :: Show a
+-- @since 1.0.0.0
+testDejafuDiscard :: Show b
   => (Either Failure a -> Maybe Discard)
   -- ^ Selectively discard results.
   -> Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
   -> String
   -- ^ The name of the test.
-  -> Predicate a
-  -- ^ The predicate to check
+  -> ProPredicate a b
+  -- ^ The predicate to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
-testDejafuDiscard discard way memtype conc name test =
-  testst discard way memtype conc [(name, test)]
+testDejafuDiscard discard way memtype name test =
+  testconc discard way memtype [(name, test)]
 
 -- | Variant of 'testDejafu' which takes a collection of predicates to
 -- test. This will share work between the predicates, rather than
 -- running the concurrent computation many times for each predicate.
 --
--- @since 0.2.0.0
-testDejafus :: Show a
-  => (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
-  -> [(TestName, Predicate a)]
-  -- ^ The list of predicates (with names) to check
+-- @since 1.0.0.0
+testDejafus :: Show b
+  => [(TestName, ProPredicate a b)]
+  -- ^ The list of predicates (with names) to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
 testDejafus = testDejafusWay defaultWay defaultMemType
 
 -- | Variant of 'testDejafus' which takes a way to execute the program
 -- and a memory model.
 --
--- @since 0.5.0.0
-testDejafusWay :: Show a
+-- @since 1.0.0.0
+testDejafusWay :: Show b
   => Way
   -- ^ How to execute the concurrent program.
   -> MemType
   -- ^ The memory model to use for non-synchronised @CRef@ operations.
-  -> (forall t. Conc.ConcST t a)
-  -- ^ The computation to test
-  -> [(TestName, Predicate a)]
-  -- ^ The list of predicates (with names) to check
+  -> [(TestName, ProPredicate a b)]
+  -- ^ The list of predicates (with names) to check.
+  -> Conc.ConcIO a
+  -- ^ The computation to test.
   -> TestTree
-testDejafusWay = testst (const Nothing)
-
--- | Variant of 'testDejafu' for computations which do 'IO'.
---
--- @since 0.2.0.0
-testDejafuIO :: Show a => Conc.ConcIO a -> TestName -> Predicate a -> TestTree
-testDejafuIO = testDejafuWayIO defaultWay defaultMemType
-
--- | Variant of 'testDejafuWay' for computations which do 'IO'.
---
--- @since 0.5.0.0
-testDejafuWayIO :: Show a
-  => Way -> MemType -> Conc.ConcIO a -> TestName -> Predicate a -> TestTree
-testDejafuWayIO = testDejafuDiscardIO (const Nothing)
-
--- | Variant of 'testDejafuDiscard' for computations which do 'IO'.
---
--- @since 0.7.0.0
-testDejafuDiscardIO :: Show a => (Either Failure a -> Maybe Discard) -> Way -> MemType -> Conc.ConcIO a -> String -> Predicate a -> TestTree
-testDejafuDiscardIO discard way memtype concio name test =
-  testio discard way memtype concio [(name, test)]
-
--- | Variant of 'testDejafus' for computations which do 'IO'.
---
--- @since 0.2.0.0
-testDejafusIO :: Show a => Conc.ConcIO a -> [(TestName, Predicate a)] -> TestTree
-testDejafusIO = testDejafusWayIO defaultWay defaultMemType
-
--- | Variant of 'dejafusWay' for computations which do 'IO'.
---
--- @since 0.5.0.0
-testDejafusWayIO :: Show a
-  => Way -> MemType -> Conc.ConcIO a -> [(TestName, Predicate a)] -> TestTree
-testDejafusWayIO = testio (const Nothing)
+testDejafusWay = testconc (const Nothing)
 
 
 -------------------------------------------------------------------------------
@@ -376,11 +285,7 @@ testPropertyFor = testprop
 -- Tasty integration
 
 data ConcTest where
-  ConcTest   :: Show a => [(Either Failure a, Conc.Trace)] -> Predicate a -> ConcTest
-  deriving Typeable
-
-data ConcIOTest where
-  ConcIOTest :: Show a => IO [(Either Failure a, Conc.Trace)] -> Predicate a -> ConcIOTest
+  ConcTest :: Show b => IO [(Either Failure a, Conc.Trace)] -> ([(Either Failure a, Conc.Trace)] -> Result b) -> ConcTest
   deriving Typeable
 
 data PropTest where
@@ -390,14 +295,7 @@ data PropTest where
 instance IsTest ConcTest where
   testOptions = pure []
 
-  run _ (ConcTest traces p) _ =
-    let err = showErr $ p traces
-     in pure (if null err then testPassed "" else testFailed err)
-
-instance IsTest ConcIOTest where
-  testOptions = pure []
-
-  run _ (ConcIOTest iotraces p) _ = do
+  run _ (ConcTest iotraces p) _ = do
     traces <- iotraces
     let err = showErr $ p traces
     pure (if null err then testPassed "" else testFailed err)
@@ -417,41 +315,23 @@ instance IsTest PropTest where
         ]
       Nothing -> testPassed ""
 
--- | Produce a Tasty 'TestTree' from a Deja Fu test.
-testst :: Show a
-  => (Either Failure a -> Maybe Discard)
-  -> Way
-  -> MemType
-  -> (forall t. Conc.ConcST t a)
-  -> [(TestName, Predicate a)]
-  -> TestTree
-testst discard way memtype conc tests = case map toTest tests of
-  [t] -> t
-  ts  -> testGroup "Deja Fu Tests" ts
-
-  where
-    toTest (name, p) = singleTest name $ ConcTest traces p
-
-    traces = runSCTst discard way memtype conc
-
--- | Produce a Tasty 'Test' from an IO-using Deja Fu test.
-testio :: Show a
+-- | Produce a Tasty 'Test' from a Deja Fu unit test.
+testconc :: Show b
   => (Either Failure a -> Maybe Discard)
   -> Way
   -> MemType
+  -> [(TestName, ProPredicate a b)]
   -> Conc.ConcIO a
-  -> [(TestName, Predicate a)]
   -> TestTree
-testio discard way memtype concio tests = case map toTest tests of
+testconc discard way memtype tests concio = case map toTest tests of
   [t] -> t
   ts  -> testGroup "Deja Fu Tests" ts
 
   where
-    toTest (name, p) = singleTest name $ ConcIOTest traces p
-
-    -- As with HUnit, constructing a test is side-effect free, so
-    -- sharing of traces can't happen here.
-    traces = runSCTio discard way memtype concio
+    toTest (name, p) =
+      let discarder = D.strengthenDiscard discard (pdiscard p)
+          traces    = SCT.runSCTDiscard discarder way memtype concio
+      in singleTest name $ ConcTest traces (peval p)
 
 -- | Produce a Tasty 'TestTree' from a Deja Fu refinement property test.
 testprop :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
@@ -463,7 +343,7 @@ testprop sn vn name = singleTest name . PropTest sn vn
 showErr :: Show a => Result a -> String
 showErr res
   | _pass res = ""
-  | otherwise = "Failed after " ++ show (_casesChecked res) ++ " cases:\n" ++ msg ++ unlines failures ++ rest where
+  | otherwise = "Failed:\n" ++ msg ++ unlines failures ++ rest where
 
   msg = if null (_failureMsg res) then "" else _failureMsg res ++ "\n"
 

tasty-dejafu/tasty-dejafu.cabal

@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                tasty-dejafu
-version:             0.7.1.1
+version:             1.0.0.0
 synopsis:            Deja Fu support for the Tasty test framework.
 
 description:
@@ -17,7 +17,7 @@ license:             MIT
 license-file:        LICENSE
 author:              Michael Walker
 maintainer:          mike@barrucadu.co.uk
--- copyright:           
+copyright:           (c) 2015--2017 Michael Walker
 category:            Testing
 build-type:          Simple
 extra-source-files:  README.markdown CHANGELOG.markdown
@@ -30,14 +30,14 @@ source-repository head
 source-repository this
   type:     git
   location: https://github.com/barrucadu/dejafu.git
-  tag:      tasty-dejafu-0.7.1.1
+  tag:      tasty-dejafu-1.0.0.0
 
 library
   exposed-modules:     Test.Tasty.DejaFu
   -- other-modules:       
   -- other-extensions:    
   build-depends:       base   >=4.8  && <5
-                     , dejafu >=0.7.1  && <0.10
+                     , dejafu >=1.0  && <1.1
                      , random >=1.0  && <1.2
                      , tagged >=0.8  && <0.9
                      , tasty  >=0.10 && <0.13