dejafu (empty) → 0.1.0.0

raw patch · 24 files changed

+4280/−0 lines, 24 filesdep +basedep +containersdep +deepseqsetup-changed

Dependencies added: base, containers, deepseq, dejafu, exceptions, monad-loops, mtl, random, stm, transformers

Files

• Control/Concurrent/CVar.hs +123/−0
• Control/Concurrent/CVar/Strict.hs +97/−0
• Control/Concurrent/STM/CTMVar.hs +86/−0
• Control/Concurrent/STM/CTVar.hs +34/−0
• Control/Monad/Conc/Class.hs +536/−0
• Control/Monad/STM/Class.hs +163/−0
• Data/List/Extra.hs +60/−0
• LICENSE +20/−0
• Setup.hs +2/−0
• Test/DejaFu.hs +387/−0
• Test/DejaFu/Deterministic.hs +345/−0
• Test/DejaFu/Deterministic/IO.hs +337/−0
• Test/DejaFu/Deterministic/Internal.hs +390/−0
• Test/DejaFu/Deterministic/Internal/CVar.hs +54/−0
• Test/DejaFu/Deterministic/Internal/Common.hs +345/−0
• Test/DejaFu/Deterministic/Internal/Threading.hs +174/−0
• Test/DejaFu/Deterministic/Schedule.hs +57/−0
• Test/DejaFu/Internal.hs +34/−0
• Test/DejaFu/SCT.hs +239/−0
• Test/DejaFu/SCT/Internal.hs +334/−0
• Test/DejaFu/STM.hs +145/−0
• Test/DejaFu/STM/Internal.hs +180/−0
• dejafu.cabal +101/−0
• tests/Tests.hs +37/−0

@@ -0,0 +1,123 @@+-- | Combinators using @CVar@s. These provide many of the helpful+-- functions found in Control.Concurrent.MVar, but for @CVar@s.+module Control.Concurrent.CVar+ ( -- *@CVar@s+  CVar+ , newEmptyCVar+ , newCVar+ , takeCVar+ , putCVar+ , readCVar+ , swapCVar+ , tryTakeCVar+ , tryPutCVar+ , isEmptyCVar+ , withCVar+ , withCVarMasked+ , modifyCVar_+ , modifyCVar+ , modifyCVarMasked_+ , modifyCVarMasked++ -- * Binary semaphores+ -- | A common use of @CVar@s is in making binary semaphores to+ -- control mutual exclusion over a resource, so a couple of helper+ -- functions are provided.+ , lock+ , unlock+ ) where++import Control.Monad (liftM)+import Control.Monad.Catch (mask_, onException)+import Control.Monad.Conc.Class++-- | Create a new @CVar@ containing a value.+newCVar :: MonadConc m => a -> m (CVar m a)+newCVar a = do+  cvar <- newEmptyCVar+  putCVar cvar a+  return cvar++-- | Swap the contents of a @CVar@, and return the value taken. This+-- function is atomic only if there are no other producers fro this+-- @CVar@.+swapCVar :: MonadConc m => CVar m a -> a -> m a+swapCVar cvar a = mask_ $ do+  old <- takeCVar cvar+  putCVar cvar a+  return old++-- | Check if a @CVar@ is empty.+isEmptyCVar :: MonadConc m => CVar m a -> m Bool+isEmptyCVar cvar = do+  val <- tryTakeCVar cvar+  case val of+    Just val' -> putCVar cvar val' >> return True+    Nothing   -> return False++-- | Operate on the contents of a @CVar@, replacing the contents after+-- finishing. This operation is exception-safe: it will replace the+-- original contents of the @CVar@ if an exception is raised. However,+-- it is only atomic if there are no other producers for this @CVar@.+{-# INLINE withCVar #-}+withCVar :: MonadConc m => CVar m a -> (a -> m b) -> m b+withCVar cvar f = mask $ \restore -> do+  val <- takeCVar cvar+  out <- restore (f val) `onException` putCVar cvar val+  putCVar cvar val++  return out++-- | Like 'withCVar', but the @IO@ action in the second argument is+-- executed with asynchronous exceptions masked.+{-# INLINE withCVarMasked #-}+withCVarMasked :: MonadConc m => CVar m a -> (a -> m b) -> m b+withCVarMasked cvar f = mask_ $ do+  val <- takeCVar cvar+  out <- f val `onException` putCVar cvar val+  putCVar cvar val++  return out++-- | An exception-safe wrapper for modifying the contents of a @CVar@.+-- Like 'withCVar', 'modifyCVar' will replace the original contents of+-- the @CVar@ if an exception is raised during the operation. This+-- function is only atomic if there are no other producers for this+-- @CVar@.+{-# INLINE modifyCVar_ #-}+modifyCVar_ :: MonadConc m => CVar m a -> (a -> m a) -> m ()+modifyCVar_ cvar f = modifyCVar cvar $ liftM (\a -> (a,())) . f++-- | A slight variation on 'modifyCVar_' that allows a value to be+-- returned (@b@) in addition to the modified value of the @CVar@.+{-# INLINE modifyCVar #-}+modifyCVar :: MonadConc m => CVar m a -> (a -> m (a, b)) -> m b+modifyCVar cvar f = mask $ \restore -> do+  val <- takeCVar cvar+  (val', out) <- restore (f val) `onException` putCVar cvar val+  putCVar cvar val'+  return out++-- | Like 'modifyCVar_', but the @IO@ action in the second argument is+-- executed with asynchronous exceptions masked.+{-# INLINE modifyCVarMasked_ #-}+modifyCVarMasked_ :: MonadConc m => CVar m a -> (a -> m a) -> m ()+modifyCVarMasked_ cvar f = modifyCVarMasked cvar $ liftM (\a -> (a,())) . f++-- | Like 'modifyCVar', but the @IO@ action in the second argument is+-- executed with asynchronous exceptions masked.+{-# INLINE modifyCVarMasked #-}+modifyCVarMasked :: MonadConc m => CVar m a -> (a -> m (a, b)) -> m b+modifyCVarMasked cvar f = mask_ $ do+  val <- takeCVar cvar+  (val', out) <- f val `onException` putCVar cvar val+  putCVar cvar val'+  return out++-- | Put a @()@ into a @CVar@, claiming the lock. This is atomic.+lock :: MonadConc m => CVar m () -> m ()+lock = flip putCVar ()++-- | Empty a @CVar@, releasing the lock. This is atomic.+unlock :: MonadConc m => CVar m () -> m ()+unlock = takeCVar

@@ -0,0 +1,97 @@+-- | Strict alternatives to the functions in+-- Control.Monad.Conc.CVar. Specifically, values are evaluated to+-- normal form before being put into a @CVar@.+module Control.Concurrent.CVar.Strict+ ( -- *@CVar@s+  CVar+ , newEmptyCVar+ , newCVar+ , takeCVar+ , putCVar+ , readCVar+ , swapCVar+ , tryTakeCVar+ , tryPutCVar+ , isEmptyCVar+ , withCVar+ , withCVarMasked+ , modifyCVar_+ , modifyCVar+ , modifyCVarMasked_+ , modifyCVarMasked++ -- * Binary semaphores+ -- | A common use of @CVar@s is in making binary semaphores to+ -- control mutual exclusion over a resource, so a couple of helper+ -- functions are provided.+ , lock+ , unlock+ ) where++import Control.Concurrent.CVar (isEmptyCVar, withCVar, withCVarMasked, lock, unlock)+import Control.DeepSeq (NFData, force)+import Control.Monad (liftM)+import Control.Monad.Catch (mask_, onException)+import Control.Monad.Conc.Class hiding (newEmptyCVar, putCVar, tryPutCVar)++import qualified Control.Concurrent.CVar  as V+import qualified Control.Monad.Conc.Class as C++-- | Create a new empty @CVar@.+newEmptyCVar :: (MonadConc m, NFData a) => m (CVar m a)+newEmptyCVar = C.newEmptyCVar++-- | Create a new @CVar@ containing a value.+newCVar :: (MonadConc m, NFData a) => a -> m (CVar m a)+newCVar = V.newCVar . force++-- | Swap the contents of a @CVar@, and return the value taken.+swapCVar :: (MonadConc m, NFData a) => CVar m a -> a -> m a+swapCVar cvar = V.swapCVar cvar . force++-- | Put a value into a @CVar@. If there is already a value there,+-- this will block until that value has been taken, at which point the+-- value will be stored.+putCVar :: (MonadConc m, NFData a) => CVar m a -> a -> m ()+putCVar cvar = C.putCVar cvar . force++-- | Attempt to put a value in a @CVar@, returning 'True' (and filling+-- the @CVar@) if there was nothing there, otherwise returning+-- 'False'.+tryPutCVar :: (MonadConc m, NFData a) => CVar m a -> a -> m Bool+tryPutCVar cvar = C.tryPutCVar cvar . force++-- | An exception-safe wrapper for modifying the contents of a @CVar@.+-- Like 'withCVar', 'modifyCVar' will replace the original contents of+-- the @CVar@ if an exception is raised during the operation. This+-- function is only atomic if there are no other producers for this+-- @CVar@.+{-# INLINE modifyCVar_ #-}+modifyCVar_ :: (MonadConc m, NFData a) => CVar m a -> (a -> m a) -> m ()+modifyCVar_ cvar f = modifyCVar cvar $ liftM (\a -> (a,())) . f++-- | A slight variation on 'modifyCVar_' that allows a value to be+-- returned (@b@) in addition to the modified value of the @CVar@.+{-# INLINE modifyCVar #-}+modifyCVar :: (MonadConc m, NFData a) => CVar m a -> (a -> m (a, b)) -> m b+modifyCVar cvar f = mask $ \restore -> do+  val <- takeCVar cvar+  (val', out) <- restore (f val) `onException` putCVar cvar val+  putCVar cvar val'+  return out++-- | Like 'modifyCVar_', but the @IO@ action in the second argument is+-- executed with asynchronous exceptions masked.+{-# INLINE modifyCVarMasked_ #-}+modifyCVarMasked_ :: (MonadConc m, NFData a) => CVar m a -> (a -> m a) -> m ()+modifyCVarMasked_ cvar f = modifyCVarMasked cvar $ liftM (\a -> (a,())) . f++-- | Like 'modifyCVar', but the @IO@ action in the second argument is+-- executed with asynchronous exceptions masked.+{-# INLINE modifyCVarMasked #-}+modifyCVarMasked :: (MonadConc m, NFData a) => CVar m a -> (a -> m (a, b)) -> m b+modifyCVarMasked cvar f = mask_ $ do+  val <- takeCVar cvar+  (val', out) <- f val `onException` putCVar cvar val+  putCVar cvar val'+  return out

@@ -0,0 +1,86 @@+-- | Transactional @CVar@s, for use with 'MonadSTM'.+module Control.Concurrent.STM.CTMVar+  ( -- * @CTMVar@s+    CTMVar+  , newCTMVar+  , newEmptyCTMVar+  , takeCTMVar+  , putCTMVar+  , readCTMVar+  , tryTakeCTMVar+  , tryPutCTMVar+  , tryReadCTMVar+  , isEmptyCTMVar+  , swapCTMVar+  ) where++import Control.Monad (liftM, when, unless)+import Control.Monad.STM.Class+import Data.Maybe (isJust, isNothing)++-- | A @CTMVar@ is like an @MVar@ or a @CVar@, but using transactional+-- memory. As transactions are atomic, this makes dealing with+-- multiple @CTMVar@s easier than wrangling multiple @CVar@s.+newtype CTMVar m a = CTMVar (CTVar m (Maybe a))++-- | Create a 'CTMVar' containing the given value.+newCTMVar :: MonadSTM m => a -> m (CTMVar m a)+newCTMVar a = do+  ctvar <- newCTVar $ Just a+  return $ CTMVar ctvar++-- | Create a new empty 'CTMVar'.+newEmptyCTMVar :: MonadSTM m => m (CTMVar m a)+newEmptyCTMVar = do+  ctvar <- newCTVar Nothing+  return $ CTMVar ctvar++-- | Take the contents of a 'CTMVar', or 'retry' if it is empty.+takeCTMVar :: MonadSTM m => CTMVar m a -> m a+takeCTMVar ctmvar = do+  taken <- tryTakeCTMVar ctmvar+  maybe retry return taken++-- | Write to a 'CTMVar', or 'retry' if it is full.+putCTMVar :: MonadSTM m => CTMVar m a -> a -> m ()+putCTMVar ctmvar a = do+  putted <- tryPutCTMVar ctmvar a+  unless putted retry++-- | Read from a 'CTMVar' without emptying, or 'retry' if it is empty.+readCTMVar :: MonadSTM m => CTMVar m a -> m a+readCTMVar ctmvar = do+  readed <- tryReadCTMVar ctmvar+  maybe retry return readed++-- | Try to take the contents of a 'CTMVar', returning 'Nothing' if it+-- is empty.+tryTakeCTMVar :: MonadSTM m => CTMVar m a -> m (Maybe a)+tryTakeCTMVar (CTMVar ctvar) = do+  val <- readCTVar ctvar+  when (isJust val) $ writeCTVar ctvar Nothing+  return val++-- | Try to write to a 'CTMVar', returning 'False' if it is full.+tryPutCTMVar :: MonadSTM m => CTMVar m a -> a -> m Bool+tryPutCTMVar (CTMVar ctvar) a = do+  val <- readCTVar ctvar+  when (isNothing val) $ writeCTVar ctvar (Just a)+  return $ isNothing val++-- | Try to read from a 'CTMVar' without emptying, returning 'Nothing'+-- if it is empty.+tryReadCTMVar :: MonadSTM m => CTMVar m a -> m (Maybe a)+tryReadCTMVar (CTMVar ctvar) = readCTVar ctvar++-- | Check if a 'CTMVar' is empty or not.+isEmptyCTMVar :: MonadSTM m => CTMVar m a -> m Bool+isEmptyCTMVar ctmvar = isNothing `liftM` tryReadCTMVar ctmvar++-- | Swap the contents of a 'CTMVar' returning the old contents, or+-- 'retry' if it is empty.+swapCTMVar :: MonadSTM m => CTMVar m a -> a -> m a+swapCTMVar ctmvar a = do+  val <- takeCTMVar ctmvar+  putCTMVar ctmvar a+  return val

@@ -0,0 +1,34 @@+-- | Transactional variables, for use with 'MonadSTM'.+module Control.Concurrent.STM.CTVar+  ( -- * @CTVar@s+    CTVar+  , newCTVar+  , readCTVar+  , writeCTVar+  , modifyCTVar+  , modifyCTVar'+  , swapCTVar+  ) where++import Control.Monad.STM.Class++-- * @CTVar@s++-- | Mutate the contents of a 'CTVar'. This is non-strict.+modifyCTVar :: MonadSTM m => CTVar m a -> (a -> a) -> m ()+modifyCTVar ctvar f = do+  a <- readCTVar ctvar+  writeCTVar ctvar $ f a++-- | Mutate the contents of a 'CTVar' strictly.+modifyCTVar' :: MonadSTM m => CTVar m a -> (a -> a) -> m ()+modifyCTVar' ctvar f = do+  a <- readCTVar ctvar+  writeCTVar ctvar $! f a++-- | Swap the contents of a 'CTVar', returning the old value.+swapCTVar :: MonadSTM m => CTVar m a -> a -> m a+swapCTVar ctvar a = do+  old <- readCTVar ctvar+  writeCTVar ctvar a+  return old

@@ -0,0 +1,536 @@+{-# LANGUAGE CPP              #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE RankNTypes       #-}+{-# LANGUAGE TypeFamilies     #-}++-- | This module captures in a typeclass the interface of concurrency+-- monads.+module Control.Monad.Conc.Class+  ( MonadConc(..)+  -- * Utilities+  , spawn+  , forkFinally+  , killThread+  ) where++import Control.Concurrent (forkIO)+import Control.Concurrent.MVar (MVar, readMVar, newEmptyMVar, putMVar, tryPutMVar, takeMVar, tryTakeMVar)+import Control.Exception (Exception, AsyncException(ThreadKilled), SomeException)+import Control.Monad (liftM)+import Control.Monad.Catch (MonadCatch, MonadThrow, MonadMask)+import Control.Monad.Reader (ReaderT(..), runReaderT)+import Control.Monad.STM (STM)+import Control.Monad.STM.Class (MonadSTM, CTVar)+import Control.Monad.Trans (lift)+import Data.IORef (IORef, atomicModifyIORef, newIORef, readIORef)++import qualified Control.Concurrent as C+import qualified Control.Monad.Catch as Ca+import qualified Control.Monad.RWS.Lazy as RL+import qualified Control.Monad.RWS.Strict as RS+import qualified Control.Monad.STM as S+import qualified Control.Monad.State.Lazy as SL+import qualified Control.Monad.State.Strict as SS+import qualified Control.Monad.Writer.Lazy as WL+import qualified Control.Monad.Writer.Strict as WS++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative (Applicative)+import Data.Monoid (Monoid, mempty)+#endif++-- | @MonadConc@ is an abstraction over GHC's typical concurrency+-- abstraction. It captures the interface of concurrency monads in+-- terms of how they can operate on shared state and in the presence+-- of exceptions.+--+-- There are a few notable differences between this and the @Par@+-- monad approach: firstly, @Par@ imposes 'NFData' constraints on+-- everything, as it achieves its speed-up by forcing evaluation in+-- separate threads. @MonadConc@ doesn't do that, and so you need to+-- be careful about where evaluation occurs, just like with+-- 'MVar's. Secondly, this builds on @Par@'s futures by allowing+-- @CVar@s which threads can read from and write to, possibly multiple+-- times, whereas with the @Par@ monads it is illegal to write+-- multiple times to the same @IVar@ (or to non-blockingly read from+-- it) which, when there are no exceptions, removes the possibility of+-- data races.+--+-- Every @MonadConc@ has an associated 'MonadSTM', transactions of+-- which can be run atomically.+class ( Applicative m, Monad m+      , MonadCatch m, MonadThrow m, MonadMask m+      , MonadSTM (STMLike m)+      , Eq (ThreadId m), Show (ThreadId m)) => MonadConc m  where+  -- | The associated 'MonadSTM' for this class.+  type STMLike m :: * -> *++  -- | The mutable reference type, like 'MVar's. This may contain one+  -- value at a time, attempting to read or take from an \"empty\"+  -- @CVar@ will block until it is full, and attempting to put to a+  -- \"full\" @CVar@ will block until it is empty.+  type CVar m :: * -> *++  -- | The mutable non-blocking reference type. These are like+  -- 'IORef's, but don't have the potential re-ordering problem+  -- mentioned in Data.IORef.+  type CRef m :: * -> *++  -- | An abstract handle to a thread.+  type ThreadId m :: *++  -- | Fork a computation to happen concurrently. Communication may+  -- happen over @CVar@s.+  fork :: m () -> m (ThreadId m)++  -- | Like 'fork', but the child thread is passed a function that can+  -- be used to unmask asynchronous exceptions. This function should+  -- not be used within a 'mask' or 'uninterruptibleMask'.+  forkWithUnmask :: ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)++  -- | Fork a computation to happen on a specific processor. The+  -- specified int is the /capability number/, typically capabilities+  -- correspond to physical processors or cores but this is+  -- implementation dependent. The int is interpreted modulo to the+  -- total number of capabilities as returned by 'getNumCapabilities'.+  forkOn :: Int -> m () -> m (ThreadId m)++  -- | Get the number of Haskell threads that can run simultaneously.+  getNumCapabilities :: m Int++  -- | Get the @ThreadId@ of the current thread.+  myThreadId :: m (ThreadId m)++  -- | Create a new empty @CVar@.+  newEmptyCVar :: m (CVar m a)++  -- | Put a value into a @CVar@. If there is already a value there,+  -- this will block until that value has been taken, at which point+  -- the value will be stored.+  putCVar :: CVar m a -> a -> m ()++  -- | Attempt to put a value in a @CVar@ non-blockingly, returning+  -- 'True' (and filling the @CVar@) if there was nothing there,+  -- otherwise returning 'False'.+  tryPutCVar :: CVar m a -> a -> m Bool++  -- | Block until a value is present in the @CVar@, and then return+  -- it. As with 'readMVar', this does not \"remove\" the value,+  -- multiple reads are possible.+  readCVar :: CVar m a -> m a++  -- | Take a value from a @CVar@. This \"empties\" the @CVar@,+  -- allowing a new value to be put in. This will block if there is no+  -- value in the @CVar@ already, until one has been put.+  takeCVar :: CVar m a -> m a++  -- | Attempt to take a value from a @CVar@ non-blockingly, returning+  -- a 'Just' (and emptying the @CVar@) if there was something there,+  -- otherwise returning 'Nothing'.+  tryTakeCVar :: CVar m a -> m (Maybe a)++  -- | Create a new reference.+  newCRef :: a -> m (CRef m a)++  -- | Read the current value stored in a reference.+  readCRef :: CRef m a -> m a++  -- | Atomically modify the value stored in a reference.+  modifyCRef :: CRef m a -> (a -> (a, b)) -> m b++  -- | Replace the value stored in a reference.+  --+  -- > writeCRef r a = modifyCRef r $ const (a, ())+  writeCRef :: CRef m a -> a -> m ()+  writeCRef r a = modifyCRef r $ const (a, ())++  -- | Perform an STM transaction atomically.+  atomically :: STMLike m a -> m a++  -- | Throw an exception. This will \"bubble up\" looking for an+  -- exception handler capable of dealing with it and, if one is not+  -- found, the thread is killed.+  --+  -- > throw = Control.Monad.Catch.throwM+  throw :: Exception e => e -> m a+  throw = Ca.throwM++  -- | Catch an exception. This is only required to be able to catch+  -- exceptions raised by 'throw', unlike the more general+  -- Control.Exception.catch function. If you need to be able to catch+  -- /all/ errors, you will have to use 'IO'.+  --+  -- > catch = Control.Monad.Catch.catch+  catch :: Exception e => m a -> (e -> m a) -> m a+  catch = Ca.catch++  -- | Throw an exception to the target thread. This blocks until the+  -- exception is delivered, and it is just as if the target thread+  -- had raised it with 'throw'. This can interrupt a blocked action.+  throwTo :: Exception e => ThreadId m -> e -> m ()++  -- | Executes a computation with asynchronous exceptions+  -- /masked/. That is, any thread which attempts to raise an+  -- exception in the current thread with 'throwTo' will be blocked+  -- until asynchronous exceptions are unmasked again.+  --+  -- The argument passed to mask is a function that takes as its+  -- argument another function, which can be used to restore the+  -- prevailing masking state within the context of the masked+  -- computation. This function should not be used within an+  -- 'uninterruptibleMask'.+  --+  -- > mask = Control.Monad.Catch.mask+  mask :: ((forall a. m a -> m a) -> m b) -> m b+  mask = Ca.mask++  -- | Like 'mask', but the masked computation is not+  -- interruptible. THIS SHOULD BE USED WITH GREAT CARE, because if a+  -- thread executing in 'uninterruptibleMask' blocks for any reason,+  -- then the thread (and possibly the program, if this is the main+  -- thread) will be unresponsive and unkillable. This function should+  -- only be necessary if you need to mask exceptions around an+  -- interruptible operation, and you can guarantee that the+  -- interruptible operation will only block for a short period of+  -- time. The supplied unmasking function should not be used within a+  -- 'mask'.+  --+  -- > uninterruptibleMask = Control.Monad.Catch.uninterruptibleMask+  uninterruptibleMask :: ((forall a. m a -> m a) -> m b) -> m b+  uninterruptibleMask = Ca.uninterruptibleMask++  -- | Runs its argument, just as if the @_concNoTest@ weren't there.+  --+  -- This function is purely for testing purposes, and indicates that+  -- it's not worth considering more than one schedule here. This is+  -- useful if you have some larger computation built up out of+  -- subcomputations which you have already got tests for: you only+  -- want to consider what's unique to the large component.+  --+  -- The test runner will report a failure if the argument fails.+  --+  -- Note that inappropriate use of @_concNoTest@ can actually+  -- /suppress/ bugs! For this reason it is recommended to use it only+  -- for things which don't make use of any state from a larger+  -- scope. As a rule-of-thumb: if you can't define it as a top-level+  -- function taking no @CVRef@, @CVar@, or @CTVar@ arguments, you+  -- probably shouldn't @_concNoTest@ it.+  --+  -- > _concNoTest x = x+  _concNoTest :: m a -> m a+  _concNoTest = id++  -- | Does nothing.+  --+  -- This function is purely for testing purposes, and indicates that+  -- the thread has a reference to the provided @CVar@ or+  -- @CTVar@. This function may be called multiple times, to add new+  -- knowledge to the system. It does not need to be called when+  -- @CVar@s or @CTVar@s are created, these get recorded+  -- automatically.+  --+  -- Gathering this information allows detection of cases where the+  -- main thread is blocked on a variable no runnable thread has a+  -- reference to, which is a deadlock situation.+  --+  -- > _concKnowsAbout _ = return ()+  _concKnowsAbout :: Either (CVar m a) (CTVar (STMLike m) a) -> m ()+  _concKnowsAbout _ = return ()++  -- | Does nothing.+  --+  -- The counterpart to '_concKnowsAbout'. Indicates that the+  -- referenced variable will never be touched again by the current+  -- thread.+  --+  -- Note that inappropriate use of @_concForgets@ can result in false+  -- positives! Be very sure that the current thread will /never/+  -- refer to the variable again, for instance when leaving its scope.+  --+  -- > _concForgets _ = return ()+  _concForgets :: Either (CVar m a) (CTVar (STMLike m) a) -> m ()+  _concForgets _ = return ()++  -- | Does nothing.+  --+  -- Indicates to the test runner that all variables which have been+  -- passed in to this thread have been recorded by calls to+  -- '_concKnowsAbout'. If every thread has called '_concAllKnown',+  -- then detection of nonglobal deadlock is turned on.+  --+  -- If a thread receives references to @CVar@s or @CTVar@s in the+  -- future (for instance, if one was sent over a channel), then+  -- '_concKnowsAbout' should be called immediately, otherwise there+  -- is a risk of identifying false positives.+  --+  -- > _concAllKnown = return ()+  _concAllKnown :: m ()+  _concAllKnown = return ()++instance MonadConc IO where+  type STMLike  IO = STM+  type CVar     IO = MVar+  type CRef     IO = IORef+  type ThreadId IO = C.ThreadId++  readCVar       = readMVar+  fork           = forkIO+  forkWithUnmask = C.forkIOWithUnmask+  forkOn         = C.forkOn+  getNumCapabilities = C.getNumCapabilities+  myThreadId     = C.myThreadId+  throwTo        = C.throwTo+  newEmptyCVar   = newEmptyMVar+  putCVar        = putMVar+  tryPutCVar     = tryPutMVar+  takeCVar       = takeMVar+  tryTakeCVar    = tryTakeMVar+  newCRef        = newIORef+  readCRef       = readIORef+  modifyCRef     = atomicModifyIORef+  atomically     = S.atomically++-- | Create a concurrent computation for the provided action, and+-- return a @CVar@ which can be used to query the result.+spawn :: MonadConc m => m a -> m (CVar m a)+spawn ma = do+  cvar <- newEmptyCVar+  _ <- fork $ _concKnowsAbout (Left cvar) >> ma >>= putCVar cvar+  return cvar++-- | Fork a thread and call the supplied function when the thread is+-- about to terminate, with an exception or a returned value. The+-- function is called with asynchronous exceptions masked.+--+-- This function is useful for informing the parent when a child+-- terminates, for example.+forkFinally :: MonadConc m => m a -> (Either SomeException a -> m ()) -> m (ThreadId m)+forkFinally action and_then =+  mask $ \restore ->+    fork $ Ca.try (restore action) >>= and_then++-- | Raise the 'ThreadKilled' exception in the target thread. Note+-- that if the thread is prepared to catch this exception, it won't+-- actually kill it.+killThread :: MonadConc m => ThreadId m -> m ()+killThread tid = throwTo tid ThreadKilled++-------------------------------------------------------------------------------+-- Transformer instances++instance MonadConc m => MonadConc (ReaderT r m) where+  type STMLike  (ReaderT r m) = STMLike m+  type CVar     (ReaderT r m) = CVar m+  type CRef     (ReaderT r m) = CRef m+  type ThreadId (ReaderT r m) = ThreadId m++  fork              = reader fork+  forkOn i          = reader (forkOn i)+  forkWithUnmask ma = ReaderT $ \r -> forkWithUnmask (\f -> runReaderT (ma $ reader f) r)+  _concNoTest       = reader _concNoTest++  getNumCapabilities = lift getNumCapabilities+  myThreadId         = lift myThreadId+  throwTo t          = lift . throwTo t+  newEmptyCVar       = lift newEmptyCVar+  readCVar           = lift . readCVar+  putCVar v          = lift . putCVar v+  tryPutCVar v       = lift . tryPutCVar v+  takeCVar           = lift . takeCVar+  tryTakeCVar        = lift . tryTakeCVar+  newCRef            = lift . newCRef+  readCRef           = lift . readCRef+  modifyCRef r       = lift . modifyCRef r+  atomically         = lift . atomically+  _concKnowsAbout    = lift . _concKnowsAbout+  _concForgets       = lift . _concForgets+  _concAllKnown      = lift _concAllKnown++reader :: Monad m => (m a -> m b) -> ReaderT r m a -> ReaderT r m b+reader f ma = ReaderT $ \r -> f (runReaderT ma r)++instance (MonadConc m, Monoid w) => MonadConc (WL.WriterT w m) where+  type STMLike  (WL.WriterT w m) = STMLike m+  type CVar     (WL.WriterT w m) = CVar m+  type CRef     (WL.WriterT w m) = CRef m+  type ThreadId (WL.WriterT w m) = ThreadId m++  fork              = writerlazy fork+  forkOn i          = writerlazy (forkOn i)+  forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WL.runWriterT (ma $ writerlazy f))+  _concNoTest       = writerlazy _concNoTest++  getNumCapabilities = lift getNumCapabilities+  myThreadId         = lift myThreadId+  throwTo t          = lift . throwTo t+  newEmptyCVar       = lift newEmptyCVar+  readCVar           = lift . readCVar+  putCVar v          = lift . putCVar v+  tryPutCVar v       = lift . tryPutCVar v+  takeCVar           = lift . takeCVar+  tryTakeCVar        = lift . tryTakeCVar+  newCRef            = lift . newCRef+  readCRef           = lift . readCRef+  modifyCRef r       = lift . modifyCRef r+  atomically         = lift . atomically+  _concKnowsAbout    = lift . _concKnowsAbout+  _concForgets       = lift . _concForgets+  _concAllKnown      = lift _concAllKnown++writerlazy :: (Monad m, Monoid w) => (m a -> m b) -> WL.WriterT w m a -> WL.WriterT w m b+writerlazy f ma = lift . f $ fst `liftM` WL.runWriterT ma++instance (MonadConc m, Monoid w) => MonadConc (WS.WriterT w m) where+  type STMLike  (WS.WriterT w m) = STMLike m+  type CVar     (WS.WriterT w m) = CVar m+  type CRef     (WS.WriterT w m) = CRef m+  type ThreadId (WS.WriterT w m) = ThreadId m++  fork              = writerstrict fork+  forkOn i          = writerstrict (forkOn i)+  forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WS.runWriterT (ma $ writerstrict f))+  _concNoTest       = writerstrict _concNoTest++  getNumCapabilities = lift getNumCapabilities+  myThreadId         = lift myThreadId+  throwTo t          = lift . throwTo t+  newEmptyCVar       = lift newEmptyCVar+  readCVar           = lift . readCVar+  putCVar v          = lift . putCVar v+  tryPutCVar v       = lift . tryPutCVar v+  takeCVar           = lift . takeCVar+  tryTakeCVar        = lift . tryTakeCVar+  newCRef            = lift . newCRef+  readCRef           = lift . readCRef+  modifyCRef r       = lift . modifyCRef r+  atomically         = lift . atomically+  _concKnowsAbout    = lift . _concKnowsAbout+  _concForgets       = lift . _concForgets+  _concAllKnown      = lift _concAllKnown++writerstrict :: (Monad m, Monoid w) => (m a -> m b) -> WS.WriterT w m a -> WS.WriterT w m b+writerstrict f ma = lift . f $ fst `liftM` WS.runWriterT ma++instance MonadConc m => MonadConc (SL.StateT s m) where+  type STMLike  (SL.StateT s m) = STMLike m+  type CVar     (SL.StateT s m) = CVar m+  type CRef     (SL.StateT s m) = CRef m+  type ThreadId (SL.StateT s m) = ThreadId m++  fork              = statelazy fork+  forkOn i          = statelazy (forkOn i)+  forkWithUnmask ma = SL.StateT $ \s -> (\a -> (a,s)) `liftM` forkWithUnmask (\f -> SL.evalStateT (ma $ statelazy f) s)+  _concNoTest       = statelazy _concNoTest++  getNumCapabilities = lift getNumCapabilities+  myThreadId         = lift myThreadId+  throwTo t          = lift . throwTo t+  newEmptyCVar       = lift newEmptyCVar+  readCVar           = lift . readCVar+  putCVar v          = lift . putCVar v+  tryPutCVar v       = lift . tryPutCVar v+  takeCVar           = lift . takeCVar+  tryTakeCVar        = lift . tryTakeCVar+  newCRef            = lift . newCRef+  readCRef           = lift . readCRef+  modifyCRef r       = lift . modifyCRef r+  atomically         = lift . atomically+  _concKnowsAbout    = lift . _concKnowsAbout+  _concForgets       = lift . _concForgets+  _concAllKnown      = lift _concAllKnown++statelazy :: Monad m => (m a -> m b) -> SL.StateT s m a -> SL.StateT s m b+statelazy f ma = SL.StateT $ \s -> (\b -> (b,s)) `liftM` f (SL.evalStateT ma s)++instance MonadConc m => MonadConc (SS.StateT s m) where+  type STMLike  (SS.StateT s m) = STMLike m+  type CVar     (SS.StateT s m) = CVar m+  type CRef     (SS.StateT s m) = CRef m+  type ThreadId (SS.StateT s m) = ThreadId m++  fork              = statestrict fork+  forkOn i          = statestrict (forkOn i)+  forkWithUnmask ma = SS.StateT $ \s -> (\a -> (a,s)) `liftM` forkWithUnmask (\f -> SS.evalStateT (ma $ statestrict f) s)+  _concNoTest       = statestrict _concNoTest++  getNumCapabilities = lift getNumCapabilities+  myThreadId         = lift myThreadId+  throwTo t          = lift . throwTo t+  newEmptyCVar       = lift newEmptyCVar+  readCVar           = lift . readCVar+  putCVar v          = lift . putCVar v+  tryPutCVar v       = lift . tryPutCVar v+  takeCVar           = lift . takeCVar+  tryTakeCVar        = lift . tryTakeCVar+  newCRef            = lift . newCRef+  readCRef           = lift . readCRef+  modifyCRef r       = lift . modifyCRef r+  atomically         = lift . atomically+  _concKnowsAbout    = lift . _concKnowsAbout+  _concForgets       = lift . _concForgets+  _concAllKnown      = lift _concAllKnown++statestrict :: Monad m => (m a -> m b) -> SS.StateT s m a -> SS.StateT s m b+statestrict f ma = SS.StateT $ \s -> (\b -> (b,s)) `liftM` f (SS.evalStateT ma s)++instance (MonadConc m, Monoid w) => MonadConc (RL.RWST r w s m) where+  type STMLike  (RL.RWST r w s m) = STMLike m+  type CVar     (RL.RWST r w s m) = CVar m+  type CRef     (RL.RWST r w s m) = CRef m+  type ThreadId (RL.RWST r w s m) = ThreadId m++  fork              = rwslazy fork+  forkOn i          = rwslazy (forkOn i)+  forkWithUnmask ma = RL.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkWithUnmask (\f -> fst `liftM` RL.evalRWST (ma $ rwslazy f) r s)+  _concNoTest       = rwslazy _concNoTest++  getNumCapabilities = lift getNumCapabilities+  myThreadId         = lift myThreadId+  throwTo t          = lift . throwTo t+  newEmptyCVar       = lift newEmptyCVar+  readCVar           = lift . readCVar+  putCVar v          = lift . putCVar v+  tryPutCVar v       = lift . tryPutCVar v+  takeCVar           = lift . takeCVar+  tryTakeCVar        = lift . tryTakeCVar+  newCRef            = lift . newCRef+  readCRef           = lift . readCRef+  modifyCRef r       = lift . modifyCRef r+  atomically         = lift . atomically+  _concKnowsAbout    = lift . _concKnowsAbout+  _concForgets       = lift . _concForgets+  _concAllKnown      = lift _concAllKnown++rwslazy :: (Monad m, Monoid w) => (m a -> m b) -> RL.RWST r w s m a -> RL.RWST r w s m b+rwslazy f ma = RL.RWST $ \r s -> (\b -> (b,s,mempty)) `liftM` f (fst `liftM` RL.evalRWST ma r s)++instance (MonadConc m, Monoid w) => MonadConc (RS.RWST r w s m) where+  type STMLike  (RS.RWST r w s m) = STMLike m+  type CVar     (RS.RWST r w s m) = CVar m+  type CRef     (RS.RWST r w s m) = CRef m+  type ThreadId (RS.RWST r w s m) = ThreadId m++  fork              = rwsstrict fork+  forkOn i          = rwsstrict (forkOn i)+  forkWithUnmask ma = RS.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkWithUnmask (\f -> fst `liftM` RS.evalRWST (ma $ rwsstrict f) r s)+  _concNoTest       = rwsstrict _concNoTest++  getNumCapabilities = lift getNumCapabilities+  myThreadId         = lift myThreadId+  throwTo t          = lift . throwTo t+  newEmptyCVar       = lift newEmptyCVar+  readCVar           = lift . readCVar+  putCVar v          = lift . putCVar v+  tryPutCVar v       = lift . tryPutCVar v+  takeCVar           = lift . takeCVar+  tryTakeCVar        = lift . tryTakeCVar+  newCRef            = lift . newCRef+  readCRef           = lift . readCRef+  modifyCRef r       = lift . modifyCRef r+  atomically         = lift . atomically+  _concKnowsAbout    = lift . _concKnowsAbout+  _concForgets       = lift . _concForgets+  _concAllKnown      = lift _concAllKnown++rwsstrict :: (Monad m, Monoid w) => (m a -> m b) -> RS.RWST r w s m a -> RS.RWST r w s m b+rwsstrict f ma = RS.RWST $ \r s -> (\b -> (b,s,mempty)) `liftM` f (fst `liftM` RS.evalRWST ma r s)

@@ -0,0 +1,163 @@+{-# LANGUAGE CPP          #-}+{-# LANGUAGE TypeFamilies #-}++-- | This module provides an abstraction over 'STM', which can be used+-- with 'MonadConc'.+module Control.Monad.STM.Class where++import Control.Concurrent.STM (STM)+import Control.Concurrent.STM.TVar (TVar, newTVar, readTVar, writeTVar)+import Control.Exception (Exception)+import Control.Monad (unless)+import Control.Monad.Catch (MonadCatch, MonadThrow, throwM, catch)+import Control.Monad.Reader (ReaderT(..), runReaderT)+import Control.Monad.Trans (lift)++import qualified Control.Monad.RWS.Lazy as RL+import qualified Control.Monad.RWS.Strict as RS+import qualified Control.Monad.STM as S+import qualified Control.Monad.State.Lazy as SL+import qualified Control.Monad.State.Strict as SS+import qualified Control.Monad.Writer.Lazy as WL+import qualified Control.Monad.Writer.Strict as WS++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative (Applicative)+import Data.Monoid (Monoid)+#endif++-- | @MonadSTM@ is an abstraction over 'STM'.+--+-- This class does not provide any way to run transactions, rather+-- each 'MonadConc' has an associated @MonadSTM@ from which it can+-- atomically run a transaction.+--+-- A minimal implementation consists of 'retry', 'orElse', 'newCTVar',+-- 'readCTVar', and 'writeCTVar'.+class (Applicative m, Monad m, MonadCatch m, MonadThrow m) => MonadSTM m where+  -- | The mutable reference type. These behave like 'TVar's, in that+  -- they always contain a value and updates are non-blocking and+  -- synchronised.+  type CTVar m :: * -> *++  -- | Retry execution of this transaction because it has seen values+  -- in @CTVar@s that it shouldn't have. This will result in the+  -- thread running the transaction being blocked until any @CTVar@s+  -- referenced in it have been mutated.+  retry :: m a++  -- | Run the first transaction and, if it @retry@s, run the second+  -- instead. If the monad is an instance of+  -- 'Alternative'/'MonadPlus', 'orElse' should be the '(<|>)'/'mplus'+  -- function.+  orElse :: m a -> m a -> m a++  -- | Check whether a condition is true and, if not, call @retry@.+  --+  -- > check b = unless b retry+  check :: Bool -> m ()+  check b = unless b retry++  -- | Create a new @CTVar@ containing the given value.+  newCTVar :: a -> m (CTVar m a)++  -- | Return the current value stored in a @CTVar@.+  readCTVar :: CTVar m a -> m a++  -- | Write the supplied value into the @CTVar@.+  writeCTVar :: CTVar m a -> a -> m ()++  -- | Throw an exception. This aborts the transaction and propagates+  -- the exception.+  --+  -- > throwSTM = Control.Monad.Catch.throwM+  throwSTM :: Exception e => e -> m a+  throwSTM = throwM++  -- | Handling exceptions from 'throwSTM'.+  --+  -- > catchSTM = Control.Monad.Catch.catch+  catchSTM :: Exception e => m a -> (e -> m a) -> m a+  catchSTM = Control.Monad.Catch.catch++instance MonadSTM STM where+  type CTVar STM = TVar++  retry      = S.retry+  orElse     = S.orElse+  newCTVar   = newTVar+  readCTVar  = readTVar+  writeCTVar = writeTVar++-------------------------------------------------------------------------------+-- Transformer instances++instance MonadSTM m => MonadSTM (ReaderT r m) where+  type CTVar (ReaderT r m) = CTVar m++  retry        = lift retry+  orElse ma mb = ReaderT $ \r -> orElse (runReaderT ma r) (runReaderT mb r)+  check        = lift . check+  newCTVar     = lift . newCTVar+  readCTVar    = lift . readCTVar+  writeCTVar v = lift . writeCTVar v++instance (MonadSTM m, Monoid w) => MonadSTM (WL.WriterT w m) where+  type CTVar (WL.WriterT w m) = CTVar m++  retry        = lift retry+  orElse ma mb = WL.WriterT $ orElse (WL.runWriterT ma) (WL.runWriterT mb)+  check        = lift . check+  newCTVar     = lift . newCTVar+  readCTVar    = lift . readCTVar+  writeCTVar v = lift . writeCTVar v++instance (MonadSTM m, Monoid w) => MonadSTM (WS.WriterT w m) where+  type CTVar (WS.WriterT w m) = CTVar m++  retry        = lift retry+  orElse ma mb = WS.WriterT $ orElse (WS.runWriterT ma) (WS.runWriterT mb)+  check        = lift . check+  newCTVar     = lift . newCTVar+  readCTVar    = lift . readCTVar+  writeCTVar v = lift . writeCTVar v++instance MonadSTM m => MonadSTM (SL.StateT s m) where+  type CTVar (SL.StateT s m) = CTVar m++  retry        = lift retry+  orElse ma mb = SL.StateT $ \s -> orElse (SL.runStateT ma s) (SL.runStateT mb s)+  check        = lift . check+  newCTVar     = lift . newCTVar+  readCTVar    = lift . readCTVar+  writeCTVar v = lift . writeCTVar v++instance MonadSTM m => MonadSTM (SS.StateT s m) where+  type CTVar (SS.StateT s m) = CTVar m++  retry        = lift retry+  orElse ma mb = SS.StateT $ \s -> orElse (SS.runStateT ma s) (SS.runStateT mb s)+  check        = lift . check+  newCTVar     = lift . newCTVar+  readCTVar    = lift . readCTVar+  writeCTVar v = lift . writeCTVar v++instance (MonadSTM m, Monoid w) => MonadSTM (RL.RWST r w s m) where+  type CTVar (RL.RWST r w s m) = CTVar m++  retry        = lift retry+  orElse ma mb = RL.RWST $ \r s -> orElse (RL.runRWST ma r s) (RL.runRWST mb r s)+  check        = lift . check+  newCTVar     = lift . newCTVar+  readCTVar    = lift . readCTVar+  writeCTVar v = lift . writeCTVar v++instance (MonadSTM m, Monoid w) => MonadSTM (RS.RWST r w s m) where+  type CTVar (RS.RWST r w s m) = CTVar m++  retry        = lift retry+  orElse ma mb = RS.RWST $ \r s -> orElse (RS.runRWST ma r s) (RS.runRWST mb r s)+  check        = lift . check+  newCTVar     = lift . newCTVar+  readCTVar    = lift . readCTVar+  writeCTVar v = lift . writeCTVar v

@@ -0,0 +1,60 @@+{-# LANGUAGE CPP #-}+-- | Extra list functions and list-like types.+module Data.List.Extra where++import Control.DeepSeq (NFData(..))+import Data.Traversable (fmapDefault, foldMapDefault)++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative ((<$>), (<*>))+import Data.Foldable (Foldable(..))+import Data.Traversable (Traversable(..))+#else+-- Why does this give a redundancy warning? It's necessary in order to+-- define the toList function in the Foldable instance for NonEmpty!+import Data.Foldable (toList)+#endif++-- * Regular lists++-- | Check if a list has more than some number of elements.+moreThan :: [a] -> Int -> Bool+moreThan [] n = n < 0+moreThan _ 0  = True+moreThan (_:xs) n = moreThan xs (n-1)++-- * Non-empty lists++-- This gets exposed to users of the library, so it has a bunch of+-- classes which aren't actually used in the rest of the code to make+-- it more friendly to further use.++-- | The type of non-empty lists.+data NonEmpty a = a :| [a] deriving (Eq, Ord, Read, Show)++instance Functor NonEmpty where+  fmap = fmapDefault++instance Foldable NonEmpty where+  foldMap = foldMapDefault++#if __GLASGOW_HASKELL__ >= 710+  -- toList isn't in Foldable until GHC 7.10+  toList (a :| as) = a : as+#endif++instance Traversable NonEmpty where+  traverse f (a:|as) = (:|) <$> f a <*> traverse f as++instance NFData a => NFData (NonEmpty a) where+  rnf (x:|xs) = rnf (x, xs)++-- | Convert a 'NonEmpty' to a regular non-empty list.+toList :: NonEmpty a -> [a]+toList (a :| as) = a : as++-- | Convert a regular non-empty list to a 'NonEmpty'. This is+-- necessarily partial.+unsafeToNonEmpty :: [a] -> NonEmpty a+unsafeToNonEmpty (a:as) = a :| as+unsafeToNonEmpty [] = error "Cannot convert [] to NonEmpty!"

@@ -0,0 +1,20 @@+Copyright (c) 2015, 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+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be+included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,387 @@+{-# LANGUAGE CPP        #-}+{-# LANGUAGE RankNTypes #-}++-- | Deterministic testing for concurrent computations.+--+-- As an example, consider this program, which has two locks and a+-- shared variable. Two threads are spawned, which claim the locks,+-- update the shared variable, and release the locks. The main thread+-- waits for them both to terminate, and returns the final result.+--+-- > bad :: MonadConc m => m Int+-- > bad = do+-- >   a <- newEmptyCVar+-- >   b <- newEmptyCVar+-- >+-- >   c <- newCVar 0+-- >+-- >   j1 <- spawn $ lock a >> lock b >> modifyCVar_ c (return . succ) >> unlock b >> unlock a+-- >   j2 <- spawn $ lock b >> lock a >> modifyCVar_ c (return . pred) >> unlock a >> unlock b+-- >+-- >   takeCVar j1+-- >   takeCVar j2+-- >+-- >   takeCVar c+--+-- The correct result is 0, as it starts out as 0 and is incremented+-- and decremented by threads 1 and 2, respectively. However, note the+-- order of acquisition of the locks in the two threads. If thread 2+-- pre-empts thread 1 between the acquisition of the locks (or if+-- thread 1 pre-empts thread 2), a deadlock situation will arise, as+-- thread 1 will have lock @a@ and be waiting on @b@, and thread 2+-- will have @b@ and be waiting on @a@.+--+-- Here is what Deja Fu has to say about it:+--+-- > > autocheck bad+-- > [fail] Never Deadlocks (checked: 2)+-- >         [deadlock] S0---------S1--P2---S1-+-- > [pass] No Exceptions (checked: 11)+-- > [fail] Consistent Result (checked: 10)+-- >         0 S0---------S1---------------S0--S2---------------S0----+-- >         [deadlock] S0---------S1--P2---S1-+-- > False+--+-- It identifies the deadlock, and also the possible results the+-- computation can produce, and displays a simplified trace leading to+-- each failing outcome. It also returns @False@ as there are test+-- failures. The automatic testing functionality is good enough if you+-- only want to check your computation is deterministic, but if you+-- have more specific requirements (or have some expected and+-- tolerated level of nondeterminism), you can write tests yourself+-- using the @dejafu*@ functions.+--+-- __Warning:__ If your computation under test does @IO@, the @IO@+-- will be executed lots of times! Be sure that it is deterministic+-- enough not to invalidate your test results. Mocking may be useful+-- where possible.+module Test.DejaFu+  ( -- * Testing++  -- | Testing in Deja Fu is similar to unit testing, the programmer+  -- produces a self-contained monadic action to execute under+  -- different schedules, and supplies a list of predicates to apply+  -- to the list of results produced.+  --+  -- If you simply wish to check that something is deterministic, see+  -- the 'autocheck' and 'autocheckIO' functions.++    autocheck+  , dejafu+  , dejafus+  , dejafus'+  , autocheckIO+  , dejafuIO+  , dejafusIO+  , dejafusIO'++  -- * Results++  -- | The results of a test can be pretty-printed to the console, as+  -- with the above functions, or used in their original, much richer,+  -- form for debugging purposes. These functions provide full access+  -- to this data type which, most usefully, contains a detailed trace+  -- of execution, showing what each thread did at each point.++  , Result(..)+  , Failure(..)+  , runTest+  , runTest'+  , runTestIO+  , runTestIO'++  -- * Predicates++  -- | Predicates evaluate a list of results of execution and decide+  -- whether some test case has passed or failed. They can be lazy and+  -- make use of short-circuit evaluation to avoid needing to examine+  -- the entire list of results, and can check any property which can+  -- be defined for the return type of your monadic action.+  --+  -- A collection of common predicates are provided, along with the+  -- helper functions 'alwaysTrue', 'alwaysTrue2' and 'somewhereTrue'+  -- to lfit predicates over a single result to over a collection of+  -- results.++  , Predicate+  , deadlocksNever+  , deadlocksAlways+  , deadlocksSometimes+  , exceptionsNever+  , exceptionsAlways+  , exceptionsSometimes+  , alwaysSame+  , notAlwaysSame+  , alwaysTrue+  , alwaysTrue2+  , somewhereTrue+  ) where++import Control.Arrow (first)+import Control.DeepSeq (NFData(..))+import Control.Monad (when)+import Data.List.Extra+import Test.DejaFu.Deterministic+import Test.DejaFu.Deterministic.IO (ConcIO)+import Test.DejaFu.SCT++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative ((<$>))+import Data.Foldable (Foldable(..))+#endif++-- | 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 'autocheckIO'.+autocheck :: (Eq a, Show a)+  => (forall t. Conc t a)+  -- ^ The computation to test+  -> IO Bool+autocheck conc = dejafus conc cases where+  cases = [ ("Never Deadlocks",   deadlocksNever)+          , ("No Exceptions",     exceptionsNever)+          , ("Consistent Result", alwaysSame)+          ]++-- | Variant of 'autocheck' for computations which do 'IO'.+autocheckIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> IO Bool+autocheckIO concio = dejafusIO concio cases where+  cases = [ ("Never Deadlocks",   deadlocksNever)+          , ("No Exceptions",     exceptionsNever)+          , ("Consistent Result", alwaysSame)+          ]++-- | Check a predicate and print the result to stdout, return 'True'+-- if it passes.+dejafu :: (Eq a, Show a)+  => (forall t. Conc t a)+  -- ^ The computation to test+  -> (String, Predicate a)+  -- ^ The predicate (with a name) to check+  -> IO Bool+dejafu conc test = dejafus conc [test]++-- | Variant of 'dejafu' which takes a collection of predicates to+-- test, returning 'True' if all pass.+dejafus :: (Eq a, Show a)+  => (forall t. Conc t a)+  -- ^ The computation to test+  -> [(String, Predicate a)]+  -- ^ The list of predicates (with names) to check+  -> IO Bool+dejafus = dejafus' 2++-- | Variant of 'dejafus' which takes a pre-emption bound.+--+-- Pre-emption bounding is used to filter the large number of possible+-- schedules, and can be iteratively increased for further coverage+-- guarantees. Empirical studies (/Concurrency Testing Using Schedule Bounding: an Empirical Study/,+-- P. Thompson, A. Donaldson, and A. Betts) have found that many+-- concurrency bugs can be exhibited with as few as two threads and+-- two pre-emptions, which is what 'dejafus' uses.+--+-- __Warning:__ Using a larger pre-emption bound will almost certainly+-- significantly increase the time taken to test!+dejafus' :: (Eq a, Show a)+  => Int+  -- ^ The maximum number of pre-emptions to allow in a single+  -- execution+  -> (forall t. Conc t a)+  -- ^ The computation to test+  -> [(String, Predicate a)]+  -- ^ The list of predicates (with names) to check+  -> IO Bool+dejafus' pb conc tests = do+  let traces = sctPreBound pb conc+  results <- mapM (\(name, test) -> doTest name $ test traces) tests+  return $ and results++-- | Variant of 'dejafu' for computations which do 'IO'.+dejafuIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> (String, Predicate a) -> IO Bool+dejafuIO concio test = dejafusIO concio [test]++-- | Variant of 'dejafus' for computations which do 'IO'.+dejafusIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> [(String, Predicate a)] -> IO Bool+dejafusIO = dejafusIO' 2++-- | Variant of 'dejafus'' for computations which do 'IO'.+dejafusIO' :: (Eq a, Show a) => Int -> (forall t. ConcIO t a) -> [(String, Predicate a)] -> IO Bool+dejafusIO' pb concio tests = do+  traces  <- sctPreBoundIO pb concio+  results <- mapM (\(name, test) -> doTest name $ test traces) tests+  return $ and results++-- * Test cases++-- | The results of a test, including the number of cases checked to+-- determine the final boolean outcome.+data Result a = Result+  { _pass         :: Bool+  -- ^ Whether the test passed or not.+  , _casesChecked :: Int+  -- ^ The number of cases checked.+  , _failures     :: [(Either Failure a, Trace)]+  -- ^ The failing cases, if any.+  } deriving (Show, Eq)++instance NFData a => NFData (Result a) where+  rnf r = rnf (_pass r, _casesChecked r, _failures r)++instance Functor Result where+  fmap f r = r { _failures = map (first $ fmap f) $ _failures r }++instance Foldable Result where+  foldMap f r = foldMap f [a | (Right a, _) <- _failures r]++-- | Run a predicate over all executions with two or fewer+-- pre-emptions.+runTest ::+    Predicate a+  -- ^ The predicate to check+  -> (forall t. Conc t a)+  -- ^ The computation to test+  -> Result a+runTest = runTest' 2++-- | Variant of 'runTest' which takes a pre-emption bound.+runTest' ::+    Int+  -- ^ The maximum number of pre-emptions to allow in a single+  -- execution+  -> Predicate a+  -- ^ The predicate to check+  -> (forall t. Conc t a)+  -- ^ The computation to test+  -> Result a+runTest' pb predicate conc = predicate $ sctPreBound pb conc++-- | Variant of 'runTest' for computations which do 'IO'.+runTestIO :: Predicate a -> (forall t. ConcIO t a) -> IO (Result a)+runTestIO = runTestIO' 2++-- | Variant of 'runTest'' for computations which do 'IO'.+runTestIO' :: Int -> Predicate a -> (forall t. ConcIO t a) -> IO (Result a)+runTestIO' pb predicate conc = predicate <$> sctPreBoundIO pb conc++-- * Predicates++-- | A @Predicate@ is a function which collapses a list of results+-- into a 'Result'.+type Predicate a = [(Either Failure a, Trace)] -> Result a++-- | Check that a computation never deadlocks.+deadlocksNever :: Predicate a+deadlocksNever = alwaysTrue (not . either (`elem` [Deadlock, STMDeadlock]) (const False))++-- | Check that a computation always deadlocks.+deadlocksAlways :: Predicate a+deadlocksAlways = alwaysTrue $ either (`elem` [Deadlock, STMDeadlock]) (const False)++-- | Check that a computation deadlocks at least once.+deadlocksSometimes :: Predicate a+deadlocksSometimes = somewhereTrue $ either (`elem` [Deadlock, STMDeadlock]) (const False)++-- | Check that a computation never fails with an uncaught exception.+exceptionsNever :: Predicate a+exceptionsNever = alwaysTrue (not . either (==UncaughtException) (const False))++-- | Check that a computation always fails with an uncaught exception.+exceptionsAlways :: Predicate a+exceptionsAlways = alwaysTrue $ either (==UncaughtException) (const False)++-- | Check that a computation fails with an uncaught exception at least once.+exceptionsSometimes :: Predicate a+exceptionsSometimes = somewhereTrue $ either (==UncaughtException) (const False)++-- | Check that the result of a computation is always the same. In+-- particular this means either: (a) it always fails in the same way,+-- or (b) it never fails and the values returned are all equal.+alwaysSame :: Eq a => Predicate a+alwaysSame = alwaysTrue2 (==)++-- | Check that the result of a computation is not always the same.+notAlwaysSame :: Eq a => Predicate a+notAlwaysSame [x] = Result { _pass = False, _casesChecked = 1, _failures = [x] }+notAlwaysSame xs = go xs Result { _pass = False, _casesChecked = 0, _failures = [] } where+  go [y1,y2] res+    | fst y1 /= fst y2 = incCC res { _pass = True }+    | otherwise = incCC res { _failures = y1 : y2 : _failures res }+  go (y1:y2:ys) res+    | fst y1 /= fst y2 = go (y2:ys) . incCC $ res { _pass = True }+    | otherwise = go (y2:ys) . incCC $ res { _failures = y1 : y2 : _failures res }+  go _ res = res++-- | Check that the result of a unary boolean predicate is always+-- true.+alwaysTrue :: (Either Failure a -> Bool) -> Predicate a+alwaysTrue p xs = go xs Result { _pass = True, _casesChecked = 0, _failures = filter (not . p . fst) xs } where+  go (y:ys) res+    | p (fst y) = go ys . incCC $ res+    | otherwise = incCC $ res { _pass = False }+  go [] res = res++-- | Check that the result of a binary boolean predicate is true+-- between all pairs of results. Only properties which are transitive+-- and symmetric should be used here.+--+-- If the predicate fails, /both/ (result,trace) tuples will be added+-- to the failures list.+alwaysTrue2 :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a+alwaysTrue2 _ [_] = Result { _pass = True, _casesChecked = 1, _failures = [] }+alwaysTrue2 p xs = go xs Result { _pass = True, _casesChecked = 0, _failures = failures xs } where+  go [y1,y2] res+    | p (fst y1) (fst y2) = incCC res+    | otherwise = incCC res { _pass = False }+  go (y1:y2:ys) res+    | p (fst y1) (fst y2) = go (y2:ys) . incCC $ res+    | otherwise = go (y2:ys) . incCC $ res { _pass = False }+  go _ res = res++  failures (y1:y2:ys)+    | p (fst y1) (fst y2) = failures (y2:ys)+    | otherwise = y1 : if null ys then [y2] else failures (y2:ys)+  failures _ = []++-- | Check that the result of a unary boolean predicate is true at+-- least once.+somewhereTrue :: (Either Failure a -> Bool) -> Predicate a+somewhereTrue p xs = go xs Result { _pass = False, _casesChecked = 0, _failures = filter (not . p . fst) xs } where+  go (y:ys) res+    | p (fst y) = incCC $ res { _pass = True }+    | otherwise = go ys . incCC $ res { _failures = y : _failures res }+  go [] res = res++-- * Internal++-- | Run a test and print to stdout+doTest :: (Eq a, Show a) => String -> Result a -> IO Bool+doTest name result = do+  if _pass result+  then+    -- Display a pass message.+    putStrLn $ "\27[32m[pass]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")"+  else do+    -- Display a failure message, and the first 5 (simplified) failed traces+    putStrLn ("\27[31m[fail]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")")++    let failures = _failures result+    mapM_ (\(r, t) -> putStrLn $ "\t" ++ either showfail show r ++ " " ++ showTrace t) $ take 5 failures+    when (moreThan failures 5) $+      putStrLn "\t..."++  return $ _pass result++-- | Increment the cases+incCC :: Result a -> Result a+incCC r = r { _casesChecked = _casesChecked r + 1 }++-- | Pretty-print a failure+showfail :: Failure -> String+showfail Deadlock          = "[deadlock]"+showfail STMDeadlock       = "[stm-deadlock]"+showfail InternalError     = "[internal-error]"+showfail FailureInNoTest   = "[_concNoTest]"+showfail UncaughtException = "[exception]"

@@ -0,0 +1,345 @@+{-# LANGUAGE CPP                        #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE RankNTypes                 #-}+{-# LANGUAGE TypeFamilies               #-}++-- | Deterministic traced execution of concurrent computations which+-- don't do @IO@.+--+-- This works by executing the computation on a single thread, calling+-- out to the supplied scheduler after each step to determine which+-- thread runs next.+module Test.DejaFu.Deterministic+  ( -- * The @Conc@ Monad+    Conc+  , Failure(..)+  , runConc+  , runConc'++  -- * Concurrency+  , fork+  , forkFinally+  , forkWithUnmask+  , forkOn+  , getNumCapabilities+  , myThreadId+  , spawn+  , atomically+  , throw+  , throwTo+  , killThread+  , Test.DejaFu.Deterministic.catch+  , mask+  , uninterruptibleMask++  -- * @CVar@s+  , CVar+  , newEmptyCVar+  , putCVar+  , tryPutCVar+  , readCVar+  , takeCVar+  , tryTakeCVar++  -- * @CRef@s+  , CRef+  , newCRef+  , readCRef+  , writeCRef+  , modifyCRef++  -- * Testing+  , _concNoTest+  , _concKnowsAbout+  , _concForgets+  , _concAllKnown++  -- * Execution traces+  , Trace+  , Trace'+  , Decision(..)+  , ThreadAction(..)+  , Lookahead(..)+  , CVarId+  , CRefId+  , MaskingState(..)+  , showTrace+  , toTrace++  -- * Scheduling+  , module Test.DejaFu.Deterministic.Schedule+  ) where++import Control.Exception (Exception, MaskingState(..), SomeException(..))+import Control.Monad.Cont (cont, runCont)+import Control.Monad.ST (ST, runST)+import Data.STRef (STRef, newSTRef)+import Test.DejaFu.Deterministic.Internal+import Test.DejaFu.Deterministic.Schedule+import Test.DejaFu.Internal (refST)+import Test.DejaFu.STM (STMLike, runTransactionST)+import Test.DejaFu.STM.Internal (CTVar(..))++import qualified Control.Monad.Catch as Ca+import qualified Control.Monad.Conc.Class as C++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative (Applicative(..), (<$>))+#endif++{-# ANN module ("HLint: ignore Avoid lambda" :: String) #-}++-- | The @Conc@ monad itself. This uses the same+-- universally-quantified indexing state trick as used by 'ST' and+-- 'STRef's to prevent mutable references from leaking out of the+-- monad.+newtype Conc t a = C { unC :: M (ST t) (STRef t) (STMLike t) a } deriving (Functor, Applicative, Monad)++wrap :: (M (ST t) (STRef t) (STMLike t) a -> M (ST t) (STRef t) (STMLike t) a) -> Conc t a -> Conc t a+wrap f = C . f . unC++instance Ca.MonadCatch (Conc t) where+  catch = Test.DejaFu.Deterministic.catch++instance Ca.MonadThrow (Conc t) where+  throwM = throw++instance Ca.MonadMask (Conc t) where+  mask = mask+  uninterruptibleMask = uninterruptibleMask++instance C.MonadConc (Conc t) where+  type CVar     (Conc t) = CVar t+  type CRef     (Conc t) = CRef t+  type STMLike  (Conc t) = STMLike t (ST t) (STRef t)+  type ThreadId (Conc t) = Int++  fork           = fork+  forkWithUnmask = forkWithUnmask+  forkOn         = forkOn+  getNumCapabilities = getNumCapabilities+  myThreadId     = myThreadId+  throwTo        = throwTo+  newEmptyCVar   = newEmptyCVar+  putCVar        = putCVar+  tryPutCVar     = tryPutCVar+  readCVar       = readCVar+  takeCVar       = takeCVar+  tryTakeCVar    = tryTakeCVar+  newCRef        = newCRef+  readCRef       = readCRef+  writeCRef      = writeCRef+  modifyCRef     = modifyCRef+  atomically     = atomically+  _concNoTest    = _concNoTest+  _concKnowsAbout = _concKnowsAbout+  _concForgets   = _concForgets+  _concAllKnown  = _concAllKnown++fixed :: Fixed (ST t) (STRef t) (STMLike t)+fixed = refST $ \ma -> cont (\c -> ALift $ c <$> ma)++-- | The concurrent variable type used with the 'Conc' monad. One+-- notable difference between these and 'MVar's is that 'MVar's are+-- single-wakeup, and wake up in a FIFO order. Writing to a @CVar@+-- wakes up all threads blocked on reading it, and it is up to the+-- scheduler which one runs next. Taking from a @CVar@ behaves+-- analogously.+newtype CVar t a = Var { unV :: V (STRef t) a } deriving Eq++-- | The mutable non-blocking reference type. These are like 'IORef's,+-- but don't have the potential re-ordering problem mentioned in+-- Data.IORef.+newtype CRef t a = Ref { unR :: R (STRef t) a } deriving Eq++-- | Run the provided computation concurrently, returning the result.+spawn :: Conc t a -> Conc t (CVar t a)+spawn = C.spawn++-- | Block on a 'CVar' until it is full, then read from it (without+-- emptying).+readCVar :: CVar t a -> Conc t a+readCVar cvar = C $ cont $ AGet $ unV cvar++-- | Run the provided computation concurrently.+fork :: Conc t () -> Conc t ThreadId+fork (C ma) = C $ cont $ AFork (const' $ runCont ma $ const AStop)++-- | Get the 'ThreadId' of the current thread.+myThreadId :: Conc t ThreadId+myThreadId = C $ cont AMyTId++-- | Run the provided 'MonadSTM' transaction atomically. If 'retry' is+-- called, it will be blocked until any of the touched 'CTVar's have+-- been written to.+atomically :: STMLike t (ST t) (STRef t) a -> Conc t a+atomically stm = C $ cont $ AAtom stm++-- | Create a new empty 'CVar'.+newEmptyCVar :: Conc t (CVar t a)+newEmptyCVar = C $ cont lifted where+  lifted c = ANew $ \cvid -> c <$> newEmptyCVar' cvid+  newEmptyCVar' cvid = (\ref -> Var (cvid, ref)) <$> newSTRef Nothing++-- | Block on a 'CVar' until it is empty, then write to it.+putCVar :: CVar t a -> a -> Conc t ()+putCVar cvar a = C $ cont $ \c -> APut (unV cvar) a $ c ()++-- | Put a value into a 'CVar' if there isn't one, without blocking.+tryPutCVar :: CVar t a -> a -> Conc t Bool+tryPutCVar cvar a = C $ cont $ ATryPut (unV cvar) a++-- | Block on a 'CVar' until it is full, then read from it (with+-- emptying).+takeCVar :: CVar t a -> Conc t a+takeCVar cvar = C $ cont $ ATake $ unV cvar++-- | Read a value from a 'CVar' if there is one, without blocking.+tryTakeCVar :: CVar t a -> Conc t (Maybe a)+tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar++-- | Create a new 'CRef'.+newCRef :: a -> Conc t (CRef t a)+newCRef a = C $ cont lifted where+  lifted c = ANewRef $ \crid -> c <$> newCRef' crid+  newCRef' crid = (\ref -> Ref (crid, ref)) <$> newSTRef a++-- | Read the value from a 'CRef'.+readCRef :: CRef t a -> Conc t a+readCRef ref = C $ cont $ AReadRef $ unR ref++-- | Atomically modify the value inside a 'CRef'.+modifyCRef :: CRef t a -> (a -> (a, b)) -> Conc t b+modifyCRef ref f = C $ cont $ AModRef (unR ref) f++-- | Replace the value stored inside a 'CRef'.+writeCRef :: CRef t a -> a -> Conc t ()+writeCRef ref a = modifyCRef ref $ const (a, ())++-- | Raise an exception in the 'Conc' monad. The exception is raised+-- when the action is run, not when it is applied. It short-citcuits+-- the rest of the computation:+--+-- > throw e >> x == throw e+throw :: Exception e => e -> Conc t a+throw e = C $ cont $ \_ -> AThrow (SomeException e)++-- | Throw an exception to the target thread. This blocks until the+-- exception is delivered, and it is just as if the target thread had+-- raised it with 'throw'. This can interrupt a blocked action.+throwTo :: Exception e => ThreadId -> e -> Conc t ()+throwTo tid e = C $ cont $ \c -> AThrowTo tid (SomeException e) $ c ()++-- | Raise the 'ThreadKilled' exception in the target thread. Note+-- that if the thread is prepared to catch this exception, it won't+-- actually kill it.+killThread :: ThreadId -> Conc t ()+killThread = C.killThread++-- | Catch an exception raised by 'throw'. This __cannot__ catch+-- errors, such as evaluating 'undefined', or division by zero. If you+-- need that, use Control.Exception.catch and 'ConcIO'.+catch :: Exception e => Conc t a -> (e -> Conc t a) -> Conc t a+catch ma h = C $ cont $ ACatching (unC . h) (unC ma)++-- | Fork a thread and call the supplied function when the thread is+-- about to terminate, with an exception or a returned value. The+-- function is called with asynchronous exceptions masked.+--+-- This function is useful for informing the parent when a child+-- terminates, for example.+forkFinally :: Conc t a -> (Either SomeException a -> Conc t ()) -> Conc t ThreadId+forkFinally action and_then = mask $ \restore ->+  fork $ Ca.try (restore action) >>= and_then++-- | Like 'fork', but the child thread is passed a function that can+-- be used to unmask asynchronous exceptions. This function should not+-- be used within a 'mask' or 'uninterruptibleMask'.+forkWithUnmask :: ((forall a. Conc t a -> Conc t a) -> Conc t ()) -> Conc t ThreadId+forkWithUnmask ma = C $ cont $+  AFork (\umask -> runCont (unC $ ma $ wrap umask) $ const AStop)++-- | Executes a computation with asynchronous exceptions+-- /masked/. That is, any thread which attempts to raise an exception+-- in the current thread with 'throwTo' will be blocked until+-- asynchronous exceptions are unmasked again.+--+-- The argument passed to mask is a function that takes as its+-- argument another function, which can be used to restore the+-- prevailing masking state within the context of the masked+-- computation. This function should not be used within an+-- 'uninterruptibleMask'.+mask :: ((forall a. Conc t a -> Conc t a) -> Conc t b) -> Conc t b+-- Can't avoid the lambda here (and in uninterruptibleMask and in+-- ConcIO) because higher-ranked type inference is scary.+mask mb = C $ cont $ AMasking MaskedInterruptible (\f -> unC $ mb $ wrap f)++-- | Like 'mask', but the masked computation is not+-- interruptible. THIS SHOULD BE USED WITH GREAT CARE, because if a+-- thread executing in 'uninterruptibleMask' blocks for any reason,+-- then the thread (and possibly the program, if this is the main+-- thread) will be unresponsive and unkillable. This function should+-- only be necessary if you need to mask exceptions around an+-- interruptible operation, and you can guarantee that the+-- interruptible operation will only block for a short period of+-- time. The supplied unmasking function should not be used within a+-- 'mask'.+uninterruptibleMask :: ((forall a. Conc t a -> Conc t a) -> Conc t b) -> Conc t b+uninterruptibleMask mb = C $ cont $+  AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f)++-- | Fork a computation to happen on a specific processor. This+-- implementation only has a single processor.+forkOn :: Int -> Conc t () -> Conc t ThreadId+forkOn _ = fork++-- | Get the number of Haskell threads that can run+-- simultaneously. This implementation lies and always returns+-- 2. There is no way to verify in the computation that this is a lie,+-- and will potentially avoid special-case behaviour for 1 capability,+-- so it seems a sane choice.+getNumCapabilities :: Conc t Int+getNumCapabilities = return 2++-- | Run the argument in one step. If the argument fails, the whole+-- computation will fail.+_concNoTest :: Conc t a -> Conc t a+_concNoTest ma = C $ cont $ \c -> ANoTest (unC ma) c++-- | Record that the referenced variable is known by the current thread.+_concKnowsAbout :: Either (CVar t a) (CTVar t (STRef t) a) -> Conc t ()+_concKnowsAbout (Left  (Var (cvarid,  _))) = C $ cont $ \c -> AKnowsAbout (Left  cvarid)  (c ())+_concKnowsAbout (Right (V   (ctvarid, _))) = C $ cont $ \c -> AKnowsAbout (Right ctvarid) (c ())++-- | Record that the referenced variable will never be touched by the+-- current thread.+_concForgets :: Either (CVar t a) (CTVar t (STRef t) a) -> Conc t ()+_concForgets (Left  (Var (cvarid,  _))) = C $ cont $ \c -> AForgets (Left  cvarid)  (c ())+_concForgets (Right (V   (ctvarid, _))) = C $ cont $ \c -> AForgets (Right ctvarid) (c ())++-- | Record that all 'CVar's and 'CTVar's known by the current thread+-- have been passed to '_concKnowsAbout'.+_concAllKnown :: Conc t ()+_concAllKnown = C $ cont $ \c -> AAllKnown (c ())++-- | 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.+--+-- Note how the @t@ in 'Conc' is universally quantified, what this+-- means in practice is that you can't do something like this:+--+-- > runConc roundRobinSched () newEmptyCVar+--+-- So mutable references cannot leak out of the 'Conc' computation. If+-- this is making your head hurt, check out the \"How @runST@ works\"+-- section of+-- <https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html>+runConc :: Scheduler s -> s -> (forall t. Conc t a) -> (Either Failure a, s, Trace)+runConc sched s ma =+  let (r, s', t') = runConc' sched s ma+  in  (r, s', toTrace t')++-- | Variant of 'runConc' which produces a 'Trace''.+runConc' :: Scheduler s -> s -> (forall t. Conc t a) -> (Either Failure a, s, Trace')+runConc' sched s ma = runST $ runFixed fixed runTransactionST sched s $ unC ma

@@ -0,0 +1,337 @@+{-# LANGUAGE CPP                        #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE RankNTypes                 #-}+{-# LANGUAGE TypeFamilies               #-}++-- | Deterministic traced execution of concurrent computations which+-- may do @IO@.+--+-- __Warning:__ Blocking on the action of another thread in 'liftIO'+-- cannot be detected! So if you perform some potentially blocking+-- action in a 'liftIO' the entire collection of threads may deadlock!+-- You should therefore keep @IO@ blocks small, and only perform+-- blocking operations with the supplied primitives, insofar as+-- possible.+module Test.DejaFu.Deterministic.IO+  ( -- * The @ConcIO@ Monad+    ConcIO+  , Failure(..)+  , runConcIO+  , runConcIO'+  , liftIO++  -- * Concurrency+  , fork+  , forkFinally+  , forkWithUnmask+  , forkOn+  , getNumCapabilities+  , myThreadId+  , spawn+  , atomically+  , throw+  , throwTo+  , killThread+  , Test.DejaFu.Deterministic.IO.catch+  , mask+  , uninterruptibleMask++  -- * @CVar@s+  , CVar+  , newEmptyCVar+  , putCVar+  , tryPutCVar+  , readCVar+  , takeCVar+  , tryTakeCVar++  -- * @CRef@s+  , CRef+  , newCRef+  , readCRef+  , writeCRef+  , modifyCRef++  -- * Testing+  , _concNoTest+  , _concKnowsAbout+  , _concForgets+  , _concAllKnown++  -- * Execution traces+  , Trace+  , Trace'+  , Decision(..)+  , ThreadAction(..)+  , Lookahead(..)+  , CVarId+  , MaskingState(..)+  , showTrace+  , toTrace++  -- * Scheduling+  , module Test.DejaFu.Deterministic.Schedule+  ) where++import Control.Exception (Exception, MaskingState(..), SomeException(..))+import Control.Monad.Cont (cont, runCont)+import Data.IORef (IORef, newIORef)+import Test.DejaFu.Deterministic.Internal+import Test.DejaFu.Deterministic.Schedule+import Test.DejaFu.Internal (refIO)+import Test.DejaFu.STM (STMLike, runTransactionIO)+import Test.DejaFu.STM.Internal (CTVar(..))++import qualified Control.Monad.Catch as Ca+import qualified Control.Monad.Conc.Class as C+import qualified Control.Monad.IO.Class as IO++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative (Applicative(..), (<$>))+#endif++{-# ANN module ("HLint: ignore Avoid lambda" :: String) #-}++-- | The 'IO' variant of Test.DejaFu.Deterministic's+-- 'Test.DejaFu.Deterministic.Conc' monad.+newtype ConcIO t a = C { unC :: M IO IORef (STMLike t) a } deriving (Functor, Applicative, Monad)++wrap :: (M IO IORef (STMLike t) a -> M IO IORef (STMLike t) a) -> ConcIO t a -> ConcIO t a+wrap f = C . f . unC++instance Ca.MonadCatch (ConcIO t) where+  catch = Test.DejaFu.Deterministic.IO.catch++instance Ca.MonadThrow (ConcIO t) where+  throwM = throw++instance Ca.MonadMask (ConcIO t) where+  mask = mask+  uninterruptibleMask = uninterruptibleMask++instance IO.MonadIO (ConcIO t) where+  liftIO = liftIO++instance C.MonadConc (ConcIO t) where+  type CVar     (ConcIO t) = CVar t+  type CRef     (ConcIO t) = CRef t+  type STMLike  (ConcIO t) = STMLike t IO IORef+  type ThreadId (ConcIO t) = Int++  fork           = fork+  forkWithUnmask = forkWithUnmask+  forkOn         = forkOn+  getNumCapabilities = getNumCapabilities+  myThreadId     = myThreadId+  throwTo        = throwTo+  newEmptyCVar   = newEmptyCVar+  putCVar        = putCVar+  tryPutCVar     = tryPutCVar+  readCVar       = readCVar+  takeCVar       = takeCVar+  tryTakeCVar    = tryTakeCVar+  newCRef        = newCRef+  readCRef       = readCRef+  writeCRef      = writeCRef+  modifyCRef     = modifyCRef+  atomically     = atomically+  _concNoTest    = _concNoTest+  _concKnowsAbout = _concKnowsAbout+  _concForgets   = _concForgets+  _concAllKnown  = _concAllKnown++fixed :: Fixed IO IORef (STMLike t)+fixed = refIO $ unC . liftIO++-- | The concurrent variable type used with the 'ConcIO' monad. These+-- behave the same as @Conc@'s @CVar@s+newtype CVar t a = Var { unV :: V IORef a } deriving Eq++-- | The mutable non-blocking reference type. These behave the same as+-- @Conc@'s @CRef@s+newtype CRef t a = Ref { unR :: R IORef a } deriving Eq++-- | Lift an 'IO' action into the 'ConcIO' monad.+liftIO :: IO a -> ConcIO t a+liftIO ma = C $ cont lifted where+  lifted c = ALift $ c <$> ma++-- | Run the provided computation concurrently, returning the result.+spawn :: ConcIO t a -> ConcIO t (CVar t a)+spawn = C.spawn++-- | Block on a 'CVar' until it is full, then read from it (without+-- emptying).+readCVar :: CVar t a -> ConcIO t a+readCVar cvar = C $ cont $ AGet $ unV cvar++-- | Run the provided computation concurrently.+fork :: ConcIO t () -> ConcIO t ThreadId+fork (C ma) = C $ cont $ AFork (const' $ runCont ma $ const AStop)++-- | Get the 'ThreadId' of the current thread.+myThreadId :: ConcIO t ThreadId+myThreadId = C $ cont AMyTId++-- | Run the provided 'MonadSTM' transaction atomically. If 'retry' is+-- called, it will be blocked until any of the touched 'CTVar's have+-- been written to.+atomically :: STMLike t IO IORef a -> ConcIO t a+atomically stm = C $ cont $ AAtom stm++-- | Create a new empty 'CVar'.+newEmptyCVar :: ConcIO t (CVar t a)+newEmptyCVar = C $ cont lifted where+  lifted c = ANew $ \cvid -> c <$> newEmptyCVar' cvid+  newEmptyCVar' cvid = (\ref -> Var (cvid, ref)) <$> newIORef Nothing++-- | Block on a 'CVar' until it is empty, then write to it.+putCVar :: CVar t a -> a -> ConcIO t ()+putCVar cvar a = C $ cont $ \c -> APut (unV cvar) a $ c ()++-- | Put a value into a 'CVar' if there isn't one, without blocking.+tryPutCVar :: CVar t a -> a -> ConcIO t Bool+tryPutCVar cvar a = C $ cont $ ATryPut (unV cvar) a++-- | Block on a 'CVar' until it is full, then read from it (with+-- emptying).+takeCVar :: CVar t a -> ConcIO t a+takeCVar cvar = C $ cont $ ATake $ unV cvar++-- | Read a value from a 'CVar' if there is one, without blocking.+tryTakeCVar :: CVar t a -> ConcIO t (Maybe a)+tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar++-- | Create a new 'CRef'.+newCRef :: a -> ConcIO t (CRef t a)+newCRef a = C $ cont lifted where+  lifted c = ANewRef $ \crid -> c <$> newCRef' crid+  newCRef' crid = (\ref -> Ref (crid, ref)) <$> newIORef a++-- | Read the value from a 'CRef'.+readCRef :: CRef t a -> ConcIO t a+readCRef ref = C $ cont $ AReadRef $ unR ref++-- | Atomically modify the value inside a 'CRef'.+modifyCRef :: CRef t a -> (a -> (a, b)) -> ConcIO t b+modifyCRef ref f = C $ cont $ AModRef (unR ref) f++-- | Replace the value stored inside a 'CRef'.+writeCRef :: CRef t a -> a -> ConcIO t ()+writeCRef ref a = modifyCRef ref $ const (a, ())++-- | Raise an exception in the 'ConcIO' monad. The exception is raised+-- when the action is run, not when it is applied. It short-citcuits+-- the rest of the computation:+--+-- > throw e >> x == throw e+throw :: Exception e => e -> ConcIO t a+throw e = C $ cont $ \_ -> AThrow (SomeException e)++-- | Throw an exception to the target thread. This blocks until the+-- exception is delivered, and it is just as if the target thread had+-- raised it with 'throw'. This can interrupt a blocked action.+throwTo :: Exception e => ThreadId -> e -> ConcIO t ()+throwTo tid e = C $ cont $ \c -> AThrowTo tid (SomeException e) $ c ()++-- | Raise the 'ThreadKilled' exception in the target thread. Note+-- that if the thread is prepared to catch this exception, it won't+-- actually kill it.+killThread :: ThreadId -> ConcIO t ()+killThread = C.killThread++-- | Catch an exception raised by 'throw'. This __cannot__ catch+-- errors, such as evaluating 'undefined', or division by zero. If you+-- need that, use Control.Exception.catch and 'liftIO'.+catch :: Exception e => ConcIO t a -> (e -> ConcIO t a) -> ConcIO t a+catch ma h = C $ cont $ ACatching (unC . h) (unC ma)++-- | Fork a thread and call the supplied function when the thread is+-- about to terminate, with an exception or a returned value. The+-- function is called with asynchronous exceptions masked.+--+-- This function is useful for informing the parent when a child+-- terminates, for example.+forkFinally :: ConcIO t a -> (Either SomeException a -> ConcIO t ()) -> ConcIO t ThreadId+forkFinally action and_then = mask $ \restore ->+  fork $ Ca.try (restore action) >>= and_then++-- | Like 'fork', but the child thread is passed a function that can+-- be used to unmask asynchronous exceptions. This function should not+-- be used within a 'mask' or 'uninterruptibleMask'.+forkWithUnmask :: ((forall a. ConcIO t a -> ConcIO t a) -> ConcIO t ()) -> ConcIO t ThreadId+forkWithUnmask ma = C $ cont $+  AFork (\umask -> runCont (unC $ ma $ wrap umask) $ const AStop)++-- | Executes a computation with asynchronous exceptions+-- /masked/. That is, any thread which attempts to raise an exception+-- in the current thread with 'throwTo' will be blocked until+-- asynchronous exceptions are unmasked again.+--+-- The argument passed to mask is a function that takes as its+-- argument another function, which can be used to restore the+-- prevailing masking state within the context of the masked+-- computation. This function should not be used within an+-- 'uninterruptibleMask'.+mask :: ((forall a. ConcIO t a -> ConcIO t a) -> ConcIO t b) -> ConcIO t b+mask mb = C $ cont $ AMasking MaskedInterruptible (\f -> unC $ mb $ wrap f)++-- | Like 'mask', but the masked computation is not+-- interruptible. THIS SHOULD BE USED WITH GREAT CARE, because if a+-- thread executing in 'uninterruptibleMask' blocks for any reason,+-- then the thread (and possibly the program, if this is the main+-- thread) will be unresponsive and unkillable. This function should+-- only be necessary if you need to mask exceptions around an+-- interruptible operation, and you can guarantee that the+-- interruptible operation will only block for a short period of+-- time. The supplied unmasking function should not be used within a+-- 'mask'.+uninterruptibleMask :: ((forall a. ConcIO t a -> ConcIO t a) -> ConcIO t b) -> ConcIO t b+uninterruptibleMask mb = C $ cont $+  AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f)++-- | Fork a computation to happen on a specific processor. This+-- implementation only has a single processor.+forkOn :: Int -> ConcIO t () -> ConcIO t ThreadId+forkOn _ = fork++-- | Get the number of Haskell threads that can run+-- simultaneously. This implementation lies and always returns+-- 2. There is no way to verify in the computation that this is a lie,+-- and will potentially avoid special-case behaviour for 1 capability,+-- so it seems a sane choice.+getNumCapabilities :: ConcIO t Int+getNumCapabilities = return 2++-- | Run the argument in one step. If the argument fails, the whole+-- computation will fail.+_concNoTest :: ConcIO t a -> ConcIO t a+_concNoTest ma = C $ cont $ \c -> ANoTest (unC ma) c++-- | Record that the referenced variable is known by the current thread.+_concKnowsAbout :: Either (CVar t a) (CTVar t IORef a) -> ConcIO t ()+_concKnowsAbout (Left  (Var (cvarid,  _))) = C $ cont $ \c -> AKnowsAbout (Left  cvarid)  (c ())+_concKnowsAbout (Right (V   (ctvarid, _))) = C $ cont $ \c -> AKnowsAbout (Right ctvarid) (c ())++-- | Record that the referenced variable will never be touched by the+-- current thread.+_concForgets :: Either (CVar t a) (CTVar t IORef a) -> ConcIO t ()+_concForgets (Left  (Var (cvarid,  _))) = C $ cont $ \c -> AForgets (Left  cvarid)  (c ())+_concForgets (Right (V   (ctvarid, _))) = C $ cont $ \c -> AForgets (Right ctvarid) (c ())++-- | Record that all 'CVar's and 'CTVar's known by the current thread+-- have been passed to '_concKnowsAbout'.+_concAllKnown :: ConcIO t ()+_concAllKnown = C $ cont $ \c -> AAllKnown (c ())++-- | Run a concurrent computation with a given 'Scheduler' and initial+-- state, returning an failure reason on error. Also returned is the+-- final state of the scheduler, and an execution trace.+runConcIO :: Scheduler s -> s -> (forall t. ConcIO t a) -> IO (Either Failure a, s, Trace)+runConcIO sched s ma = do+  (r, s', t') <- runConcIO' sched s ma+  return (r, s', toTrace t')++-- | Variant of 'runConcIO' which produces a 'Trace''.+runConcIO' :: Scheduler s -> s -> (forall t. ConcIO t a) -> IO (Either Failure a, s, Trace')+runConcIO' sched s ma = runFixed fixed runTransactionIO sched s $ unC ma

@@ -0,0 +1,390 @@+{-# LANGUAGE CPP                 #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}++#if __GLASGOW_HASKELL__ < 710+-- ImpredicativeTypes are needed for the const' function, as the+-- type-checker can't otherwise unify the higher-ranked application.++{-# LANGUAGE ImpredicativeTypes #-}+#endif++-- | Concurrent monads with a fixed scheduler: internal types and+-- functions.+module Test.DejaFu.Deterministic.Internal+ ( -- * Execution+   runFixed+ , runFixed'++ -- * The @Conc@ Monad+ , M+ , V+ , R+ , Fixed++ -- * Primitive Actions+ , Action(..)++ -- * Identifiers+ , ThreadId+ , CVarId+ , CRefId++ -- * Scheduling & Traces+ , Scheduler+ , Trace+ , Decision(..)+ , ThreadAction(..)+ , Lookahead(..)+ , Trace'+ , showTrace+ , toTrace++ -- * Failures+ , Failure(..)++ -- * Utils+ , const'+ ) where++import Control.Exception (MaskingState(..))+import Control.Monad.Cont (cont, runCont)+import Data.List (sort)+import Data.List.Extra+import Data.Maybe (fromJust, isJust, isNothing, listToMaybe)+import Test.DejaFu.STM (CTVarId, Result(..))+import Test.DejaFu.Internal+import Test.DejaFu.Deterministic.Internal.Common+import Test.DejaFu.Deterministic.Internal.CVar+import Test.DejaFu.Deterministic.Internal.Threading++import qualified Data.Map as M++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative ((<$>), (<*>))+#endif++{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}++const' :: a -> (forall b. M n r s b -> M n r s b) -> a+const' = const++--------------------------------------------------------------------------------+-- * Execution++-- | Run a concurrent computation with a given 'Scheduler' and initial+-- state, returning a 'Just' if it terminates, and 'Nothing' if a+-- deadlock is detected. Also returned is the final state of the+-- scheduler, and an execution trace.+runFixed :: (Functor n, Monad n) => Fixed n r s -> (forall x. s n r x -> CTVarId -> n (Result x, CTVarId))+         -> Scheduler g -> g -> M n r s a -> n (Either Failure a, g, Trace')+runFixed fixed runstm sched s ma = (\(e,g,_,t) -> (e,g,t)) <$> runFixed' fixed runstm sched s initialIdSource ma++-- | Same as 'runFixed', be parametrised by an 'IdSource'.+runFixed' :: forall n r s g a. (Functor n, Monad n)+  => Fixed n r s -> (forall x. s n r x -> CTVarId -> n (Result x, CTVarId))+  -> Scheduler g -> g -> IdSource -> M n r s a -> n (Either Failure a, g, IdSource, Trace')+runFixed' fixed runstm sched s idSource ma = do+  ref <- newRef fixed Nothing++  let c       = ma >>= liftN fixed . writeRef fixed ref . Just . Right+  let threads = launch' Unmasked 0 (const' $ runCont c $ const AStop) M.empty++  (s', idSource', trace) <- runThreads fixed runstm sched s threads idSource ref+  out <- readRef fixed ref++  return (fromJust out, s', idSource', reverse trace)++-- | Run a collection of threads, until there are no threads left.+--+-- Note: this returns the trace in reverse order, because it's more+-- efficient to prepend to a list than append. As this function isn't+-- exposed to users of the library, this is just an internal gotcha to+-- watch out for.+runThreads :: (Functor n, Monad n) => Fixed n r s -> (forall x. s n r x -> CTVarId -> n (Result x, CTVarId))+           -> Scheduler g -> g -> Threads n r s -> IdSource -> r (Maybe (Either Failure a)) -> n (g, IdSource, Trace')+runThreads fixed runstm sched origg origthreads idsrc ref = go idsrc [] Nothing origg origthreads where+  go idSource sofar prior g threads+    | isTerminated  = return (g, idSource, sofar)+    | isDeadlocked  = writeRef fixed ref (Just $ Left Deadlock) >> return (g, idSource, sofar)+    | isSTMLocked   = writeRef fixed ref (Just $ Left STMDeadlock) >> return (g, idSource, sofar)+    | isNonexistant = writeRef fixed ref (Just $ Left InternalError) >> return (g, idSource, sofar)+    | isBlocked     = writeRef fixed ref (Just $ Left InternalError) >> return (g, idSource, sofar)+    | otherwise = do+      stepped <- stepThread fixed runconc runstm (_continuation $ fromJust thread) idSource chosen threads+      case stepped of+        Right (threads', idSource', act) ->+          let sofar' = (decision, alternatives, act) : sofar+              threads'' = if (interruptible <$> M.lookup chosen threads') == Just True then unblockWaitingOn chosen threads' else threads'+          in  go idSource' sofar' (Just chosen) g' threads''++        Left UncaughtException+          | chosen == 0 -> writeRef fixed ref (Just $ Left UncaughtException) >> return (g, idSource, sofar)+          | otherwise ->+          let sofar' = (decision, alternatives, Killed) : sofar+              threads' = unblockWaitingOn chosen $ kill chosen threads+          in go idSource sofar' (Just chosen) g' threads'++        Left failure -> writeRef fixed ref (Just $ Left failure) >> return (g, idSource, sofar)++    where+      (chosen, g')  = sched g ((\p (_,_,a) -> (p,a)) <$> prior <*> listToMaybe sofar) $ unsafeToNonEmpty runnable'+      runnable'     = [(t, nextActions t) | t <- sort $ M.keys runnable]+      runnable      = M.filter (isNothing . _blocking) threads+      thread        = M.lookup chosen threads+      isBlocked     = isJust . _blocking $ fromJust thread+      isNonexistant = isNothing thread+      isTerminated  = 0 `notElem` M.keys threads+      isDeadlocked  = isLocked 0 threads && (((~= OnCVarFull  undefined) <$> M.lookup 0 threads) == Just True ||+                                           ((~=  OnCVarEmpty undefined) <$> M.lookup 0 threads) == Just True ||+                                           ((~=  OnMask      undefined) <$> M.lookup 0 threads) == Just True)+      isSTMLocked   = isLocked 0 threads && ((~=  OnCTVar    []) <$> M.lookup 0 threads) == Just True++      runconc ma i = do { (a,_,i',_) <- runFixed' fixed runstm sched g i ma; return (a,i') }++      unblockWaitingOn tid = M.map unblock where+        unblock thrd = case _blocking thrd of+          Just (OnMask t) | t == tid -> thrd { _blocking = Nothing }+          _ -> thrd++      decision+        | Just chosen == prior = Continue+        | prior `notElem` map (Just . fst) runnable' = Start chosen+        | otherwise = SwitchTo chosen++      alternatives+        | Just chosen == prior = [(SwitchTo t, na) | (t, na) <- runnable', Just t /= prior]+        | prior `notElem` map (Just . fst) runnable' = [(Start t, na) | (t, na) <- runnable', t /= chosen]+        | otherwise = [(if Just t == prior then Continue else SwitchTo t, na) | (t, na) <- runnable', t /= chosen]++      nextActions t = unsafeToNonEmpty . nextActions' . _continuation . fromJust $ M.lookup t threads+      nextActions' (AFork _ _)             = [WillFork]+      nextActions' (AMyTId _)              = [WillMyThreadId]+      nextActions' (ANew _)                = [WillNew]+      nextActions' (APut (c, _) _ k)       = WillPut c : nextActions' k+      nextActions' (ATryPut (c, _) _ _)    = [WillTryPut c]+      nextActions' (AGet (c, _) _)         = [WillRead c]+      nextActions' (ATake (c, _) _)        = [WillTake c]+      nextActions' (ATryTake (c, _) _)     = [WillTryTake c]+      nextActions' (ANewRef _)             = [WillNewRef]+      nextActions' (AReadRef (r, _) _)     = [WillReadRef r]+      nextActions' (AModRef (r, _) _ _)    = [WillModRef r]+      nextActions' (AAtom _ _)             = [WillSTM]+      nextActions' (AThrow _)              = [WillThrow]+      nextActions' (AThrowTo tid _ k)      = WillThrowTo tid : nextActions' k+      nextActions' (ACatching _ _ _)       = [WillCatching]+      nextActions' (APopCatching k)        = WillPopCatching : nextActions' k+      nextActions' (AMasking ms _ _)       = [WillSetMasking False ms]+      nextActions' (AResetMask b1 b2 ms k) = (if b1 then WillSetMasking else WillResetMasking) b2 ms : nextActions' k+      nextActions' (ALift _)               = [WillLift]+      nextActions' (ANoTest _ _)           = [WillNoTest]+      nextActions' (AKnowsAbout _ k)       = WillKnowsAbout : nextActions' k+      nextActions' (AForgets _ k)          = WillForgets : nextActions' k+      nextActions' (AAllKnown k)           = WillAllKnown : nextActions' k+      nextActions' (AStop)                 = [WillStop]++--------------------------------------------------------------------------------+-- * Single-step execution++-- | Run a single thread one step, by dispatching on the type of+-- 'Action'.+stepThread :: forall n r s. (Functor n, Monad n) => Fixed n r s+           -> (forall x. M n r s x -> IdSource -> n (Either Failure x, IdSource))+           -- ^ Run a 'MonadConc' computation atomically.+           -> (forall x. s n r x -> CTVarId -> n (Result x, CTVarId))+           -- ^ Run a 'MonadSTM' transaction atomically.+           -> Action n r s+           -- ^ Action to step+           -> IdSource+           -- ^ Source of fresh IDs+           -> ThreadId+           -- ^ ID of the current thread+           -> Threads n r s+           -- ^ Current state of threads+           -> n (Either Failure (Threads n r s, IdSource, ThreadAction))+stepThread fixed runconc runstm action idSource tid threads = case action of+  AFork    a b     -> stepFork        a b+  AMyTId   c       -> stepMyTId       c+  APut     ref a c -> stepPut         ref a c+  ATryPut  ref a c -> stepTryPut      ref a c+  AGet     ref c   -> stepGet         ref c+  ATake    ref c   -> stepTake        ref c+  ATryTake ref c   -> stepTryTake     ref c+  AReadRef ref c   -> stepReadRef     ref c+  AModRef  ref f c -> stepModRef      ref f c+  AAtom    stm c   -> stepAtom        stm c+  ANew     na      -> stepNew         na+  ANewRef  na      -> stepNewRef      na+  ALift    na      -> stepLift        na+  AThrow   e       -> stepThrow       e+  AThrowTo t e c   -> stepThrowTo     t e c+  ACatching h ma c -> stepCatching    h ma c+  APopCatching a   -> stepPopCatching a+  AMasking m ma c  -> stepMasking     m ma c+  AResetMask b1 b2 m c -> stepResetMask b1 b2 m c+  ANoTest  ma a    -> stepNoTest      ma a+  AKnowsAbout v c  -> stepKnowsAbout  v c+  AForgets    v c  -> stepForgets v c+  AAllKnown   c    -> stepAllKnown c+  AStop            -> stepStop++  where+    -- | Start a new thread, assigning it the next 'ThreadId'+    stepFork a b = return $ Right (goto (b newtid) tid threads', idSource', Fork newtid) where+      threads' = launch tid newtid a threads+      (idSource', newtid) = nextTId idSource++    -- | Get the 'ThreadId' of the current thread+    stepMyTId c = return $ Right (goto (c tid) tid threads, idSource, MyThreadId)++    -- | Put a value into a @CVar@, blocking the thread until it's+    -- empty.+    stepPut cvar@(cvid, _) a c = do+      (success, threads', woken) <- putIntoCVar True cvar a (const c) fixed tid threads+      return $ Right (threads', idSource, if success then Put cvid woken else BlockedPut cvid)++    -- | Try to put a value into a @CVar@, without blocking.+    stepTryPut cvar@(cvid, _) a c = do+      (success, threads', woken) <- putIntoCVar False cvar a c fixed tid threads+      return $ Right (threads', idSource, TryPut cvid success woken)++    -- | Get the value from a @CVar@, without emptying, blocking the+    -- thread until it's full.+    stepGet cvar@(cvid, _) c = do+      (success, threads', _) <- readFromCVar False True cvar (c . fromJust) fixed tid threads+      return $ Right (threads', idSource, if success then Read cvid else BlockedRead cvid)++    -- | Take the value from a @CVar@, blocking the thread until it's+    -- full.+    stepTake cvar@(cvid, _) c = do+      (success, threads', woken) <- readFromCVar True True cvar (c . fromJust) fixed tid threads+      return $ Right (threads', idSource, if success then Take cvid woken else BlockedTake cvid)++    -- | Try to take the value from a @CVar@, without blocking.+    stepTryTake cvar@(cvid, _) c = do+      (success, threads', woken) <- readFromCVar True False cvar c fixed tid threads+      return $ Right (threads', idSource, TryTake cvid success woken)++    -- | Read from a @CRef@.+    stepReadRef (crid, ref) c = do+      val <- readRef fixed ref+      return $ Right (goto (c val) tid threads, idSource, ReadRef crid)++    -- | Modify a @CRef@.+    stepModRef (crid, ref) f c = do+      (new, val) <- f <$> readRef fixed ref+      writeRef fixed ref new+      return $ Right (goto (c val) tid threads, idSource, ModRef crid)++    -- | Run a STM transaction atomically.+    stepAtom stm c = do+      let oldctvid = _nextCTVId idSource+      (res, newctvid) <- runstm stm oldctvid+      case res of+        Success readen written val+          | any (<oldctvid) readen || any (<oldctvid) written ->+            let (threads', woken) = wake (OnCTVar written) threads+            in return $ Right (knows (map Right written) tid $ goto (c val) tid threads', idSource { _nextCTVId = newctvid }, STM woken)+          | otherwise ->+           return $ Right (knows (map Right written) tid $ goto (c val) tid threads, idSource { _nextCTVId = newctvid }, FreshSTM)+        Retry touched ->+          let threads' = block (OnCTVar touched) tid threads+          in return $ Right (threads', idSource { _nextCTVId = newctvid }, BlockedSTM)+        Exception e -> stepThrow e++    -- | Run a subcomputation in an exception-catching context.+    stepCatching h ma c = return $ Right (threads', idSource, Catching) where+      a     = runCont ma      (APopCatching . c)+      e exc = runCont (h exc) (APopCatching . c)++      threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = a, _handlers = Handler e : _handlers thread }) tid threads++    -- | Pop the top exception handler from the thread's stack.+    stepPopCatching a = return $ Right (threads', idSource, PopCatching) where+      threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = a, _handlers = tail $_handlers thread }) tid threads++    -- | Throw an exception, and propagate it to the appropriate+    -- handler.+    stepThrow e = return $+      case propagate e . _handlers . fromJust $ M.lookup tid threads of+        Just (act, hs) ->+          let threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = act, _handlers = hs }) tid threads+          in  Right (threads', idSource, Throw)+        Nothing -> Left UncaughtException++    -- | Throw an exception to the target thread, and propagate it to+    -- the appropriate handler.+    stepThrowTo t e c = return $+      let threads' = goto c tid threads+          blocked = M.alter (\(Just thread) -> Just $ thread { _blocking = Just (OnMask t) }) tid threads+          interrupted act hs = M.alter (\(Just thread) -> Just $ thread { _continuation = act, _blocking = Nothing, _handlers = hs }) t+      in case M.lookup t threads of+           Just thread+             | interruptible thread -> case propagate e $ _handlers thread of+               Just (act, hs) -> Right (interrupted act hs threads', idSource, ThrowTo t)+               Nothing+                 | t == 0     -> Left UncaughtException+                 | otherwise -> Right (kill t threads', idSource, ThrowTo t)+             | otherwise -> Right (blocked, idSource, BlockedThrowTo t)+           Nothing -> Right (threads', idSource, ThrowTo t)++    -- | Execute a subcomputation with a new masking state, and give+    -- it a function to run a computation with the current masking+    -- state.+    --+    -- Explicit type sig necessary for checking in the prescence of+    -- 'umask', sadly.+    stepMasking :: MaskingState+                -> ((forall b. M n r s b -> M n r s b) -> M n r s a)+                -> (a -> Action n r s)+                -> n (Either Failure (Threads n r s, IdSource, ThreadAction))+    stepMasking m ma c = return $ Right (threads', idSource, SetMasking False m) where+      a = runCont (ma umask) (AResetMask False False m' . c)++      m' = _masking . fromJust $ M.lookup tid threads+      umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> return b+      resetMask typ mask = cont $ \k -> AResetMask typ True mask $ k ()++      threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = a, _masking = m }) tid threads++    -- | Reset the masking thread of the state.+    stepResetMask b1 b2 m c = return $ Right (threads', idSource, (if b1 then SetMasking else ResetMasking) b2 m) where+      threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = c, _masking = m }) tid threads++    -- | Create a new @CVar@, using the next 'CVarId'.+    stepNew na = do+      let (idSource', newcvid) = nextCVId idSource+      a <- na newcvid+      return $ Right (knows [Left newcvid] tid $ goto a tid threads, idSource', New newcvid)++    -- | Create a new @CRef@, using the next 'CRefId'.+    stepNewRef na = do+      let (idSource', newcrid) = nextCRId idSource+      a <- na newcrid+      return $ Right (goto a tid threads, idSource', NewRef newcrid)++    -- | Lift an action from the underlying monad into the @Conc@+    -- computation.+    stepLift na = do+      a <- na+      return $ Right (goto a tid threads, idSource, Lift)++    -- | Run a computation atomically. If this fails, the entire thing fails.+    stepNoTest ma c = do+      (a, idSource') <- runconc ma idSource+      return $+        case a of+          Right a' -> Right (goto (c a') tid threads, idSource', NoTest)+          _ -> Left FailureInNoTest++    -- | Record that a variable is known about.+    stepKnowsAbout v c = return $ Right (knows [v] tid $ goto c tid threads, idSource, KnowsAbout)++    -- | Record that a variable will never be touched again.+    stepForgets v c = return $ Right (forgets [v] tid $ goto c tid threads, idSource, Forgets)++    -- | Record that all shared variables are known.+    stepAllKnown c = return $ Right (fullknown tid $ goto c tid threads, idSource, AllKnown)++    -- | Kill the current thread.+    stepStop = return $ Right (kill tid threads, idSource, Stop)

@@ -0,0 +1,54 @@+-- | Operations over @CVar@s+module Test.DejaFu.Deterministic.Internal.CVar where++import Control.Monad (when)+import Test.DejaFu.Internal+import Test.DejaFu.Deterministic.Internal.Common+import Test.DejaFu.Deterministic.Internal.Threading++--------------------------------------------------------------------------------+-- * Manipulating @CVar@s++-- | Put a value into a @CVar@, in either a blocking or nonblocking+-- way.+putIntoCVar :: Monad n+            => Bool -> V r a -> a -> (Bool -> Action n r s)+            -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+putIntoCVar blocking (cvid, ref) a c fixed threadid threads = do+  val <- readRef fixed ref++  case val of+    Just _+      | blocking ->+        let threads' = block (OnCVarEmpty cvid) threadid threads+        in return (False, threads', [])++      | otherwise ->+        return (False, goto (c False) threadid threads, [])++    Nothing -> do+      writeRef fixed ref $ Just a+      let (threads', woken) = wake (OnCVarFull cvid) threads+      return (True, goto (c True) threadid threads', woken)++-- | Take a value from a @CVar@, in either a blocking or nonblocking+-- way.+readFromCVar :: Monad n+             => Bool -> Bool -> V r a -> (Maybe a -> Action n r s)+             -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+readFromCVar emptying blocking (cvid, ref) c fixed threadid threads = do+  val <- readRef fixed ref++  case val of+    Just _ -> do+      when emptying $ writeRef fixed ref Nothing+      let (threads', woken) = wake (OnCVarEmpty cvid) threads+      return (True, goto (c val) threadid threads', woken)++    Nothing+      | blocking ->+        let threads' = block (OnCVarFull cvid) threadid threads+        in return (False, threads', [])++      | otherwise ->+        return (False, goto (c Nothing) threadid threads, [])

@@ -0,0 +1,345 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE RankNTypes                #-}++-- | Common types and utility functions for deterministic execution of+-- 'MonadConc' implementations.+module Test.DejaFu.Deterministic.Internal.Common where++import Control.DeepSeq (NFData(..))+import Control.Exception (Exception, MaskingState(..), SomeException(..))+import Control.Monad.Cont (Cont)+import Data.List.Extra+import Test.DejaFu.Internal+import Test.DejaFu.STM (CTVarId)++--------------------------------------------------------------------------------+-- * The @Conc@ Monad++-- | The underlying monad is based on continuations over Actions.+type M n r s a = Cont (Action n r s) a++-- | CVars are represented as a unique numeric identifier, and a+-- reference containing a Maybe value.+type V r a = (CVarId, r (Maybe a))++-- | CRefs are represented as a unique numeric identifier, and a+-- reference containing a value.+type R r a = (CRefId, r a)++-- | Dict of methods for implementations to override.+type Fixed n r s = Ref n r (Cont (Action n r s))++--------------------------------------------------------------------------------+-- * Primitive Actions++-- | Scheduling is done in terms of a trace of 'Action's. Blocking can+-- only occur as a result of an action, and they cover (most of) the+-- primitives of the concurrency. 'spawn' is absent as it is+-- implemented in terms of 'newEmptyCVar', 'fork', and 'putCVar'.+data Action n r s =+    AFork ((forall b. M n r s b -> M n r s b) -> Action n r s) (ThreadId -> Action n r s)+  | AMyTId (ThreadId -> Action n r s)+  | forall a. APut     (V r a) a (Action n r s)+  | forall a. ATryPut  (V r a) a (Bool -> Action n r s)+  | forall a. AGet     (V r a) (a -> Action n r s)+  | forall a. ATake    (V r a) (a -> Action n r s)+  | forall a. ATryTake (V r a) (Maybe a -> Action n r s)+  | forall a. AReadRef (R r a) (a -> Action n r s)+  | forall a b. AModRef  (R r a) (a -> (a, b)) (b -> Action n r s)+  | forall a. ANoTest  (M n r s a) (a -> Action n r s)+  | forall a. AAtom    (s n r a) (a -> Action n r s)+  | ANew  (CVarId -> n (Action n r s))+  | ANewRef (CRefId -> n (Action n r s))+  | ALift (n (Action n r s))+  | AThrow SomeException+  | AThrowTo ThreadId SomeException (Action n r s)+  | forall a e. Exception e => ACatching (e -> M n r s a) (M n r s a) (a -> Action n r s)+  | APopCatching (Action n r s)+  | forall a. AMasking MaskingState ((forall b. M n r s b -> M n r s b) -> M n r s a) (a -> Action n r s)+  | AResetMask Bool Bool MaskingState (Action n r s)+  | AKnowsAbout (Either CVarId CTVarId) (Action n r s)+  | AForgets (Either CVarId CTVarId) (Action n r s)+  | AAllKnown (Action n r s)+  | AStop++--------------------------------------------------------------------------------+-- * Identifiers++-- | Every live thread has a unique identitifer.+type ThreadId = Int++-- | Every 'CVar' has a unique identifier.+type CVarId = Int++-- | Every 'CRef' has a unique identifier.+type CRefId = Int++-- | The number of ID parameters was getting a bit unwieldy, so this+-- hides them all away.+data IdSource = Id { _nextCRId :: CRefId, _nextCVId :: CVarId, _nextCTVId :: CTVarId, _nextTId :: ThreadId }++-- | Get the next free 'CRefId'.+nextCRId :: IdSource -> (IdSource, CRefId)+nextCRId idsource = let newid = _nextCRId idsource + 1 in (idsource { _nextCRId = newid }, newid)++-- | Get the next free 'CVarId'.+nextCVId :: IdSource -> (IdSource, CVarId)+nextCVId idsource = let newid = _nextCVId idsource + 1 in (idsource { _nextCVId = newid }, newid)++-- | Get the next free 'CTVarId'.+nextCTVId :: IdSource -> (IdSource, CTVarId)+nextCTVId idsource = let newid = _nextCTVId idsource + 1 in (idsource { _nextCTVId = newid }, newid)++-- | Get the next free 'ThreadId'.+nextTId :: IdSource -> (IdSource, ThreadId)+nextTId idsource = let newid = _nextTId idsource + 1 in (idsource { _nextTId = newid }, newid)++-- | The initial ID source.+initialIdSource :: IdSource+initialIdSource = Id 0 0 0 0++--------------------------------------------------------------------------------+-- * Scheduling & Traces++-- | A @Scheduler@ maintains some internal state, @s@, takes the+-- 'ThreadId' of the last thread scheduled, or 'Nothing' if this is+-- the first decision, and the list of runnable threads along with+-- what each will do in the next steps (as far as can be+-- determined). It produces a 'ThreadId' to schedule, and a new state.+--+-- __Note:__ In order to prevent computation from hanging, the runtime+-- will assume that a deadlock situation has arisen if the scheduler+-- attempts to (a) schedule a blocked thread, or (b) schedule a+-- nonexistent thread. In either of those cases, the computation will+-- be halted.+type Scheduler s = s -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, NonEmpty Lookahead) -> (ThreadId, s)++-- | One of the outputs of the runner is a @Trace@, which is a log of+-- decisions made, alternative decisions (including what action would+-- have been performed had that decision been taken), and the action a+-- thread took in its step.+type Trace = [(Decision, [(Decision, Lookahead)], ThreadAction)]++-- | Like a 'Trace', but gives more lookahead (where possible) for+-- alternative decisions.+type Trace' = [(Decision, [(Decision, NonEmpty Lookahead)], ThreadAction)]++-- | Throw away information from a 'Trace'' to get just a 'Trace'.+toTrace :: Trace' -> Trace+toTrace = map go where+  go (dec, alters, act) = (dec, map (\(d, a:|_) -> (d, a)) alters, act)++-- | Pretty-print a trace.+showTrace :: Trace -> String+showTrace = trace "" 0 where+  trace prefix num ((Start tid,_,_):ds)    = thread prefix num ++ trace ("S" ++ show tid) 1 ds+  trace prefix num ((SwitchTo tid,_,_):ds) = thread prefix num ++ trace ("P" ++ show tid) 1 ds+  trace prefix num ((Continue,_,_):ds)     = trace prefix (num + 1) ds+  trace prefix num []                      = thread prefix num++  thread prefix num = prefix ++ replicate num '-'++-- | 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.+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)++instance NFData Decision where+  rnf (Start    tid) = rnf tid+  rnf (SwitchTo tid) = rnf tid+  rnf Continue = ()++-- | All the actions that a thread can perform.+data ThreadAction =+    Fork ThreadId+  -- ^ Start a new thread.+  | MyThreadId+  -- ^ Get the 'ThreadId' of the current thread.+  | New CVarId+  -- ^ Create a new 'CVar'.+  | Put CVarId [ThreadId]+  -- ^ Put into a 'CVar', possibly waking up some threads.+  | BlockedPut CVarId+  -- ^ Get blocked on a put.+  | TryPut CVarId Bool [ThreadId]+  -- ^ Try to put into a 'CVar', possibly waking up some threads.+  | Read CVarId+  -- ^ Read from a 'CVar'.+  | BlockedRead CVarId+  -- ^ Get blocked on a read.+  | Take CVarId [ThreadId]+  -- ^ Take from a 'CVar', possibly waking up some threads.+  | BlockedTake CVarId+  -- ^ Get blocked on a take.+  | TryTake CVarId Bool [ThreadId]+  -- ^ Try to take from a 'CVar', possibly waking up some threads.+  | NewRef CRefId+  -- ^ Create a new 'CRef'.+  | ReadRef CRefId+  -- ^ Read from a 'CRef'.+  | ModRef CRefId+  -- ^ Modify a 'CRef'.+  | STM [ThreadId]+  -- ^ An STM transaction was executed, possibly waking up some+  -- threads.+  | FreshSTM+  -- ^ An STM transaction was executed, and all it did was create and+  -- write to new 'CTVar's, no existing 'CTVar's were touched.+  | BlockedSTM+  -- ^ 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.+  | Lift+  -- ^ Lift an action from the underlying monad. Note that the+  -- penultimate action in a trace will always be a @Lift@, this is an+  -- artefact of how the runner works.+  | NoTest+  -- ^ A computation annotated with '_concNoTest' was executed in a+  -- single step.+  | KnowsAbout+  -- ^ A '_concKnowsAbout' annotation was processed.+  | Forgets+  -- ^ A '_concForgets' annotation was processed.+  | AllKnown+  -- ^ A '_concALlKnown' annotation was processed.+  | Stop+  -- ^ Cease execution and terminate.+  deriving (Eq, Show)++instance NFData ThreadAction where+  rnf (TryTake c b tids) = rnf (c, b, tids)+  rnf (TryPut  c b tids) = rnf (c, b, tids)+  rnf (SetMasking   b m) = m `seq` b `seq` ()+  rnf (ResetMasking b m) = m `seq` b `seq` ()+  rnf (BlockedRead c) = rnf c+  rnf (BlockedTake c) = rnf c+  rnf (BlockedPut  c) = rnf c+  rnf (ThrowTo tid) = rnf tid+  rnf (Take c tids) = rnf (c, tids)+  rnf (Put  c tids) = rnf (c, tids)+  rnf (STM  tids) = rnf tids+  rnf (Fork tid)  = rnf tid+  rnf (New  c) = rnf c+  rnf (Read c) = rnf c+  rnf ta = ta `seq` ()++-- | A one-step look-ahead at what a thread will do next.+data Lookahead =+    WillFork+  -- ^ Will start a new thread.+  | WillMyThreadId+  -- ^ Will get the 'ThreadId'.+  | WillNew+  -- ^ Will create a new 'CVar'.+  | WillPut CVarId+  -- ^ Will put into a 'CVar', possibly waking up some threads.+  | WillTryPut CVarId+  -- ^ Will try to put into a 'CVar', possibly waking up some threads.+  | WillRead CVarId+  -- ^ Will read from a 'CVar'.+  | WillTake CVarId+  -- ^ Will take from a 'CVar', possibly waking up some threads.+  | WillTryTake CVarId+  -- ^ Will try to take from a 'CVar', possibly waking up some threads.+  | WillNewRef+  -- ^ Will create a new 'CRef'.+  | WillReadRef CRefId+  -- ^ Will read from a 'CRef'.+  | WillModRef CRefId+  -- ^ Will modify a '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.+  | WillLift+  -- ^ Will lift an action from the underlying monad. Note that the+  -- penultimate action in a trace will always be a @Lift@, this is an+  -- artefact of how the runner works.+  | WillNoTest+  -- ^ Will execute a computation annotated with '_concNoTest' in a+  -- single step.+  | WillKnowsAbout+  -- ^ Will process a '_concKnowsAbout' annotation.+  | WillForgets+  -- ^ Will process a '_concForgets' annotation.+  | WillAllKnown+  -- ^ Will process a '_concALlKnown' annotation.+  | WillStop+  -- ^ Will cease execution and terminate.+  deriving (Eq, Show)++instance NFData Lookahead where+  rnf (WillSetMasking   b ms) = b `seq` ms `seq` ()+  rnf (WillResetMasking b ms) = b `seq` ms `seq` ()+  rnf (WillPut     c) = rnf c+  rnf (WillTryPut  c) = rnf c+  rnf (WillRead    c) = rnf c+  rnf (WillTake    c) = rnf c+  rnf (WillTryTake c) = rnf c+  rnf (WillReadRef c) = rnf c+  rnf (WillModRef  c) = rnf c+  rnf ta = ta `seq` ()++--------------------------------------------------------------------------------+-- * Failures++-- | An indication of how a concurrent computation failed.+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.+  | Deadlock+  -- ^ The computation became blocked indefinitely on @CVar@s.+  | STMDeadlock+  -- ^ The computation became blocked indefinitely on @CTVar@s.+  | UncaughtException+  -- ^ An uncaught exception bubbled to the top of the computation.+  | FailureInNoTest+  -- ^ A computation annotated with '_concNoTest' produced a failure,+  -- rather than a result.+  deriving (Eq, Show)++instance NFData Failure where+  rnf f = f `seq` () -- WHNF == NF

@@ -0,0 +1,174 @@+{-# LANGUAGE CPP                       #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE RankNTypes                #-}++-- | Operations and types for threads.+module Test.DejaFu.Deterministic.Internal.Threading where++import Control.Exception (Exception, MaskingState(..), SomeException(..), fromException)+import Control.Monad.Cont (cont)+import Data.List (intersect, nub)+import Data.Map (Map)+import Data.Maybe (fromMaybe, isJust, isNothing)+import Test.DejaFu.STM (CTVarId)+import Test.DejaFu.Deterministic.Internal.Common++import qualified Data.Map as M++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative ((<$>))+#endif++--------------------------------------------------------------------------------+-- * Threads++-- | Threads are stored in a map index by 'ThreadId'.+type Threads n r s = Map ThreadId (Thread n r s)++-- | All the state of a thread.+data Thread n r s = Thread+  { _continuation :: Action n r s+  -- ^ The next action to execute.+  , _blocking     :: Maybe BlockedOn+  -- ^ The state of any blocks.+  , _handlers     :: [Handler n r s]+  -- ^ Stack of exception handlers+  , _masking      :: MaskingState+  -- ^ The exception masking state.+  , _known        :: [Either CVarId CTVarId]+  -- ^ Shared variables the thread knows about.+  , _fullknown    :: Bool+  -- ^ Whether the referenced variables of the thread are completely+  -- known. If every thread has _fullknown == True, then turn on+  -- detection of nonglobal deadlock.+  }++--------------------------------------------------------------------------------+-- * Blocking++-- | A @BlockedOn@ is used to determine what sort of variable a thread+-- is blocked on.+data BlockedOn = OnCVarFull CVarId | OnCVarEmpty CVarId | OnCTVar [CTVarId] | OnMask ThreadId deriving Eq++-- | Determine if a thread is blocked in a certain way.+(~=) :: Thread n r s -> BlockedOn -> Bool+thread ~= theblock = case (_blocking thread, theblock) of+  (Just (OnCVarFull  _), OnCVarFull  _) -> True+  (Just (OnCVarEmpty _), OnCVarEmpty _) -> True+  (Just (OnCTVar     _), OnCTVar     _) -> True+  (Just (OnMask      _), OnMask      _) -> True+  _ -> False++-- | Determine if a thread is deadlocked. If at least one thread is+-- not in a fully-known state, this will only check for global+-- deadlock.+isLocked :: ThreadId -> Threads n r a -> Bool+isLocked tid ts+  | allKnown = case M.lookup tid ts of+    Just thread -> noRefs $ _blocking thread+    Nothing -> False+  | otherwise = M.null $ M.filter (isNothing . _blocking) ts++  where+    -- | Check if all threads are in a fully-known state.+    allKnown = all _fullknown $ M.elems ts++    -- | Check if no other runnable thread has a reference to anything+    -- the block references.+    noRefs (Just (OnCVarFull  cvarid)) = null $ findCVar   cvarid+    noRefs (Just (OnCVarEmpty cvarid)) = null $ findCVar   cvarid+    noRefs (Just (OnCTVar     ctvids)) = null $ findCTVars ctvids+    noRefs _ = True++    -- | Get IDs of all threads (other than the one under+    -- consideration) which reference a 'CVar'.+    findCVar cvarid = M.keys $ M.filterWithKey (check [Left cvarid]) ts++    -- | Get IDs of all runnable threads (other than the one under+    -- consideration) which reference some 'CTVar's.+    findCTVars ctvids = M.keys $ M.filterWithKey (check (map Right ctvids)) ts++    -- | Check if a thread references a variable, and if it's not the+    -- thread under consideration.+    check lookingfor thetid thethread+      | thetid == tid = False+      | otherwise    = (not . null $ lookingfor `intersect` _known thethread) && isNothing (_blocking thethread)++--------------------------------------------------------------------------------+-- * Exceptions++-- | An exception handler.+data Handler n r s = forall e. Exception e => Handler (e -> Action n r s)++-- | Propagate an exception upwards, finding the closest handler+-- which can deal with it.+propagate :: SomeException -> [Handler n r s] -> Maybe (Action n r s, [Handler n r s])+propagate _ [] = Nothing+propagate e (Handler h:hs) = maybe (propagate e hs) (\act -> Just (act, hs)) $ h <$> e' where+  e' = fromException e++-- | Check if a thread can be interrupted by an exception.+interruptible :: Thread n r s -> Bool+interruptible thread = _masking thread == Unmasked || (_masking thread == MaskedInterruptible && isJust (_blocking thread))++--------------------------------------------------------------------------------+-- * Manipulating threads++-- | Replace the @Action@ of a thread.+goto :: Action n r s -> ThreadId -> Threads n r s -> Threads n r s+goto a = M.alter $ \(Just thread) -> Just (thread { _continuation = a })++-- | Start a thread with the given ID, inheriting the masking state+-- from the parent thread. This ID must not already be in use!+launch :: ThreadId -> ThreadId -> ((forall b. M n r s b -> M n r s b) -> Action n r s) -> Threads n r s -> Threads n r s+launch parent tid a threads = launch' mask tid a threads where+  mask = fromMaybe Unmasked $ _masking <$> M.lookup parent threads++-- | 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 s b -> M n r s b) -> Action n r s) -> Threads n r s -> Threads n r s+launch' mask tid a = M.insert tid thread where+  thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = mask, _known = [], _fullknown = False }++  umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False mask >> return b+  resetMask typ m = cont $ \k -> AResetMask typ True m $ k ()++-- | Kill a thread.+kill :: ThreadId -> Threads n r s -> Threads n r s+kill = M.delete++-- | Block a thread.+block :: BlockedOn -> ThreadId -> Threads n r s -> Threads n r s+block blockedOn = M.alter doBlock where+  doBlock (Just thread) = Just $ thread { _blocking = Just blockedOn }+  doBlock _ = error "Invariant failure in 'block': thread does NOT exist!"++-- | Unblock all threads waiting on the appropriate block. For 'CTVar'+-- blocks, this will wake all threads waiting on at least one of the+-- given 'CTVar's.+wake :: BlockedOn -> Threads n r s -> (Threads n r s, [ThreadId])+wake blockedOn threads = (M.map unblock threads, M.keys $ M.filter isBlocked threads) where+  unblock thread+    | isBlocked thread = thread { _blocking = Nothing }+    | otherwise = thread++  isBlocked thread = case (_blocking thread, blockedOn) of+    (Just (OnCTVar ctvids), OnCTVar blockedOn') -> ctvids `intersect` blockedOn' /= []+    (theblock, _) -> theblock == Just blockedOn++-- | Record that a thread knows about a shared variable.+knows :: [Either CVarId CTVarId] -> ThreadId -> Threads n r s -> Threads n r s+knows theids = M.alter go where+  go (Just thread) = Just $ thread { _known = nub $ theids ++ _known thread }+  go _ = error "Invariant failure in 'knows': thread does NOT exist!"++-- | Forget about a shared variable.+forgets :: [Either CVarId CTVarId] -> ThreadId -> Threads n r s -> Threads n r s+forgets theids = M.alter go where+  go (Just thread) = Just $ thread { _known = filter (`notElem` theids) $ _known thread }+  go _ = error "Invariant failure in 'forgets': thread does NOT exist!"++-- | Record that a thread's shared variable state is fully known.+fullknown :: ThreadId -> Threads n r s -> Threads n r s+fullknown = M.alter go where+  go (Just thread) = Just $ thread { _fullknown = True }+  go _ = error "Invariant failure in 'fullknown': thread does NOT exist!"

@@ -0,0 +1,57 @@+-- | Deterministic scheduling for concurrent computations.+module Test.DejaFu.Deterministic.Schedule+  ( Scheduler+  , ThreadId+  , NonEmpty(..)+  -- * Pre-emptive+  , randomSched+  , roundRobinSched+  -- * Non pre-emptive+  , randomSchedNP+  , roundRobinSchedNP+  -- * Utilities+  , makeNP+  , toList+  ) where++import Data.List.Extra+import System.Random (RandomGen, randomR)+import Test.DejaFu.Deterministic.Internal++-- | A simple random scheduler which, at every step, picks a random+-- thread to run.+randomSched :: RandomGen g => Scheduler g+randomSched g _ threads = (threads' !! choice, g') where+  (choice, g') = randomR (0, length threads' - 1) g+  threads' = map fst $ toList threads++-- | A random scheduler which doesn't pre-empt the running+-- thread. That is, if the last thread scheduled is still runnable,+-- run that, otherwise schedule randomly.+randomSchedNP :: RandomGen g => Scheduler g+randomSchedNP = makeNP randomSched++-- | A round-robin scheduler which, at every step, schedules the+-- thread with the next 'ThreadId'.+roundRobinSched :: Scheduler ()+roundRobinSched _ Nothing _ = (0, ())+roundRobinSched _ (Just (prior, _)) threads+  | prior >= maximum threads' = (minimum threads', ())+  | otherwise = (minimum $ filter (>prior) threads', ())++  where+    threads' = map fst $ toList threads++-- | A round-robin scheduler which doesn't pre-empt the running+-- thread.+roundRobinSchedNP :: Scheduler ()+roundRobinSchedNP = makeNP roundRobinSched++-- | Turn a potentially pre-emptive scheduler into a non-preemptive+-- one.+makeNP :: Scheduler s -> Scheduler s+makeNP sched = newsched where+  newsched s p@(Just (prior, _)) threads+    | prior `elem` map fst (toList threads) = (prior, s)+    | otherwise = sched s p threads+  newsched s Nothing threads = sched s Nothing threads

@@ -0,0 +1,34 @@+{-# LANGUAGE RankNTypes #-}++-- | Dealing with mutable state.+module Test.DejaFu.Internal where++import Control.Monad.ST (ST)+import Data.IORef (IORef, newIORef, readIORef, writeIORef)+import Data.STRef (STRef, newSTRef, readSTRef, writeSTRef)++-- | Mutable references.+data Ref n r m = Ref+  { newRef   :: forall a. a -> n (r a)+  , readRef  :: forall a. r a -> n a+  , writeRef :: forall a. r a -> a -> n ()+  , liftN    :: forall a. n a -> m a+  }++-- | Method dict for 'ST'.+refST :: (forall a. ST t a -> m a) -> Ref (ST t) (STRef t) m+refST lftN = Ref+  { newRef   = newSTRef+  , readRef  = readSTRef+  , writeRef = writeSTRef+  , liftN    = lftN+  }++-- | Method dict for 'IO'.+refIO :: (forall a. IO a -> m a) -> Ref IO IORef m+refIO lftN = Ref+  { newRef   = newIORef+  , readRef  = readIORef+  , writeRef = writeIORef+  , liftN    = lftN+  }

@@ -0,0 +1,239 @@+{-# LANGUAGE CPP        #-}+{-# LANGUAGE RankNTypes #-}++-- | Systematic testing for concurrent computations.+module Test.DejaFu.SCT+  ( -- * Bounded Partial-order Reduction++  -- | We can characterise the state of a concurrent computation by+  -- considering the ordering of dependent events. This is a partial+  -- order: independent events can be performed in any order without+  -- affecting the result, and so are /not/ ordered.+  --+  -- Partial-order reduction is a technique for computing these+  -- partial orders, and only testing one total order for each partial+  -- order. This cuts down the amount of work to be done+  -- significantly. /Bounded/ partial-order reduction is a further+  -- optimisation, which only considers schedules within some bound.+  --+  -- This module provides both a generic function for BPOR, and also a+  -- pre-emption bounding BPOR runner, which is used by the+  -- "Test.DejaFu" module.+  --+  -- See /Bounded partial-order reduction/, K. Coons, M. Musuvathi,+  -- K. McKinley for more details.++    BacktrackStep(..)+  , sctBounded+  , sctBoundedIO++  -- * 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.++  , sctPreBound+  , sctPreBoundIO++  -- * Utilities++  , tidOf+  , decisionOf+  , activeTid+  , preEmpCount+  , initialCVState+  , updateCVState+  , willBlock+  , willBlockSafely+  ) where++import Control.DeepSeq (force)+import Data.Functor.Identity (Identity(..), runIdentity)+import Data.IntMap.Strict (IntMap)+import Data.Sequence (Seq, (|>))+import Data.Maybe (maybeToList, isNothing)+import Test.DejaFu.Deterministic+import Test.DejaFu.Deterministic.IO (ConcIO, runConcIO')+import Test.DejaFu.SCT.Internal++import qualified Data.IntMap.Strict as I+import qualified Data.Set as S+import qualified Data.Sequence as Sq++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative ((<$>), (<*>))+#endif++-- * Pre-emption bounding++-- | An SCT runner using a pre-emption bounding scheduler.+sctPreBound ::+    Int+  -- ^ The maximum number of pre-emptions to allow in a single+  -- execution+  -> (forall t. Conc t a)+  -- ^ The computation to run many times+  -> [(Either Failure a, Trace)]+sctPreBound pb = sctBounded (pbBv pb) pbBacktrack pbInitialise++-- | Variant of 'sctPreBound' for computations which do 'IO'.+sctPreBoundIO :: Int -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]+sctPreBoundIO pb = sctBoundedIO (pbBv pb) pbBacktrack pbInitialise++-- | Check if a schedule is in the bound.+pbBv :: Int -> [Decision] -> Bool+pbBv pb ds = preEmpCount ds <= pb++-- | Add a backtrack point, and also conservatively add one prior to+-- the most recent transition before that point. This may result in+-- the same state being reached multiple times, but is needed because+-- of the artificial dependency imposed by the bound.+pbBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]+pbBacktrack bs i tid = maybe id (\j' b -> backtrack True b j' tid) j $ backtrack False bs i tid where+  -- Index of the conservative point+  j = goJ . reverse . pairs $ zip [0..i-1] bs where+    goJ (((_,b1), (j',b2)):rest)+      | _threadid b1 /= _threadid b2 = Just j'+      | otherwise = goJ rest+    goJ [] = Nothing++  {-# INLINE pairs #-}+  pairs = zip <*> tail++  -- Add a backtracking point. If the thread isn't runnable, add all+  -- runnable threads.+  backtrack c bx@(b:rest) 0 t+    -- If the backtracking point is already present, don't re-add it,+    -- UNLESS this would force it to backtrack (it's conservative)+    -- where before it might not.+    | t `S.member` _runnable b =+      let val = I.lookup t $ _backtrack b+      in  if isNothing val || (val == Just False && c)+          then b { _backtrack = I.insert t c $ _backtrack b } : rest+          else bx++    -- Otherwise just backtrack to everything runnable.+    | otherwise = b { _backtrack = I.fromList [ (t',c) | t' <- S.toList $ _runnable b ] } : rest++  backtrack c (b:rest) n t = b : backtrack c rest (n-1) t+  backtrack _ [] _ _ = error "Ran out of schedule whilst backtracking!"++-- | Pick a new thread to run. Choose the current thread if available,+-- otherwise add all runnable threads.+pbInitialise :: Maybe (ThreadId, a) -> NonEmpty (ThreadId, b) -> NonEmpty ThreadId+pbInitialise prior threads@((nextTid, _):|rest) = case prior of+  Just (tid, _)+    | any (\(t, _) -> t == tid) $ toList threads -> tid:|[]+  _ -> nextTid:|map fst rest++-- * BPOR++-- | SCT via BPOR.+--+-- Schedules are generated by running the computation with a+-- deterministic scheduler with some initial list of decisions, after+-- which the supplied function is called. At each step of execution,+-- possible-conflicting actions are looked for, if any are found,+-- \"backtracking points\" are added, to cause the events to happen in+-- a different order in a future execution.+--+-- Note that unlike with non-bounded partial-order reduction, this may+-- do some redundant work as the introduction of a bound can make+-- previously non-interfering events interfere with each other.+sctBounded :: ([Decision] -> Bool)+           -- ^ Check if a prefix trace is within the bound.+           -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])+           -- ^ Add a new backtrack point, this takes the history of+           -- the execution so far, the index to insert the+           -- backtracking point, and the thread to backtrack to. This+           -- may insert more than one backtracking point.+           -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId)+           -- ^ Produce possible scheduling decisions, all will be+           -- tried.+           -> (forall t. Conc t a) -> [(Either Failure a, Trace)]+sctBounded bv backtrack initialise c = runIdentity $ sctBoundedM bv backtrack initialise run where+  run sched s = Identity $ runConc' sched s c++-- | Variant of 'sctBounded' for computations which do 'IO'.+sctBoundedIO :: ([Decision] -> Bool)+             -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])+             -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId)+             -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]+sctBoundedIO bv backtrack initialise c = sctBoundedM bv backtrack initialise run where+  run sched s = runConcIO' sched s c++-- | Generic SCT runner.+sctBoundedM :: (Functor m, Monad m)+            => ([Decision] -> Bool)+            -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])+            -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId)+            -> (Scheduler SchedState -> SchedState -> m (Either Failure a, SchedState, Trace'))+            -- ^ Monadic runner, with computation fixed.+            -> m [(Either Failure a, Trace)]+sctBoundedM bv backtrack initialise run = go initialState where+  go bpor = case next bpor of+    Just (sched, conservative, bpor') -> do+      (res, s, trace) <- run (bporSched initialise) (initialSchedState sched)++      let bpoints = findBacktrack backtrack (_sbpoints s) trace+      let bpor''  = grow conservative trace bpor'+      let bpor''' = todo bv bpoints bpor''++      ((res, toTrace trace):) <$> go bpor'''++    Nothing -> return []++-- * BPOR Scheduler++-- | The scheduler state+data SchedState = SchedState+  { _sprefix  :: [ThreadId]+  -- ^ Decisions still to make+  , _sbpoints :: Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])+  -- ^ Which threads are runnable at each step, and the alternative+  -- decisions still to make.+  , _scvstate :: IntMap Bool+  -- ^ The 'CVar' block state.+  }++-- | Initial scheduler state for a given prefix+initialSchedState :: [ThreadId] -> SchedState+initialSchedState prefix = SchedState+  { _sprefix  = prefix+  , _sbpoints = Sq.empty+  , _scvstate = initialCVState+  }++-- | BPOR scheduler: takes a list of decisions, and maintains a trace+-- including the runnable threads, and the alternative choices allowed+-- by the bound-specific initialise function.+bporSched :: (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId)+          -> Scheduler SchedState+bporSched initialise = force $ \s prior threads -> case _sprefix s of+  -- If there is a decision available, make it+  (d:ds) ->+    let threads' = fmap (\(t,a:|_) -> (t,a)) threads+        cvstate' = maybe (_scvstate s) (updateCVState (_scvstate s) . snd) prior+    in  (d, s { _sprefix = ds, _sbpoints = _sbpoints s |> (threads', []), _scvstate = cvstate' })++  -- Otherwise query the initialise function for a list of possible+  -- choices, and make one of them arbitrarily (recording the others).+  [] ->+    let threads' = fmap (\(t,a:|_) -> (t,a)) threads+        choices  = initialise prior threads'+        cvstate' = maybe (_scvstate s) (updateCVState (_scvstate s) . snd) prior+        choices' = [t+                   | t  <- toList choices+                   , as <- maybeToList $ lookup t (toList threads)+                   , not . willBlockSafely cvstate' $ toList as+                   ]+    in  case choices' of+          (nextTid:rest) -> (nextTid, s { _sbpoints = _sbpoints s |> (threads', rest), _scvstate = cvstate' })++          -- TODO: abort the execution here.+          [] -> case choices of+                 (nextTid:|_) -> (nextTid, s { _sbpoints = _sbpoints s |> (threads', []), _scvstate = cvstate' })

@@ -0,0 +1,334 @@+{-# LANGUAGE CPP #-}++-- | Internal utilities and types for BPOR.+module Test.DejaFu.SCT.Internal where++import Control.DeepSeq (NFData(..))+import Data.IntMap.Strict (IntMap)+import Data.List (foldl', partition, maximumBy)+import Data.Maybe (mapMaybe, fromJust)+import Data.Ord (comparing)+import Data.Sequence (Seq, ViewL(..))+import Data.Set (Set)+import Test.DejaFu.Deterministic++import qualified Data.IntMap.Strict as I+import qualified Data.Sequence as Sq+import qualified Data.Set as S++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative ((<$>), (<*>))+#endif++-- * BPOR state++-- | One step of the execution, including information for backtracking+-- purposes. This backtracking information is used to generate new+-- schedules.+data BacktrackStep = BacktrackStep+  { _threadid  :: ThreadId+  -- ^ The thread running at this step+  , _decision  :: (Decision, ThreadAction)+  -- ^ What happened at this step.+  , _runnable  :: Set ThreadId+  -- ^ The threads runnable at this step+  , _backtrack :: IntMap Bool+  -- ^ The list of alternative threads to run, and whether those+  -- alternatives were added conservatively due to the bound.+  } deriving (Eq, Show)++instance NFData BacktrackStep where+  rnf b = rnf (_threadid b, _decision b, _runnable b, _backtrack b)++-- | BPOR execution is represented as a tree of states, characterised+-- by the decisions that lead to that state.+data BPOR = BPOR+  { _brunnable :: Set ThreadId+  -- ^ What threads are runnable at this step.+  , _btodo     :: IntMap Bool+  -- ^ Follow-on decisions still to make, and whether that decision+  -- was added conservatively due to the bound.+  , _bignore   :: Set ThreadId+  -- ^ Follow-on decisions never to make, because they will result in+  -- the chosen thread immediately blocking without achieving+  -- anything, which can't have any effect on the result of the+  -- program.+  , _bdone     :: IntMap BPOR+  -- ^ Follow-on decisions that have been made.+  , _bsleep    :: IntMap ThreadAction+  -- ^ Transitions to ignore (in this node and children) until a+  -- dependent transition happens.+  , _btaken    :: IntMap ThreadAction+  -- ^ Transitions which have been taken, excluding+  -- conservatively-added ones, in the (reverse) order that they were+  -- taken, as the 'Map' doesn't preserve insertion order. This is+  -- used in implementing sleep sets.+  }++-- | Initial BPOR state.+initialState :: BPOR+initialState = BPOR+  { _brunnable = S.singleton 0+  , _btodo     = I.singleton 0 False+  , _bignore   = S.empty+  , _bdone     = I.empty+  , _bsleep    = I.empty+  , _btaken    = I.empty+  }++-- | Produce a new schedule from a BPOR tree. If there are no new+-- schedules remaining, return 'Nothing'. Also returns whether the+-- decision made was added conservatively.+--+-- This returns the longest prefix, on the assumption that this will+-- lead to lots of backtracking points being identified before+-- higher-up decisions are reconsidered, so enlarging the sleep sets.+next :: BPOR -> Maybe ([ThreadId], Bool, BPOR)+next = go 0 where+  go tid bpor =+        -- All the possible prefix traces from this point, with+        -- updated BPOR subtrees if taken from the done list.+    let prefixes = mapMaybe go' (I.toList $ _bdone bpor) ++ [Left t | t <- I.toList $ _btodo bpor]+        -- Sort by number of preemptions, in descending order.+        cmp   = comparing $ preEmps tid bpor . either (\(a,_) -> [a]) (\(a,_,_) -> a)++    in if null prefixes+       then Nothing+       else case maximumBy cmp prefixes of+              -- If the prefix with the most preemptions is from the done list, update that.+              Right (ts@(t:_), c, b) -> Just (ts, c, bpor { _bdone = I.insert t b $ _bdone bpor })+              Right ([], _, _) -> error "Invariant failure in 'next': empty done prefix!"++              -- If from the todo list, remove it.+              Left (t,c) -> Just ([t], c, bpor { _btodo = I.delete t $ _btodo bpor })++  go' (tid, bpor) = (\(ts,c,b) -> Right (tid:ts, c, b)) <$> go tid bpor++  preEmps tid bpor (t:ts) =+    let rest = preEmps t (fromJust . I.lookup t $ _bdone bpor) ts+    in  if tid /= t && tid `S.member` _brunnable bpor then 1 + rest else rest+  preEmps _ _ [] = 0::Int++-- | Produce a list of new backtracking points from an execution+-- trace.+findBacktrack :: ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])+              -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])+              -> Trace'+              -> [BacktrackStep]+findBacktrack backtrack = go S.empty 0 [] . Sq.viewl where+  go allThreads tid bs ((e,i):<is) ((d,_,a):ts) =+    let tid' = tidOf tid d+        this        = BacktrackStep { _threadid  = tid'+                                    , _decision  = (d, a)+                                    , _runnable  = S.fromList . map fst . toList $ e+                                    , _backtrack = I.fromList $ map (\i' -> (i', False)) i+                                    }+        bs'         = doBacktrack allThreads (toList e) bs+        allThreads' = allThreads `S.union` _runnable this+    in go allThreads' tid' (bs' ++ [this]) (Sq.viewl is) ts+  go _ _ bs _ _ = bs++  doBacktrack allThreads enabledThreads bs =+    let tagged = reverse $ zip [0..] bs+        idxs   = [ (head is, u)+                 | (u, n) <- enabledThreads+                 , v <- S.toList allThreads+                 , u /= v+                 , let is = [ i+                            | (i, b) <- tagged+                            , _threadid b == v+                            , dependent' (snd $ _decision b) (u, n)+                            ]+                 , not $ null is] :: [(Int, ThreadId)]+    in foldl' (\b (i, u) -> backtrack b i u) bs idxs++-- | Add a new trace to the tree, creating a new subtree.+grow :: Bool -> Trace' -> BPOR -> BPOR+grow conservative = grow' initialCVState 0 where+  grow' cvstate tid trc@((d, _, a):rest) bpor =+    let tid'     = tidOf tid d+        cvstate' = updateCVState cvstate a+    in  case I.lookup tid' $ _bdone bpor of+          Just bpor' -> bpor { _bdone  = I.insert tid' (grow' cvstate' tid' rest bpor') $ _bdone bpor }+          Nothing    -> bpor { _btaken = if conservative then _btaken bpor else I.insert tid' a $ _btaken bpor+                            , _bdone  = I.insert tid' (subtree cvstate' tid' (_bsleep bpor `I.union` _btaken bpor) trc) $ _bdone bpor }+  grow' _ _ [] bpor = bpor++  subtree cvstate tid sleep ((d, ts, a):rest) =+    let cvstate' = updateCVState cvstate a+        sleep'   = I.filterWithKey (\t a' -> not $ dependent a (t,a')) sleep+    in BPOR+        { _brunnable = S.fromList $ tids tid d a ts+        , _btodo     = I.empty+        , _bignore   = S.fromList [tidOf tid d' | (d',as) <- ts, willBlockSafely cvstate' $ toList as]+        , _bdone     = I.fromList $ case rest of+          ((d', _, _):_) ->+            let tid' = tidOf tid d'+            in  [(tid', subtree cvstate' tid' sleep' rest)]+          [] -> []+        , _bsleep = sleep'+        , _btaken = case rest of+          ((d', _, a'):_) -> I.singleton (tidOf tid d') a'+          [] -> I.empty+        }+  subtree _ _ _ [] = error "Invariant failure in 'subtree': suffix empty!"++  tids tid d (Fork t)           ts = tidOf tid d : t : map (tidOf tid . fst) ts+  tids tid _ (BlockedPut _)     ts = map (tidOf tid . fst) ts+  tids tid _ (BlockedRead _)    ts = map (tidOf tid . fst) ts+  tids tid _ (BlockedTake _)    ts = map (tidOf tid . fst) ts+  tids tid _ BlockedSTM         ts = map (tidOf tid . fst) ts+  tids tid _ (BlockedThrowTo _) ts = map (tidOf tid . fst) ts+  tids tid _ Stop               ts = map (tidOf tid . fst) ts+  tids tid d _ ts = tidOf tid d : map (tidOf tid . fst) ts++-- | Add new backtracking points, if they have not already been+-- visited, fit into the bound, and aren't in the sleep set.+todo :: ([Decision] -> Bool) -> [BacktrackStep] -> BPOR -> BPOR+todo bv = step where+  step bs bpor =+    let (bpor', bs') = go 0 [] Nothing bs bpor+    in  if all (I.null . _backtrack) bs'+        then bpor'+        else step bs' bpor'++  go tid pref lastb (b:bs) bpor =+    let (bpor', blocked) = backtrack pref b bpor+        tid'   = tidOf tid . fst $ _decision b+        (child, blocked')  = go tid' (pref++[fst $ _decision b]) (Just b) bs . fromJust $ I.lookup tid' (_bdone bpor)+        bpor'' = bpor' { _bdone = I.insert tid' child $ _bdone bpor' }+    in  case lastb of+         Just b' -> (bpor'', b' { _backtrack = blocked } : blocked')+         Nothing -> (bpor'', blocked')++  go _ _ (Just b') _ bpor = (bpor, [b' { _backtrack = I.empty }])+  go _ _ Nothing   _ bpor = (bpor, [])++  backtrack pref b bpor =+    let todo' = [ x+                | x@(t,c) <- I.toList $ _backtrack b+                , bv $ pref ++ [decisionOf (Just $ activeTid pref) (_brunnable bpor) t]+                , t `notElem` I.keys (_bdone bpor)+                , c || I.notMember t (_bsleep bpor)+                ]+        (blocked, nxt) = partition (\(t,_) -> t `S.member` _bignore bpor) todo'+    in  (bpor { _btodo = _btodo bpor `I.union` I.fromList nxt }, I.fromList blocked)++-- * Utilities++-- | Get the resultant 'ThreadId' of a 'Decision', with a default case+-- for 'Continue'.+tidOf :: ThreadId -> Decision -> ThreadId+tidOf _ (Start t)    = t+tidOf _ (SwitchTo t) = t+tidOf tid Continue   = tid++-- | Get the 'Decision' that would have resulted in this 'ThreadId',+-- given a prior 'ThreadId' (if any) and list of runnable threads.+decisionOf :: Maybe ThreadId -> Set ThreadId -> ThreadId -> Decision+decisionOf prior runnable chosen+  | prior == Just chosen = Continue+  | prior `S.member` S.map Just runnable = SwitchTo chosen+  | otherwise = Start chosen++-- | Get the tid of the currently active thread after executing a+-- series of decisions. The list MUST begin with a 'Start'.+activeTid :: [Decision] -> ThreadId+activeTid = foldl' go 0 where+  go _ (Start t)    = t+  go _ (SwitchTo t) = t+  go t Continue     = t++-- | Count the number of pre-emptions in a schedule+preEmpCount :: [Decision] -> Int+preEmpCount (SwitchTo _:ds) = 1 + preEmpCount ds+preEmpCount (_:ds) = preEmpCount ds+preEmpCount [] = 0++-- | Check if an action is dependent on another, assumes the actions+-- are from different threads (two actions in the same thread are+-- always dependent).+dependent :: ThreadAction -> (ThreadId, ThreadAction) -> Bool+dependent Lift (_, Lift) = True+dependent (ThrowTo t) (t2, _) = t == t2+dependent d1 (_, d2) = cref || cvar || ctvar where+  cref = Just True == ((\(r1, w1) (r2, w2) -> r1 == r2 && (w1 || w2)) <$> cref' d1 <*> cref' d2)+  cref'  (ReadRef  r) = Just (r, False)+  cref'  (ModRef   r) = Just (r, True)+  cref'  _ = Nothing++  cvar = Just True == ((==) <$> cvar' d1 <*> cvar' d2)+  cvar'  (TryPut  c _ _) = Just c+  cvar'  (TryTake c _ _) = Just c+  cvar'  (Put  c _) = Just c+  cvar'  (Read c)   = Just c+  cvar'  (Take c _) = Just c+  cvar'  _ = Nothing++  ctvar = ctvar' d1 && ctvar' d2+  ctvar' (STM _) = True+  ctvar' _ = False++-- | Variant of 'dependent' to handle 'ThreadAction''s+dependent' :: ThreadAction -> (ThreadId, Lookahead) -> Bool+dependent' Lift (_, WillLift) = True+dependent' (ThrowTo t) (t2, _) = t == t2+dependent' d1 (_, d2) = cref || cvar || ctvar where+  cref = Just True == ((\(r1, w1) (r2, w2) -> r1 == r2 && (w1 || w2)) <$> cref' d1 <*> cref'' d2)+  cref'  (ReadRef  r) = Just (r, False)+  cref'  (ModRef   r) = Just (r, True)+  cref'  _ = Nothing+  cref'' (WillReadRef r) = Just (r, False)+  cref'' (WillModRef  r) = Just (r, True)+  cref'' _ = Nothing++  cvar = Just True == ((==) <$> cvar' d1 <*> cvar'' d2)+  cvar'  (TryPut  c _ _) = Just c+  cvar'  (TryTake c _ _) = Just c+  cvar'  (Put  c _) = Just c+  cvar'  (Read c)   = Just c+  cvar'  (Take c _) = Just c+  cvar'  _ = Nothing+  cvar'' (WillTryPut  c) = Just c+  cvar'' (WillTryTake c) = Just c+  cvar'' (WillPut  c) = Just c+  cvar'' (WillRead c) = Just c+  cvar'' (WillTake c) = Just c+  cvar'' _ = Nothing++  ctvar = ctvar' d1 && ctvar'' d2+  ctvar' (STM _) = True+  ctvar' _ = False+  ctvar'' WillSTM = True+  ctvar'' _ = False++-- * Keeping track of 'CVar' full/empty states++-- | Initial global 'CVar' state+initialCVState :: IntMap Bool+initialCVState = I.empty++-- | Update the 'CVar' state with the action that has just happened.+updateCVState :: IntMap Bool -> ThreadAction -> IntMap Bool+updateCVState cvstate (Put  c _) = I.insert c True  cvstate+updateCVState cvstate (Take c _) = I.insert c False cvstate+updateCVState cvstate (TryPut  c True _) = I.insert c True  cvstate+updateCVState cvstate (TryTake c True _) = I.insert c False cvstate+updateCVState cvstate _ = cvstate++-- | Check if an action will block.+willBlock :: IntMap Bool -> Lookahead -> Bool+willBlock cvstate (WillPut  c) = I.lookup c cvstate == Just True+willBlock cvstate (WillTake c) = I.lookup c cvstate == Just False+willBlock _ _ = False++-- | Check if a list of actions will block safely (without modifying+-- any global state). This allows further lookahead at, say, the+-- 'spawn' of a thread (which always starts with 'KnowsAbout').+willBlockSafely :: IntMap Bool -> [Lookahead] -> Bool+willBlockSafely cvstate (WillKnowsAbout:as) = willBlockSafely cvstate as+willBlockSafely cvstate (WillForgets:as)    = willBlockSafely cvstate as+willBlockSafely cvstate (WillAllKnown:as)   = willBlockSafely cvstate as+willBlockSafely cvstate (WillPut  c:_) = willBlock cvstate (WillPut  c)+willBlockSafely cvstate (WillTake c:_) = willBlock cvstate (WillTake c)+willBlockSafely _ _ = False

@@ -0,0 +1,145 @@+{-# LANGUAGE CPP                        #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE RankNTypes                 #-}+{-# LANGUAGE TypeFamilies               #-}++-- | A 'MonadSTM' implementation, which can be run on top of 'IO' or+-- 'ST'.+module Test.DejaFu.STM+  ( -- * The @STMLike@ Monad+    STMLike+  , STMST+  , STMIO+  , Result(..)+  , runTransaction+  , runTransactionST+  , runTransactionIO++  -- * Software Transactional Memory+  , retry+  , orElse+  , check+  , throwSTM+  , catchSTM++  -- * @CTVar@s+  , CTVar+  , CTVarId+  , newCTVar+  , readCTVar+  , writeCTVar+  ) where++import Control.Exception (Exception, SomeException(..))+import Control.Monad (liftM)+import Control.Monad.Catch (MonadCatch(..), MonadThrow(..))+import Control.Monad.Cont (cont)+import Control.Monad.ST (ST, runST)+import Data.IORef (IORef)+import Data.STRef (STRef)+import Test.DejaFu.Internal+import Test.DejaFu.STM.Internal++import qualified Control.Monad.STM.Class as C++#if __GLASGOW_HASKELL__ < 710+import Control.Applicative (Applicative)+#endif++{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}++-- | The 'MonadSTM' implementation, it encapsulates a single atomic+-- transaction. The environment, that is, the collection of defined+-- 'CTVar'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).+newtype STMLike t n r a = S { unS :: M t n r a } deriving (Functor, Applicative, Monad)++-- | A convenience wrapper around 'STMLike' using 'STRef's.+type STMST t a = STMLike t (ST t) (STRef t) a++-- | A convenience wrapper around 'STMLike' using 'IORef's.+type STMIO t a = STMLike t IO IORef a++instance MonadThrow (STMLike t n r) where+  throwM = throwSTM++instance MonadCatch (STMLike t n r) where+  catch = catchSTM++instance Monad n => C.MonadSTM (STMLike t n r) where+  type CTVar (STMLike t n r) = CTVar t r++  retry      = retry+  orElse     = orElse+  newCTVar   = newCTVar+  readCTVar  = readCTVar+  writeCTVar = writeCTVar++-- | Abort the current transaction, restoring any 'CTVar's written to,+-- and returning the list of 'CTVar's read.+retry :: Monad n => STMLike t n r a+retry = S $ cont $ const ARetry++-- | Run the first transaction and, if it 'retry's, +orElse :: Monad n => STMLike t n r a -> STMLike t n r a -> STMLike t n r a+orElse a b = S $ cont $ AOrElse (unS a) (unS b)++-- | Check whether a condition is true and, if not, call 'retry'.+check :: Monad n => Bool -> STMLike t n r ()+check = C.check++-- | Throw an exception. This aborts the transaction and propagates+-- the exception.+throwSTM :: Exception e => e -> STMLike t n r a+throwSTM e = S $ cont $ const $ AThrow (SomeException e)++-- | Handling exceptions from 'throwSTM'.+catchSTM :: Exception e => STMLike t n r a -> (e -> STMLike t n r a) -> STMLike t n r a+catchSTM stm handler = S $ cont $ ACatch (unS stm) (unS . handler)++-- | Create a new 'CTVar' containing the given value.+newCTVar :: Monad n => a -> STMLike t n r (CTVar t r a)+newCTVar a = S $ cont lifted where+  lifted c = ANew $ \ref ctvid -> c `liftM` newCTVar' ref ctvid+  newCTVar' ref ctvid = (\r -> V (ctvid, r)) `liftM` newRef ref a++-- | Return the current value stored in a 'CTVar'.+readCTVar :: Monad n => CTVar t r a -> STMLike t n r a+readCTVar ctvar = S $ cont $ ARead ctvar++-- | Write the supplied value into the 'CTVar'.+writeCTVar :: Monad n => CTVar t r a -> a -> STMLike t n r ()+writeCTVar ctvar a = S $ cont $ \c -> AWrite ctvar a $ c ()++-- | Run a transaction in the 'ST' monad, starting from a clean+-- environment, and discarding the environment afterwards. This is+-- suitable for testing individual transactions, but not for composing+-- multiple ones.+runTransaction :: (forall t. STMST t a) -> Result a+runTransaction ma = fst $ runST $ runTransactionST ma 0++-- | Run a transaction in the 'ST' monad, returning the result and new+-- initial 'CTVarId'. If the transaction ended by calling 'retry', any+-- 'CTVar' modifications are undone.+runTransactionST :: STMST t a -> CTVarId -> ST t (Result a, CTVarId)+runTransactionST = runTransactionM fixedST where+  fixedST = refST $ \mb -> cont (\c -> ALift $ c `liftM` mb)++-- | Run a transaction in the 'IO' monad, returning the result and new+-- initial 'CTVarId'. If the transaction ended by calling 'retry', any+-- 'CTVar' modifications are undone.+runTransactionIO :: STMIO t a -> CTVarId -> IO (Result a, CTVarId)+runTransactionIO = runTransactionM fixedIO where+  fixedIO = refIO $ \mb -> cont (\c -> ALift $ c `liftM` mb)++-- | Run a transaction in an arbitrary monad.+runTransactionM :: Monad n+  => Fixed t n r -> STMLike t n r a -> CTVarId -> n (Result a, CTVarId)+runTransactionM ref ma ctvid = do+  (res, undo, ctvid') <- doTransaction ref (unS ma) ctvid++  case res of+    Success _ _ _ -> return (res, ctvid')+    _ -> undo >> return (res, ctvid)

@@ -0,0 +1,180 @@+{-# LANGUAGE CPP                       #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE RankNTypes                #-}+{-# LANGUAGE ScopedTypeVariables       #-}++-- | 'MonadSTM' testing implementation, internal types and+-- definitions.+module Test.DejaFu.STM.Internal where++import Control.Exception (Exception, SomeException(..), fromException)+import Control.Monad.Cont (Cont, runCont)+import Data.List (nub)+import Test.DejaFu.Internal++#if __GLASGOW_HASKELL__ < 710+import Data.Foldable (Foldable(..))+import Data.Monoid (mempty)+#endif++--------------------------------------------------------------------------------+-- The @STMLike@ monad++-- | The underlying monad is based on continuations over primitive+-- actions.+type M t n r a = Cont (STMAction t n r) a++-- | Dict of methods for implementations to override.+type Fixed t n r = Ref n r (Cont (STMAction t n r))++--------------------------------------------------------------------------------+-- * Primitive actions++-- | STM transactions are represented as a sequence of primitive+-- actions.+data STMAction t n r+  = forall a e. Exception e => ACatch (M t n r a) (e -> M t n r a) (a -> STMAction t n r)+  | forall a. ARead  (CTVar t r a) (a -> STMAction t n r)+  | forall a. AWrite (CTVar t r a) a (STMAction t n r)+  | forall a. AOrElse (M t n r a) (M t n r a) (a -> STMAction t n r)+  | ANew (Fixed t n r -> CTVarId -> n (STMAction t n r))+  | ALift (n (STMAction t n r))+  | AThrow SomeException+  | ARetry+  | AStop++--------------------------------------------------------------------------------+-- * @CTVar@s++-- | A 'CTVar' is a tuple of a unique ID and the value contained. The+-- ID is so that blocked transactions can be re-run when a 'CTVar'+-- they depend on has changed.+newtype CTVar t r a = V (CTVarId, r a)++-- | The unique ID of a 'CTVar'. Only meaningful within a single+-- concurrent computation.+type CTVarId = Int++--------------------------------------------------------------------------------+-- * Output++-- | The result of an STM transaction, along with which 'CTVar's it+-- touched whilst executing.+data Result a =+    Success [CTVarId] [CTVarId] a+  -- ^ The transaction completed successfully, reading the first list+  -- 'CTVar's and writing to the second.+  | Retry   [CTVarId]+  -- ^ The transaction aborted by calling 'retry', and read the+  -- returned 'CTVar's. It should be retried when at least one of the+  -- 'CTVar's has been mutated.+  | Exception SomeException+  -- ^ The transaction aborted by throwing an exception.+  deriving Show++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 STM transaction, returning an action to undo its effects.+doTransaction :: Monad n => Fixed t n r -> M t n r a -> CTVarId -> n (Result a, n (), CTVarId)+doTransaction fixed ma newctvid = do+  ref <- newRef fixed Nothing++  let c = runCont (ma >>= liftN fixed . writeRef fixed ref . Just . Right) $ const AStop++  (newctvid', undo, readen, written) <- go ref c (return ()) newctvid [] []++  res <- readRef fixed ref++  case res of+    Just (Right val) -> return (Success (nub readen) (nub written) val, undo, newctvid')++    Just (Left  exc) -> undo >> return (Exception exc,      return (), newctvid)+    Nothing          -> undo >> return (Retry $ nub readen, return (), newctvid)++  where+    go ref act undo nctvid readen written = do+      (act', undo', nctvid', readen', written') <- stepTrans fixed act nctvid+      let ret = (nctvid', undo >> undo', readen' ++ readen, written' ++ written)+      case act' of+        AStop      -> return ret+        ARetry     -> writeRef fixed ref Nothing >> return ret+        AThrow exc -> writeRef fixed ref (Just $ Left exc) >> return ret++        _ -> go ref act' (undo >> undo') nctvid' (readen' ++ readen) (written' ++ written)++-- | Run a transaction for one step.+stepTrans :: forall t n r. Monad n => Fixed t n r -> STMAction t n r -> CTVarId -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId])+stepTrans fixed act newctvid = case act of+  ACatch  stm h c -> stepCatch stm h c+  ARead   ref c   -> stepRead ref c+  AWrite  ref a c -> stepWrite ref a c+  ANew    na      -> stepNew na+  AOrElse a b c   -> stepOrElse a b c+  ALift   na      -> stepLift na++  AThrow exc -> return (AThrow exc, nothing, newctvid, [], [])+  ARetry     -> return (ARetry,     nothing, newctvid, [], [])+  AStop      -> return (AStop,      nothing, newctvid, [], [])++  where+    nothing = return ()++    stepCatch :: Exception e => M t n r a -> (e -> M t n r a) -> (a -> STMAction t n r) -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId])+    stepCatch stm h c = do+      (res, undo, newctvid') <- doTransaction fixed stm newctvid+      case res of+        Success readen written val -> return (c val, undo, newctvid', readen, written)+        Retry readen -> return (ARetry, nothing, newctvid, readen, [])+        Exception exc -> case fromException exc of+          Just exc' -> do+            (rese, undoe, newctvide') <- doTransaction fixed (h exc') newctvid+            case rese of+              Success readen written val -> return (c val, undoe, newctvide', readen, written)+              Exception exce -> return (AThrow exce, nothing, newctvid, [], [])+              Retry readen -> return (ARetry, nothing, newctvid, readen, [])+          Nothing -> return (AThrow exc, nothing, newctvid, [], [])++    stepRead :: CTVar t r a -> (a -> STMAction t n r) -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId])+    stepRead (V (ctvid, ref)) c = do+      val <- readRef fixed ref+      return (c val, nothing, newctvid, [ctvid], [])++    stepWrite :: CTVar t r a -> a -> STMAction t n r -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId])+    stepWrite (V (ctvid, ref)) a c = do+      old <- readRef fixed ref+      writeRef fixed ref a+      return (c, writeRef fixed ref old, newctvid, [], [ctvid])++    stepNew :: (Fixed t n r -> CTVarId -> n (STMAction t n r)) -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId])+    stepNew na = do+      let newctvid' = newctvid + 1+      a <- na fixed newctvid+      return (a, nothing, newctvid', [], [newctvid])++    stepOrElse :: M t n r a -> M t n r a -> (a -> STMAction t n r) -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId])+    stepOrElse a b c = do+      (resa, undoa, newctvida') <- doTransaction fixed a newctvid+      case resa of+        Success readen written val -> return (c val, undoa, newctvida', readen, written)+        Exception exc -> return (AThrow exc, nothing, newctvid, [], [])+        Retry _ -> do+          (resb, undob, newctvidb') <- doTransaction fixed b newctvid+          case resb of+            Success readen written val -> return (c val, undob, newctvidb', readen, written)+            Exception exc -> return (AThrow exc, nothing, newctvid, [], [])+            Retry readen -> return (ARetry, nothing, newctvid, readen, [])++    stepLift :: n (STMAction t n r) -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId])+    stepLift na = do+      a <- na+      return (a, nothing, newctvid, [], [])

@@ -0,0 +1,101 @@+-- Initial monad-conc.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++name:                dejafu+version:             0.1.0.0+synopsis:            Overloadable primitives for testable, potentially non-deterministic, concurrency.++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 provides a class of monads for potentially+  nondeterministic concurrency, with an interface in the spirit of+  GHC's normal concurrency abstraction.+  .+  == @MonadConc@ with 'IO':+  .+  The intention of the @MonadConc@ class is to provide concurrency+  where 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. This+  assumption is used by the testing functionality provided by+  Test.DejaFu.+  .+  Whilst this assumption may not hold in general when 'IO' is+  involved, you should strive to produce test cases where it does.+  .+  See the <https://github.com/barrucadu/dejafu README> for more+  details.++homepage:            https://github.com/barrucadu/dejafu+license:             MIT+license-file:        LICENSE+author:              Michael Walker+maintainer:          mike@barrucadu.co.uk+-- copyright:           +category:            Concurrency+build-type:          Simple+-- extra-source-files:  +cabal-version:       >=1.10++source-repository head+  type:     git+  location: https://github.com/barrucadu/dejafu.git++source-repository this+  type:     git+  location: https://github.com/barrucadu/dejafu.git+  tag:      0.1.0.0++library+  exposed-modules:     Control.Monad.Conc.Class+                     , Control.Monad.STM.Class++                     , Control.Concurrent.CVar+                     , Control.Concurrent.CVar.Strict+                     , Control.Concurrent.STM.CTVar+                     , Control.Concurrent.STM.CTMVar++                     , Test.DejaFu+                     , Test.DejaFu.Deterministic+                     , Test.DejaFu.Deterministic.IO+                     , Test.DejaFu.Deterministic.Schedule+                     , Test.DejaFu.SCT+                     , Test.DejaFu.STM++  other-modules:       Test.DejaFu.Deterministic.Internal+                     , Test.DejaFu.Deterministic.Internal.Common+                     , Test.DejaFu.Deterministic.Internal.CVar+                     , Test.DejaFu.Deterministic.Internal.Threading+                     , Test.DejaFu.Internal+                     , Test.DejaFu.SCT.Internal+                     , Test.DejaFu.STM.Internal++                     , Data.List.Extra++  -- other-extensions:    +  build-depends:       base >=4.5 && <5+                     , containers+                     , deepseq+                     , exceptions >=0.7+                     , monad-loops+                     , mtl+                     , random+                     , stm+                     , transformers+  -- hs-source-dirs:      +  default-language:    Haskell2010+  ghc-options:         -Wall++test-suite tests+  hs-source-dirs:      tests+  type:                exitcode-stdio-1.0+  main-is:             Tests.hs+  build-depends:       dejafu, base+  default-language:    Haskell2010

@@ -0,0 +1,37 @@+module Main (main) where++import Test.DejaFu+import System.Exit (exitFailure, exitSuccess)++import qualified Tests.Cases  as C+import qualified Tests.Logger as L++andM :: (Functor m, Monad m) => [m Bool] -> m Bool+andM = fmap and . sequence++runTests :: IO Bool+runTests =+  andM [dejafu  C.simple2Deadlock ("Simple 2-Deadlock", deadlocksSometimes)+       ,dejafu (C.philosophers 2) ("2 Philosophers",    deadlocksSometimes)+       ,dejafu (C.philosophers 3) ("3 Philosophers",    deadlocksSometimes)+       ,dejafu (C.philosophers 4) ("4 Philosophers",    deadlocksSometimes)+       ,dejafu  C.thresholdValue  ("Threshold Value",   notAlwaysSame)+       ,dejafu  C.forgottenUnlock ("Forgotten Unlock",  deadlocksAlways)+       ,dejafu  C.simple2Race     ("Simple 2-Race",     notAlwaysSame)+       ,dejafu  C.raceyStack      ("Racey Stack",       notAlwaysSame)+       ,dejafu  C.threadKill      ("killThread",        deadlocksSometimes)+       ,dejafu  C.threadKillMask  ("killThread+mask 1", deadlocksNever)+       ,dejafu  C.threadKillUmask ("killThread+mask 2", deadlocksSometimes)+       ,dejafu  C.stmAtomic       ("STM Atomicity",     alwaysTrue (\r -> fmap (`elem` [0,2]) r == Right True))+       ,dejafu  C.stmRetry        ("STM Retry",         alwaysSame)+       ,dejafu  C.stmOrElse       ("STM orElse",        alwaysSame)+       ,dejafu  C.stmExc          ("STM Exceptions",    alwaysSame)+       ,dejafu  C.excNest         ("Nested Excs",       alwaysSame)+       ,dejafus L.badLogger      [("Logger (Valid)",    L.validResult)+                                 ,("Logger (Good)",     L.isGood)+                                 ,("Logger (Bad",       L.isBad)]]++main :: IO ()+main = do+  success <- runTests+  if success then exitSuccess else exitFailure