dejafu 0.2.0.0 → 0.3.0.0

raw patch · 32 files changed

+2576/−2269 lines, 32 filesdep +arraydep +dpordep +monad-controldep −randomdep ~atomic-primopsdep ~basedep ~containers

Dependencies added: array, dpor, monad-control, semigroups, template-haskell, transformers-base

Dependencies removed: random

Dependency ranges changed: atomic-primops, base, containers, deepseq, exceptions, monad-loops, mtl, stm, transformers

Files

• Control/Concurrent/CVar.hs +0/−123
• Control/Concurrent/CVar/Strict.hs +0/−97
• Control/Concurrent/Classy.hs +32/−0
• Control/Concurrent/Classy/CRef.hs +106/−0
• Control/Concurrent/Classy/Chan.hs +71/−0
• Control/Concurrent/Classy/MVar.hs +120/−0
• Control/Concurrent/Classy/QSem.hs +37/−0
• Control/Concurrent/Classy/QSemN.hs +89/−0
• Control/Concurrent/Classy/STM.hs +20/−0
• Control/Concurrent/Classy/STM/TArray.hs +48/−0
• Control/Concurrent/Classy/STM/TBQueue.hs +138/−0
• Control/Concurrent/Classy/STM/TChan.hs +127/−0
• Control/Concurrent/Classy/STM/TMVar.hs +110/−0
• Control/Concurrent/Classy/STM/TQueue.hs +105/−0
• Control/Concurrent/Classy/STM/TVar.hs +54/−0
• Control/Concurrent/STM/CTMVar.hs +0/−86
• Control/Concurrent/STM/CTVar.hs +0/−34
• Control/Monad/Conc/Class.hs +465/−407
• Control/Monad/STM/Class.hs +128/−109
• Data/List/Extra.hs +0/−60
• Test/DejaFu.hs +43/−30
• Test/DejaFu/Deterministic.hs +47/−47
• Test/DejaFu/Deterministic/Internal.hs +92/−98
• Test/DejaFu/Deterministic/Internal/Common.hs +294/−179
• Test/DejaFu/Deterministic/Internal/Memory.hs +66/−59
• Test/DejaFu/Deterministic/Internal/Threading.hs +22/−28
• Test/DejaFu/Deterministic/Schedule.hs +0/−57
• Test/DejaFu/SCT.hs +248/−305
• Test/DejaFu/SCT/Internal.hs +0/−437
• Test/DejaFu/STM.hs +25/−27
• Test/DejaFu/STM/Internal.hs +68/−76
• dejafu.cabal +21/−10

@@ -1,123 +0,0 @@--- | 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

@@ -1,97 +0,0 @@--- | 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,32 @@+-- | Classy concurrency.+--+-- Concurrency is \"lightweight\", which means that both thread+-- creation and context switching overheads are extremely+-- low. Scheduling of Haskell threads is done internally in the+-- Haskell runtime system, and doesn't make use of any operating+-- system-supplied thread packages.+--+-- Haskell threads can communicate via @MVar@s, a kind of synchronised+-- mutable variable (see "Control.Concurrent.Classy.MVar"). Several+-- common concurrency abstractions can be built from @MVar@s, and+-- these are provided by the "Control.Concurrent.Classy"+-- library. Threads may also communicate via exceptions.+module Control.Concurrent.Classy+  ( module Control.Monad.Conc.Class+  , module Control.Concurrent.Classy.Chan+  , module Control.Concurrent.Classy.CRef+  , module Control.Concurrent.Classy.MVar+  , module Control.Concurrent.Classy.STM+  , module Control.Concurrent.Classy.QSem+  , module Control.Concurrent.Classy.QSemN+  ) where++import Control.Monad.Conc.Class+import Control.Concurrent.Classy.Chan+import Control.Concurrent.Classy.CRef+import Control.Concurrent.Classy.MVar+import Control.Concurrent.Classy.STM+import Control.Concurrent.Classy.QSem+import Control.Concurrent.Classy.QSemN++{-# ANN module ("HLint: ignore Use import/export shortcut" :: String) #-}

@@ -0,0 +1,106 @@+-- | Mutable references in a concurrency monad.+--+-- __Deviations:__ There is no @Eq@ instance for @MonadConc@ the+-- @CRef@ type. Furthermore, the @mkWeakIORef@ function is not+-- provided.+module Control.Concurrent.Classy.CRef+  ( -- * CRefs+    newCRef+  , readCRef+  , writeCRef+  , modifyCRef+  , modifyCRef'+  , atomicModifyCRef+  , atomicModifyCRef'+  , atomicWriteCRef++  -- * Memory Model++  -- | In a concurrent program, @CRef@ operations may appear+  -- out-of-order to another thread, depending on the memory model of+  -- the underlying processor architecture. For example, on x86 (which+  -- uses total store order), loads can move ahead of stores. Consider+  -- this example:+  --+  -- > crefs :: MonadConc m => m (Bool, Bool)+  -- > crefs = do+  -- >   r1 <- newCRef False+  -- >   r2 <- newCRef False+  -- >+  -- >   x <- spawn $ writeCRef r1 True >> readCRef r2+  -- >   y <- spawn $ writeCRef r2 True >> readCRef r1+  -- >+  -- >   (,) <$> readCVar x <*> readCVar y+  --+  -- Under a sequentially consistent memory model the possible results+  -- are @(True, True)@, @(True, False)@, and @(False, True)@. Under+  -- total or partial store order, @(False, False)@ is also a possible+  -- result, even though there is no interleaving of the threads which+  -- can lead to this.+  --+  -- We can see this by testing with different memory models:+  --+  -- > > autocheck' SequentialConsistency crefs+  -- > [pass] Never Deadlocks (checked: 6)+  -- > [pass] No Exceptions (checked: 6)+  -- > [fail] Consistent Result (checked: 5)+  -- >         (False,True) S0-------S1-----S0--S2-----S0---+  -- >         (True,False) S0-------S1-P2-----S1----S0----+  -- >         (True,True) S0-------S1--P2-----S1---S0----+  -- >         (False,True) S0-------S1---P2-----S1--S0----+  -- >         (True,False) S0-------S2-----S1-----S0----+  -- >         ...+  -- > False+  --+  -- > > autocheck' TotalStoreOrder crefs+  -- > [pass] Never Deadlocks (checked: 303)+  -- > [pass] No Exceptions (checked: 303)+  -- > [fail] Consistent Result (checked: 302)+  -- >         (False,True) S0-------S1-----C-S0--S2-----C-S0---+  -- >         (True,False) S0-------S1-P2-----C-S1----S0----+  -- >         (True,True) S0-------S1-P2--C-S1----C-S0--S2---S0---+  -- >         (False,True) S0-------S1-P2--P1--C-C-S1--S0--S2---S0---+  -- >         (False,False) S0-------S1-P2--P1----S2---C-C-S0----+  -- >         ...+  -- > False+  --+  -- Traces for non-sequentially-consistent memory models show where+  -- writes to @CRef@s are /committed/, which makes a write visible to+  -- all threads rather than just the one which performed the+  -- write. Only 'writeCRef' is broken up into separate write and+  -- commit steps, 'atomicModifyCRef' is still atomic and imposes a+  -- memory barrier.+  ) where++import Control.Monad.Conc.Class++-- | Mutate the contents of a @CRef@.+--+-- Be warned that 'modifyCRef' does not apply the function strictly.+-- This means if the program calls 'modifyCRef' many times, but+-- seldomly uses the value, thunks will pile up in memory resulting in+-- a space leak. This is a common mistake made when using a @CRef@ as+-- a counter. For example, the following will likely produce a stack+-- overflow:+--+-- >ref <- newCRef 0+-- >replicateM_ 1000000 $ modifyCRef ref (+1)+-- >readCRef ref >>= print+--+-- To avoid this problem, use 'modifyCRef'' instead.+modifyCRef :: MonadConc m => CRef m a -> (a -> a) -> m ()+modifyCRef ref f = readCRef ref >>= writeCRef ref . f++-- | Strict version of 'modifyCRef'+modifyCRef' :: MonadConc m => CRef m a -> (a -> a) -> m ()+modifyCRef' ref f = do+  x <- readCRef ref+  writeCRef ref $! f x++-- | Strict version of 'atomicModifyCRef'. This forces both the value+-- stored in the @CRef@ as well as the value returned.+atomicModifyCRef' :: MonadConc m => CRef m a -> (a -> (a,b)) -> m b+atomicModifyCRef' ref f = do+  b <- atomicModifyCRef ref $ \a -> case f a of+    v@(a',_) -> a' `seq` v+  pure $! b

@@ -0,0 +1,71 @@+-- | Unbounded channels.+--+-- __Deviations:__ @Chan@ as defined here does not have an @Eq@+-- instance, this is because the @MonadConc@ @MVar@ type does not have+-- an @Eq@ constraint. The deprecated @unGetChan@ and @isEmptyCHan@+-- functions are not provided. Furthermore, the @getChanContents@+-- function is not provided as it needs unsafe I/O.+module Control.Concurrent.Classy.Chan+  ( -- * The 'Chan' type+    Chan++  -- * Operations+  , newChan+  , writeChan+  , readChan+  , dupChan++  -- * Stream interface+  , writeList2Chan+  ) where++import Control.Concurrent.Classy.MVar+import Control.Monad.Catch (mask_)+import Control.Monad.Conc.Class (MonadConc)++-- | 'Chan' is an abstract type representing an unbounded FIFO+-- channel.+data Chan m a+  = Chan (MVar m (Stream m a))+         (MVar m (Stream m a)) -- Invariant: the Stream a is always an empty MVar++type Stream m a = MVar m (ChItem m a)++data ChItem m a = ChItem a (Stream m a)++-- | Build and returns a new instance of 'Chan'.+newChan :: MonadConc m => m (Chan m a)+newChan = do+  hole  <- newEmptyMVar+  readVar  <- newMVar hole+  writeVar <- newMVar hole+  pure (Chan readVar writeVar)++-- | Write a value to a 'Chan'.+writeChan :: MonadConc m => Chan m a -> a -> m ()+writeChan (Chan _ writeVar) val = do+  new_hole <- newEmptyMVar+  mask_ $ do+    old_hole <- takeMVar writeVar+    putMVar old_hole (ChItem val new_hole)+    putMVar writeVar new_hole++-- | Read the next value from the 'Chan'.+readChan :: MonadConc m => Chan m a -> m a+readChan (Chan readVar _) =  modifyMVarMasked readVar $ \read_end -> do+  (ChItem val new_read_end) <- readMVar read_end+  pure (new_read_end, val)++-- | Duplicate a 'Chan': the duplicate channel begins empty, but data+-- written to either channel from then on will be available from both.+-- Hence this creates a kind of broadcast channel, where data written+-- by anyone is seen by everyone else.+dupChan :: MonadConc m => Chan m a -> m (Chan m a)+dupChan (Chan _ writeVar) = do+  hole       <- readMVar writeVar+  newReadVar <- newMVar hole+  pure (Chan newReadVar writeVar)++-- | Write an entire list of items to a 'Chan'.+writeList2Chan :: MonadConc m => Chan m a -> [a] -> m ()+writeList2Chan = mapM_ . writeChan

@@ -0,0 +1,120 @@+-- | An @'MVar' t@ is mutable location that is either empty or contains a+-- value of type @t@.  It has two fundamental operations: 'putMVar'+-- which fills an 'MVar' if it is empty and blocks otherwise, and+-- 'takeMVar' which empties an 'MVar' if it is full and blocks+-- otherwise.  They can be used in multiple different ways:+--+--   1. As synchronized mutable variables,+--+--   2. As channels, with 'takeMVar' and 'putMVar' as receive and+--      send, and+--+--   3. As a binary semaphore @'MVar' ()@, with 'takeMVar' and+--      'putMVar' as wait and signal.+--+-- __Deviations:__ There is no @Eq@ instance for @MonadConc@ the+-- @MVar@ type. Furthermore, the @mkWeakMVar@ and @addMVarFinalizer@+-- functions are not provided. Finally, normal @MVar@s have a fairness+-- guarantee, which dejafu does not currently make use of when+-- generating schedules to test, so your program may be tested with+-- /unfair/ schedules.+module Control.Concurrent.Classy.MVar+ ( -- *@MVar@s+  MVar+ , newEmptyMVar+ , newEmptyMVarN+ , newMVar+ , newMVarN+ , takeMVar+ , putMVar+ , readMVar+ , swapMVar+ , tryTakeMVar+ , tryPutMVar+ , isEmptyMVar+ , withMVar+ , withMVarMasked+ , modifyMVar_+ , modifyMVar+ , modifyMVarMasked_+ , modifyMVarMasked+ ) where++import Control.Monad.Catch (mask_, onException)+import Control.Monad.Conc.Class++-- | Swap the contents of a @MVar@, and return the value taken. This+-- function is atomic only if there are no other producers fro this+-- @MVar@.+swapMVar :: MonadConc m => MVar m a -> a -> m a+swapMVar cvar a = mask_ $ do+  old <- takeMVar cvar+  putMVar cvar a+  return old++-- | Check if a @MVar@ is empty.+isEmptyMVar :: MonadConc m => MVar m a -> m Bool+isEmptyMVar cvar = do+  val <- tryTakeMVar cvar+  case val of+    Just val' -> putMVar cvar val' >> return True+    Nothing   -> return False++-- | Operate on the contents of a @MVar@, replacing the contents after+-- finishing. This operation is exception-safe: it will replace the+-- original contents of the @MVar@ if an exception is raised. However,+-- it is only atomic if there are no other producers for this @MVar@.+{-# INLINE withMVar #-}+withMVar :: MonadConc m => MVar m a -> (a -> m b) -> m b+withMVar cvar f = mask $ \restore -> do+  val <- takeMVar cvar+  out <- restore (f val) `onException` putMVar cvar val+  putMVar cvar val++  return out++-- | Like 'withMVar', but the @IO@ action in the second argument is+-- executed with asynchronous exceptions masked.+{-# INLINE withMVarMasked #-}+withMVarMasked :: MonadConc m => MVar m a -> (a -> m b) -> m b+withMVarMasked cvar f = mask_ $ do+  val <- takeMVar cvar+  out <- f val `onException` putMVar cvar val+  putMVar cvar val++  return out++-- | An exception-safe wrapper for modifying the contents of a @MVar@.+-- Like 'withMVar', 'modifyMVar' will replace the original contents of+-- the @MVar@ if an exception is raised during the operation. This+-- function is only atomic if there are no other producers for this+-- @MVar@.+{-# INLINE modifyMVar_ #-}+modifyMVar_ :: MonadConc m => MVar m a -> (a -> m a) -> m ()+modifyMVar_ cvar f = modifyMVar cvar $ fmap (\a -> (a,())) . f++-- | A slight variation on 'modifyMVar_' that allows a value to be+-- returned (@b@) in addition to the modified value of the @MVar@.+{-# INLINE modifyMVar #-}+modifyMVar :: MonadConc m => MVar m a -> (a -> m (a, b)) -> m b+modifyMVar cvar f = mask $ \restore -> do+  val <- takeMVar cvar+  (val', out) <- restore (f val) `onException` putMVar cvar val+  putMVar cvar val'+  return out++-- | Like 'modifyMVar_', but the @IO@ action in the second argument is+-- executed with asynchronous exceptions masked.+{-# INLINE modifyMVarMasked_ #-}+modifyMVarMasked_ :: MonadConc m => MVar m a -> (a -> m a) -> m ()+modifyMVarMasked_ cvar f = modifyMVarMasked cvar $ fmap (\a -> (a,())) . f++-- | Like 'modifyMVar', but the @IO@ action in the second argument is+-- executed with asynchronous exceptions masked.+{-# INLINE modifyMVarMasked #-}+modifyMVarMasked :: MonadConc m => MVar m a -> (a -> m (a, b)) -> m b+modifyMVarMasked cvar f = mask_ $ do+  val <- takeMVar cvar+  (val', out) <- f val `onException` putMVar cvar val+  putMVar cvar val'+  return out

@@ -0,0 +1,37 @@+-- | Simple quantity semaphores.+module Control.Concurrent.Classy.QSem+  ( -- * Simple Quantity Semaphores+    QSem+  , newQSem+  , waitQSem+  , signalQSem+  ) where++import Control.Concurrent.Classy.QSemN+import Control.Monad.Conc.Class (MonadConc)++-- | @QSem@ is a quantity semaphore in which the resource is acquired+-- and released in units of one. It provides guaranteed FIFO ordering+-- for satisfying blocked 'waitQSem' calls.+--+-- The pattern+--+-- > bracket_ qaitQSem signalSSem (...)+--+-- is safe; it never loses a unit of the resource.+newtype QSem m = QSem (QSemN m)++-- | Build a new 'QSem' with a supplied initial quantity. The initial+-- quantity must be at least 0.+newQSem :: MonadConc m => Int -> m (QSem m)+newQSem initial+  | initial < 0 = fail "newQSem: Initial quantity mus tbe non-negative."+  | otherwise   = QSem <$> newQSemN initial++-- | Wait for a unit to become available.+waitQSem :: MonadConc m => QSem m -> m ()+waitQSem (QSem qSemN) = waitQSemN qSemN 1++-- | Signal that a unit of the 'QSem' is available.+signalQSem :: MonadConc m => QSem m -> m ()+signalQSem (QSem qSemN) = signalQSemN qSemN 1

@@ -0,0 +1,89 @@+-- | Quantity semaphores in which each thread may wait for an arbitrary+-- \"amount\".+module Control.Concurrent.Classy.QSemN+  ( -- * General Quantity Semaphores+    QSemN+  , newQSemN+  , waitQSemN+  , signalQSemN+  ) where++import Control.Monad.Conc.Class (MonadConc)+import Control.Concurrent.Classy.MVar+import Control.Monad.Catch (mask_, onException, uninterruptibleMask_)+import Data.Maybe++-- | 'QSemN' is a quantity semaphore in which the resource is aqcuired+-- and released in units of one. It provides guaranteed FIFO ordering+-- for satisfying blocked `waitQSemN` calls.+--+-- The pattern+--+-- > bracket_ (waitQSemN n) (signalQSemN n) (...)+--+-- is safe; it never loses any of the resource.+newtype QSemN m = QSemN (MVar m (Int, [(Int, MVar m ())], [(Int, MVar m ())]))++-- | Build a new 'QSemN' with a supplied initial quantity.+--  The initial quantity must be at least 0.+newQSemN :: MonadConc m => Int -> m (QSemN m)+newQSemN initial+  | initial < 0 = fail "newQSemN: Initial quantity must be non-negative"+  | otherwise   = QSemN <$> newMVar (initial, [], [])++-- | Wait for the specified quantity to become available+waitQSemN :: MonadConc m => QSemN m -> Int -> m ()+waitQSemN (QSemN m) sz = mask_ $ do+  (quantity, b1, b2) <- takeMVar m+  let remaining = quantity - sz+  if remaining < 0+  -- Enqueue and block the thread+  then do+    b <- newEmptyMVar+    putMVar m (quantity, b1, (sz,b):b2)+    wait b+  -- Claim the resource+  else+    putMVar m (remaining, b1, b2)++  where+    wait b = takeMVar b `onException` uninterruptibleMask_ (do+      (quantity, b1, b2) <- takeMVar m+      r  <- tryTakeMVar b+      r' <- if isJust r+           then signal sz (quantity, b1, b2)+           else putMVar b () >> pure (quantity, b1, b2)+      putMVar m r')++-- | Signal that a given quantity is now available from the 'QSemN'.+signalQSemN :: MonadConc m => QSemN m -> Int -> m ()+signalQSemN (QSemN m) sz = uninterruptibleMask_ $ do+  r  <- takeMVar m+  r' <- signal sz r+  putMVar m r'++-- | Fix the queue and signal as many threads as we can.+signal :: MonadConc m+  => Int+  -> (Int, [(Int,MVar m ())], [(Int,MVar m ())])+  -> m (Int, [(Int,MVar m ())], [(Int,MVar m ())])+signal sz0 (i,a1,a2) = loop (sz0 + i) a1 a2 where+  -- No more resource left, done.+  loop 0 bs b2 = pure (0,  bs, b2)++  -- Fix the queue+  loop sz [] [] = pure (sz, [], [])+  loop sz [] b2 = loop sz (reverse b2) []++  -- Signal as many threads as there is enough resource to satisfy,+  -- stopping as soon as one thread requires more resource than there+  -- is.+  loop sz ((j,b):bs) b2+    | j > sz = do+      r <- isEmptyMVar b+      if r then pure (sz, (j,b):bs, b2)+           else loop sz bs b2+    | otherwise = do+      r <- tryPutMVar b ()+      if r then loop (sz-j) bs b2+           else loop sz bs b2

@@ -0,0 +1,20 @@+-- | Classy software transactional memory.+module Control.Concurrent.Classy.STM+  ( module Control.Monad.STM.Class+  , module Control.Concurrent.Classy.STM.TVar+  , module Control.Concurrent.Classy.STM.TMVar+  , module Control.Concurrent.Classy.STM.TChan+  , module Control.Concurrent.Classy.STM.TQueue+  , module Control.Concurrent.Classy.STM.TBQueue+  , module Control.Concurrent.Classy.STM.TArray+  ) where++import Control.Monad.STM.Class+import Control.Concurrent.Classy.STM.TVar+import Control.Concurrent.Classy.STM.TMVar+import Control.Concurrent.Classy.STM.TChan+import Control.Concurrent.Classy.STM.TQueue+import Control.Concurrent.Classy.STM.TBQueue+import Control.Concurrent.Classy.STM.TArray++{-# ANN module ("HLint: ignore Use import/export shortcut" :: String) #-}

@@ -0,0 +1,48 @@+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}++-- | TArrays: transactional arrays, for use in STM-like monads.+--+-- __Deviations:__ @TArray@ as defined here does not have an @Eq@+-- instance, this is because the @MonadSTM@ @TVar@ type does not have+-- an @Eq@ constraint.+module Control.Concurrent.Classy.STM.TArray (TArray) where++import Data.Array (Array, bounds)+import Data.Array.Base (listArray, arrEleBottom, unsafeAt, MArray(..),+                        IArray(numElements))+import Data.Ix (rangeSize)++import Control.Monad.STM.Class++-- | @TArray@ is a transactional array, supporting the usual 'MArray'+-- interface for mutable arrays.+--+-- It is currently implemented as @Array ix (TVar stm e)@, but it may+-- be replaced by a more efficient implementation in the future (the+-- interface will remain the same, however).+newtype TArray stm i e = TArray (Array i (TVar stm e))++instance MonadSTM stm => MArray (TArray stm) e stm where+  getBounds (TArray a) = pure (bounds a)++  newArray b e = do+    a <- rep (rangeSize b) (newTVar e)+    pure $ TArray (listArray b a)++  newArray_ b = newArray b arrEleBottom++  unsafeRead  (TArray a) = readTVar  . unsafeAt a+  unsafeWrite (TArray a) = writeTVar . unsafeAt a++  getNumElements (TArray a) = pure (numElements a)++-- | Like 'replicateM' but uses an accumulator to prevent stack overflows.+-- Unlike 'replicateM' the returned list is in reversed order.  This+-- doesn't matter though since this function is only used to create+-- arrays with identical elements.+rep :: Monad m => Int -> m a -> m [a]+rep n m = go n [] where+  go 0 xs = pure xs+  go i xs = do+    x <- m+    go (i-1) (x:xs)

@@ -0,0 +1,138 @@+-- | 'TBQueue' is a bounded version of 'TQueue'. The queue has a maximum+-- capacity set when it is created.  If the queue already contains the+-- maximum number of elements, then 'writeTBQueue' blocks until an+-- element is removed from the queue.+--+-- The implementation is based on the traditional purely-functional+-- queue representation that uses two lists to obtain amortised /O(1)/+-- enqueue and dequeue operations.+--+-- __Deviations:__ @TBQueue@ as defined here does not have an @Eq@+-- instance, this is because the @MonadSTM@ @TVar@ type does not have+-- an @Eq@ constraint. Furthermore, the @newTBQueueIO@ function is not+-- provided.+module Control.Concurrent.Classy.STM.TBQueue+  ( -- * TBQueue+    TBQueue+  , newTBQueue+  , readTBQueue+  , tryReadTBQueue+  , peekTBQueue+  , tryPeekTBQueue+  , writeTBQueue+  , unGetTBQueue+  , isEmptyTBQueue+  , isFullTBQueue+  ) where++import Control.Monad.STM.Class++-- | 'TBQueue' is an abstract type representing a bounded FIFO+-- channel.+data TBQueue stm a+   = TBQueue (TVar stm Int)+             (TVar stm [a])+             (TVar stm Int)+             (TVar stm [a])++-- | Build and returns a new instance of 'TBQueue'+newTBQueue :: MonadSTM stm+  => Int   -- ^ maximum number of elements the queue can hold+  -> stm (TBQueue stm a)+newTBQueue size = do+  readT  <- newTVar []+  writeT <- newTVar []+  rsize <- newTVar 0+  wsize <- newTVar size+  pure (TBQueue rsize readT wsize writeT)++-- | Write a value to a 'TBQueue'; retries if the queue is full.+writeTBQueue :: MonadSTM stm => TBQueue stm a -> a -> stm ()+writeTBQueue (TBQueue rsize _ wsize writeT) a = do+  w <- readTVar wsize+  if w /= 0+  then writeTVar wsize (w - 1)+  else do+    r <- readTVar rsize+    if r /= 0+    then do+      writeTVar rsize 0+      writeTVar wsize (r - 1)+    else retry+  listend <- readTVar writeT+  writeTVar writeT (a:listend)++-- | Read the next value from the 'TBQueue'.+readTBQueue :: MonadSTM stm => TBQueue stm a -> stm a+readTBQueue (TBQueue rsize readT _ writeT) = do+  xs <- readTVar readT+  r  <- readTVar rsize+  writeTVar rsize (r + 1)+  case xs of+    (x:xs') -> do+      writeTVar readT xs'+      pure x+    [] -> do+      ys <- readTVar writeT+      case ys of+        [] -> retry+        _  -> do+          let (z:zs) = reverse ys+          writeTVar writeT []+          writeTVar readT zs+          pure z++-- | A version of 'readTBQueue' which does not retry. Instead it+-- returns @Nothing@ if no value is available.+tryReadTBQueue :: MonadSTM stm => TBQueue stm a -> stm (Maybe a)+tryReadTBQueue c = (Just <$> readTBQueue c) `orElse` pure Nothing++-- | Get the next value from the @TBQueue@ without removing it,+-- retrying if the channel is empty.+peekTBQueue :: MonadSTM stm => TBQueue stm a -> stm a+peekTBQueue c = do+  x <- readTBQueue c+  unGetTBQueue c x+  return x++-- | A version of 'peekTBQueue' which does not retry. Instead it+-- returns @Nothing@ if no value is available.+tryPeekTBQueue :: MonadSTM stm => TBQueue stm a -> stm (Maybe a)+tryPeekTBQueue c = do+  m <- tryReadTBQueue c+  case m of+    Nothing -> pure Nothing+    Just x  -> do+      unGetTBQueue c x+      pure m++-- | Put a data item back onto a channel, where it will be the next item read.+-- Retries if the queue is full.+unGetTBQueue :: MonadSTM stm => TBQueue stm a -> a -> stm ()+unGetTBQueue (TBQueue rsize readT wsize _) a = do+  r <- readTVar rsize+  if r > 0+  then writeTVar rsize (r - 1)+  else do+    w <- readTVar wsize+    if w > 0+    then writeTVar wsize (w - 1)+    else retry+  xs <- readTVar readT+  writeTVar readT (a:xs)++-- | Returns 'True' if the supplied 'TBQueue' is empty.+isEmptyTBQueue :: MonadSTM stm => TBQueue stm a -> stm Bool+isEmptyTBQueue (TBQueue _ readT _ writeT) = do+  xs <- readTVar readT+  case xs of+    (_:_) -> pure False+    [] -> null <$> readTVar writeT++-- | Returns 'True' if the supplied 'TBQueue' is full.+isFullTBQueue :: MonadSTM stm => TBQueue stm a -> stm Bool+isFullTBQueue (TBQueue rsize _ wsize _) = do+  w <- readTVar wsize+  if w > 0+  then pure False+  else (>0) <$> readTVar rsize

@@ -0,0 +1,127 @@+-- | Transactional channels+--+-- __Deviations:__ @TChan@ as defined here does not have an @Eq@+-- instance, this is because the @MonadSTM@ @TVar@ type does not have+-- an @Eq@ constraint. Furthermore, the @newTChanIO@ and+-- @newBroadcastTChanIO@ functions are not provided.+module Control.Concurrent.Classy.STM.TChan+  ( -- * TChans+    TChan++  -- * Construction+  , newTChan+  , newBroadcastTChan+  , dupTChan+  , cloneTChan++  -- * Reading and writing+  , readTChan+  , tryReadTChan+  , peekTChan+  , tryPeekTChan+  , writeTChan+  , unGetTChan+  , isEmptyTChan+  ) where++import Control.Monad.STM.Class++-- | 'TChan' is an abstract type representing an unbounded FIFO+-- channel.+data TChan stm a = TChan (TVar stm (TVarList stm a))+                         (TVar stm (TVarList stm a))++type TVarList stm a = TVar stm (TList stm a)+data TList stm a = TNil | TCons a (TVarList stm a)++-- |Build and return a new instance of 'TChan'+newTChan :: MonadSTM stm => stm (TChan stm a)+newTChan = do+  hole   <- newTVar TNil+  readH  <- newTVar hole+  writeH <- newTVar hole+  pure (TChan readH writeH)++-- | Create a write-only 'TChan'.  More precisely, 'readTChan' will 'retry'+-- even after items have been written to the channel.  The only way to+-- read a broadcast channel is to duplicate it with 'dupTChan'.+newBroadcastTChan :: MonadSTM stm => stm (TChan stm a)+newBroadcastTChan = do+    hole   <- newTVar TNil+    readT  <- newTVar (error "reading from a TChan created by newBroadcastTChan; use dupTChan first")+    writeT <- newTVar hole+    pure (TChan readT writeT)++-- | Write a value to a 'TChan'.+writeTChan :: MonadSTM stm => TChan stm a -> a -> stm ()+writeTChan (TChan _ writeT) a = do+  listend  <- readTVar writeT+  listend' <- newTVar TNil+  writeTVar listend (TCons a listend')+  writeTVar writeT listend'++-- | Read the next value from the 'TChan'.+readTChan :: MonadSTM stm => TChan stm a -> stm a+readTChan tchan = tryReadTChan tchan >>= maybe retry pure++-- | A version of 'readTChan' which does not retry. Instead it+-- returns @Nothing@ if no value is available.+tryReadTChan :: MonadSTM stm => TChan stm a -> stm (Maybe a)+tryReadTChan (TChan readT _) = do+  listhead <- readTVar readT+  hd <- readTVar listhead+  case hd of+    TNil       -> pure Nothing+    TCons a tl -> do+      writeTVar readT tl+      pure (Just a)++-- | Get the next value from the 'TChan' without removing it,+-- retrying if the channel is empty.+peekTChan :: MonadSTM stm => TChan stm a -> stm a+peekTChan tchan = tryPeekTChan tchan >>= maybe retry pure++-- | A version of 'peekTChan' which does not retry. Instead it+-- returns @Nothing@ if no value is available.+tryPeekTChan :: MonadSTM stm => TChan stm a -> stm (Maybe a)+tryPeekTChan (TChan readT _) = do+  listhead <- readTVar readT+  hd <- readTVar listhead+  pure $ case hd of+    TNil      -> Nothing+    TCons a _ -> Just a++-- | Duplicate a 'TChan': the duplicate channel begins empty, but data written to+-- either channel from then on will be available from both.  Hence+-- this creates a kind of broadcast channel, where data written by+-- anyone is seen by everyone else.+dupTChan :: MonadSTM stm => TChan stm a -> stm (TChan stm a)+dupTChan (TChan _ writeT) = do+  hole   <- readTVar writeT+  readT' <- newTVar hole+  return (TChan readT' writeT)++-- | Put a data item back onto a channel, where it will be the next+-- item read.+unGetTChan :: MonadSTM stm => TChan stm a -> a -> stm ()+unGetTChan (TChan readT _) a = do+   listhead <- readTVar readT+   head' <- newTVar (TCons a listhead)+   writeTVar readT head'++-- | Returns 'True' if the supplied 'TChan' is empty.+isEmptyTChan :: MonadSTM stm => TChan stm a -> stm Bool+isEmptyTChan (TChan readT _) = do+  listhead <- readTVar readT+  hd <- readTVar listhead+  pure $ case hd of+    TNil -> True+    TCons _ _ -> False++-- | Clone a 'TChan': similar to 'dupTChan', but the cloned channel starts with the+-- same content available as the original channel.+cloneTChan :: MonadSTM stm => TChan stm a -> stm (TChan stm a)+cloneTChan (TChan readT writeT) = do+  readpos <- readTVar readT+  readT' <- newTVar readpos+  pure (TChan readT' writeT)

@@ -0,0 +1,110 @@+-- | Transactional @MVar@s, for use with 'MonadSTM'.+--+-- __Deviations:__ @TMVar@ as defined here does not have an @Eq@+-- instance, this is because the @MonadSTM@ @TVar@ type does not have+-- an @Eq@ constraint. Furthermore, the @newTMVarIO@,+-- @newEmptyTMVarIO@, and @mkWeakTMVar@ functions are not provided.+module Control.Concurrent.Classy.STM.TMVar+  ( -- * @TMVar@s+    TMVar+  , newTMVar+  , newTMVarN+  , newEmptyTMVar+  , newEmptyTMVarN+  , takeTMVar+  , putTMVar+  , readTMVar+  , tryTakeTMVar+  , tryPutTMVar+  , tryReadTMVar+  , isEmptyTMVar+  , swapTMVar+  ) where++import Control.Monad (liftM, when, unless)+import Control.Monad.STM.Class+import Data.Maybe (isJust, isNothing)++-- | A @TMVar@ is like an @MVar@ or a @mVar@, but using transactional+-- memory. As transactions are atomic, this makes dealing with+-- multiple @TMVar@s easier than wrangling multiple @mVar@s.+newtype TMVar stm a = TMVar (TVar stm (Maybe a))++-- | Create a 'TMVar' containing the given value.+newTMVar :: MonadSTM stm => a -> stm (TMVar stm a)+newTMVar = newTMVarN ""++-- | Create a 'TMVar' containing the given value, with the given+-- name.+--+-- Name conflicts are handled as usual for 'TVar's. The name is+-- prefixed with \"ctmvar-\".+newTMVarN :: MonadSTM stm => String -> a -> stm (TMVar stm a)+newTMVarN n a = do+  let n' = if null n then "ctmvar" else "ctmvar-" ++ n+  ctvar <- newTVarN n' $ Just a+  return $ TMVar ctvar++-- | Create a new empty 'TMVar'.+newEmptyTMVar :: MonadSTM stm => stm (TMVar stm a)+newEmptyTMVar = newEmptyTMVarN ""++-- | Create a new empty 'TMVar' with the given name.+--+-- Name conflicts are handled as usual for 'TVar's. The name is+-- prefixed with \"ctmvar-\".+newEmptyTMVarN :: MonadSTM stm => String -> stm (TMVar stm a)+newEmptyTMVarN n = do+  let n' = if null n then "ctmvar" else "ctmvar-" ++ n+  ctvar <- newTVarN n' Nothing+  return $ TMVar ctvar++-- | Take the contents of a 'TMVar', or 'retry' if it is empty.+takeTMVar :: MonadSTM stm => TMVar stm a -> stm a+takeTMVar ctmvar = do+  taken <- tryTakeTMVar ctmvar+  maybe retry return taken++-- | Write to a 'TMVar', or 'retry' if it is full.+putTMVar :: MonadSTM stm => TMVar stm a -> a -> stm ()+putTMVar ctmvar a = do+  putted <- tryPutTMVar ctmvar a+  unless putted retry++-- | Read from a 'TMVar' without emptying, or 'retry' if it is empty.+readTMVar :: MonadSTM stm => TMVar stm a -> stm a+readTMVar ctmvar = do+  readed <- tryReadTMVar ctmvar+  maybe retry return readed++-- | Try to take the contents of a 'TMVar', returning 'Nothing' if it+-- is empty.+tryTakeTMVar :: MonadSTM stm => TMVar stm a -> stm (Maybe a)+tryTakeTMVar (TMVar ctvar) = do+  val <- readTVar ctvar+  when (isJust val) $ writeTVar ctvar Nothing+  return val++-- | Try to write to a 'TMVar', returning 'False' if it is full.+tryPutTMVar :: MonadSTM stm => TMVar stm a -> a -> stm Bool+tryPutTMVar (TMVar ctvar) a = do+  val <- readTVar ctvar+  when (isNothing val) $ writeTVar ctvar (Just a)+  return $ isNothing val++-- | Try to read from a 'TMVar' without emptying, returning 'Nothing'+-- if it is empty.+tryReadTMVar :: MonadSTM stm => TMVar stm a -> stm (Maybe a)+tryReadTMVar (TMVar ctvar) = readTVar ctvar++-- | Check if a 'TMVar' is empty or not.+isEmptyTMVar :: MonadSTM stm => TMVar stm a -> stm Bool+isEmptyTMVar ctmvar = isNothing `liftM` tryReadTMVar ctmvar++-- | Swap the contents of a 'TMVar' returning the old contents, or+-- 'retry' if it is empty.+swapTMVar :: MonadSTM stm => TMVar stm a -> a -> stm a+swapTMVar ctmvar a = do+  val <- takeTMVar ctmvar+  putTMVar ctmvar a+  return val

@@ -0,0 +1,105 @@+-- | A 'TQueue' is like a 'TChan', with two important differences:+--+--  * it has faster throughput than both 'TChan' and 'Chan' (although+--    the costs are amortised, so the cost of individual operations+--    can vary a lot).+--+--  * it does /not/ provide equivalents of the 'dupTChan' and+--    'cloneTChan' operations.+--+-- The implementation is based on the traditional purely-functional+-- queue representation that uses two lists to obtain amortised /O(1)/+-- enqueue and dequeue operations.+--+-- __Deviations:__ @TQueue@ as defined here does not have an @Eq@+-- instance, this is because the @MonadSTM@ @TVar@ type does not have+-- an @Eq@ constraint. Furthermore, the @newTQueueIO@ function is not+-- provided.+module Control.Concurrent.Classy.STM.TQueue+  ( -- * TQueue+    TQueue+  , newTQueue+  , readTQueue+  , tryReadTQueue+  , peekTQueue+  , tryPeekTQueue+  , writeTQueue+  , unGetTQueue+  , isEmptyTQueue+  ) where++import Control.Monad.STM.Class++-- | 'TQueue' is an abstract type representing an unbounded FIFO channel.+data TQueue stm a = TQueue (TVar stm [a])+                           (TVar stm [a])++-- | Build and returns a new instance of 'TQueue'+newTQueue :: MonadSTM stm => stm (TQueue stm a)+newTQueue = do+  readT  <- newTVar []+  writeT <- newTVar []+  pure (TQueue readT writeT)++-- | Write a value to a 'TQueue'.+writeTQueue :: MonadSTM stm => TQueue stm a -> a -> stm ()+writeTQueue (TQueue _ writeT) a = do+  listend <- readTVar writeT+  writeTVar writeT (a:listend)++-- | Read the next value from the 'TQueue'.+readTQueue :: MonadSTM stm => TQueue stm a -> stm a+readTQueue (TQueue readT writeT) = do+  xs <- readTVar readT+  case xs of+    (x:xs') -> do+      writeTVar readT xs'+      pure x+    [] -> do+      ys <- readTVar writeT+      case ys of+        [] -> retry+        _  -> case reverse ys of+               [] -> error "readTQueue"+               (z:zs) -> do+                 writeTVar writeT []+                 writeTVar readT zs+                 pure z++-- | A version of 'readTQueue' which does not retry. Instead it+-- returns @Nothing@ if no value is available.+tryReadTQueue :: MonadSTM stm => TQueue stm a -> stm (Maybe a)+tryReadTQueue c = (Just <$> readTQueue c) `orElse` pure Nothing++-- | Get the next value from the @TQueue@ without removing it,+-- retrying if the channel is empty.+peekTQueue :: MonadSTM stm => TQueue stm a -> stm a+peekTQueue c = do+  x <- readTQueue c+  unGetTQueue c x+  pure x++-- | A version of 'peekTQueue' which does not retry. Instead it+-- returns @Nothing@ if no value is available.+tryPeekTQueue :: MonadSTM stm => TQueue stm a -> stm (Maybe a)+tryPeekTQueue c = do+  m <- tryReadTQueue c+  case m of+    Nothing -> pure Nothing+    Just x  -> do+      unGetTQueue c x+      pure m++-- |Put a data item back onto a channel, where it will be the next item read.+unGetTQueue :: MonadSTM stm => TQueue stm a -> a -> stm ()+unGetTQueue (TQueue readT _) a = do+  xs <- readTVar readT+  writeTVar readT (a:xs)++-- |Returns 'True' if the supplied 'TQueue' is empty.+isEmptyTQueue :: MonadSTM stm => TQueue stm a -> stm Bool+isEmptyTQueue (TQueue readT writeT) = do+  xs <- readTVar readT+  case xs of+    (_:_) -> pure False+    [] -> null <$> readTVar writeT

@@ -0,0 +1,54 @@+-- | Transactional variables, for use with 'MonadSTM'.+--+-- __Deviations:__ There is no @Eq@ instance for @MonadSTM@ the @TVar@+-- type. Furthermore, the @newTVarIO@ and @mkWeakTVar@ functions are+-- not provided.+module Control.Concurrent.Classy.STM.TVar+  ( -- * @TVar@s+    TVar+  , newTVar+  , newTVarN+  , readTVar+  , readTVarConc+  , writeTVar+  , modifyTVar+  , modifyTVar'+  , swapTVar+  , registerDelay+  ) where++import Control.Monad.STM.Class+import Control.Monad.Conc.Class+import Data.Functor (void)++-- * @TVar@s++-- | Mutate the contents of a 'TVar'. This is non-strict.+modifyTVar :: MonadSTM stm => TVar stm a -> (a -> a) -> stm ()+modifyTVar ctvar f = do+  a <- readTVar ctvar+  writeTVar ctvar $ f a++-- | Mutate the contents of a 'TVar' strictly.+modifyTVar' :: MonadSTM stm => TVar stm a -> (a -> a) -> stm ()+modifyTVar' ctvar f = do+  a <- readTVar ctvar+  writeTVar ctvar $! f a++-- | Swap the contents of a 'TVar', returning the old value.+swapTVar :: MonadSTM stm => TVar stm a -> a -> stm a+swapTVar ctvar a = do+  old <- readTVar ctvar+  writeTVar ctvar a+  return old++-- | Set the value of returned 'TVar' to @True@ after a given number+-- of microseconds. The caveats associated with 'threadDelay' also+-- apply.+registerDelay :: MonadConc m => Int -> m (TVar (STM m) Bool)+registerDelay delay = do+  var <- atomically (newTVar False)+  void . fork $ do+    threadDelay delay+    atomically (writeTVar var True)+  pure var

@@ -1,86 +0,0 @@--- | 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

@@ -1,34 +0,0 @@--- | 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

@@ -1,54 +1,88 @@ {-# LANGUAGE CPP              #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE RankNTypes       #-}+{-# LANGUAGE TemplateHaskell  #-} {-# LANGUAGE TypeFamilies     #-}  -- | This module captures in a typeclass the interface of concurrency -- monads.+--+-- __Deviations:__ An instance of @MonadCoonc@ is not required to be+-- an instance of @MonadFix@, unlike @IO@. The @CRef@, @MVar@, and+-- @Ticket@ types are not required to be instances of @Show@ or @Eq@,+-- unlike their normal counterparts. The @threadCapability@,+-- @threadWaitRead@, @threadWaitWrite@, @threadWaitReadSTM@,+-- @threadWaitWriteSTM@, and @mkWeakThreadId@ functions are not+-- provided. The @threadDelay@ function is not required to delay the+-- thread, merely to yield it. Bound threads are not supported. The+-- @BlockedIndefinitelyOnMVar@ (and similar) exceptions are /not/+-- thrown during testing, so do not rely on them at all. module Control.Monad.Conc.Class   ( MonadConc(..) -  -- * Utilities+  -- * Threads   , spawn   , forkFinally   , killThread-  , cas -  -- * Bound Threads+  -- ** Named Threads+  , forkN+  , forkOnN+  , lineNum +  -- ** Bound Threads+   -- | @MonadConc@ does not support bound threads, if you need that   -- sort of thing you will have to use regular @IO@.    , rtsSupportsBoundThreads   , isCurrentThreadBound++  -- * Exceptions+  , throw+  , catch+  , mask+  , uninterruptibleMask++  -- * Mutable State+  , newMVar+  , newMVarN+  , cas++  -- * Utilities for instance writers+  , makeTransConc+  , liftedF+  , liftedFork   ) where -import Control.Concurrent (forkIO)-import Control.Concurrent.MVar (MVar, readMVar, newEmptyMVar, putMVar, tryPutMVar, takeMVar, tryTakeMVar)+-- for the class and utilities 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, writeIORef, atomicWriteIORef)--import qualified Control.Concurrent as C import qualified Control.Monad.Catch as Ca+import Control.Monad.STM.Class (MonadSTM, TVar, readTVar)+import Control.Monad.Trans.Control (MonadTransControl, StT, liftWith)+import Data.Typeable (Typeable)+import Language.Haskell.TH (Q, DecsQ, Exp, Loc(..), Info(VarI), Name, Type(..), reify, location, varE)++-- for the 'IO' instance+import qualified Control.Concurrent as IO+import qualified Control.Concurrent.STM.TVar as IO+import qualified Control.Monad.STM as IO+import qualified Data.Atomics as IO+import qualified Data.IORef as IO++-- for the transformer instances+import Control.Monad.Reader (ReaderT)+import Control.Monad.Trans (lift)+import Control.Monad.Trans.Identity (IdentityT) 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-import qualified Data.Atomics as A -#if __GLASGOW_HASKELL__ < 710-import Control.Applicative (Applicative)-import Data.Monoid (Monoid, mempty)-#endif+{-# ANN module ("HLint: ignore Use const" :: String) #-}  -- | @MonadConc@ is an abstraction over GHC's typical concurrency -- abstraction. It captures the interface of concurrency monads in@@ -59,20 +93,45 @@ -- 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+      , MonadSTM (STM m)+      , Ord (ThreadId m), Show (ThreadId m)) => MonadConc m  where++  {-# MINIMAL+        (forkWithUnmask | forkWithUnmaskN)+      , (forkOnWithUnmask | forkOnWithUnmaskN)+      , getNumCapabilities+      , setNumCapabilities+      , myThreadId+      , yield+      , (newEmptyMVar | newEmptyMVarN)+      , putMVar+      , tryPutMVar+      , readMVar+      , takeMVar+      , tryTakeMVar+      , (newCRef | newCRefN)+      , atomicModifyCRef+      , writeCRef+      , readForCAS+      , peekTicket+      , casCRef+      , modifyCRefCAS+      , atomically+      , throwTo+    #-}+   -- | The associated 'MonadSTM' for this class.-  type STMLike m :: * -> *+  type STM 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 :: * -> *+  -- @MVar@ will block until it is full, and attempting to put to a+  -- \"full\" @MVar@ will block until it is empty.+  type MVar m :: * -> *    -- | The mutable non-blocking reference type. These may suffer from   -- relaxed memory effects if functions outside the set @newCRef@,-  -- @readCRef@, @modifyCRef@, and @atomicWriteCRef@ are used.+  -- @readCRef@, @atomicModifyCRef@, and @atomicWriteCRef@ are used.   type CRef m :: * -> *    -- | When performing compare-and-swap operations on @CRef@s, a@@ -84,7 +143,7 @@   type ThreadId m :: *    -- | Fork a computation to happen concurrently. Communication may-  -- happen over @CVar@s.+  -- happen over @MVar@s.   --   -- > fork ma = forkWithUnmask (\_ -> ma)   fork :: m () -> m (ThreadId m)@@ -93,8 +152,22 @@   -- | 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 = forkWithUnmaskN ""   forkWithUnmask :: ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)+  forkWithUnmask = forkWithUnmaskN "" +  -- | Like 'forkWithUnmask', but the thread is given a name which may+  -- be used to present more useful debugging information.+  --+  -- If an empty name is given, the @ThreadId@ is used. If names+  -- conflict, successive threads with the same name are given a+  -- numeric suffix, counting up from 1.+  --+  -- > forkWithUnmaskN _ = forkWithUnmask+  forkWithUnmaskN :: String -> ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)+  forkWithUnmaskN _ = forkWithUnmask+   -- | 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@@ -105,10 +178,20 @@   forkOn :: Int -> m () -> m (ThreadId m)   forkOn c ma = forkOnWithUnmask c (\_ -> ma) -  -- | Like 'forkWithUnmask' but the child thread is pinned to the+  -- | Like 'forkWithUnmask', but the child thread is pinned to the   -- given CPU, as with 'forkOn'.+  --+  -- > forkOnWithUnmask = forkOnWithUnmaskN ""   forkOnWithUnmask :: Int -> ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)+  forkOnWithUnmask = forkOnWithUnmaskN "" +  -- | Like 'forkWithUnmaskN', but the child thread is pinned to the+  -- given CPU, as with 'forkOn'.+  --+  -- > forkOnWithUnmaskN _ = forkOnWithUnmask+  forkOnWithUnmaskN :: String -> Int -> ((forall a. m a -> m a) -> m ()) -> m (ThreadId m)+  forkOnWithUnmaskN _ = forkOnWithUnmask+   -- | Get the number of Haskell threads that can run simultaneously.   getNumCapabilities :: m Int @@ -122,37 +205,76 @@   -- (if any).   yield :: m () -  -- | Create a new empty @CVar@.-  newEmptyCVar :: m (CVar m a)+  -- | Yields the current thread, and optionally suspends the current+  -- thread for a given number of microseconds.+  --+  -- If suspended, there is no guarantee that the thread will be+  -- rescheduled promptly when the delay has expired, but the thread+  -- will never continue to run earlier than specified.+  --+  -- > threadDelay _ = yield+  threadDelay :: Int -> m ()+  threadDelay _ = yield -  -- | Put a value into a @CVar@. If there is already a value there,+  -- | Create a new empty @MVar@.+  --+  -- > newEmptyMVar = newEmptyMVarN ""+  newEmptyMVar :: m (MVar m a)+  newEmptyMVar = newEmptyMVarN ""++  -- | Create a new empty @MVar@, but it is given a name which may be+  -- used to present more useful debugging information.+  --+  -- If an empty name is given, a counter starting from 0 is used. If+  -- names conflict, successive @MVar@s with the same name are given a+  -- numeric suffix, counting up from 1.+  --+  -- > newEmptyMVarN _ = newEmptyMVar+  newEmptyMVarN :: String -> m (MVar m a)+  newEmptyMVarN _ = newEmptyMVar++  -- | Put a value into a @MVar@. 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 ()+  putMVar :: MVar 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,+  -- | Attempt to put a value in a @MVar@ non-blockingly, returning+  -- 'True' (and filling the @MVar@) if there was nothing there,   -- otherwise returning 'False'.-  tryPutCVar :: CVar m a -> a -> m Bool+  tryPutMVar :: MVar m a -> a -> m Bool -  -- | Block until a value is present in the @CVar@, and then return+  -- | Block until a value is present in the @MVar@, and then return   -- it. As with 'readMVar', this does not \"remove\" the value,   -- multiple reads are possible.-  readCVar :: CVar m a -> m a+  readMVar :: MVar m a -> m a -  -- | Take a value from a @CVar@. This \"empties\" the @CVar@,+  -- | Take a value from a @MVar@. This \"empties\" the @MVar@,   -- 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+  -- value in the @MVar@ already, until one has been put.+  takeMVar :: MVar 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,+  -- | Attempt to take a value from a @MVar@ non-blockingly, returning+  -- a 'Just' (and emptying the @MVar@) if there was something there,   -- otherwise returning 'Nothing'.-  tryTakeCVar :: CVar m a -> m (Maybe a)+  tryTakeMVar :: MVar m a -> m (Maybe a)    -- | Create a new reference.+  --+  -- > newCRef = newCRefN ""   newCRef :: a -> m (CRef m a)+  newCRef = newCRefN "" +  -- | Create a new reference, but it is given a name which may be+  -- used to present more useful debugging information.+  --+  -- If an empty name is given, a counter starting from 0 is used. If+  -- names conflict, successive @CRef@s with the same name are given a+  -- numeric suffix, counting up from 1.+  --+  -- > newCRefN _ = newCRef+  newCRefN :: String -> a -> m (CRef m a)+  newCRefN _ = newCRef+   -- | Read the current value stored in a reference.   --   -- > readCRef cref = readForCAS cref >>= peekTicket@@ -161,18 +283,18 @@    -- | Atomically modify the value stored in a reference. This imposes   -- a full memory barrier.-  modifyCRef :: CRef m a -> (a -> (a, b)) -> m b+  atomicModifyCRef :: CRef m a -> (a -> (a, b)) -> m b    -- | Write a new value into an @CRef@, without imposing a memory   -- barrier. This means that relaxed memory effects can be observed.   writeCRef :: CRef m a -> a -> m ()    -- | Replace the value stored in a reference, with the-  -- barrier-to-reordering property that 'modifyCRef' has.+  -- barrier-to-reordering property that 'atomicModifyCRef' has.   ---  -- > atomicWriteCRef r a = modifyCRef r $ const (a, ())+  -- > atomicWriteCRef r a = atomicModifyCRef r $ const (a, ())   atomicWriteCRef :: CRef m a -> a -> m ()-  atomicWriteCRef r a = modifyCRef r $ const (a, ())+  atomicWriteCRef r a = atomicModifyCRef r $ const (a, ())    -- | Read the current value stored in a reference, returning a   -- @Ticket@, for use in future compare-and-swap operations.@@ -192,7 +314,7 @@   -- This is strict in the \"new\" value argument.   casCRef :: CRef m a -> Ticket m a -> a -> m (Bool, Ticket m a) -  -- | A replacement for 'modifyCRef' using a compare-and-swap.+  -- | A replacement for 'atomicModifyCRef' using a compare-and-swap.   --   -- This is strict in the \"new\" value argument.   modifyCRefCAS :: CRef m a -> (a -> (a, b)) -> m b@@ -204,76 +326,35 @@   modifyCRefCAS_ cref f = modifyCRefCAS cref (\a -> (f 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+  atomically :: STM m a -> m a -  -- | 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'.+  -- | Read the current value stored in a @TVar@. This may be+  -- implemented differently for speed.   ---  -- > catch = Control.Monad.Catch.catch-  catch :: Exception e => m a -> (e -> m a) -> m a-  catch = Ca.catch+  -- > readTVarConc = atomically . readTVar+  readTVarConc :: TVar (STM m) a -> m a+  readTVarConc = atomically . readTVar    -- | 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-   -- | 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.+  -- the thread has a reference to the provided @MVar@ or @TVar@. This+  -- function may be called multiple times, to add new knowledge to+  -- the system. It does not need to be called when @MVar@s or @TVar@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 ()+  -- > _concKnowsAbout _ = pure ()+  _concKnowsAbout :: Either (MVar m a) (TVar (STM m) a) -> m ()+  _concKnowsAbout _ = pure ()    -- | Does nothing.   --@@ -285,9 +366,9 @@   -- 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 ()+  -- > _concForgets _ = pure ()+  _concForgets :: Either (MVar m a) (TVar (STM m) a) -> m ()+  _concForgets _ = pure ()    -- | Does nothing.   --@@ -296,55 +377,50 @@   -- '_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+  -- If a thread receives references to @MVar@s or @TVar@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 = pure ()   _concAllKnown :: m ()-  _concAllKnown = return ()+  _concAllKnown = pure () -instance MonadConc IO where-  type STMLike  IO = STM-  type CVar     IO = MVar-  type CRef     IO = IORef-  type Ticket   IO = A.Ticket-  type ThreadId IO = C.ThreadId+  -- | Does nothing.+  --+  -- During testing, records a message which shows up in the trace.+  --+  -- > _concMessage _ = pure ()+  _concMessage :: Typeable a => a -> m ()+  _concMessage _ = pure () -  readCVar       = readMVar-  fork           = forkIO-  forkWithUnmask = C.forkIOWithUnmask-  forkOn         = C.forkOn-  forkOnWithUnmask = C.forkOnWithUnmask-  getNumCapabilities = C.getNumCapabilities-  setNumCapabilities = C.setNumCapabilities-  myThreadId     = C.myThreadId-  yield          = C.yield-  throwTo        = C.throwTo-  newEmptyCVar   = newEmptyMVar-  putCVar        = putMVar-  tryPutCVar     = tryPutMVar-  takeCVar       = takeMVar-  tryTakeCVar    = tryTakeMVar-  newCRef        = newIORef-  readCRef       = readIORef-  modifyCRef     = atomicModifyIORef-  writeCRef      = writeIORef-  atomicWriteCRef = atomicWriteIORef-  readForCAS     = A.readForCAS-  peekTicket     = return . A.peekTicket-  casCRef        = A.casIORef-  modifyCRefCAS  = A.atomicModifyIORefCAS-  atomically     = S.atomically+-------------------------------------------------------------------------------+-- Utilities +-- | Get the current line number as a String. Useful for automatically+-- naming threads, @MVar@s, and @CRef@s.+--+-- Example usage:+--+-- > forkN $lineNum ...+--+-- Unfortunately this can't be packaged up into a+-- @forkL@/@forkOnL@/etc set of functions, because this imposes a+-- 'Lift' constraint on the monad, which 'IO' does not have.+lineNum :: Q Exp+lineNum = do+  line <- show . fst . loc_start <$> location+  [| line |]++-- Threads+ -- | 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)+-- return a @MVar@ which can be used to query the result.+spawn :: MonadConc m => m a -> m (MVar m a) spawn ma = do-  cvar <- newEmptyCVar-  _ <- fork $ _concKnowsAbout (Left cvar) >> ma >>= putCVar cvar-  return cvar+  cvar <- newEmptyMVar+  _ <- fork $ _concKnowsAbout (Left cvar) >> ma >>= putMVar cvar+  pure cvar  -- | Fork a thread and call the supplied function when the thread is -- about to terminate, with an exception or a returned value. The@@ -363,303 +439,285 @@ killThread :: MonadConc m => ThreadId m -> m () killThread tid = throwTo tid ThreadKilled +-- | Like 'fork', but the thread is given a name which may be used to+-- present more useful debugging information.+--+-- If no name is given, the @ThreadId@ is used. If names conflict,+-- successive threads with the same name are given a numeric suffix,+-- counting up from 1.+forkN :: MonadConc m => String -> m () -> m (ThreadId m)+forkN name ma = forkWithUnmaskN name (\_ -> ma)++-- | Like 'forkOn', but the thread is given a name which may be used+-- to present more useful debugging information.+--+-- If no name is given, the @ThreadId@ is used. If names conflict,+-- successive threads with the same name are given a numeric suffix,+-- counting up from 1.+forkOnN :: MonadConc m => String -> Int -> m () -> m (ThreadId m)+forkOnN name i ma = forkOnWithUnmaskN name i (\_ -> ma)++-- Bound Threads+ -- | Provided for compatibility, always returns 'False'. rtsSupportsBoundThreads :: Bool rtsSupportsBoundThreads = False  -- | Provided for compatibility, always returns 'False'. isCurrentThreadBound :: MonadConc m => m Bool-isCurrentThreadBound = return False+isCurrentThreadBound = pure False --- | Compare-and-swap a value in a @CRef@, returning an indication of--- success and the new value.-cas :: MonadConc m => CRef m a -> a -> m (Bool, a)-cas cref a = do-  tick         <- readForCAS cref-  (suc, tick') <- casCRef cref tick a-  a'           <- peekTicket tick'+-- Exceptions -  return (suc, 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 :: (MonadConc m, Exception e) => e -> m a+throw = Ca.throwM ----------------------------------------------------------------------------------- Transformer instances+-- | 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 :: (MonadConc m, Exception e) => m a -> (e -> m a) -> m a+catch = Ca.catch -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 Ticket   (ReaderT r m) = Ticket m-  type ThreadId (ReaderT r m) = ThreadId 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 :: MonadConc m => ((forall a. m a -> m a) -> m b) -> m b+mask = Ca.mask -  fork              = reader fork-  forkOn i          = reader (forkOn i)-  forkWithUnmask ma = ReaderT $ \r -> forkWithUnmask (\f -> runReaderT (ma $ reader f) r)-  forkOnWithUnmask i ma = ReaderT $ \r -> forkOnWithUnmask i (\f -> runReaderT (ma $ reader f) r)+-- | 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 :: MonadConc m => ((forall a. m a -> m a) -> m b) -> m b+uninterruptibleMask = Ca.uninterruptibleMask -  getNumCapabilities = lift getNumCapabilities-  setNumCapabilities = lift . setNumCapabilities-  myThreadId         = lift myThreadId-  yield              = lift yield-  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-  writeCRef r        = lift . writeCRef r-  atomicWriteCRef r  = lift . atomicWriteCRef r-  readForCAS         = lift . readForCAS-  peekTicket         = lift . peekTicket-  casCRef r t        = lift . casCRef r t-  modifyCRefCAS r    = lift . modifyCRefCAS r-  atomically         = lift . atomically-  _concKnowsAbout    = lift . _concKnowsAbout-  _concForgets       = lift . _concForgets-  _concAllKnown      = lift _concAllKnown+-- Mutable Variables -reader :: Monad m => (m a -> m b) -> ReaderT r m a -> ReaderT r m b-reader f ma = ReaderT $ \r -> f (runReaderT ma r)+-- | Create a new @MVar@ containing a value.+newMVar :: MonadConc m => a -> m (MVar m a)+newMVar a = do+  cvar <- newEmptyMVar+  putMVar cvar a+  pure cvar -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 Ticket   (WL.WriterT w m) = Ticket m-  type ThreadId (WL.WriterT w m) = ThreadId m+-- | Create a new @MVar@ containing a value, but it is given a name+-- which may be used to present more useful debugging information.+--+-- If no name is given, a counter starting from 0 is used. If names+-- conflict, successive @MVar@s with the same name are given a numeric+-- suffix, counting up from 1.+newMVarN :: MonadConc m => String -> a -> m (MVar m a)+newMVarN n a = do+  cvar <- newEmptyMVarN n+  putMVar cvar a+  pure cvar -  fork              = writerlazy fork-  forkOn i          = writerlazy (forkOn i)-  forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WL.runWriterT (ma $ writerlazy f))-  forkOnWithUnmask i ma = lift $ forkOnWithUnmask i (\f -> fst `liftM` WL.runWriterT (ma $ writerlazy f))+-- | Compare-and-swap a value in a @CRef@, returning an indication of+-- success and the new value.+cas :: MonadConc m => CRef m a -> a -> m (Bool, a)+cas cref a = do+  tick         <- readForCAS cref+  (suc, tick') <- casCRef cref tick a+  a'           <- peekTicket tick' -  getNumCapabilities = lift getNumCapabilities-  setNumCapabilities = lift . setNumCapabilities-  myThreadId         = lift myThreadId-  yield              = lift yield-  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-  writeCRef r        = lift . writeCRef r-  atomicWriteCRef r  = lift . atomicWriteCRef r-  readForCAS         = lift . readForCAS-  peekTicket         = lift . peekTicket-  casCRef r t        = lift . casCRef r t-  modifyCRefCAS r    = lift . modifyCRefCAS r-  atomically         = lift . atomically-  _concKnowsAbout    = lift . _concKnowsAbout-  _concForgets       = lift . _concForgets-  _concAllKnown      = lift _concAllKnown+  pure (suc, a') -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+-------------------------------------------------------------------------------+-- Concrete instances -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 Ticket   (WS.WriterT w m) = Ticket m-  type ThreadId (WS.WriterT w m) = ThreadId m+instance MonadConc IO where+  type STM      IO = IO.STM+  type MVar     IO = IO.MVar+  type CRef     IO = IO.IORef+  type Ticket   IO = IO.Ticket+  type ThreadId IO = IO.ThreadId -  fork              = writerstrict fork-  forkOn i          = writerstrict (forkOn i)-  forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WS.runWriterT (ma $ writerstrict f))-  forkOnWithUnmask i ma = lift $ forkOnWithUnmask i (\f -> fst `liftM` WS.runWriterT (ma $ writerstrict f))+  fork   = IO.forkIO+  forkOn = IO.forkOn -  getNumCapabilities = lift getNumCapabilities-  setNumCapabilities = lift . setNumCapabilities-  myThreadId         = lift myThreadId-  yield              = lift yield-  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-  writeCRef r        = lift . writeCRef r-  atomicWriteCRef r  = lift . atomicWriteCRef r-  readForCAS         = lift . readForCAS-  peekTicket         = lift . peekTicket-  casCRef r t        = lift . casCRef r t-  modifyCRefCAS r    = lift . modifyCRefCAS r-  atomically         = lift . atomically-  _concKnowsAbout    = lift . _concKnowsAbout-  _concForgets       = lift . _concForgets-  _concAllKnown      = lift _concAllKnown+  forkWithUnmask   = IO.forkIOWithUnmask+  forkOnWithUnmask = IO.forkOnWithUnmask -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+  getNumCapabilities = IO.getNumCapabilities+  setNumCapabilities = IO.setNumCapabilities+  readMVar           = IO.readMVar+  myThreadId         = IO.myThreadId+  yield              = IO.yield+  threadDelay        = IO.threadDelay+  throwTo            = IO.throwTo+  newEmptyMVar       = IO.newEmptyMVar+  putMVar            = IO.putMVar+  tryPutMVar         = IO.tryPutMVar+  takeMVar           = IO.takeMVar+  tryTakeMVar        = IO.tryTakeMVar+  newCRef            = IO.newIORef+  readCRef           = IO.readIORef+  atomicModifyCRef   = IO.atomicModifyIORef+  writeCRef          = IO.writeIORef+  atomicWriteCRef    = IO.atomicWriteIORef+  readForCAS         = IO.readForCAS+  peekTicket         = pure . IO.peekTicket+  casCRef            = IO.casIORef+  modifyCRefCAS      = IO.atomicModifyIORefCAS+  atomically         = IO.atomically+  readTVarConc       = IO.readTVarIO -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 Ticket   (SL.StateT s m) = Ticket m-  type ThreadId (SL.StateT s m) = ThreadId m+-------------------------------------------------------------------------------+-- Transformer instances -  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)-  forkOnWithUnmask i ma = SL.StateT $ \s -> (\a -> (a,s)) `liftM` forkOnWithUnmask i (\f -> SL.evalStateT (ma $ statelazy f) s)+#define INSTANCE(T,C,F)                                          \+instance C => MonadConc (T m) where                             { \+  type STM      (T m) = STM m                                  ; \+  type MVar     (T m) = MVar m                                 ; \+  type CRef     (T m) = CRef m                                 ; \+  type Ticket   (T m) = Ticket m                               ; \+  type ThreadId (T m) = ThreadId m                             ; \+                                                                 \+  fork   = liftedF F fork                                      ; \+  forkOn = liftedF F . forkOn                                  ; \+                                                                 \+  forkWithUnmask        = liftedFork F forkWithUnmask          ; \+  forkWithUnmaskN   n   = liftedFork F (forkWithUnmaskN   n  ) ; \+  forkOnWithUnmask    i = liftedFork F (forkOnWithUnmask    i) ; \+  forkOnWithUnmaskN n i = liftedFork F (forkOnWithUnmaskN n i) ; \+                                                                 \+  getNumCapabilities = lift getNumCapabilities                 ; \+  setNumCapabilities = lift . setNumCapabilities               ; \+  myThreadId         = lift myThreadId                         ; \+  yield              = lift yield                              ; \+  threadDelay        = lift . threadDelay                      ; \+  throwTo t          = lift . throwTo t                        ; \+  newEmptyMVar       = lift newEmptyMVar                       ; \+  newEmptyMVarN      = lift . newEmptyMVarN                    ; \+  readMVar           = lift . readMVar                         ; \+  putMVar v          = lift . putMVar v                        ; \+  tryPutMVar v       = lift . tryPutMVar v                     ; \+  takeMVar           = lift . takeMVar                         ; \+  tryTakeMVar        = lift . tryTakeMVar                      ; \+  newCRef            = lift . newCRef                          ; \+  newCRefN n         = lift . newCRefN n                       ; \+  readCRef           = lift . readCRef                         ; \+  atomicModifyCRef r = lift . atomicModifyCRef r               ; \+  writeCRef r        = lift . writeCRef r                      ; \+  atomicWriteCRef r  = lift . atomicWriteCRef r                ; \+  readForCAS         = lift . readForCAS                       ; \+  peekTicket         = lift . peekTicket                       ; \+  casCRef r t        = lift . casCRef r t                      ; \+  modifyCRefCAS r    = lift . modifyCRefCAS r                  ; \+  atomically         = lift . atomically                       ; \+  readTVarConc       = lift . readTVarConc                     ; \+                                                                 \+  _concKnowsAbout = lift . _concKnowsAbout                     ; \+  _concForgets    = lift . _concForgets                        ; \+  _concAllKnown   = lift _concAllKnown                         ; \+  _concMessage    = lift . _concMessage                        } -  getNumCapabilities = lift getNumCapabilities-  setNumCapabilities = lift . setNumCapabilities-  myThreadId         = lift myThreadId-  yield              = lift yield-  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-  writeCRef r        = lift . writeCRef r-  atomicWriteCRef r  = lift . atomicWriteCRef r-  readForCAS         = lift . readForCAS-  peekTicket         = lift . peekTicket-  casCRef r t        = lift . casCRef r t-  modifyCRefCAS r    = lift . modifyCRefCAS r-  atomically         = lift . atomically-  _concKnowsAbout    = lift . _concKnowsAbout-  _concForgets       = lift . _concForgets-  _concAllKnown      = lift _concAllKnown+INSTANCE(ReaderT r, MonadConc m, id) -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(IdentityT, MonadConc m, id) -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 Ticket   (SS.StateT s m) = Ticket m-  type ThreadId (SS.StateT s m) = ThreadId m+INSTANCE(WL.WriterT w, (MonadConc m, Monoid w), fst)+INSTANCE(WS.WriterT w, (MonadConc m, Monoid w), fst) -  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)-  forkOnWithUnmask i ma = SS.StateT $ \s -> (\a -> (a,s)) `liftM` forkOnWithUnmask i (\f -> SS.evalStateT (ma $ statestrict f) s)+INSTANCE(SL.StateT s, MonadConc m, fst)+INSTANCE(SS.StateT s, MonadConc m, fst) -  getNumCapabilities = lift getNumCapabilities-  setNumCapabilities = lift . setNumCapabilities-  myThreadId         = lift myThreadId-  yield              = lift yield-  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-  writeCRef r        = lift . writeCRef r-  atomicWriteCRef r  = lift . atomicWriteCRef r-  readForCAS         = lift . readForCAS-  peekTicket         = lift . peekTicket-  casCRef r t        = lift . casCRef r t-  modifyCRefCAS r    = lift . modifyCRefCAS r-  atomically         = lift . atomically-  _concKnowsAbout    = lift . _concKnowsAbout-  _concForgets       = lift . _concForgets-  _concAllKnown      = lift _concAllKnown+INSTANCE(RL.RWST r w s, (MonadConc m, Monoid w), (\(a,_,_) -> a))+INSTANCE(RS.RWST r w s, (MonadConc m, Monoid w), (\(a,_,_) -> a)) -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)+#undef INSTANC -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 Ticket   (RL.RWST r w s m) = Ticket 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)-  forkOnWithUnmask i ma = RL.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkOnWithUnmask i (\f -> fst `liftM` RL.evalRWST (ma $ rwslazy f) r s)+-- | Make an instance @MonadConc m => MonadConc (t m)@ for a given+-- transformer, @t@. The parameter should be the name of a function+-- @:: forall a. StT t a -> a@.+makeTransConc :: Name -> DecsQ+makeTransConc unstN = do+  unstI <- reify unstN+  case unstI of+    VarI _ (ForallT _ _ (AppT (AppT ArrowT (AppT (AppT (ConT _) t) _)) _)) _ _ ->+      [d|+        instance (MonadConc m) => MonadConc ($(pure t) m) where+          type STM      ($(pure t) m) = STM m+          type MVar     ($(pure t) m) = MVar m+          type CRef     ($(pure t) m) = CRef m+          type Ticket   ($(pure t) m) = Ticket m+          type ThreadId ($(pure t) m) = ThreadId m -  getNumCapabilities = lift getNumCapabilities-  setNumCapabilities = lift . setNumCapabilities-  myThreadId         = lift myThreadId-  yield              = lift yield-  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-  writeCRef r        = lift . writeCRef r-  atomicWriteCRef r  = lift . atomicWriteCRef r-  readForCAS         = lift . readForCAS-  peekTicket         = lift . peekTicket-  casCRef r t        = lift . casCRef r t-  modifyCRefCAS r    = lift . modifyCRefCAS r-  atomically         = lift . atomically-  _concKnowsAbout    = lift . _concKnowsAbout-  _concForgets       = lift . _concForgets-  _concAllKnown      = lift _concAllKnown+          fork   = liftedF $(varE unstN) fork+          forkOn = liftedF $(varE unstN) . forkOn -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)+          forkWithUnmask        = liftedFork $(varE unstN) forkWithUnmask+          forkWithUnmaskN   n   = liftedFork $(varE unstN) (forkWithUnmaskN   n  )+          forkOnWithUnmask    i = liftedFork $(varE unstN) (forkOnWithUnmask    i)+          forkOnWithUnmaskN n i = liftedFork $(varE unstN) (forkOnWithUnmaskN n i) -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 Ticket   (RS.RWST r w s m) = Ticket m-  type ThreadId (RS.RWST r w s m) = ThreadId m+          getNumCapabilities = lift getNumCapabilities+          setNumCapabilities = lift . setNumCapabilities+          myThreadId         = lift myThreadId+          yield              = lift yield+          threadDelay        = lift . threadDelay+          throwTo tid        = lift . throwTo tid+          newEmptyMVar       = lift newEmptyMVar+          newEmptyMVarN      = lift . newEmptyMVarN+          readMVar           = lift . readMVar+          putMVar v          = lift . putMVar v+          tryPutMVar v       = lift . tryPutMVar v+          takeMVar           = lift . takeMVar+          tryTakeMVar        = lift . tryTakeMVar+          newCRef            = lift . newCRef+          newCRefN n         = lift . newCRefN n+          readCRef           = lift . readCRef+          atomicModifyCRef r = lift . atomicModifyCRef r+          writeCRef r        = lift . writeCRef r+          atomicWriteCRef r  = lift . atomicWriteCRef r+          readForCAS         = lift . readForCAS+          peekTicket         = lift . peekTicket+          casCRef r tick     = lift . casCRef r tick+          modifyCRefCAS r    = lift . modifyCRefCAS r+          atomically         = lift . atomically+          readTVarConc       = lift . readTVarConc -  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)-  forkOnWithUnmask i ma = RS.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkOnWithUnmask i (\f -> fst `liftM` RS.evalRWST (ma $ rwsstrict f) r s)+          _concKnowsAbout = lift . _concKnowsAbout+          _concForgets    = lift . _concForgets+          _concAllKnown   = lift _concAllKnown+          _concMessage    = lift . _concMessage+      |]+    _ -> fail "Expected a value of type (forall a -> StT t a -> a)" -  getNumCapabilities = lift getNumCapabilities-  setNumCapabilities = lift . setNumCapabilities-  myThreadId         = lift myThreadId-  yield              = lift yield-  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-  writeCRef r        = lift . writeCRef r-  atomicWriteCRef r  = lift . atomicWriteCRef r-  readForCAS         = lift . readForCAS-  peekTicket         = lift . peekTicket-  casCRef r t        = lift . casCRef r t-  modifyCRefCAS r    = lift . modifyCRefCAS r-  atomically         = lift . atomically-  _concKnowsAbout    = lift . _concKnowsAbout-  _concForgets       = lift . _concForgets-  _concAllKnown      = lift _concAllKnown+-- | Given a function to remove the transformer-specific state, lift+-- a function invocation.+liftedF :: (MonadTransControl t, MonadConc m)+  => (forall x. StT t x -> x)+  -> (m a -> m b)+  -> t m a+  -> t m b+liftedF unst f ma = liftWith $ \run -> f (unst <$> run ma) -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)+-- | Given a function to remove the transformer-specific state, lift+-- a @fork(on)WithUnmask@ invocation.+liftedFork :: (MonadTransControl t, MonadConc m)+  => (forall x. StT t x -> x)+  -> (((forall x. m x -> m x) -> m a) -> m b)+  -> ((forall x. t m x -> t m x) -> t m a)+  -> t m b+liftedFork unst f ma = liftWith $ \run ->+  f (\unmask -> unst <$> run (ma $ liftedF unst unmask))

@@ -1,163 +1,182 @@-{-# LANGUAGE CPP          #-}-{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE CPP             #-}+{-# LANGUAGE RankNTypes      #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies    #-}  -- | This module provides an abstraction over 'STM', which can be used -- with 'MonadConc'.-module Control.Monad.STM.Class where+--+-- This module only defines the 'STM' class; you probably want to+-- import "Control.Concurrent.Classy.STM" (which exports+-- "Control.Monad.STM.Class").+--+-- __Deviations:__ An instance of @MonadSTM@ is not required to be an+-- @Alternative@, @MonadPlus@, and @MonadFix@, unlike @STM@. The+-- @always@ and @alwaysSucceeds@ functions are not provided; if you+-- need these file an issue and I'll look into it.+module Control.Monad.STM.Class+  ( MonadSTM(..)+  , check+  , throwSTM+  , catchSTM -import Control.Concurrent.STM (STM)-import Control.Concurrent.STM.TVar (TVar, newTVar, readTVar, writeTVar)+  -- * Utilities for instance writers+  , makeTransSTM+  , liftedOrElse+  ) where+ 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.Reader (ReaderT) import Control.Monad.Trans (lift)+import Control.Monad.Trans.Control (MonadTransControl, StT, liftWith)+import Control.Monad.Trans.Identity (IdentityT)+import Language.Haskell.TH (DecsQ, Info(VarI), Name, Type(..), reify, varE) +import qualified Control.Concurrent.STM as STM+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)-#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+class Ca.MonadCatch stm => MonadSTM stm where+  {-# MINIMAL+        retry+      , orElse+      , (newTVar | newTVarN)+      , readTVar+      , writeTVar+    #-}+   -- | 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 :: * -> *+  type TVar stm :: * -> *    -- | 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+  -- in @TVar@s that it shouldn't have. This will result in the+  -- thread running the transaction being blocked until any @TVar@s   -- referenced in it have been mutated.-  retry :: m a+  retry :: stm 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+  orElse :: stm a -> stm a -> stm a -  -- | Check whether a condition is true and, if not, call @retry@.+  -- | Create a new @TVar@ containing the given value.   ---  -- > check b = unless b retry-  check :: Bool -> m ()-  check b = unless b retry+  -- > newTVar = newTVarN ""+  newTVar :: a -> stm (TVar stm a)+  newTVar = newTVarN "" -  -- | Create a new @CTVar@ containing the given value.-  newCTVar :: a -> m (CTVar m a)+  -- | Create a new @TVar@ containing the given value, but it is+  -- given a name which may be used to present more useful debugging+  -- information.+  --+  -- If an empty name is given, a counter starting from 0 is used. If+  -- names conflict, successive @TVar@s with the same name are given+  -- a numeric suffix, counting up from 1.+  --+  -- > newTVarN _ = newTVar+  newTVarN :: String -> a -> stm (TVar stm a)+  newTVarN _ = newTVar -  -- | Return the current value stored in a @CTVar@.-  readCTVar :: CTVar m a -> m a+  -- | Return the current value stored in a @TVar@.+  readTVar :: TVar stm a -> stm a -  -- | Write the supplied value into the @CTVar@.-  writeCTVar :: CTVar m a -> a -> m ()+  -- | Write the supplied value into the @TVar@.+  writeTVar :: TVar stm a -> a -> stm () -  -- | Throw an exception. This aborts the transaction and propagates-  -- the exception.-  ---  -- > throwSTM = Control.Monad.Catch.throwM-  throwSTM :: Exception e => e -> m a-  throwSTM = throwM+-- | Check whether a condition is true and, if not, call @retry@.+check :: MonadSTM stm => Bool -> stm ()+check b = unless b retry -  -- | Handling exceptions from 'throwSTM'.-  ---  -- > catchSTM = Control.Monad.Catch.catch-  catchSTM :: Exception e => m a -> (e -> m a) -> m a-  catchSTM = Control.Monad.Catch.catch+-- | Throw an exception. This aborts the transaction and propagates+-- the exception.+throwSTM :: (MonadSTM stm, Exception e) => e -> stm a+throwSTM = Ca.throwM -instance MonadSTM STM where-  type CTVar STM = TVar+-- | Handling exceptions from 'throwSTM'.+catchSTM :: (MonadSTM stm, Exception e) => stm a -> (e -> stm a) -> stm a+catchSTM = Ca.catch -  retry      = S.retry-  orElse     = S.orElse-  newCTVar   = newTVar-  readCTVar  = readTVar-  writeCTVar = writeTVar+instance MonadSTM STM.STM where+  type TVar STM.STM = STM.TVar +  retry     = STM.retry+  orElse    = STM.orElse+  newTVar   = STM.newTVar+  readTVar  = STM.readTVar+  writeTVar = STM.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+#define INSTANCE(T,C,F)                                  \+instance C => MonadSTM (T stm) where { \+  type TVar (T stm) = TVar stm      ; \+                                      \+  retry       = lift retry          ; \+  orElse      = liftedOrElse F      ; \+  newTVar     = lift . newTVar      ; \+  newTVarN n  = lift . newTVarN n   ; \+  readTVar    = lift . readTVar     ; \+  writeTVar v = lift . writeTVar v  } -instance (MonadSTM m, Monoid w) => MonadSTM (WS.WriterT w m) where-  type CTVar (WS.WriterT w m) = CTVar m+INSTANCE(ReaderT r, MonadSTM stm, id) -  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(IdentityT, MonadSTM stm, id) -instance MonadSTM m => MonadSTM (SL.StateT s m) where-  type CTVar (SL.StateT s m) = CTVar m+INSTANCE(WL.WriterT w, (MonadSTM stm, Monoid w), fst)+INSTANCE(WS.WriterT w, (MonadSTM stm, Monoid w), fst) -  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(SL.StateT s, MonadSTM stm, fst)+INSTANCE(SS.StateT s, MonadSTM stm, fst) -instance MonadSTM m => MonadSTM (SS.StateT s m) where-  type CTVar (SS.StateT s m) = CTVar m+INSTANCE(RL.RWST r w s, (MonadSTM stm, Monoid w), (\(a,_,_) -> a))+INSTANCE(RS.RWST r w s, (MonadSTM stm, Monoid w), (\(a,_,_) -> a)) -  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+#undef INSTANC -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+-- | Make an instance @MonadSTM m => MonadSTM (t m)@ for a given+-- transformer, @t@. The parameter should be the name of a function+-- @:: forall a. StT t a -> a@.+makeTransSTM :: Name -> DecsQ+makeTransSTM unstN = do+  unstI <- reify unstN+  case unstI of+    VarI _ (ForallT _ _ (AppT (AppT ArrowT (AppT (AppT (ConT _) t) _)) _)) _ _ ->+      [d|+        instance (MonadSTM stm, MonadTransControl $(pure t)) => MonadSTM ($(pure t) stm) where+          type TVar ($(pure t) stm) = TVar stm -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      = liftedOrElse $(varE unstN)+          newTVar     = lift . newTVar+          newTVarN n  = lift . newTVarN n+          readTVar    = lift . readTVar+          writeTVar v = lift . writeTVar v+      |]+    _ -> fail "Expected a value of type (forall a -> StT t a -> a)" -  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+-- | Given a function to remove the transformer-specific state, lift+-- an @orElse@ invocation.+liftedOrElse :: (MonadTransControl t, MonadSTM stm)+  => (forall x. StT t x -> x)+  -> t stm a -> t stm a -> t stm a+liftedOrElse unst ma mb = liftWith $ \run ->+  let ma' = unst <$> run ma+      mb' = unst <$> run mb+  in ma' `orElse` mb'

@@ -1,60 +0,0 @@-{-# 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!"

@@ -1,4 +1,3 @@-{-# LANGUAGE CPP        #-} {-# LANGUAGE RankNTypes #-}  -- | Deterministic testing for concurrent computations.@@ -10,18 +9,21 @@ -- -- > example1 :: MonadConc m => m Int -- > example1 = do--- >   a <- newEmptyCVar--- >   b <- newEmptyCVar+-- >   a <- newEmptyMVar+-- >   b <- newEmptyMVar -- >--- >   c <- newCVar 0+-- >   c <- newMVar 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+-- >   let lock m = putMVar m ()+-- >   let unlock = takeMVar -- >--- >   takeCVar j1--- >   takeCVar j2+-- >   j1 <- spawn $ lock a >> lock b >> modifyMVar_ c (return . succ) >> unlock b >> unlock a+-- >   j2 <- spawn $ lock b >> lock a >> modifyMVar_ c (return . pred) >> unlock a >> unlock b -- >--- >   takeCVar c+-- >   takeMVar j1+-- >   takeMVar j2+-- >+-- >   takeMVar 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@@ -109,7 +111,7 @@   -- >   x <- spawn $ writeCRef r1 True >> readCRef r2   -- >   y <- spawn $ writeCRef r2 True >> readCRef r1   -- >-  -- >   (,) <$> readCVar x <*> readCVar y+  -- >   (,) <$> readMVar x <*> readMVar y   --   -- Under a sequentially consistent memory model the possible results   -- are @(True, True)@, @(True, False)@, and @(False, True)@. Under@@ -147,8 +149,8 @@   -- writes to @CRef@s are /committed/, which makes a write visible to   -- all threads rather than just the one which performed the   -- write. Only 'writeCRef' is broken up into separate write and-  -- commit steps, 'modifyCRef' is still atomic and imposes a memory-  -- barrier.+  -- commit steps, 'atomicModifyCRef' is still atomic and imposes a+  -- memory barrier.    , MemType(..)   , defaultMemType@@ -169,6 +171,7 @@    , Bounds(..)   , defaultBounds+  , noBounds   , PreemptionBound(..)   , defaultPreemptionBound   , FairBound(..)@@ -228,18 +231,13 @@ import Control.DeepSeq (NFData(..)) import Control.Monad (when, unless) import Data.Function (on)-import Data.List (minimumBy)-import Data.List.Extra-import Data.Monoid ((<>))+import Data.List (intercalate, intersperse, minimumBy)+--import Data.List.NonEmpty import Data.Ord (comparing) import Test.DejaFu.Deterministic+import Test.DejaFu.Deterministic.Internal (preEmpCount) import Test.DejaFu.SCT -#if __GLASGOW_HASKELL__ < 710-import Control.Applicative ((<$>))-import Data.Foldable (Foldable(..))-#endif- -- | The default memory model: @TotalStoreOrder@ defaultMemType :: MemType defaultMemType = TotalStoreOrder@@ -372,14 +370,14 @@   -- ^ Whether the test passed or not.   , _casesChecked :: Int   -- ^ The number of cases checked.-  , _failures     :: [(Either Failure a, Trace)]+  , _failures     :: [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]   -- ^ The failing cases, if any.   , _failureMsg   :: String   -- ^ A message to display on failure, if nonempty-  } deriving (Show, Eq)+  } deriving Show  -- | A failed result, taking the given list of failures.-defaultFail :: [(Either Failure a, Trace)] -> Result a+defaultFail :: [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] -> Result a defaultFail failures = Result False 0 failures ""  -- | A passed result.@@ -431,7 +429,7 @@  -- | A @Predicate@ is a function which collapses a list of results -- into a 'Result'.-type Predicate a = [(Either Failure a, Trace)] -> Result a+type Predicate a = [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] -> Result a  -- | Reduce the list of failures in a @Predicate@ to one -- representative trace for each unique result.@@ -443,15 +441,18 @@ representative p xs = result { _failures = choose . collect $ _failures result } where   result  = p xs   collect = groupBy' [] ((==) `on` fst)-  choose  = map $ minimumBy (comparing $ \(_, trc) -> (preEmpCount' trc, length trc))+  choose  = map $ minimumBy (comparing $ \(_, trc) -> (preEmps trc, length trc)) +  preEmps trc = preEmpCount (map (\(d,_,a) -> (d, a)) trc) (Continue, WillStop)+   groupBy' res _ [] = res-  groupBy' res eq (x:xs) = groupBy' (insert' eq x res) eq xs+  groupBy' res eq (y:ys) = groupBy' (insert' eq y res) eq ys -  insert' eq x [] = [[x]]+  insert' _ x [] = [[x]]   insert' eq x (ys@(y:_):yss)     | x `eq` y  = (x:ys) : yss     | otherwise = ys : insert' eq x yss+  insert' _ _ ([]:_) = undefined  -- | Check that a computation never aborts. abortsNever :: Predicate a@@ -598,12 +599,24 @@       putStrLn $ _failureMsg 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..."+    let output = map (\(r, t) -> putStrLn . indent $ either showFail show r ++ " " ++ showTrace t) $ take 5 failures+    sequence_ $ intersperse (putStrLn "") output+    when (moreThan 5 failures) $+      putStrLn (indent "...")    return $ _pass result +-- | Check if a list is longer than some value, without needing to+-- compute the entire length.+moreThan :: Int -> [a] -> Bool+moreThan n [] = n < 0+moreThan 0 _ = True+moreThan n (_:rest) = moreThan (n-1) rest+ -- | Increment the cases incCC :: Result a -> Result a incCC r = r { _casesChecked = _casesChecked r + 1 }++-- | Indent every line of a string.+indent :: String -> String+indent = intercalate "\n" . map ('\t':) . lines

@@ -1,6 +1,6 @@-{-# LANGUAGE CPP                        #-} {-# LANGUAGE FlexibleInstances          #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses      #-} {-# LANGUAGE RankNTypes                 #-} {-# LANGUAGE TypeFamilies               #-} {-# LANGUAGE TypeSynonymInstances       #-}@@ -21,44 +21,39 @@   , MemType(..)   , runConcST   , runConcIO-  , runConcST'-  , runConcIO'    -- * Execution traces   , Trace-  , Trace'   , Decision(..)+  , ThreadId(..)   , ThreadAction(..)   , Lookahead(..)-  , CVarId+  , MVarId   , CRefId   , MaskingState(..)-  , toTrace   , showTrace   , showFail    -- * Scheduling-  , module Test.DejaFu.Deterministic.Schedule+  , module Test.DPOR.Schedule   ) where  import Control.Exception (MaskingState(..)) import Control.Monad.ST (ST, runST)+import Data.Dynamic (toDyn) import Data.IORef (IORef) import Data.STRef (STRef) import Test.DejaFu.Deterministic.Internal-import Test.DejaFu.Deterministic.Schedule import Test.DejaFu.Internal (refST, refIO) import Test.DejaFu.STM (STMLike, STMIO, STMST, runTransactionIO, runTransactionST)-import Test.DejaFu.STM.Internal (CTVar(..))+import Test.DejaFu.STM.Internal (TVar(..))+import Test.DPOR.Schedule +import qualified Control.Monad.Base as Ba 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) #-} {-# ANN module ("HLint: ignore Use const"    :: String) #-} @@ -80,6 +75,9 @@ instance IO.MonadIO ConcIO where   liftIO ma = toConc (\c -> ALift (fmap c ma)) +instance Ba.MonadBase IO ConcIO where+  liftBase = IO.liftIO+ instance Ca.MonadCatch (Conc n r s) where   catch ma h = toConc (ACatching (unC . h) (unC ma)) @@ -91,16 +89,16 @@   uninterruptibleMask mb = toConc (AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f))  instance Monad n => C.MonadConc (Conc n r (STMLike n r)) where-  type CVar     (Conc n r (STMLike n r)) = CVar r+  type MVar     (Conc n r (STMLike n r)) = MVar r   type CRef     (Conc n r (STMLike n r)) = CRef r   type Ticket   (Conc n r (STMLike n r)) = Ticket-  type STMLike  (Conc n r (STMLike n r)) = STMLike n r+  type STM      (Conc n r (STMLike n r)) = STMLike n r   type ThreadId (Conc n r (STMLike n r)) = ThreadId    -- ---------- -  forkWithUnmask  ma = toConc (AFork (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop)))-  forkOnWithUnmask _ = C.forkWithUnmask+  forkWithUnmaskN   n ma = toConc (AFork n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop)))+  forkOnWithUnmaskN n _  = C.forkWithUnmaskN n    -- This implementation lies and returns 2 until a value is set. This   -- will potentially avoid special-case behaviour for 1 capability,@@ -114,7 +112,7 @@    -- ---------- -  newCRef a = toConc (\c -> ANewRef a c)+  newCRefN n a = toConc (\c -> ANewRef n a c)    readCRef   ref = toConc (AReadRef    ref)   readForCAS ref = toConc (AReadRefCas ref)@@ -124,19 +122,19 @@   writeCRef ref      a = toConc (\c -> AWriteRef ref a (c ()))   casCRef   ref tick a = toConc (ACasRef ref tick a) -  modifyCRef    ref f = toConc (AModRef    ref f)-  modifyCRefCAS ref f = toConc (AModRefCas ref f)+  atomicModifyCRef ref f = toConc (AModRef    ref f)+  modifyCRefCAS    ref f = toConc (AModRefCas ref f)    -- ---------- -  newEmptyCVar = toConc (\c -> ANewVar c)+  newEmptyMVarN n = toConc (\c -> ANewVar n c) -  putCVar  var a = toConc (\c -> APutVar var a (c ()))-  readCVar var   = toConc (AReadVar var)-  takeCVar var   = toConc (ATakeVar var)+  putMVar  var a = toConc (\c -> APutVar var a (c ()))+  readMVar var   = toConc (AReadVar var)+  takeMVar var   = toConc (ATakeVar var) -  tryPutCVar  var a = toConc (ATryPutVar  var a)-  tryTakeCVar var   = toConc (ATryTakeVar var)+  tryPutMVar  var a = toConc (ATryPutVar  var a)+  tryTakeMVar var   = toConc (ATryTakeVar var)    -- ---------- @@ -148,14 +146,16 @@    -- ---------- -  _concKnowsAbout (Left  (CVar  (cvarid,  _))) = toConc (\c -> AKnowsAbout (Left  cvarid)  (c ()))-  _concKnowsAbout (Right (CTVar (ctvarid, _))) = toConc (\c -> AKnowsAbout (Right ctvarid) (c ()))+  _concKnowsAbout (Left  (MVar cvarid  _)) = toConc (\c -> AKnowsAbout (Left  cvarid)  (c ()))+  _concKnowsAbout (Right (TVar (ctvarid, _))) = toConc (\c -> AKnowsAbout (Right ctvarid) (c ())) -  _concForgets (Left  (CVar  (cvarid,  _))) = toConc (\c -> AForgets (Left  cvarid)  (c ()))-  _concForgets (Right (CTVar (ctvarid, _))) = toConc (\c -> AForgets (Right ctvarid) (c ()))+  _concForgets (Left  (MVar cvarid  _)) = toConc (\c -> AForgets (Left  cvarid)  (c ()))+  _concForgets (Right (TVar (ctvarid, _))) = toConc (\c -> AForgets (Right ctvarid) (c ()))    _concAllKnown = toConc (\c -> AAllKnown (c ())) +  _concMessage msg = toConc (\c -> AMessage (toDyn msg) (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.@@ -163,20 +163,20 @@ -- 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 SequentialConsistency () newEmptyCVar+-- > runConc roundRobinSched SequentialConsistency () newEmptyMVar -- -- 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>-runConcST :: Scheduler s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace)-runConcST sched memtype s ma =-  let (r, s', t') = runConcST' sched memtype s ma-  in  (r, s', toTrace t')---- | Variant of 'runConcST' which produces a 'Trace''.-runConcST' :: Scheduler s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace')-runConcST' sched memtype s ma = runST $ runFixed fixed runTransactionST sched memtype s $ unC ma where+--+-- __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.+runConcST :: Scheduler ThreadId ThreadAction Lookahead s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)+runConcST sched memtype s ma = runST $ runFixed fixed runTransactionST sched memtype s $ unC ma where   fixed = refST $ \mb -> cont (\c -> ALift $ c <$> mb)  -- | Run a concurrent computation in the @IO@ monad with a given@@ -190,12 +190,12 @@ -- You should therefore keep @IO@ blocks small, and only perform -- blocking operations with the supplied primitives, insofar as -- possible.-runConcIO :: Scheduler s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace)-runConcIO sched memtype s ma = do-  (r, s', t') <- runConcIO' sched memtype s ma-  return (r, s', toTrace t')---- | Variant of 'runConcIO' which produces a 'Trace''.-runConcIO' :: Scheduler s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace')-runConcIO' sched memtype s ma = runFixed fixed runTransactionIO sched memtype s $ unC ma where+--+-- __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.+runConcIO :: Scheduler ThreadId ThreadAction Lookahead s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)+runConcIO sched memtype s ma = runFixed fixed runTransactionIO sched memtype s $ unC ma where   fixed = refIO $ \mb -> cont (\c -> ALift $ c <$> mb)

@@ -1,4 +1,3 @@-{-# LANGUAGE CPP                 #-} {-# LANGUAGE RankNTypes          #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -11,7 +10,7 @@   -- * The @Conc@ Monad  , M(..)- , CVar(..)+ , MVar(..)  , CRef(..)  , Ticket(..)  , Fixed@@ -23,8 +22,9 @@   -- * Identifiers  , ThreadId(..)- , CVarId(..)+ , MVarId(..)  , CRefId(..)+ , initialThread   -- * Memory Models  , MemType(..)@@ -35,16 +35,17 @@  , Decision(..)  , ThreadAction(..)  , Lookahead(..)- , Trace'+ , isBlock  , lookahead  , willRelease- , toTrace+ , preEmpCount  , showTrace  , showFail   -- * Synchronised and Unsynchronised Actions  , ActionType(..)  , isBarrier+ , isCommit  , synchronises  , crefOf  , cvarOf@@ -55,23 +56,20 @@  , Failure(..)  ) where -import Control.Exception (MaskingState(..), SomeException(..))+import Control.Exception (MaskingState(..), toException)+import Data.Functor (void) import Data.List (sort)-import Data.List.Extra-import Data.Maybe (fromJust, isJust, fromMaybe, isNothing, listToMaybe)-import Data.Typeable (cast)-import Test.DejaFu.STM (CTVarId, Result(..))+import Data.List.NonEmpty (NonEmpty(..), fromList)+import Data.Maybe (fromJust, isJust, isNothing, listToMaybe)+import Test.DejaFu.STM (Result(..)) import Test.DejaFu.Internal import Test.DejaFu.Deterministic.Internal.Common import Test.DejaFu.Deterministic.Internal.Memory import Test.DejaFu.Deterministic.Internal.Threading+import Test.DPOR (Decision(..), Scheduler, Trace)  import qualified Data.Map.Strict as M -#if __GLASGOW_HASKELL__ < 710-import Control.Applicative ((<$>), (<*>))-#endif- {-# ANN module ("HLint: ignore Use record patterns" :: String) #-} {-# ANN module ("HLint: ignore Use const"           :: String) #-} @@ -82,19 +80,19 @@ -- 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 x -> CTVarId -> n (Result x, CTVarId))-         -> Scheduler g -> MemType -> g -> M n r s a -> n (Either Failure a, g, Trace')+runFixed :: (Functor n, Monad n) => Fixed n r s -> (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))+         -> Scheduler ThreadId ThreadAction Lookahead g -> MemType -> g -> M n r s a -> n (Either Failure a, g, Trace ThreadId ThreadAction Lookahead) runFixed fixed runstm sched memtype s ma = (\(e,g,_,t) -> (e,g,t)) <$> runFixed' fixed runstm sched memtype 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 x -> CTVarId -> n (Result x, CTVarId))-  -> Scheduler g -> MemType -> g -> IdSource -> M n r s a -> n (Either Failure a, g, IdSource, Trace')+  => Fixed n r s -> (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))+  -> Scheduler ThreadId ThreadAction Lookahead g -> MemType -> g -> IdSource -> M n r s a -> n (Either Failure a, g, IdSource, Trace ThreadId ThreadAction Lookahead) runFixed' fixed runstm sched memtype s idSource ma = do   ref <- newRef fixed Nothing    let c       = ma >>= liftN fixed . writeRef fixed ref . Just . Right-  let threads = launch' Unmasked 0 ((\a _ -> a) $ runCont c $ const AStop) M.empty+  let threads = launch' Unmasked initialThread ((\a _ -> a) $ runCont c $ const AStop) M.empty    (s', idSource', trace) <- runThreads fixed runstm sched memtype s threads idSource ref   out <- readRef fixed ref@@ -107,8 +105,8 @@ -- 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 x -> CTVarId -> n (Result x, CTVarId))-           -> Scheduler g -> MemType -> g -> Threads n r s -> IdSource -> r (Maybe (Either Failure a)) -> n (g, IdSource, Trace')+runThreads :: (Functor n, Monad n) => Fixed n r s -> (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))+           -> Scheduler ThreadId ThreadAction Lookahead g -> MemType -> g -> Threads n r s -> IdSource -> r (Maybe (Either Failure a)) -> n (g, IdSource, Trace ThreadId ThreadAction Lookahead) runThreads fixed runstm sched memtype origg origthreads idsrc ref = go idsrc [] Nothing origg origthreads emptyBuffer 2 where   go idSource sofar prior g threads wb caps     | isTerminated  = stop g@@ -123,13 +121,13 @@         Right (threads', idSource', act, wb', caps') -> loop threads' idSource' act wb' caps'          Left UncaughtException-          | chosen == 0 -> die g' UncaughtException+          | chosen == initialThread -> die g' UncaughtException           | otherwise -> loop (kill chosen threads) idSource Killed wb caps          Left failure -> die g' failure      where-      (choice, g')  = sched g (map (\(d,_,a) -> (d,a)) $ reverse sofar) ((\p (_,_,a) -> (p,a)) <$> prior <*> listToMaybe sofar) $ unsafeToNonEmpty runnable'+      (choice, g')  = sched (map (\(d,_,a) -> (d,a)) $ reverse sofar) ((\p (_,_,a) -> (p,a)) <$> prior <*> listToMaybe sofar) (fromList $ map (\(t,l:|_) -> (t,l)) runnable') g       chosen        = fromJust choice       runnable'     = [(t, nextActions t) | t <- sort $ M.keys runnable]       runnable      = M.filter (isNothing . _blocking) threadsc@@ -138,11 +136,13 @@       isAborted     = isNothing choice       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+      isTerminated  = initialThread `notElem` M.keys threads+      isDeadlocked  = isLocked initialThread threads &&+        (((~=  OnMVarFull  undefined) <$> M.lookup initialThread threads) == Just True ||+         ((~=  OnMVarEmpty undefined) <$> M.lookup initialThread threads) == Just True ||+         ((~=  OnMask      undefined) <$> M.lookup initialThread threads) == Just True)+      isSTMLocked = isLocked initialThread threads &&+        ((~=  OnTVar []) <$> M.lookup initialThread threads) == Just True        unblockWaitingOn tid = fmap unblock where         unblock thrd = case _blocking thrd of@@ -154,18 +154,13 @@         | 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 = lookahead . _continuation . fromJust $ M.lookup t threadsc        stop outg = return (outg, idSource, sofar)       die  outg reason = writeRef fixed ref (Just $ Left reason) >> stop outg        loop threads' idSource' act wb' =-        let sofar' = ((decision, alternatives, act) : sofar)+        let sofar' = ((decision, runnable', act) : sofar)             threads'' = if (interruptible <$> M.lookup chosen threads') /= Just False then unblockWaitingOn chosen threads' else threads'         in go idSource' sofar' (Just chosen) g' (delCommitThreads threads'') wb' @@ -175,7 +170,7 @@ -- | 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. s x -> CTVarId -> n (Result x, CTVarId))+  -> (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))   -- ^ Run a 'MonadSTM' transaction atomically.   -> MemType   -- ^ The memory model@@ -193,18 +188,18 @@   -- ^ The number of capabilities   -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int)) stepThread fixed runstm memtype action idSource tid threads wb caps = case action of-  AFork    a b     -> stepFork        a b+  AFork    n a b   -> stepFork        n a b   AMyTId   c       -> stepMyTId       c   AGetNumCapabilities   c -> stepGetNumCapabilities c   ASetNumCapabilities i c -> stepSetNumCapabilities i c   AYield   c       -> stepYield       c-  ANewVar  c       -> stepNewVar      c+  ANewVar  n c     -> stepNewVar      n c   APutVar  var a c -> stepPutVar      var a c   ATryPutVar var a c -> stepTryPutVar var a c   AReadVar var c   -> stepReadVar     var c   ATakeVar var c   -> stepTakeVar     var c   ATryTakeVar var c -> stepTryTakeVar var c-  ANewRef  a c     -> stepNewRef      a c+  ANewRef  n a c   -> stepNewRef      n a c   AReadRef ref c   -> stepReadRef     ref c   AReadRefCas ref c -> stepReadRefCas ref c   APeekTicket tick c -> stepPeekTicket tick c@@ -225,13 +220,14 @@   AKnowsAbout v c  -> stepKnowsAbout  v c   AForgets    v c  -> stepForgets v c   AAllKnown   c    -> stepAllKnown c+  AMessage    m c  -> stepMessage m 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, wb, caps) where+    stepFork n a b = return $ Right (goto (b newtid) tid threads', idSource', Fork newtid, wb, caps) where       threads' = launch tid newtid a threads-      (idSource', newtid) = nextTId idSource+      (idSource', newtid) = nextTId n idSource      -- | Get the 'ThreadId' of the current thread     stepMyTId c = simple (goto (c tid) tid threads) MyThreadId@@ -245,62 +241,62 @@     -- | Yield the current thread     stepYield c = simple (goto c tid threads) Yield -    -- | Put a value into a @CVar@, blocking the thread until it's+    -- | Put a value into a @MVar@, blocking the thread until it's     -- empty.-    stepPutVar cvar@(CVar (cvid, _)) a c = synchronised $ do-      (success, threads', woken) <- putIntoCVar cvar a c fixed tid threads+    stepPutVar cvar@(MVar cvid _) a c = synchronised $ do+      (success, threads', woken) <- putIntoMVar cvar a c fixed tid threads       simple threads' $ if success then PutVar cvid woken else BlockedPutVar cvid -    -- | Try to put a value into a @CVar@, without blocking.-    stepTryPutVar cvar@(CVar (cvid, _)) a c = synchronised $ do-      (success, threads', woken) <- tryPutIntoCVar cvar a c fixed tid threads+    -- | Try to put a value into a @MVar@, without blocking.+    stepTryPutVar cvar@(MVar cvid _) a c = synchronised $ do+      (success, threads', woken) <- tryPutIntoMVar cvar a c fixed tid threads       simple threads' $ TryPutVar cvid success woken -    -- | Get the value from a @CVar@, without emptying, blocking the+    -- | Get the value from a @MVar@, without emptying, blocking the     -- thread until it's full.-    stepReadVar cvar@(CVar (cvid, _)) c = synchronised $ do-      (success, threads', _) <- readFromCVar cvar c fixed tid threads+    stepReadVar cvar@(MVar cvid _) c = synchronised $ do+      (success, threads', _) <- readFromMVar cvar c fixed tid threads       simple threads' $ if success then ReadVar cvid else BlockedReadVar cvid -    -- | Take the value from a @CVar@, blocking the thread until it's+    -- | Take the value from a @MVar@, blocking the thread until it's     -- full.-    stepTakeVar cvar@(CVar (cvid, _)) c = synchronised $ do-      (success, threads', woken) <- takeFromCVar cvar c fixed tid threads+    stepTakeVar cvar@(MVar cvid _) c = synchronised $ do+      (success, threads', woken) <- takeFromMVar cvar c fixed tid threads       simple threads' $ if success then TakeVar cvid woken else BlockedTakeVar cvid -    -- | Try to take the value from a @CVar@, without blocking.-    stepTryTakeVar cvar@(CVar (cvid, _)) c = synchronised $ do-      (success, threads', woken) <- tryTakeFromCVar cvar c fixed tid threads+    -- | Try to take the value from a @MVar@, without blocking.+    stepTryTakeVar cvar@(MVar cvid _) c = synchronised $ do+      (success, threads', woken) <- tryTakeFromMVar cvar c fixed tid threads       simple threads' $ TryTakeVar cvid success woken      -- | Read from a @CRef@.-    stepReadRef cref@(CRef (crid, _)) c = do+    stepReadRef cref@(CRef crid _) c = do       val <- readCRef fixed cref tid       simple (goto (c val) tid threads) $ ReadRef crid      -- | Read from a @CRef@ for future compare-and-swap operations.-    stepReadRefCas cref@(CRef (crid, _)) c = do+    stepReadRefCas cref@(CRef crid _) c = do       tick <- readForTicket fixed cref tid       simple (goto (c tick) tid threads) $ ReadRefCas crid      -- | Extract the value from a @Ticket@.-    stepPeekTicket (Ticket (crid, _, a)) c = simple (goto (c a) tid threads) $ PeekTicket crid+    stepPeekTicket (Ticket crid _ a) c = simple (goto (c a) tid threads) $ PeekTicket crid      -- | Modify a @CRef@.-    stepModRef cref@(CRef (crid, _)) f c = synchronised $ do+    stepModRef cref@(CRef crid _) f c = synchronised $ do       (new, val) <- f <$> readCRef fixed cref tid       writeImmediate fixed cref new       simple (goto (c val) tid threads) $ ModRef crid      -- | Modify a @CRef@ using a compare-and-swap.-    stepModRefCas cref@(CRef (crid, _)) f c = synchronised $ do-      tick@(Ticket (_, _, old)) <- readForTicket fixed cref tid+    stepModRefCas cref@(CRef crid _) f c = synchronised $ do+      tick@(Ticket _ _ old) <- readForTicket fixed cref tid       let (new, val) = f old-      casCRef fixed cref tid tick new+      void $ casCRef fixed cref tid tick new       simple (goto (c val) tid threads) $ ModRefCas crid      -- | Write to a @CRef@ without synchronising-    stepWriteRef cref@(CRef (crid, _)) a c = case memtype of+    stepWriteRef cref@(CRef crid _) a c = case memtype of       -- Write immediately.       SequentialConsistency -> do         writeImmediate fixed cref a@@ -308,51 +304,49 @@        -- Add to buffer using thread id.       TotalStoreOrder -> do-        let (ThreadId tid') = tid-        wb' <- bufferWrite fixed wb tid' cref a tid+        wb' <- bufferWrite fixed wb (tid, Nothing) cref a         return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps) -      -- Add to buffer using cref id+      -- Add to buffer using both thread id and cref id       PartialStoreOrder -> do-        let (CRefId crid') = crid-        wb' <- bufferWrite fixed wb crid' cref a tid+        wb' <- bufferWrite fixed wb (tid, Just crid) cref a         return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps)      -- | Perform a compare-and-swap on a @CRef@.-    stepCasRef cref@(CRef (crid, _)) tick a c = synchronised $ do+    stepCasRef cref@(CRef crid _) tick a c = synchronised $ do       (suc, tick') <- casCRef fixed cref tid tick a       simple (goto (c (suc, tick')) tid threads) $ CasRef crid suc      -- | Commit a @CRef@ write-    stepCommit t@(ThreadId t') c@(CRefId c') = do+    stepCommit t c = do       wb' <- case memtype of         -- Shouldn't ever get here         SequentialConsistency ->           error "Attempting to commit under SequentialConsistency"          -- Commit using the thread id.-        TotalStoreOrder -> commitWrite fixed wb t'+        TotalStoreOrder -> commitWrite fixed wb (t, Nothing)          -- Commit using the cref id.-        PartialStoreOrder -> commitWrite fixed wb c'+        PartialStoreOrder -> commitWrite fixed wb (t, Just c)        return $ Right (threads, idSource, CommitRef t c, wb', caps)      -- | Run a STM transaction atomically.     stepAtom stm c = synchronised $ do-      let oldctvid = _nextCTVId idSource-      (res, newctvid) <- runstm stm oldctvid+      (res, idSource', trace) <- runstm stm idSource       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, wb, caps)-          | otherwise ->-           return $ Right (knows (map Right written) tid $ goto (c val) tid threads, idSource { _nextCTVId = newctvid }, FreshSTM, wb, caps)+        Success _ written val ->+          let (threads', woken) = wake (OnTVar written) threads+          in return $ Right (knows (map Right written) tid $ goto (c val) tid threads', idSource', STM trace woken, wb, caps)         Retry touched ->-          let threads' = block (OnCTVar touched) tid threads-          in return $ Right (threads', idSource { _nextCTVId = newctvid }, BlockedSTM, wb, caps)-        Exception e -> stepThrow e+          let threads' = block (OnTVar touched) tid threads+          in return $ Right (threads', idSource', BlockedSTM trace, wb, caps)+        Exception e -> do+          res' <- stepThrow e+          return $ case res' of+            Right (threads', _, _, _, _) -> Right (threads', idSource', Throw, wb, caps)+            Left err -> Left err      -- | Run a subcomputation in an exception-catching context.     stepCatching h ma c = simple threads' Catching where@@ -368,7 +362,7 @@     -- | Throw an exception, and propagate it to the appropriate     -- handler.     stepThrow e =-      case propagate (wrap e) tid threads of+      case propagate (toException e) tid threads of         Just threads' -> simple threads' Throw         Nothing -> return $ Left UncaughtException @@ -379,10 +373,10 @@           blocked  = block (OnMask t) tid threads       in case M.lookup t threads of            Just thread-             | interruptible thread -> case propagate (wrap e) t threads' of+             | interruptible thread -> case propagate (toException e) t threads' of                Just threads'' -> simple threads'' $ ThrowTo t                Nothing-                 | t == 0     -> return $ Left UncaughtException+                 | t == initialThread -> return $ Left UncaughtException                  | otherwise -> simple (kill t threads') $ ThrowTo t              | otherwise -> simple blocked $ BlockedThrowTo t            Nothing -> simple threads' $ ThrowTo t@@ -407,22 +401,22 @@       threads' = goto a tid (mask m tid threads)      -- | Reset the masking thread of the state.-    stepResetMask b1 b2 m c = simple threads' action where-      action   = (if b1 then SetMasking else ResetMasking) b2 m+    stepResetMask b1 b2 m c = simple threads' act where+      act      = (if b1 then SetMasking else ResetMasking) b2 m       threads' = goto c tid (mask m tid threads) -    -- | Create a new @CVar@, using the next 'CVarId'.-    stepNewVar c = do-      let (idSource', newcvid) = nextCVId idSource+    -- | Create a new @MVar@, using the next 'MVarId'.+    stepNewVar n c = do+      let (idSource', newcvid) = nextCVId n idSource       ref <- newRef fixed Nothing-      let cvar = CVar (newcvid, ref)+      let cvar = MVar newcvid ref       return $ Right (knows [Left newcvid] tid $ goto (c cvar) tid threads, idSource', NewVar newcvid, wb, caps)      -- | Create a new @CRef@, using the next 'CRefId'.-    stepNewRef a c = do-      let (idSource', newcrid) = nextCRId idSource+    stepNewRef n a c = do+      let (idSource', newcrid) = nextCRId n idSource       ref <- newRef fixed (M.empty, 0, a)-      let cref = CRef (newcrid, ref)+      let cref = CRef newcrid ref       return $ Right (goto (c cref) tid threads, idSource', NewRef newcrid, wb, caps)      -- | Lift an action from the underlying monad into the @Conc@@@ -443,6 +437,9 @@     -- | Record that all shared variables are known.     stepAllKnown c = simple (fullknown tid $ goto c tid threads) AllKnown +    -- | Add a message to the trace.+    stepMessage m c = simple (goto c tid threads) (Message m)+     -- | Kill the current thread.     stepStop = simple (kill tid threads) Stop @@ -458,6 +455,3 @@       return $ case res of         Right (threads', idSource', act', _, caps') -> Right (threads', idSource', act', emptyBuffer, caps')         _ -> res--    -- | Helper function for wrapping up exceptions.-    wrap e = fromMaybe (SomeException e) $ cast e

@@ -1,7 +1,5 @@-{-# LANGUAGE CPP                        #-}-{-# LANGUAGE ExistentialQuantification  #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE RankNTypes                 #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE RankNTypes                #-}  -- | Common types and utility functions for deterministic execution of -- 'MonadConc' implementations.@@ -9,19 +7,28 @@  import Control.DeepSeq (NFData(..)) import Control.Exception (Exception, MaskingState(..))+import Data.Dynamic (Dynamic) import Data.Map.Strict (Map)-import Data.List.Extra+import Data.Maybe (mapMaybe)+import Data.List (sort, nub, intercalate)+import Data.List.NonEmpty (NonEmpty, fromList) import Test.DejaFu.Internal-import Test.DejaFu.STM (CTVarId)+import Test.DPOR (Decision(..), Trace) -#if __GLASGOW_HASKELL__ < 710-import Control.Applicative (Applicative(..))-#endif+{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}  -------------------------------------------------------------------------------- -- * The @Conc@ Monad --- | The underlying monad is based on continuations over Actions.+-- | The underlying monad is based on continuations over 'Action's.+--+-- One might wonder why the return type isn't reflected in 'Action',+-- and a free monad formulation used. This would remove the need for a+-- @Lift@ action as the penultimate action of thread 0 used to+-- communicate back the result, and be more pleasing in a+-- sense. However, this makes the current expression of threads and+-- exception handlers very difficult (perhaps even not possible+-- without significant reworking), so I abandoned the attempt. newtype M n r s a = M { runM :: (a -> Action n r s) -> Action n r s }  instance Functor (M n r s) where@@ -37,14 +44,14 @@  -- | 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@+-- single-wakeup, and wake up in a FIFO order. Writing to a @MVar@ -- wakes up all threads blocked on reading it, and it is up to the--- scheduler which one runs next. Taking from a @CVar@ behaves+-- scheduler which one runs next. Taking from a @MVar@ behaves -- analogously.------ @CVar@s are represented as a unique numeric identifier, and a--- reference containing a Maybe value.-newtype CVar r a = CVar (CVarId, r (Maybe a))+data MVar r a = MVar+  { _cvarId   :: MVarId+  , _cvarVal  :: r (Maybe a)+  }  -- | The mutable non-blocking reference type. These are like 'IORef's. --@@ -53,7 +60,10 @@ -- (so each thread sees its latest write), (b) a commit count (used in -- compare-and-swaps), and (c) the current value visible to all -- threads.-newtype CRef r a = CRef (CRefId, r (Map ThreadId a, Integer, a))+data CRef r a = CRef+  { _crefId   :: CRefId+  , _crefVal  :: r (Map ThreadId a, Integer, a)+  }  -- | The compare-and-swap proof type. --@@ -62,7 +72,11 @@ -- produced, and an @a@ value. This doesn't work in the source package -- (atomic-primops) because of the need to use pointer equality. Here -- we can just pack extra information into 'CRef' to avoid that need.-newtype Ticket a = Ticket (CRefId, Integer, a)+data Ticket a = Ticket+  { _ticketCRef   :: CRefId+  , _ticketWrites :: Integer+  , _ticketVal    :: a+  }  -- | Dict of methods for implementations to override. type Fixed n r s = Ref n r (M n r s)@@ -81,22 +95,22 @@ -- | 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'.+-- implemented in terms of 'newEmptyMVar', 'fork', and 'putMVar'. 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)+    AFork  String ((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)    | AGetNumCapabilities (Int -> Action n r s)   | ASetNumCapabilities Int (Action n r s) -  | forall a. ANewVar     (CVar r a -> Action n r s)-  | forall a. APutVar     (CVar r a) a (Action n r s)-  | forall a. ATryPutVar  (CVar r a) a (Bool -> Action n r s)-  | forall a. AReadVar    (CVar r a) (a -> Action n r s)-  | forall a. ATakeVar    (CVar r a) (a -> Action n r s)-  | forall a. ATryTakeVar (CVar r a) (Maybe a -> Action n r s)+  | forall a. ANewVar String (MVar r a -> Action n r s)+  | forall a. APutVar     (MVar r a) a (Action n r s)+  | forall a. ATryPutVar  (MVar r a) a (Bool -> Action n r s)+  | forall a. AReadVar    (MVar r a) (a -> Action n r s)+  | forall a. ATakeVar    (MVar r a) (a -> Action n r s)+  | forall a. ATryTakeVar (MVar r a) (Maybe a -> Action n r s) -  | forall a.   ANewRef a   (CRef r a -> Action n r s)+  | forall a.   ANewRef String a (CRef r a -> Action n r s)   | forall a.   AReadRef    (CRef r a) (a -> Action n r s)   | forall a.   AReadRefCas (CRef r a) (Ticket a -> Action n r s)   | forall a.   APeekTicket (Ticket a) (a -> Action n r s)@@ -112,9 +126,10 @@   | 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)+  | AKnowsAbout (Either MVarId TVarId) (Action n r s)+  | AForgets    (Either MVarId TVarId) (Action n r s)   | AAllKnown   (Action n r s)+  | AMessage    Dynamic (Action n r s)    | forall a. AAtom (s a) (a -> Action n r s)   | ALift (n (Action n r s))@@ -127,117 +142,150 @@ -- * Identifiers  -- | Every live thread has a unique identitifer.-newtype ThreadId = ThreadId Int-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral)+data ThreadId = ThreadId (Maybe String) Int+  deriving Eq +instance Ord ThreadId where+  compare (ThreadId _ i) (ThreadId _ j) = compare i j+ instance Show ThreadId where-  show (ThreadId i) = show i+  show (ThreadId (Just n) _) = n+  show (ThreadId Nothing  i) = show i --- | Every 'CVar' has a unique identifier.-newtype CVarId = CVarId Int-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral)+instance NFData ThreadId where+  rnf (ThreadId n i) = rnf (n, i) -instance Show CVarId where-  show (CVarId i) = show i+-- | The ID of the initial thread.+initialThread :: ThreadId+initialThread = ThreadId (Just "main") 0 --- | Every 'CRef' has a unique identifier.-newtype CRefId = CRefId Int-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral)+-- | Every @MVar@ has a unique identifier.+data MVarId = MVarId (Maybe String) Int+  deriving Eq +instance Ord MVarId where+  compare (MVarId _ i) (MVarId _ j) = compare i j++instance Show MVarId where+  show (MVarId (Just n) _) = n+  show (MVarId Nothing  i) = show i++instance NFData MVarId where+  rnf (MVarId n i) = rnf (n, i)++-- | Every @CRef@ has a unique identifier.+data CRefId = CRefId (Maybe String) Int+  deriving Eq++instance Ord CRefId where+  compare (CRefId _ i) (CRefId _ j) = compare i j+ instance Show CRefId where-  show (CRefId i) = show i+  show (CRefId (Just n) _) = n+  show (CRefId Nothing  i) = show i +instance NFData CRefId where+  rnf (CRefId n i) = rnf (n, i)++-- | Every @TVar@ has a unique identifier.+data TVarId = TVarId (Maybe String) Int+  deriving Eq++instance Ord TVarId where+  compare (TVarId _ i) (TVarId _ j) = compare i j++instance Show TVarId where+  show (TVarId (Just n) _) = n+  show (TVarId Nothing  i) = show i++instance NFData TVarId where+  rnf (TVarId n i) = rnf (n, i)+ -- | 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 }+data IdSource = Id+  { _nextCRId  :: Int+  , _nextCVId  :: Int+  , _nextTVId  :: Int+  , _nextTId   :: Int+  , _usedCRNames :: [String]+  , _usedCVNames :: [String]+  , _usedTVNames :: [String]+  , _usedTNames  :: [String] }  -- | Get the next free 'CRefId'.-nextCRId :: IdSource -> (IdSource, CRefId)-nextCRId idsource = let newid = _nextCRId idsource + 1 in (idsource { _nextCRId = newid }, newid)+nextCRId :: String -> IdSource -> (IdSource, CRefId)+nextCRId name idsource = (idsource { _nextCRId = newid, _usedCRNames = newlst }, CRefId newname newid) where+  newid  = _nextCRId idsource + 1+  newlst+    | null name = _usedCRNames idsource+    | otherwise = name : _usedCRNames idsource+  newname+    | null name       = Nothing+    | occurrences > 0 = Just (name ++ "-" ++ show occurrences)+    | otherwise       = Just name+  occurrences = length . filter (==name) $ _usedCRNames idsource --- | 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 'MVarId'.+nextCVId :: String -> IdSource -> (IdSource, MVarId)+nextCVId name idsource = (idsource { _nextCVId = newid, _usedCVNames = newlst }, MVarId newname newid) where+  newid  = _nextCVId idsource + 1+  newlst+    | null name = _usedCVNames idsource+    | otherwise = name : _usedCVNames idsource+  newname+    | null name       = Nothing+    | occurrences > 0 = Just (name ++ "-" ++ show occurrences)+    | otherwise       = Just name+  occurrences = length . filter (==name) $ _usedCVNames idsource --- | 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 'TVarId'.+nextTVId :: String -> IdSource -> (IdSource, TVarId)+nextTVId name idsource = (idsource { _nextTVId = newid, _usedTVNames = newlst }, TVarId newname newid) where+  newid  = _nextTVId idsource + 1+  newlst+    | null name = _usedTVNames idsource+    | otherwise = name : _usedTVNames idsource+  newname+    | null name       = Nothing+    | occurrences > 0 = Just (name ++ "-" ++ show occurrences)+    | otherwise       = Just name+  occurrences = length . filter (==name) $ _usedTVNames idsource  -- | Get the next free 'ThreadId'.-nextTId :: IdSource -> (IdSource, ThreadId)-nextTId idsource = let newid = _nextTId idsource + 1 in (idsource { _nextTId = newid }, newid)+nextTId :: String -> IdSource -> (IdSource, ThreadId)+nextTId name idsource = (idsource { _nextTId = newid, _usedTNames = newlst }, ThreadId newname newid) where+  newid  = _nextTId idsource + 1+  newlst+    | null name = _usedTNames idsource+    | otherwise = name : _usedTNames idsource+  newname+    | null name       = Nothing+    | occurrences > 0 = Just (name ++ "-" ++ show occurrences)+    | otherwise       = Just name+  occurrences = length . filter (==name) $ _usedTNames idsource  -- | The initial ID source. initialIdSource :: IdSource-initialIdSource = Id 0 0 0 0+initialIdSource = Id 0 0 0 0 [] [] [] []  -------------------------------------------------------------------------------- -- * Scheduling & Traces --- | A @Scheduler@ maintains some internal state; @s@, takes the trace--- so far; the 'ThreadId' and 'ThreadAction' of the last thread--- scheduled (or 'Nothing' if this is the first decision); and the--- list of runnable threads including a lookahead (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 -> [(Decision, ThreadAction)] -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, NonEmpty Lookahead) -> (Maybe 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 (_, alters, CommitRef t c) = (Commit, goA alters, CommitRef t c)-  go (dec, alters, act) = (dec, goA alters, act)--  goA = map $ \x -> case x of-    (_, WillCommitRef t c:|_) -> (Commit, WillCommitRef t c)-    (d, a:|_) -> (d, a)---- | 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 ((Commit,_,_):ds)       = thread prefix num ++ trace "C" 1 ds-  trace prefix num []                      = thread prefix num+-- | Pretty-print a trace, including a key of the thread IDs. Each+-- line of the key is indented by two spaces.+showTrace :: Trace ThreadId ThreadAction Lookahead -> String+showTrace trc = intercalate "\n" $ trace "" 0 trc : (map ("  "++) . sort . nub $ mapMaybe toKey trc) where+  trace prefix num ((_,_,CommitRef _ _):ds) = thread prefix num ++ trace "C" 1 ds+  trace prefix num ((Start    (ThreadId _ i),_,_):ds) = thread prefix num ++ trace ("S" ++ show i) 1 ds+  trace prefix num ((SwitchTo (ThreadId _ i),_,_):ds) = thread prefix num ++ trace ("P" ++ show i) 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.-  | Commit-  -- ^ Commit a 'CRef' write action so that every thread can see the-  -- result.-  deriving (Eq, Show)--instance NFData Decision where-  rnf (Start    tid) = rnf tid-  rnf (SwitchTo tid) = rnf tid-  rnf d = d `seq` ()+  toKey (Start (ThreadId (Just name) i), _, _) = Just $ show i ++ ": " ++ name+  toKey _ = Nothing  -- | All the actions that a thread can perform. data ThreadAction =@@ -251,24 +299,24 @@   -- ^ Set the number of Haskell threads that can run simultaneously.   | Yield   -- ^ Yield the current thread.-  | NewVar CVarId-  -- ^ Create a new 'CVar'.-  | PutVar CVarId [ThreadId]-  -- ^ Put into a 'CVar', possibly waking up some threads.-  | BlockedPutVar CVarId+  | NewVar MVarId+  -- ^ Create a new 'MVar'.+  | PutVar MVarId [ThreadId]+  -- ^ Put into a 'MVar', possibly waking up some threads.+  | BlockedPutVar MVarId   -- ^ Get blocked on a put.-  | TryPutVar CVarId Bool [ThreadId]-  -- ^ Try to put into a 'CVar', possibly waking up some threads.-  | ReadVar CVarId-  -- ^ Read from a 'CVar'.-  | BlockedReadVar CVarId+  | TryPutVar MVarId Bool [ThreadId]+  -- ^ Try to put into a 'MVar', possibly waking up some threads.+  | ReadVar MVarId+  -- ^ Read from a 'MVar'.+  | BlockedReadVar MVarId   -- ^ Get blocked on a read.-  | TakeVar CVarId [ThreadId]-  -- ^ Take from a 'CVar', possibly waking up some threads.-  | BlockedTakeVar CVarId+  | TakeVar MVarId [ThreadId]+  -- ^ Take from a 'MVar', possibly waking up some threads.+  | BlockedTakeVar MVarId   -- ^ Get blocked on a take.-  | TryTakeVar CVarId Bool [ThreadId]-  -- ^ Try to take from a 'CVar', possibly waking up some threads.+  | TryTakeVar MVarId Bool [ThreadId]+  -- ^ Try to take from a 'MVar', possibly waking up some threads.   | NewRef CRefId   -- ^ Create a new 'CRef'.   | ReadRef CRefId@@ -289,13 +337,10 @@   | CommitRef ThreadId CRefId   -- ^ Commit the last write to the given 'CRef' by the given thread,   -- so that all threads can see the updated value.-  | STM [ThreadId]+  | STM TTrace [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+  | BlockedSTM TTrace   -- ^ Got blocked in an STM transaction.   | Catching   -- ^ Register a new exception handler@@ -329,9 +374,11 @@   -- ^ A '_concForgets' annotation was processed.   | AllKnown   -- ^ A '_concALlKnown' annotation was processed.+  | Message Dynamic+  -- ^ A '_concMessage' annotation was processed.   | Stop   -- ^ Cease execution and terminate.-  deriving (Eq, Show)+  deriving Show  instance NFData ThreadAction where   rnf (Fork t) = rnf t@@ -355,13 +402,63 @@   rnf (WriteRef c) = rnf c   rnf (CasRef c b) = rnf (c, b)   rnf (CommitRef t c) = rnf (t, c)-  rnf (STM ts) = rnf ts+  rnf (STM s ts) = rnf (s, ts)+  rnf (BlockedSTM s) = rnf s   rnf (ThrowTo t) = rnf t   rnf (BlockedThrowTo t) = rnf t   rnf (SetMasking b m) = b `seq` m `seq` ()   rnf (ResetMasking b m) = b `seq` m `seq` ()+  rnf (Message m) = m `seq` ()   rnf a = a `seq` () +-- | Check if a @ThreadAction@ immediately blocks.+isBlock :: ThreadAction -> Bool+isBlock (BlockedThrowTo  _) = True+isBlock (BlockedTakeVar _) = True+isBlock (BlockedReadVar _) = True+isBlock (BlockedPutVar  _) = True+isBlock (BlockedSTM _) = True+isBlock _ = False++-- | A trace of an STM transaction is just a list of actions that+-- occurred, as there are no scheduling decisions to make.+type TTrace = [TAction]++-- | All the actions that an STM transaction can perform.+data TAction =+    TNew+  -- ^ Create a new @TVar@+  | TRead  TVarId+  -- ^ Read from a @TVar@.+  | TWrite TVarId+  -- ^ Write to a @TVar@.+  | TRetry+  -- ^ Abort and discard effects.+  | TOrElse TTrace (Maybe TTrace)+  -- ^ Execute a transaction until it succeeds (@STMStop@) or aborts+  -- (@STMRetry@) and, if it aborts, execute the other transaction.+  | TThrow+  -- ^ Throw an exception, abort, and discard effects.+  | TCatch TTrace (Maybe TTrace)+  -- ^ Execute a transaction until it succeeds (@STMStop@) or aborts+  -- (@STMThrow@). If the exception is of the appropriate type, it is+  -- handled and execution continues; otherwise aborts, propagating+  -- the exception upwards.+  | TStop+  -- ^ Terminate successfully and commit effects.+  | TLift+  -- ^ Lifts 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.+  deriving (Eq, Show)++instance NFData TAction where+  rnf (TRead  v) = rnf v+  rnf (TWrite v) = rnf v+  rnf (TCatch  s m) = rnf (s, m)+  rnf (TOrElse s m) = rnf (s, m)+  rnf a = a `seq` ()+ -- | A one-step look-ahead at what a thread will do next. data Lookahead =     WillFork@@ -377,17 +474,17 @@   | WillYield   -- ^ Will yield the current thread.   | WillNewVar-  -- ^ Will create a new 'CVar'.-  | WillPutVar CVarId-  -- ^ Will put into a 'CVar', possibly waking up some threads.-  | WillTryPutVar CVarId-  -- ^ Will try to put into a 'CVar', possibly waking up some threads.-  | WillReadVar CVarId-  -- ^ Will read from a 'CVar'.-  | WillTakeVar CVarId-  -- ^ Will take from a 'CVar', possibly waking up some threads.-  | WillTryTakeVar CVarId-  -- ^ Will try to take from a 'CVar', possibly waking up some threads.+  -- ^ Will create a new 'MVar'.+  | WillPutVar MVarId+  -- ^ Will put into a 'MVar', possibly waking up some threads.+  | WillTryPutVar MVarId+  -- ^ Will try to put into a 'MVar', possibly waking up some threads.+  | WillReadVar MVarId+  -- ^ Will read from a 'MVar'.+  | WillTakeVar MVarId+  -- ^ Will take from a 'MVar', possibly waking up some threads.+  | WillTryTakeVar MVarId+  -- ^ Will try to take from a 'MVar', possibly waking up some threads.   | WillNewRef   -- ^ Will create a new 'CRef'.   | WillReadRef CRefId@@ -438,9 +535,11 @@   -- ^ Will process a '_concForgets' annotation.   | WillAllKnown   -- ^ Will process a '_concALlKnown' annotation.+  | WillMessage Dynamic+  -- ^ Will process a _concMessage' annotation.   | WillStop   -- ^ Will cease execution and terminate.-  deriving (Eq, Show)+  deriving Show  instance NFData Lookahead where   rnf (WillSetNumCapabilities i) = rnf i@@ -460,29 +559,30 @@   rnf (WillThrowTo t) = rnf t   rnf (WillSetMasking b m) = b `seq` m `seq` ()   rnf (WillResetMasking b m) = b `seq` m `seq` ()+  rnf (WillMessage m) = m `seq` ()   rnf l = l `seq` ()  -- | Look as far ahead in the given continuation as possible. lookahead :: Action n r s -> NonEmpty Lookahead-lookahead = unsafeToNonEmpty . lookahead' where-  lookahead' (AFork _ _)             = [WillFork]+lookahead = fromList . lookahead' where+  lookahead' (AFork _ _ _)           = [WillFork]   lookahead' (AMyTId _)              = [WillMyThreadId]   lookahead' (AGetNumCapabilities _) = [WillGetNumCapabilities]   lookahead' (ASetNumCapabilities i k) = WillSetNumCapabilities i : lookahead' k-  lookahead' (ANewVar _)             = [WillNewVar]-  lookahead' (APutVar (CVar (c, _)) _ k)    = WillPutVar c : lookahead' k-  lookahead' (ATryPutVar (CVar (c, _)) _ _) = [WillTryPutVar c]-  lookahead' (AReadVar (CVar (c, _)) _)     = [WillReadVar c]-  lookahead' (ATakeVar (CVar (c, _)) _)     = [WillTakeVar c]-  lookahead' (ATryTakeVar (CVar (c, _)) _)  = [WillTryTakeVar c]-  lookahead' (ANewRef _ _)           = [WillNewRef]-  lookahead' (AReadRef (CRef (r, _)) _)     = [WillReadRef r]-  lookahead' (AReadRefCas (CRef (r, _)) _)  = [WillReadRefCas r]-  lookahead' (APeekTicket (Ticket (r, _, _)) _) = [WillPeekTicket r]-  lookahead' (AModRef (CRef (r, _)) _ _)    = [WillModRef r]-  lookahead' (AModRefCas (CRef (r, _)) _ _) = [WillModRefCas r]-  lookahead' (AWriteRef (CRef (r, _)) _ k) = WillWriteRef r : lookahead' k-  lookahead' (ACasRef (CRef (r, _)) _ _ _) = [WillCasRef r]+  lookahead' (ANewVar _ _)           = [WillNewVar]+  lookahead' (APutVar (MVar c _) _ k)    = WillPutVar c : lookahead' k+  lookahead' (ATryPutVar (MVar c _) _ _) = [WillTryPutVar c]+  lookahead' (AReadVar (MVar c _) _)     = [WillReadVar c]+  lookahead' (ATakeVar (MVar c _) _)     = [WillTakeVar c]+  lookahead' (ATryTakeVar (MVar c _) _)  = [WillTryTakeVar c]+  lookahead' (ANewRef _ _ _)         = [WillNewRef]+  lookahead' (AReadRef (CRef r _) _)     = [WillReadRef r]+  lookahead' (AReadRefCas (CRef r _) _)  = [WillReadRefCas r]+  lookahead' (APeekTicket (Ticket r _ _) _) = [WillPeekTicket r]+  lookahead' (AModRef (CRef r _) _ _)    = [WillModRef r]+  lookahead' (AModRefCas (CRef r _) _ _) = [WillModRefCas r]+  lookahead' (AWriteRef (CRef r _) _ k) = WillWriteRef r : lookahead' k+  lookahead' (ACasRef (CRef r _) _ _ _) = [WillCasRef r]   lookahead' (ACommit t c)           = [WillCommitRef t c]   lookahead' (AAtom _ _)             = [WillSTM]   lookahead' (AThrow _)              = [WillThrow]@@ -495,6 +595,7 @@   lookahead' (AKnowsAbout _ k)       = WillKnowsAbout : lookahead' k   lookahead' (AForgets _ k)          = WillForgets : lookahead' k   lookahead' (AAllKnown k)           = WillAllKnown : lookahead' k+  lookahead' (AMessage m k)          = WillMessage m : lookahead' k   lookahead' (AYield k)              = WillYield : lookahead' k   lookahead' (AReturn k)             = WillReturn : lookahead' k   lookahead' AStop                   = [WillStop]@@ -515,6 +616,16 @@ willRelease WillStop = True willRelease _ = False +-- Count the number of pre-emptions in a schedule prefix.+preEmpCount :: [(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Int+preEmpCount ts (d, _) = go Nothing ts where+  go p ((d', a):rest) = preEmpC p d' + go (Just a) rest+  go p [] = preEmpC p d++  preEmpC (Just Yield) (SwitchTo _) = 0+  preEmpC _ (SwitchTo t) = if t >= initialThread then 1 else 0+  preEmpC _ _ = 0+ -- | A simplified view of the possible actions a thread can perform. data ActionType =     UnsynchronisedRead  CRefId@@ -532,10 +643,10 @@   -- ^ A 'modifyCRefCAS'   | SynchronisedModify  CRefId   -- ^ An 'atomicModifyCRef'.-  | SynchronisedRead    CVarId-  -- ^ A 'readCVar' or 'takeCVar' (or @try@/@blocked@ variants).-  | SynchronisedWrite   CVarId-  -- ^ A 'putCVar' (or @try@/@blocked@ variant).+  | SynchronisedRead    MVarId+  -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants).+  | SynchronisedWrite   MVarId+  -- ^ A 'putMVar' (or @try@/@blocked@ variant).   | SynchronisedOther   -- ^ Some other action which does require cross-thread   -- communication.@@ -560,12 +671,16 @@ isBarrier SynchronisedOther = True isBarrier _ = False --- | Check if an action is synchronises a given 'CRef'.+-- | Check if an action commits a given 'CRef'.+isCommit :: ActionType -> CRefId -> Bool+isCommit (PartiallySynchronisedCommit c) r = c == r+isCommit (PartiallySynchronisedWrite  c) r = c == r+isCommit (PartiallySynchronisedModify c) r = c == r+isCommit _ _ = False++-- | Check if an action synchronises a given 'CRef'. synchronises :: ActionType -> CRefId -> Bool-synchronises (PartiallySynchronisedCommit c) r = c == r-synchronises (PartiallySynchronisedWrite  c) r = c == r-synchronises (PartiallySynchronisedModify c) r = c == r-synchronises a _ = isBarrier a+synchronises a r = isCommit a r || isBarrier a  -- | Get the 'CRef' affected. crefOf :: ActionType -> Maybe CRefId@@ -577,8 +692,8 @@ crefOf (PartiallySynchronisedModify r) = Just r crefOf _ = Nothing --- | Get the 'CVar' affected.-cvarOf :: ActionType -> Maybe CVarId+-- | Get the 'MVar' affected.+cvarOf :: ActionType -> Maybe MVarId cvarOf (SynchronisedRead  c) = Just c cvarOf (SynchronisedWrite c) = Just c cvarOf _ = Nothing@@ -604,8 +719,8 @@ simplify (WriteRef r)    = UnsynchronisedWrite r simplify (CasRef r _)    = PartiallySynchronisedWrite r simplify (CommitRef _ r) = PartiallySynchronisedCommit r-simplify (STM _)            = SynchronisedOther-simplify BlockedSTM         = SynchronisedOther+simplify (STM _ _)          = SynchronisedOther+simplify (BlockedSTM _)     = SynchronisedOther simplify (ThrowTo _)        = SynchronisedOther simplify (BlockedThrowTo _) = SynchronisedOther simplify _ = UnsynchronisedOther@@ -643,9 +758,9 @@   -- bounds (there have been too many pre-emptions, the computation   -- has executed for too long, or there have been too many yields).   | Deadlock-  -- ^ The computation became blocked indefinitely on @CVar@s.+  -- ^ The computation became blocked indefinitely on @MVar@s.   | STMDeadlock-  -- ^ The computation became blocked indefinitely on @CTVar@s.+  -- ^ The computation became blocked indefinitely on @TVar@s.   | UncaughtException   -- ^ An uncaught exception bubbled to the top of the computation.   deriving (Eq, Show, Read, Ord, Enum, Bounded)

@@ -1,12 +1,20 @@ {-# LANGUAGE BangPatterns #-}-{-# LANGUAGE CPP          #-} {-# LANGUAGE GADTs        #-} --- | Operations over @CRef@s and @CVar@s+-- | Operations over @CRef@s and @MVar@s+--+-- Relaxed memory operations over @CRef@s are implemented with an+-- explicit write buffer: one per thread for TSO, and one per+-- thread/variable combination for PSO. Unsynchronised writes append+-- to this buffer, and periodically separate threads commit from these+-- buffers to the \"actual\" @CRef@.+--+-- This model comes from /Dynamic Partial Order Reduction for Relaxed+-- Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015). module Test.DejaFu.Deterministic.Internal.Memory where  import Control.Monad (when)-import Data.IntMap.Strict (IntMap)+import Data.Map.Strict (Map) import Data.Maybe (isJust, fromJust) import Data.Monoid ((<>)) import Data.Sequence (Seq, ViewL(..), (><), singleton, viewl)@@ -14,22 +22,18 @@ import Test.DejaFu.Deterministic.Internal.Threading import Test.DejaFu.Internal -import qualified Data.IntMap.Strict as I import qualified Data.Map.Strict as M -#if __GLASGOW_HASKELL__ < 710-import Data.Foldable (mapM_)-import Prelude hiding (mapM_)-#endif- -------------------------------------------------------------------------------- -- * Manipulating @CRef@s  -- | In non-sequentially-consistent memory models, non-synchronised -- writes get buffered. ----- In TSO, the keys are @ThreadId@s. In PSO, the keys are @CRefId@s.-newtype WriteBuffer r = WriteBuffer { buffer :: IntMap (Seq (BufferedWrite r)) }+-- The @CRefId@ parameter is only used under PSO. Under TSO each+-- thread has a single buffer.+newtype WriteBuffer r = WriteBuffer+  { buffer :: Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite r)) }  -- | A buffered write is a reference to the variable, and the value to -- write. Universally quantified over the value type so that the only@@ -39,28 +43,28 @@  -- | An empty write buffer. emptyBuffer :: WriteBuffer r-emptyBuffer = WriteBuffer I.empty+emptyBuffer = WriteBuffer M.empty  -- | Add a new write to the end of a buffer.-bufferWrite :: Monad n => Fixed n r s -> WriteBuffer r -> Int -> CRef r a -> a -> ThreadId -> n (WriteBuffer r)-bufferWrite fixed (WriteBuffer wb) i cref@(CRef (_, ref)) new tid = do+bufferWrite :: Monad n => Fixed n r s -> WriteBuffer r -> (ThreadId, Maybe CRefId) -> CRef r a -> a -> n (WriteBuffer r)+bufferWrite fixed (WriteBuffer wb) k@(tid, _) cref@(CRef _ ref) new = do   -- Construct the new write buffer   let write = singleton $ BufferedWrite tid cref new-  let buffer' = I.insertWith (><) i write wb+  let buffer' = M.insertWith (flip (><)) k write wb    -- Write the thread-local value to the @CRef@'s update map.-  (map, count, def) <- readRef fixed ref-  writeRef fixed ref (M.insert tid new map, count, def)+  (locals, count, def) <- readRef fixed ref+  writeRef fixed ref (M.insert tid new locals, count, def)    return $ WriteBuffer buffer'  -- | Commit the write at the head of a buffer.-commitWrite :: Monad n => Fixed n r s -> WriteBuffer r -> Int -> n (WriteBuffer r)-commitWrite fixed w@(WriteBuffer wb) i = case maybe EmptyL viewl $ I.lookup i wb of+commitWrite :: Monad n => Fixed n r s -> WriteBuffer r -> (ThreadId, Maybe CRefId) -> n (WriteBuffer r)+commitWrite fixed w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of   BufferedWrite _ cref a :< rest -> do     writeImmediate fixed cref a-    return . WriteBuffer $ I.insert i rest wb-    +    return . WriteBuffer $ M.insert k rest wb+   EmptyL -> return w  -- | Read from a @CRef@, returning a newer thread-local non-committed@@ -73,15 +77,15 @@ -- | Read from a @CRef@, returning a @Ticket@ representing the current -- view of the thread. readForTicket :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (Ticket a)-readForTicket fixed cref@(CRef (crid, _)) tid = do+readForTicket fixed cref@(CRef crid _) tid = do   (val, count) <- readCRefPrim fixed cref tid-  return $ Ticket (crid, count, val)+  return $ Ticket crid count val  -- | Perform a compare-and-swap on a @CRef@ if the ticket is still -- valid. This is strict in the \"new\" value argument. casCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a)-casCRef fixed cref tid (Ticket (_, cc, _)) !new = do-  tick'@(Ticket (_, cc', _)) <- readForTicket fixed cref tid+casCRef fixed cref tid (Ticket _ cc _) !new = do+  tick'@(Ticket _ cc' _) <- readForTicket fixed cref tid    if cc == cc'   then do@@ -92,7 +96,7 @@  -- | Read the local state of a @CRef@. readCRefPrim :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (a, Integer)-readCRefPrim fixed (CRef (_, ref)) tid = do+readCRefPrim fixed (CRef _ ref) tid = do   (vals, count, def) <- readRef fixed ref    return (M.findWithDefault def tid vals, count)@@ -100,65 +104,68 @@ -- | Write and commit to a @CRef@ immediately, clearing the update map -- and incrementing the write count. writeImmediate :: Monad n => Fixed n r s -> CRef r a -> a -> n ()-writeImmediate fixed (CRef (_, ref)) a = do+writeImmediate fixed (CRef _ ref) a = do   (_, count, _) <- readRef fixed ref   writeRef fixed ref (M.empty, count + 1, a)  -- | Flush all writes in the buffer. writeBarrier :: Monad n => Fixed n r s -> WriteBuffer r -> n ()-writeBarrier fixed (WriteBuffer wb) = mapM_ flush $ I.elems wb where+writeBarrier fixed (WriteBuffer wb) = mapM_ flush $ M.elems wb where   flush = mapM_ $ \(BufferedWrite _ cref a) -> writeImmediate fixed cref a  -- | Add phantom threads to the thread list to commit pending writes. addCommitThreads :: WriteBuffer r -> Threads n r s -> Threads n r s addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where-  phantoms = [(ThreadId $ negate k - 1, mkthread $ fromJust c) | (k, b) <- I.toList wb, let c = go $ viewl b, isJust c]-  go (BufferedWrite tid (CRef (crid, _)) _ :< _) = Just $ ACommit tid crid+  phantoms = [ (ThreadId Nothing $ negate tid, mkthread $ fromJust c)+             | ((k, b), tid) <- zip (M.toList wb) [1..]+             , let c = go $ viewl b+             , isJust c]+  go (BufferedWrite tid (CRef crid _) _ :< _) = Just $ ACommit tid crid   go EmptyL = Nothing  -- | Remove phantom threads. delCommitThreads :: Threads n r s -> Threads n r s-delCommitThreads = M.filterWithKey $ \k _ -> k >= 0+delCommitThreads = M.filterWithKey $ \k _ -> k >= initialThread  ----------------------------------------------------------------------------------- * Manipulating @CVar@s+-- * Manipulating @MVar@s --- | Put into a @CVar@, blocking if full.-putIntoCVar :: Monad n => CVar r a -> a -> Action n r s+-- | Put into a @MVar@, blocking if full.+putIntoMVar :: Monad n => MVar r a -> a -> Action n r s              -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])-putIntoCVar cvar a c = mutCVar True cvar a (const c)+putIntoMVar cvar a c = mutMVar True cvar a (const c) --- | Try to put into a @CVar@, not blocking if full.-tryPutIntoCVar :: Monad n => CVar r a -> a -> (Bool -> Action n r s)+-- | Try to put into a @MVar@, not blocking if full.+tryPutIntoMVar :: Monad n => MVar r a -> a -> (Bool -> Action n r s)                  -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])-tryPutIntoCVar = mutCVar False+tryPutIntoMVar = mutMVar False --- | Read from a @CVar@, blocking if empty.-readFromCVar :: Monad n => CVar r a -> (a -> Action n r s)+-- | Read from a @MVar@, blocking if empty.+readFromMVar :: Monad n => MVar r a -> (a -> Action n r s)               -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])-readFromCVar cvar c = seeCVar False True cvar (c . fromJust)+readFromMVar cvar c = seeMVar False True cvar (c . fromJust) --- | Take from a @CVar@, blocking if empty.-takeFromCVar :: Monad n => CVar r a -> (a -> Action n r s)+-- | Take from a @MVar@, blocking if empty.+takeFromMVar :: Monad n => MVar r a -> (a -> Action n r s)               -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])-takeFromCVar cvar c = seeCVar True True cvar (c . fromJust)+takeFromMVar cvar c = seeMVar True True cvar (c . fromJust) --- | Try to take from a @CVar@, not blocking if empty.-tryTakeFromCVar :: Monad n => CVar r a -> (Maybe a -> Action n r s)+-- | Try to take from a @MVar@, not blocking if empty.+tryTakeFromMVar :: Monad n => MVar r a -> (Maybe a -> Action n r s)                   -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])-tryTakeFromCVar = seeCVar True False+tryTakeFromMVar = seeMVar True False --- | Mutate a @CVar@, in either a blocking or nonblocking way.-mutCVar :: Monad n-         => Bool -> CVar r a -> a -> (Bool -> Action n r s)+-- | Mutate a @MVar@, in either a blocking or nonblocking way.+mutMVar :: Monad n+         => Bool -> MVar r a -> a -> (Bool -> Action n r s)          -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])-mutCVar blocking (CVar (cvid, ref)) a c fixed threadid threads = do+mutMVar blocking (MVar cvid ref) a c fixed threadid threads = do   val <- readRef fixed ref    case val of     Just _       | blocking ->-        let threads' = block (OnCVarEmpty cvid) threadid threads+        let threads' = block (OnMVarEmpty cvid) threadid threads         in return (False, threads', [])        | otherwise ->@@ -166,26 +173,26 @@      Nothing -> do       writeRef fixed ref $ Just a-      let (threads', woken) = wake (OnCVarFull cvid) threads+      let (threads', woken) = wake (OnMVarFull cvid) threads       return (True, goto (c True) threadid threads', woken) --- | Read a @CVar@, in either a blocking or nonblocking+-- | Read a @MVar@, in either a blocking or nonblocking -- way.-seeCVar :: Monad n-         => Bool -> Bool -> CVar r a -> (Maybe a -> Action n r s)+seeMVar :: Monad n+         => Bool -> Bool -> MVar r a -> (Maybe a -> Action n r s)          -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])-seeCVar emptying blocking (CVar (cvid, ref)) c fixed threadid threads = do+seeMVar emptying blocking (MVar 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+      let (threads', woken) = wake (OnMVarEmpty cvid) threads       return (True, goto (c val) threadid threads', woken)      Nothing       | blocking ->-        let threads' = block (OnCVarFull cvid) threadid threads+        let threads' = block (OnMVarFull cvid) threadid threads         in return (False, threads', [])        | otherwise ->

@@ -1,4 +1,3 @@-{-# LANGUAGE CPP                       #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE RankNTypes                #-} @@ -9,15 +8,10 @@ import Data.List (intersect, nub) import Data.Map.Strict (Map) import Data.Maybe (fromMaybe, isJust, isNothing)-import Test.DejaFu.STM (CTVarId) import Test.DejaFu.Deterministic.Internal.Common  import qualified Data.Map.Strict as M -#if __GLASGOW_HASKELL__ < 710-import Control.Applicative ((<$>))-#endif- -------------------------------------------------------------------------------- -- * Threads @@ -34,7 +28,7 @@   -- ^ Stack of exception handlers   , _masking      :: MaskingState   -- ^ The exception masking state.-  , _known        :: [Either CVarId CTVarId]+  , _known        :: [Either MVarId TVarId]   -- ^ Shared variables the thread knows about.   , _fullknown    :: Bool   -- ^ Whether the referenced variables of the thread are completely@@ -51,14 +45,14 @@  -- | 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+data BlockedOn = OnMVarFull MVarId | OnMVarEmpty MVarId | OnTVar [TVarId] | 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 (OnMVarFull  _), OnMVarFull  _) -> True+  (Just (OnMVarEmpty _), OnMVarEmpty _) -> True+  (Just (OnTVar      _), OnTVar      _) -> True   (Just (OnMask      _), OnMask      _) -> True   _ -> False @@ -78,18 +72,18 @@      -- | 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 (Just (OnMVarFull  cvarid)) = null $ findMVar  cvarid+    noRefs (Just (OnMVarEmpty cvarid)) = null $ findMVar  cvarid+    noRefs (Just (OnTVar      tvids))  = null $ findTVars tvids     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+    -- consideration) which reference a 'MVar'.+    findMVar 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+    -- consideration) which reference some 'TVar's.+    findTVars tvids = M.keys $ M.filterWithKey (check (map Right tvids)) ts      -- | Check if a thread references a variable, and if it's not the     -- thread under consideration.@@ -144,15 +138,15 @@ -- | 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+launch parent tid a threads = launch' ms tid a threads where+  ms = 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 }+launch' ms tid a = M.insert tid thread where+  thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = ms, _known = [], _fullknown = False } -  umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False mask >> return b+  umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False ms >> return b   resetMask typ m = cont $ \k -> AResetMask typ True m $ k ()  -- | Kill a thread.@@ -165,9 +159,9 @@   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'+-- | Unblock all threads waiting on the appropriate block. For 'TVar' -- blocks, this will wake all threads waiting on at least one of the--- given 'CTVar's.+-- given 'TVar's. wake :: BlockedOn -> Threads n r s -> (Threads n r s, [ThreadId]) wake blockedOn threads = (unblock <$> threads, M.keys $ M.filter isBlocked threads) where   unblock thread@@ -175,17 +169,17 @@     | otherwise = thread    isBlocked thread = case (_blocking thread, blockedOn) of-    (Just (OnCTVar ctvids), OnCTVar blockedOn') -> ctvids `intersect` blockedOn' /= []+    (Just (OnTVar tvids), OnTVar blockedOn') -> tvids `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 :: [Either MVarId TVarId] -> 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 :: [Either MVarId TVarId] -> 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!"

@@ -1,57 +0,0 @@--- | 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 = (Just $ 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 _ = (Just 0, ())-roundRobinSched _ _ (Just (prior, _)) threads-  | prior >= maximum threads' = (Just $ minimum threads', ())-  | otherwise = (Just . 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 trc p@(Just (prior, _)) threads-    | prior `elem` map fst (toList threads) = (Just prior, s)-    | otherwise = sched s trc p threads-  newsched s trc Nothing threads = sched s trc Nothing threads

@@ -1,6 +1,4 @@-{-# LANGUAGE CPP                        #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE RankNTypes                 #-}+{-# LANGUAGE RankNTypes #-}  -- | Systematic testing for concurrent computations. module Test.DejaFu.SCT@@ -25,7 +23,6 @@   -- K. McKinley for more details.      BacktrackStep(..)-  , BoundFunc    , sctBounded   , sctBoundedIO@@ -44,6 +41,7 @@    , Bounds(..)   , defaultBounds+  , noBounds    , sctBound   , sctBoundIO@@ -63,6 +61,8 @@   , defaultPreemptionBound   , sctPreBound   , sctPreBoundIO+  , pBacktrack+  , pBound    -- ** Fair Bounding @@ -76,6 +76,8 @@   , defaultFairBound   , sctFairBound   , sctFairBoundIO+  , fBacktrack+  , fBound    -- ** Length Bounding @@ -86,73 +88,50 @@   , defaultLengthBound   , sctLengthBound   , sctLengthBoundIO--  -- * Utilities--  , (&+&)-  , trueBound-  , tidOf-  , decisionOf-  , activeTid-  , preEmpCount-  , preEmpCount'-  , yieldCount-  , maxYieldCountDiff-  , initialise-  , initialCVState-  , updateCVState-  , willBlock-  , willBlockSafely   ) where -import Control.DeepSeq (NFData, force) import Data.Functor.Identity (Identity(..), runIdentity)-import Data.List (nub, partition)-import Data.Sequence (Seq, (|>))-import Data.Map (Map)-import Data.Maybe (isNothing, isJust, fromJust)-import Test.DejaFu.Deterministic-import Test.DejaFu.Deterministic.Internal (willRelease)-import Test.DejaFu.SCT.Internal-+import Data.Map.Strict (Map) import qualified Data.Map.Strict as M-import qualified Data.Sequence as Sq-import qualified Data.Set as S--#if __GLASGOW_HASKELL__ < 710-import Control.Applicative ((<$>), (<*>))-#endif---- | A bounding function takes the scheduling decisions so far and a--- decision chosen to come next, and returns if that decision is--- within the bound.-type BoundFunc = [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool---- | Combine two bounds into a larger bound, where both must be--- satisfied.-(&+&) :: BoundFunc -> BoundFunc -> BoundFunc-(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl+import Data.Maybe (isJust, fromJust)+import Test.DPOR ( DPOR(..), dpor+                 , BacktrackStep(..), backtrackAt+                 , BoundFunc, (&+&), trueBound+                 , PreemptionBound(..), defaultPreemptionBound, preempBacktrack+                 , FairBound(..), defaultFairBound, fairBound, fairBacktrack+                 , LengthBound(..), defaultLengthBound, lenBound, lenBacktrack+                 ) --- | The \"true\" bound, which allows everything.-trueBound :: BoundFunc-trueBound _ _ = True+import Test.DejaFu.Deterministic (ConcIO, ConcST, runConcIO, runConcST)+import Test.DejaFu.Deterministic.Internal --- * Combined Bounds+-------------------------------------------------------------------------------+-- Combined Bounds  data Bounds = Bounds-  { preemptionBound :: Maybe PreemptionBound-  , fairBound       :: Maybe FairBound-  , lengthBound     :: Maybe LengthBound+  { boundPreemp :: Maybe PreemptionBound+  , boundFair   :: Maybe FairBound+  , boundLength :: Maybe LengthBound   }  -- | All bounds enabled, using their default values. defaultBounds :: Bounds defaultBounds = Bounds-  { preemptionBound = Just defaultPreemptionBound-  , fairBound       = Just defaultFairBound-  , lengthBound     = Just defaultLengthBound+  { boundPreemp = Just defaultPreemptionBound+  , boundFair   = Just defaultFairBound+  , boundLength = Just defaultLengthBound   } +-- | No bounds enabled. This forces the scheduler to just use+-- partial-order reduction and sleep sets to prune the search+-- space. This will /ONLY/ work if your computation always terminated!+noBounds :: Bounds+noBounds = Bounds+  { boundPreemp = Nothing+  , boundFair   = Nothing+  , boundLength = Nothing+  }+ -- | An SCT runner using a bounded scheduler sctBound :: MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.@@ -160,33 +139,37 @@   -- ^ The combined bounds.   -> (forall t. ConcST t a)   -- ^ The computation to run many times-  -> [(Either Failure a, Trace)]+  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] sctBound memtype cb = sctBounded memtype (cBound cb) (cBacktrack cb)  -- | Variant of 'sctBound' for computations which do 'IO'.-sctBoundIO :: MemType -> Bounds -> ConcIO a -> IO [(Either Failure a, Trace)]+sctBoundIO :: MemType+  -> Bounds+  -> ConcIO a+  -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] sctBoundIO memtype cb = sctBoundedIO memtype (cBound cb) (cBacktrack cb)  -- | Combination bound function-cBound :: Bounds -> BoundFunc-cBound (Bounds pb fb lb) = maybe trueBound pbBound pb &+& maybe trueBound fBound fb &+& maybe trueBound lBound lb+cBound :: Bounds -> BoundFunc ThreadId ThreadAction Lookahead+cBound (Bounds pb fb lb) = maybe trueBound pBound pb &+& maybe trueBound fBound fb &+& maybe trueBound lenBound lb  -- | Combination backtracking function. Add all backtracking points -- corresponding to enabled bound functions.-cBacktrack :: Bounds -> [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]+--+-- If no bounds are enabled, just backtrack to the given point.+cBacktrack :: Bounds+  -> [BacktrackStep ThreadId ThreadAction Lookahead s]+  -> Int+  -> ThreadId+  -> [BacktrackStep ThreadId ThreadAction Lookahead s]+cBacktrack (Bounds Nothing Nothing Nothing) bs i t = backtrackAt (const False) False bs i t cBacktrack (Bounds pb fb lb) bs i t = lBack . fBack $ pBack bs where-  pBack backs = if isJust pb then pbBacktrack backs i t else backs-  fBack backs = if isJust fb then fBacktrack  backs i t else backs-  lBack backs = if isJust lb then lBacktrack  backs i t else backs---- * Pre-emption bounding--newtype PreemptionBound = PreemptionBound Int-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)+  pBack backs = if isJust pb then pBacktrack   backs i t else backs+  fBack backs = if isJust fb then fBacktrack   backs i t else backs+  lBack backs = if isJust lb then lenBacktrack backs i t else backs --- | A sensible default pre-emption bound: 2-defaultPreemptionBound :: PreemptionBound-defaultPreemptionBound = 2+-------------------------------------------------------------------------------+-- Pre-emption bounding  -- | An SCT runner using a pre-emption bounding scheduler. sctPreBound :: MemType@@ -196,77 +179,37 @@   -- execution   -> (forall t. ConcST t a)   -- ^ The computation to run many times-  -> [(Either Failure a, Trace)]-sctPreBound memtype pb = sctBounded memtype (pbBound pb) pbBacktrack+  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]+sctPreBound memtype pb = sctBounded memtype (pBound pb) pBacktrack  -- | Variant of 'sctPreBound' for computations which do 'IO'.-sctPreBoundIO :: MemType -> PreemptionBound -> ConcIO a -> IO [(Either Failure a, Trace)]-sctPreBoundIO memtype pb = sctBoundedIO memtype (pbBound pb) pbBacktrack---- | Pre-emption bound function-pbBound :: PreemptionBound -> BoundFunc-pbBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb---- | Count the number of pre-emptions in a schedule prefix.-preEmpCount :: [(Decision, ThreadAction)] -> (Decision, a) -> Int-preEmpCount ts (d, _) = go Nothing ts where-  go p ((d, a):rest) = preEmpC p d + go (Just a) rest-  go p [] = preEmpC p d--  preEmpC (Just Yield) (SwitchTo _) = 0-  preEmpC _ (SwitchTo t) = if t >= 0 then 1 else 0-  preEmpC _ _ = 0---- | Count the number of pre-emptions in an entire trace-preEmpCount' :: Trace -> Int-preEmpCount' trc = preEmpCount (map (\(d,_,a) -> (d, a)) trc) (Continue, WillStop)+sctPreBoundIO :: MemType+  -> PreemptionBound+  -> ConcIO a+  -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]+sctPreBoundIO memtype pb = sctBoundedIO memtype (pBound pb) pBacktrack  -- | 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 && not (commit b1) && not (commit b2) = Just j'-      | otherwise = goJ rest-    goJ [] = Nothing--  {-# INLINE pairs #-}-  pairs = zip <*> tail--  commit b = case _decision b of-    (_, CommitRef _ _) -> True-    _ -> False--  -- 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 `M.member` _runnable b =-      let val = M.lookup t $ _backtrack b-      in  if isNothing val || (val == Just False && c)-          then b { _backtrack = M.insert t c $ _backtrack b } : rest-          else bx--    -- Otherwise just backtrack to everything runnable.-    | otherwise = b { _backtrack = M.fromList [ (t',c) | t' <- M.keys $ _runnable b ] } : rest--  backtrack c (b:rest) n t = b : backtrack c rest (n-1) t-  backtrack _ [] _ _ = error "Ran out of schedule whilst backtracking!"---- * Fair bounding+pBacktrack :: [BacktrackStep ThreadId ThreadAction Lookahead s]+  -- ^ The current backtracking points.+  -> Int+  -- ^ The point to backtrack to.+  -> ThreadId+  -- ^ The thread to backtrack to.+  -> [BacktrackStep ThreadId ThreadAction Lookahead s]+pBacktrack = preempBacktrack isCommitRef -newtype FairBound = FairBound Int-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)+-- | Pre-emption bound function. This is different to @preempBound@ in+-- that it does not count pre-emptive context switches to a commit+-- thread.+pBound :: PreemptionBound -> BoundFunc ThreadId ThreadAction Lookahead+pBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb --- | A sensible default fair bound: 5-defaultFairBound :: FairBound-defaultFairBound = 5+-------------------------------------------------------------------------------+-- Fair bounding  -- | An SCT runner using a fair bounding scheduler. sctFairBound :: MemType@@ -276,67 +219,33 @@   -- performed by different threads.   -> (forall t. ConcST t a)   -- ^ The computation to run many times-  -> [(Either Failure a, Trace)]+  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] sctFairBound memtype fb = sctBounded memtype (fBound fb) fBacktrack  -- | Variant of 'sctFairBound' for computations which do 'IO'.-sctFairBoundIO :: MemType -> FairBound -> ConcIO a -> IO [(Either Failure a, Trace)]+sctFairBoundIO :: MemType+  -> FairBound+  -> ConcIO a+  -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] sctFairBoundIO memtype fb = sctBoundedIO memtype (fBound fb) fBacktrack  -- | Fair bound function-fBound :: FairBound -> BoundFunc-fBound (FairBound fb) ts dl = maxYieldCountDiff ts dl <= fb---- | Count the number of yields by a thread in a schedule prefix.-yieldCount :: ThreadId -> [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Int-yieldCount tid ts (_, l) = go 0 ts where-  go t ((Start    t', Yield):rest) = (if t == tid then 1 else 0) + go t' rest-  go t ((SwitchTo t', Yield):rest) = (if t == tid then 1 else 0) + go t' rest-  go t ((Continue,    Yield):rest) = (if t == tid then 1 else 0) + go t  rest-  go _ ((Start    t', _):rest) = go t' rest-  go _ ((SwitchTo t', _):rest) = go t' rest-  go t ((Continue,    _):rest) = go t  rest-  go t (_:rest) = go t rest-  go t [] = if l == WillYield && t == tid then 1 else 0---- | Get the maximum difference between the yield counts of all--- threads in this schedule prefix.-maxYieldCountDiff :: [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Int-maxYieldCountDiff ts dl = maximum yieldCountDiffs where-  yieldCounts = [yieldCount tid ts dl | tid <- nub $ allTids ts]-  yieldCountDiffs = [y1 - y2 | y1 <- yieldCounts, y2 <- yieldCounts]--  allTids ((_, Fork tid):rest) = tid : allTids rest-  allTids (_:rest) = allTids rest-  allTids [] = [0]+fBound :: FairBound -> BoundFunc ThreadId ThreadAction Lookahead+fBound = fairBound didYield willYield (\act -> case act of Fork t -> [t]; _ -> [])  -- | Add a backtrack point. If the thread isn't runnable, or performs -- a release operation, add all runnable threads.-fBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]-fBacktrack 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.-  | Just False == (willRelease <$> M.lookup t (_runnable b)) =-    let val = M.lookup t $ _backtrack b-    in  if isNothing val-        then b { _backtrack = M.insert t False $ _backtrack b } : rest-        else bx--  -- Otherwise just backtrack to everything runnable.-  | otherwise = b { _backtrack = M.fromList [ (t',False) | t' <- M.keys $ _runnable b ] } : rest--fBacktrack (b:rest) n t = b : fBacktrack rest (n-1) t-fBacktrack [] _ _ = error "Ran out of schedule whilst backtracking!"---- * Length Bounding--newtype LengthBound = LengthBound Int-  deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)+fBacktrack :: [BacktrackStep ThreadId ThreadAction Lookahead s]+  -- ^ The current backtracking points.+  -> Int+  -- ^ The point to backtrack to.+  -> ThreadId+  -- ^ The thread to backtrack to.+  -> [BacktrackStep ThreadId ThreadAction Lookahead s]+fBacktrack = fairBacktrack willRelease --- | A sensible default length bound: 250-defaultLengthBound :: LengthBound-defaultLengthBound = 250+-------------------------------------------------------------------------------+-- Length bounding  -- | An SCT runner using a length bounding scheduler. sctLengthBound :: MemType@@ -346,31 +255,18 @@   -- actions.   -> (forall t. ConcST t a)   -- ^ The computation to run many times-  -> [(Either Failure a, Trace)]-sctLengthBound memtype lb = sctBounded memtype (lBound lb) lBacktrack+  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]+sctLengthBound memtype lb = sctBounded memtype (lenBound lb) lenBacktrack  -- | Variant of 'sctFairBound' for computations which do 'IO'.-sctLengthBoundIO :: MemType -> LengthBound -> ConcIO a -> IO [(Either Failure a, Trace)]-sctLengthBoundIO memtype lb = sctBoundedIO memtype (lBound lb) lBacktrack---- | Length bound function-lBound :: LengthBound -> BoundFunc-lBound (LengthBound lb) ts _ = length ts < lb---- | Add a backtrack point. If the thread isn't runnable, add all--- runnable threads.-lBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]-lBacktrack bx@(b:rest) 0 t-  | t `M.member` _runnable b =-    let val = M.lookup t $ _backtrack b-    in  if isNothing val-        then b { _backtrack = M.insert t False $ _backtrack b } : rest-        else bx-  | otherwise = b { _backtrack = M.fromList [ (t',False) | t' <- M.keys $ _runnable b ] } : rest-lBacktrack (b:rest) n t = b : lBacktrack rest (n-1) t-lBacktrack [] _ _ = error "Ran out of schedule whilst backtracking!"+sctLengthBoundIO :: MemType+  -> LengthBound+  -> ConcIO a+  -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]+sctLengthBoundIO memtype lb = sctBoundedIO memtype (lenBound lb) lenBacktrack --- * BPOR+-------------------------------------------------------------------------------+-- DPOR  -- | SCT via BPOR. --@@ -386,129 +282,176 @@ -- previously non-interfering events interfere with each other. sctBounded :: MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> BoundFunc+  -> BoundFunc ThreadId ThreadAction Lookahead   -- ^ Check if a prefix trace is within the bound-  -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])+  -> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState])   -- ^ 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.-  -> (forall t. ConcST t a) -> [(Either Failure a, Trace)]+  -> (forall t. ConcST t a) -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] sctBounded memtype bf backtrack c = runIdentity $ sctBoundedM memtype bf backtrack run where-  run memty sched s = Identity $ runConcST' sched memty s c+  run memty sched s = Identity $ runConcST sched memty s c  -- | Variant of 'sctBounded' for computations which do 'IO'.-sctBoundedIO :: MemType -> BoundFunc-  -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])-  -> ConcIO a -> IO [(Either Failure a, Trace)]+sctBoundedIO :: MemType+  -> BoundFunc ThreadId ThreadAction Lookahead+  -> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState])+  -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] sctBoundedIO memtype bf backtrack c = sctBoundedM memtype bf backtrack run where-  run memty sched s = runConcIO' sched memty s c+  run memty sched s = runConcIO sched memty s c  -- | Generic SCT runner.-sctBoundedM :: (Functor m, Monad m)+sctBoundedM :: Monad m   => MemType-  -> ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool)-  -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])-  -> (MemType -> Scheduler SchedState -> SchedState -> m (Either Failure a, SchedState, Trace'))+  -> ([(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Bool)+  -> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState])+  -> (forall s. MemType -> Scheduler ThreadId ThreadAction Lookahead s -> s -> m (Either Failure a, s, Trace ThreadId ThreadAction Lookahead))   -- ^ Monadic runner, with computation fixed.-  -> m [(Either Failure a, Trace)]-sctBoundedM memtype bf backtrack run = go initialState where-  go bpor = case next bpor of-    Just (sched, conservative, sleep) -> do-      (res, s, trace) <- run memtype (bporSched memtype $ initialise bf) (initialSchedState sleep sched)+  -> m [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]+sctBoundedM memtype bf backtrack run =+  dpor didYield+       willYield+       initialCRState+       updateCRState+       (dependent  memtype)+       (dependent' memtype)+       initialThread+       (>=initialThread)+       bf+       backtrack+       pruneCommits+       (run memtype) -      let bpoints = findBacktrack memtype backtrack (_sbpoints s) trace-      let newBPOR = grow memtype conservative trace bpor+-------------------------------------------------------------------------------+-- Post-processing -      if _signore s-      then go newBPOR-      else ((res, toTrace trace):) <$> go (pruneCommits $ todo bf bpoints newBPOR)+-- | Remove commits from the todo sets where every other action will+-- result in a write barrier (and so a commit) occurring.+--+-- To get the benefit from this, do not execute commit actions from+-- the todo set until there are no other choises.+pruneCommits :: DPOR ThreadId ThreadAction -> DPOR ThreadId ThreadAction+pruneCommits bpor+  | not onlycommits || not alldonesync = go bpor+  | otherwise = go bpor { dporTodo = M.empty } -    Nothing -> return []+  where+    go b = b { dporDone = pruneCommits <$> dporDone bpor } --- * BPOR Scheduler+    onlycommits = all (<initialThread) . M.keys $ dporTodo bpor+    alldonesync = all barrier . M.elems $ dporDone bpor --- | The scheduler state-data SchedState = SchedState-  { _ssleep   :: Map ThreadId ThreadAction-  -- ^ The sleep set: decisions not to make until something dependent-  -- with them happens.-  , _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.-  , _signore  :: Bool-  -- ^ Whether to ignore this execution or not: @True@ if the-  -- execution is aborted due to all possible decisions being in the-  -- sleep set, as then everything in this execution is covered by-  -- another.-  } deriving Show+    barrier = isBarrier . simplify . fromJust . dporAction --- | Initial scheduler state for a given prefix-initialSchedState :: Map ThreadId ThreadAction -> [ThreadId] -> SchedState-initialSchedState sleep prefix = SchedState-  { _ssleep   = sleep-  , _sprefix  = prefix-  , _sbpoints = Sq.empty-  , _signore  = False-  }+-------------------------------------------------------------------------------+-- Dependency function --- | 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 :: MemType-  -> ([(Decision, ThreadAction)] -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> [ThreadId])-  -> Scheduler SchedState-bporSched memtype init = force $ \s trc prior threads -> case _sprefix s of-  -- If there is a decision available, make it-  (d:ds) ->-    let threads' = fmap (\(t,a:|_) -> (t,a)) threads-    in  (Just d, s { _sprefix = ds, _sbpoints = _sbpoints s |> (threads', []) })+-- | Check if an action is dependent on another.+dependent :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool+dependent _ _ (_, Lift) (_, Lift) = True+dependent _ _ (_, ThrowTo t) (t2, Stop) | t == t2 = False+dependent _ _ (t2, Stop) (_, ThrowTo t) | t == t2 = False+dependent _ _ (_, ThrowTo t) (t2, _) = t == t2+dependent _ _ (t2, _) (_, ThrowTo t) = t == t2+dependent _ _ (_, STM _ _) (_, STM _ _) = True+dependent _ _ (_, GetNumCapabilities a) (_, SetNumCapabilities b) = a /= b+dependent _ _ (_, SetNumCapabilities a) (_, GetNumCapabilities b) = a /= b+dependent _ _ (_, SetNumCapabilities a) (_, SetNumCapabilities b) = a /= b+dependent memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify d2) -  -- Otherwise query the initialise function for a list of possible-  -- choices, filter out anything in the sleep set, and make one of-  -- them arbitrarily (recording the others).-  [] ->-    let threads' = fmap (\(t,a:|_) -> (t,a)) threads-        choices  = init trc prior threads'-        checkDep t a = case prior of-          Just (tid, act) -> dependent memtype unknownCRState (tid, act) (t, a)-          Nothing -> False-        ssleep'  = M.filterWithKey (\t a -> not $ checkDep t a) $ _ssleep s-        choices' = filter (`notElem` M.keys ssleep') choices-        signore' = not (null choices) && all (`elem` M.keys ssleep') choices-    in  case choices' of-          (nextTid:rest) -> (Just nextTid, s { _sbpoints = _sbpoints s |> (threads', rest), _ssleep = ssleep' })-          [] -> (Nothing, s { _sbpoints = _sbpoints s |> (threads', []), _signore = signore' })+-- | Variant of 'dependent' to handle 'ThreadAction''s+dependent' :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, Lookahead) -> Bool+dependent' _ _ (_, Lift) (_, WillLift) = True+dependent' _ _ (_, ThrowTo t) (t2, WillStop) | t == t2 = False+dependent' _ _ (t2, Stop) (_, WillThrowTo t) | t == t2 = False+dependent' _ _ (_, ThrowTo t) (t2, _)     = t == t2+dependent' _ _ (t2, _) (_, WillThrowTo t) = t == t2+dependent' _ _ (_, STM _ _) (_, WillSTM) = True+dependent' _ _ (_, GetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b+dependent' _ _ (_, SetNumCapabilities _) (_, WillGetNumCapabilities)   = True+dependent' _ _ (_, SetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b+-- This is safe because, if the thread blocks anyway, a context switch+-- will occur anyway so there's no point pre-empting the action.+--+-- UNLESS the pre-emption would possibly allow for a different relaxed+-- memory stage.+dependent' _ _ (_, a1) (_, a2) | isBlock a1 && isBarrier (simplify' a2) = False+dependent' memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify' d2) --- | Pick a new thread to run, which does not exceed the bound. Choose--- the current thread if available and it hasn't just yielded,--- otherwise add all runnable threads.-initialise :: BoundFunc-  -> [(Decision, ThreadAction)]-  -> Maybe (ThreadId, ThreadAction)-  -> NonEmpty (ThreadId, Lookahead)-  -> [ThreadId]-initialise bf trc prior threads = restrictToBound . yieldsToEnd $ case prior of-  Just (_, Yield) -> map fst threads'-  Just (tid, _)-    | any (\(t, _) -> t == tid) threads' -> [tid]-  _ -> map fst threads'+-- | Check if two 'ActionType's are dependent. Note that this is not+-- sufficient to know if two 'ThreadAction's are dependent, without+-- being so great an over-approximation as to be useless!+dependentActions :: MemType -> CRState -> ActionType -> ActionType -> Bool+dependentActions memtype buf a1 a2 = case (a1, a2) of+  -- Unsynchronised reads and writes are always dependent, even under+  -- a relaxed memory model, as an unsynchronised write gives rise to+  -- a commit, which synchronises.+  (UnsynchronisedRead  r1, UnsynchronisedWrite r2) -> r1 == r2+  (UnsynchronisedWrite r1, UnsynchronisedRead  r2) -> r1 == r2+  (UnsynchronisedWrite r1, UnsynchronisedWrite r2) -> r1 == r2 +  -- Unsynchronised writes and synchronisation where the buffer is not+  -- empty.+  --+  -- See [RMMVerification], lemma 5.25.+  (UnsynchronisedWrite r1, _) | same crefOf && isCommit a2 r1 && isBuffered buf r1 -> False+  (_, UnsynchronisedWrite r2) | same crefOf && isCommit a1 r2 && isBuffered buf r2 -> False++  -- Unsynchronised reads where a memory barrier would flush a+  -- buffered write+  (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered buf r1 && memtype /= SequentialConsistency+  (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered buf r2 && memtype /= SequentialConsistency++  (_, _)+    -- Two actions on the same CRef where at least one is synchronised+    | same crefOf && (synchronises a1 (fromJust $ crefOf a1) || synchronises a2 (fromJust $ crefOf a2)) -> True+    -- Two actions on the same MVar+    | same cvarOf -> True++  _ -> False+   where-    -- Restrict the possible decisions to those in the bound.-    restrictToBound = fst . partition (\t -> bf trc (decision t, action t))+    same f = isJust (f a1) && f a1 == f a2 -    -- Move the threads which will immediately yield to the end of the list-    yieldsToEnd ts = case partition ((== WillYield) . action) ts of-      (willYield, noYield) -> noYield ++ willYield+-------------------------------------------------------------------------------+-- Dependency function state -    -- Get the decision that will lead to a thread being scheduled.-    decision = decisionOf (fst <$> prior) (S.fromList $ map fst threads')+type CRState = Map CRefId Bool -    -- Get the action of a thread-    action t = fromJust $ lookup t threads'+-- | Initial global 'CRef buffer state.+initialCRState :: CRState+initialCRState = M.empty -    -- The list of threads-    threads' = toList threads+-- | Update the 'CRef' buffer state with the action that has just+-- happened.+updateCRState :: CRState -> ThreadAction -> CRState+updateCRState crstate (CommitRef _ r) = M.delete r crstate+updateCRState crstate (WriteRef r) = M.insert r True crstate+updateCRState crstate ta+  | isBarrier $ simplify ta = initialCRState+  | otherwise = crstate++-- | Check if a 'CRef' has a buffered write pending.+--+-- If the state is @Unknown@, this assumes @True@.+isBuffered :: CRState -> CRefId -> Bool+isBuffered crstate r = M.findWithDefault False r crstate++-------------------------------------------------------------------------------+-- Utilities++-- | Determine if an action is a commit or not.+isCommitRef :: ThreadAction -> Bool+isCommitRef (CommitRef _ _) = True+isCommitRef _ = False++-- | Check if a thread yielded.+didYield :: ThreadAction -> Bool+didYield Yield = True+didYield _ = False++-- | Check if a thread will yield.+willYield :: Lookahead -> Bool+willYield WillYield = True+willYield _ = False

@@ -1,437 +0,0 @@-{-# LANGUAGE CPP #-}---- | Internal utilities and types for BPOR.-module Test.DejaFu.SCT.Internal where--import Control.DeepSeq (NFData(..))-import Data.List (foldl', partition, sortBy, intercalate)-import Data.Map.Strict (Map)-import Data.Maybe (mapMaybe, isJust, fromJust, listToMaybe)-import Data.Ord (Down(..), comparing)-import Data.Sequence (Seq, ViewL(..))-import Data.Set (Set)-import Test.DejaFu.Deterministic.Internal-import Test.DejaFu.Deterministic.Schedule--import qualified Data.Map.Strict as M-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  :: Map ThreadId Lookahead-  -- ^ The threads runnable at this step-  , _backtrack :: Map ThreadId 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     :: Map ThreadId 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     :: Map ThreadId BPOR-  -- ^ Follow-on decisions that have been made.-  , _bsleep    :: Map ThreadId ThreadAction-  -- ^ Transitions to ignore (in this node and children) until a-  -- dependent transition happens.-  , _btaken    :: Map ThreadId ThreadAction-  -- ^ Transitions which have been taken, excluding-  -- conservatively-added ones. This is used in implementing sleep-  -- sets.-  , _baction    :: Maybe ThreadAction-  -- ^ What happened at this step. This will be 'Nothing' at the root,-  -- 'Just' everywhere else.-  }---- | Render a 'BPOR' value as a graph in GraphViz \"dot\" format.-toDot :: BPOR -> String-toDot bpor = "digraph {\n" ++ go "L" bpor ++ "\n}" where-  go l b = unlines $ node l b : [edge l l' i ++ go l' b' | (i, b') <- M.toList (_bdone b), let l' = l ++ show' i]--  -- Display a labelled node.-  node n b = n ++ " [label=\"" ++ label b ++ "\"]"--  -- A node label, summary of the BPOR state at that node.-  label b = intercalate ","-    [ show $ _baction b-    , "Run:" ++ show (S.toList $ _brunnable b)-    , "Tod:" ++ show (M.keys   $ _btodo     b)-    , "Ign:" ++ show (S.toList $ _bignore   b)-    , "Slp:" ++ show (M.toList $ _bsleep    b)-    ]--  -- Display a labelled edge-  edge n1 n2 l = n1 ++ "-> " ++ n2 ++ " [label=\"" ++ show l ++ "\"]\n"--  -- Show a number, replacing a minus sign for \"N\".-  show' i = if i < 0 then "N" ++ show (negate i) else show i---- | Variant of 'toDot' which doesn't include aborted subtrees.-toDotSmall :: BPOR -> String-toDotSmall bpor = "digraph {\n" ++ go "L" bpor ++ "\n}" where-  go l b = unlines $ node l b : [edge l l' i ++ go l' b' | (i, b') <- M.toList (_bdone b), check b', let l' = l ++ show' i]--  -- Check that a subtree has at least one non-aborted branch.-  check b = S.null (_brunnable b) || any check (M.elems $ _bdone b)--  -- Display a labelled node.-  node n b = n ++ " [label=\"" ++ label b ++ "\"]"--  -- A node label, summary of the BPOR state at that node.-  label b = intercalate ","-    [ show $ _baction b-    , "Run:" ++ show (S.toList $ _brunnable b)-    , "Tod:" ++ show (M.keys   $ _btodo     b)-    , "Ign:" ++ show (S.toList $ _bignore   b)-    , "Slp:" ++ show (M.toList $ _bsleep    b)-    ]--  -- Display a labelled edge-  edge n1 n2 l = n1 ++ "-> " ++ n2 ++ " [label=\"" ++ show l ++ "\"]\n"--  -- Show a number, replacing a minus sign for \"N\".-  show' i = if i < 0 then "N" ++ show (negate i) else show i---- | Initial BPOR state.-initialState :: BPOR-initialState = BPOR-  { _brunnable = S.singleton (ThreadId 0)-  , _btodo     = M.singleton (ThreadId 0) False-  , _bignore   = S.empty-  , _bdone     = M.empty-  , _bsleep    = M.empty-  , _btaken    = M.empty-  , _baction   = Nothing-  }---- | Produce a new schedule from a BPOR tree. If there are no new--- schedules remaining, return 'Nothing'. Also returns whether the--- decision was added conservatively, and the sleep set at the point--- where divergence happens.------ 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, Map ThreadId ThreadAction)-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' (M.toList $ _bdone bpor) ++ [([t], c, sleeps bpor) | (t, c) <- M.toList $ _btodo bpor]-        -- Sort by number of preemptions, in descending order.-        cmp = preEmps tid bpor . (\(a,_,_) -> a)--    in if null prefixes-       then Nothing-       else case partition (\(t:_,_,_) -> t < 0) $ sortBy (comparing $ Down . cmp) prefixes of-              (commits, others)-                | not $ null others  -> listToMaybe others-                | not $ null commits -> listToMaybe commits-                | otherwise -> error "Invariant failure in 'next': empty prefix list!"--  go' (tid, bpor) = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> go tid bpor--  sleeps bpor = _bsleep bpor `M.union` _btaken bpor--  preEmps tid bpor (t:ts) =-    let rest = preEmps t (fromJust . M.lookup t $ _bdone bpor) ts-    in  if t > 0 && 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 :: MemType-  -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])-  -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])-  -> Trace'-  -> [BacktrackStep]-findBacktrack memtype backtrack = go initialCRState S.empty 0 [] . Sq.viewl where-  go crstate allThreads tid bs ((e,i):<is) ((d,_,a):ts) =-    let tid' = tidOf tid d-        crstate' = updateCRState crstate a-        this = BacktrackStep-          { _threadid  = tid'-          , _decision  = (d, a)-          , _runnable  = M.fromList . toList $ e-          , _backtrack = M.fromList $ map (\i' -> (i', False)) i-          }-        allThreads' = allThreads `S.union` S.fromList (M.keys $ _runnable this)-        killsEarly = null ts && any (/=0) (M.keys $ _runnable this)-        bs' = doBacktrack killsEarly crstate' allThreads' (toList e) (bs++[this])-    in go crstate' allThreads' tid' bs' (Sq.viewl is) ts-  go _ _ _ bs _ _ = bs--  doBacktrack killsEarly crstate 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-                            , killsEarly || dependent' memtype crstate (_threadid b, 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 :: MemType -> Bool -> Trace' -> BPOR -> BPOR-grow memtype conservative = grow' initialCVState initialCRState 0 where-  grow' cvstate crstate tid trc@((d, _, a):rest) bpor =-    let tid'     = tidOf tid d-        cvstate' = updateCVState cvstate a-        crstate' = updateCRState crstate a-    in  case M.lookup tid' $ _bdone bpor of-          Just bpor' -> bpor { _bdone  = M.insert tid' (grow' cvstate' crstate' tid' rest bpor') $ _bdone bpor }-          Nothing    -> bpor { _btaken = if conservative then _btaken bpor else M.insert tid' a $ _btaken bpor-                            , _btodo  = M.delete tid' $ _btodo bpor-                            , _bdone  = M.insert tid' (subtree cvstate' crstate' tid' (_bsleep bpor `M.union` _btaken bpor) trc) $ _bdone bpor }-  grow' _ _ _ [] bpor = bpor--  subtree cvstate crstate tid sleep ((d, ts, a):rest) =-    let cvstate' = updateCVState cvstate a-        crstate' = updateCRState crstate a-        sleep'   = M.filterWithKey (\t a' -> not $ dependent memtype crstate' (tid, a) (t,a')) sleep-    in BPOR-        { _brunnable = S.fromList $ tids tid d a ts-        , _btodo     = M.empty-        , _bignore   = S.fromList [tidOf tid d' | (d',as) <- ts, willBlockSafely cvstate' $ toList as]-        , _bdone     = M.fromList $ case rest of-          ((d', _, _):_) ->-            let tid' = tidOf tid d'-            in  [(tid', subtree cvstate' crstate' tid' sleep' rest)]-          [] -> []-        , _bsleep = sleep'-        , _btaken = case rest of-          ((d', _, a'):_) -> M.singleton (tidOf tid d') a'-          [] -> M.empty-        , _baction = Just a-        }-  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 _ (BlockedPutVar _)  ts = map (tidOf tid . fst) ts-  tids tid _ (BlockedReadVar _) ts = map (tidOf tid . fst) ts-  tids tid _ (BlockedTakeVar _) 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, ThreadAction)] -> (Decision, Lookahead) -> Bool) -> [BacktrackStep] -> BPOR -> BPOR-todo bv = step where-  step bs bpor =-    let (bpor', bs') = go 0 [] Nothing bs bpor-    in  if all (M.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-        pref'  = pref ++ [_decision b]-        (child, blocked')  = go tid' pref' (Just b) bs . fromJust $ M.lookup tid' (_bdone bpor)-        bpor'' = bpor' { _bdone = M.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 = M.empty }])-  go _ _ Nothing   _ bpor = (bpor, [])--  backtrack pref b bpor =-    let todo' = [ x-                | x@(t,c) <- M.toList $ _backtrack b-                , let decision  = decisionOf (Just . activeTid $ map fst pref) (_brunnable bpor) t-                , let lookahead = fromJust . M.lookup t $ _runnable b-                , bv pref (decision, lookahead)-                , t `notElem` M.keys (_bdone bpor)-                , c || M.notMember t (_bsleep bpor)-                ]-        (blocked, nxt) = partition (\(t,_) -> t `S.member` _bignore bpor) todo'-    in  (bpor { _btodo = _btodo bpor `M.union` M.fromList nxt }, M.fromList blocked)---- | Remove commits from the todo sets where every other action will--- result in a write barrier (and so a commit) occurring.------ To get the benefit from this, do not execute commit actions from--- the todo set until there are no other choises.-pruneCommits :: BPOR -> BPOR-pruneCommits bpor-  | not onlycommits || not alldonesync = go bpor-  | otherwise = go bpor { _btodo = M.empty, _bdone = pruneCommits <$> _bdone bpor }--  where-    go b = b { _bdone = pruneCommits <$> _bdone bpor }--    onlycommits = all (<0) . M.keys $ _btodo bpor-    alldonesync = all barrier . M.elems $ _bdone bpor--    barrier = isBarrier . simplify . fromJust . _baction---- * 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 _          = 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' tidOf 0---- | Check if an action is dependent on another.-dependent :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool-dependent _ _ (_, Lift) (_, Lift) = True-dependent _ _ (_, ThrowTo t) (t2, a) = t == t2 && a /= Stop-dependent _ _ (t2, a) (_, ThrowTo t) = t == t2 && a /= Stop-dependent _ _ (_, STM _) (_, STM _) = True-dependent _ _ (_, GetNumCapabilities a) (_, SetNumCapabilities b) = a /= b-dependent _ _ (_, SetNumCapabilities a) (_, GetNumCapabilities b) = a /= b-dependent _ _ (_, SetNumCapabilities a) (_, SetNumCapabilities b) = a /= b-dependent memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify d2)---- | Variant of 'dependent' to handle 'ThreadAction''s-dependent' :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, Lookahead) -> Bool-dependent' _ _ (_, Lift) (_, WillLift) = True-dependent' _ _ (_, ThrowTo t) (t2, a)     = t == t2 && a /= WillStop-dependent' _ _ (t2, a) (_, WillThrowTo t) = t == t2 && a /= Stop-dependent' _ _ (_, STM _) (_, WillSTM) = True-dependent' _ _ (_, GetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b-dependent' _ _ (_, SetNumCapabilities a) (_, WillGetNumCapabilities)   = True-dependent' _ _ (_, SetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b-dependent' memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify' d2)---- | Check if two 'ActionType's are dependent. Note that this is not--- sufficient to know if two 'ThreadAction's are dependent, without--- being so great an over-approximation as to be useless!-dependentActions :: MemType -> CRState -> ActionType -> ActionType -> Bool-dependentActions memtype buf a1 a2 = case (a1, a2) of-  -- Unsynchronised reads and writes are always dependent, even under-  -- a relaxed memory model, as an unsynchronised write gives rise to-  -- a commit, which synchronises.-  (UnsynchronisedRead  r1, UnsynchronisedWrite r2) -> r1 == r2-  (UnsynchronisedWrite r1, UnsynchronisedRead  r2) -> r1 == r2-  (UnsynchronisedWrite r1, UnsynchronisedWrite r2) -> r1 == r2--  -- Unsynchronised reads where a memory barrier would flush a-  -- buffered write-  (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered buf r1 && memtype /= SequentialConsistency-  (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered buf r2 && memtype /= SequentialConsistency--  (_, _)-    -- Two actions on the same CRef where at least one is synchronised-    | same crefOf && (synchronises a1 (fromJust $ crefOf a1) || synchronises a2 (fromJust $ crefOf a2)) -> True-    -- Two actions on the same CVar-    | same cvarOf -> True--  _ -> False--  where-    same f = isJust (f a1) && f a1 == f a2---- * Keeping track of 'CVar' full/empty states--type CVState = Map CVarId Bool---- | Initial global 'CVar' state-initialCVState :: CVState-initialCVState = M.empty---- | Update the 'CVar' state with the action that has just happened.-updateCVState :: CVState -> ThreadAction -> CVState-updateCVState cvstate (PutVar  c _) = M.insert c True  cvstate-updateCVState cvstate (TakeVar c _) = M.insert c False cvstate-updateCVState cvstate (TryPutVar  c True _) = M.insert c True  cvstate-updateCVState cvstate (TryTakeVar c True _) = M.insert c False cvstate-updateCVState cvstate _ = cvstate---- | Check if an action will block.-willBlock :: CVState -> Lookahead -> Bool-willBlock cvstate (WillPutVar  c) = M.lookup c cvstate == Just True-willBlock cvstate (WillTakeVar c) = M.lookup c cvstate == Just False-willBlock cvstate (WillReadVar c) = M.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 :: CVState -> [Lookahead] -> Bool-willBlockSafely cvstate (WillMyThreadId:as) = willBlockSafely cvstate as-willBlockSafely cvstate (WillNewVar:as)     = willBlockSafely cvstate as-willBlockSafely cvstate (WillNewRef:as)     = willBlockSafely cvstate as-willBlockSafely cvstate (WillReturn:as)     = willBlockSafely cvstate as-willBlockSafely cvstate (WillKnowsAbout:as) = willBlockSafely cvstate as-willBlockSafely cvstate (WillForgets:as)    = willBlockSafely cvstate as-willBlockSafely cvstate (WillAllKnown:as)   = willBlockSafely cvstate as-willBlockSafely cvstate (WillPutVar  c:_) = willBlock cvstate (WillPutVar  c)-willBlockSafely cvstate (WillTakeVar c:_) = willBlock cvstate (WillTakeVar c)-willBlockSafely _ _ = False---- * Keeping track of 'CRef' buffer state--data CRState = Known (Map CRefId Bool) | Unknown---- | Initial global 'CRef buffer state.-initialCRState :: CRState-initialCRState = Known M.empty---- | 'CRef' buffer state with nothing known.-unknownCRState :: CRState-unknownCRState = Unknown---- | Update the 'CRef' buffer state with the action that has just--- happened.-updateCRState :: CRState -> ThreadAction -> CRState-updateCRState Unknown _ = Unknown-updateCRState (Known crstate) (CommitRef _ r) = Known $ M.delete r crstate-updateCRState (Known crstate) (WriteRef r) = Known $ M.insert r True crstate-updateCRState crstate ta-  | isBarrier $ simplify ta = initialCRState-  | otherwise = crstate---- | Check if a 'CRef' has a buffered write pending.------ If the state is @Unknown@, this assumes @True@.-isBuffered :: CRState -> CRefId -> Bool-isBuffered Unknown _ = True-isBuffered (Known crstate) r = M.findWithDefault False r crstate

@@ -1,4 +1,3 @@-{-# LANGUAGE CPP                        #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE RankNTypes                 #-} {-# LANGUAGE TypeFamilies               #-}@@ -13,7 +12,9 @@    -- * Executing Transactions   , Result(..)-  , CTVarId+  , TTrace+  , TAction(..)+  , TVarId   , runTransactionST   , runTransactionIO   ) where@@ -24,15 +25,12 @@ import Control.Monad.ST (ST) import Data.IORef (IORef) import Data.STRef (STRef)+import Test.DejaFu.Deterministic.Internal.Common (TVarId, IdSource, TAction(..), TTrace) 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) #-}  newtype STMLike n r a = S { runSTM :: M n r a } deriving (Functor, Applicative, Monad)@@ -43,7 +41,7 @@  -- | A 'MonadSTM' implementation using @ST@, 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+-- defined 'TVar's is implicit, there is no list of them, they exist -- purely as references. This makes the types simpler, but means you -- can't really get an aggregate of them (if you ever wanted to for -- some reason).@@ -51,51 +49,51 @@  -- | A 'MonadSTM' implementation using @ST@, 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+-- defined 'TVar's is implicit, there is no list of them, they exist -- purely as references. This makes the types simpler, but means you -- can't really get an aggregate of them (if you ever wanted to for -- some reason). type STMIO = STMLike IO IORef  instance MonadThrow (STMLike n r) where-  throwM e = toSTM (\_ -> SThrow e)+  throwM = toSTM . const . SThrow  instance MonadCatch (STMLike n r) where-  catch stm handler = toSTM (SCatch (runSTM . handler) (runSTM stm))+  catch (S stm) handler = toSTM (SCatch (runSTM . handler) stm)  instance Monad n => C.MonadSTM (STMLike n r) where-  type CTVar (STMLike n r) = CTVar r+  type TVar (STMLike n r) = TVar r -  retry = toSTM (\_ -> SRetry)+  retry = toSTM (const SRetry) -  orElse a b = toSTM (SOrElse (runSTM a) (runSTM b))+  orElse (S a) (S b) = toSTM (SOrElse a b) -  newCTVar a = toSTM (SNew a)+  newTVarN n = toSTM . SNew n -  readCTVar ctvar = toSTM (SRead ctvar)+  readTVar = toSTM . SRead -  writeCTVar ctvar a = toSTM (\c -> SWrite ctvar a (c ()))+  writeTVar tvar a = toSTM (\c -> SWrite tvar a (c ()))  -- | 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)+-- initial 'TVarId'. If the transaction ended by calling 'retry', any+-- 'TVar' modifications are undone.+runTransactionST :: STMST t a -> IdSource -> ST t (Result a, IdSource, TTrace) runTransactionST = runTransactionM fixedST where   fixedST = refST $ \mb -> cont (\c -> SLift $ 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 a -> CTVarId -> IO (Result a, CTVarId)+-- initial 'TVarId'. If the transaction ended by calling 'retry', any+-- 'TVar' modifications are undone.+runTransactionIO :: STMIO a -> IdSource -> IO (Result a, IdSource, TTrace) runTransactionIO = runTransactionM fixedIO where   fixedIO = refIO $ \mb -> cont (\c -> SLift $ c `liftM` mb)  -- | Run a transaction in an arbitrary monad. runTransactionM :: Monad n-  => Fixed n r -> STMLike n r a -> CTVarId -> n (Result a, CTVarId)-runTransactionM ref ma ctvid = do-  (res, undo, ctvid') <- doTransaction ref (runSTM ma) ctvid+  => Fixed n r -> STMLike n r a -> IdSource -> n (Result a, IdSource, TTrace)+runTransactionM ref ma tvid = do+  (res, undo, tvid', trace) <- doTransaction ref (runSTM ma) tvid    case res of-    Success _ _ _ -> return (res, ctvid')-    _ -> undo >> return (res, ctvid)+    Success _ _ _ -> return (res, tvid', trace)+    _ -> undo >> return (res, tvid, trace)

@@ -1,24 +1,16 @@-{-# 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.Exception (Exception, SomeException, fromException, toException) import Control.Monad.Cont (Cont, runCont) import Data.List (nub)-import Data.Maybe (fromMaybe)-import Data.Typeable (cast)+import Test.DejaFu.Deterministic.Internal.Common (TVarId, IdSource, TAction(..), TTrace, nextTVId) import Test.DejaFu.Internal -#if __GLASGOW_HASKELL__ < 710-import Data.Foldable (Foldable(..))-import Data.Monoid (mempty)-#endif- -------------------------------------------------------------------------------- -- The @STMLike@ monad @@ -36,40 +28,36 @@ -- actions. data STMAction n r   = forall a e. Exception e => SCatch (e -> M n r a) (M n r a) (a -> STMAction n r)-  | forall a. SRead  (CTVar r a) (a -> STMAction n r)-  | forall a. SWrite (CTVar r a) a (STMAction n r)+  | forall a. SRead  (TVar r a) (a -> STMAction n r)+  | forall a. SWrite (TVar r a) a (STMAction n r)   | forall a. SOrElse (M n r a) (M n r a) (a -> STMAction n r)-  | forall a. SNew a (CTVar r a -> STMAction n r)+  | forall a. SNew String a (TVar r a -> STMAction n r)   | SLift (n (STMAction n r))   | forall e. Exception e => SThrow e   | SRetry   | SStop  ----------------------------------------------------------------------------------- * @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 r a = CTVar (CTVarId, r a)+-- * @TVar@s --- | The unique ID of a 'CTVar'. Only meaningful within a single--- concurrent computation.-type CTVarId = Int+-- | A 'TVar' is a tuple of a unique ID and the value contained. The+-- ID is so that blocked transactions can be re-run when a 'TVar' they+-- depend on has changed.+newtype TVar r a = TVar (TVarId, r a)  -------------------------------------------------------------------------------- -- * Output --- | The result of an STM transaction, along with which 'CTVar's it+-- | The result of an STM transaction, along with which 'TVar's it -- touched whilst executing. data Result a =-    Success [CTVarId] [CTVarId] a+    Success [TVarId] [TVarId] a   -- ^ The transaction completed successfully, reading the first list-  -- 'CTVar's and writing to the second.-  | Retry   [CTVarId]+  -- 'TVar's and writing to the second.+  | Retry [TVarId]   -- ^ 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.+  -- returned 'TVar's. It should be retried when at least one of the+  -- 'TVar's has been mutated.   | Exception SomeException   -- ^ The transaction aborted by throwing an exception.   deriving Show@@ -87,90 +75,94 @@ -- * Execution  -- | Run a STM transaction, returning an action to undo its effects.-doTransaction :: Monad n => Fixed n r -> M n r a -> CTVarId -> n (Result a, n (), CTVarId)-doTransaction fixed ma newctvid = do+doTransaction :: Monad n => Fixed n r -> M n r a -> IdSource -> n (Result a, n (), IdSource, TTrace)+doTransaction fixed ma idsource = do   ref <- newRef fixed Nothing    let c = runCont (ma >>= liftN fixed . writeRef fixed ref . Just . Right) $ const SStop -  (newctvid', undo, readen, written) <- go ref c (return ()) newctvid [] []+  (idsource', undo, readen, written, trace) <- go ref c (return ()) idsource [] [] []    res <- readRef fixed ref    case res of-    Just (Right val) -> return (Success (nub readen) (nub written) val, undo, newctvid')+    Just (Right val) -> return (Success (nub readen) (nub written) val, undo, idsource', reverse trace) -    Just (Left  exc) -> undo >> return (Exception exc,      return (), newctvid)-    Nothing          -> undo >> return (Retry $ nub readen, return (), newctvid)+    Just (Left  exc) -> undo >> return (Exception exc,      return (), idsource, reverse trace)+    Nothing          -> undo >> return (Retry $ nub readen, return (), idsource, reverse trace)    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-        SStop  -> return ret-        SRetry -> writeRef fixed ref Nothing >> return ret-        SThrow exc -> writeRef fixed ref (Just . Left $ wrap exc) >> return ret+    go ref act undo nidsrc readen written sofar = do+      (act', undo', nidsrc', readen', written', tact) <- stepTrans fixed act nidsrc -        _ -> go ref act' (undo >> undo') nctvid' (readen' ++ readen) (written' ++ written)+      let newIDSource = nidsrc'+          newAct = act'+          newUndo = undo >> undo'+          newReaden = readen' ++ readen+          newWritten = written' ++ written+          newSofar = tact : sofar -    -- | This wraps up an uncaught exception inside a @SomeException@,-    -- unless it already is a @SomeException@. This is because-    -- multiple levels of @SomeException@ do not play nicely with-    -- @fromException@.-    wrap e = fromMaybe (SomeException e) $ cast e+      case tact of+        TStop  -> return (newIDSource, newUndo, newReaden, newWritten, TStop:newSofar)+        TRetry -> writeRef fixed ref Nothing+          >> return (newIDSource, newUndo, newReaden, newWritten, TRetry:newSofar)+        TThrow -> writeRef fixed ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)+          >> return (newIDSource, newUndo, newReaden, newWritten, TThrow:newSofar)+        _ -> go ref newAct newUndo newIDSource newReaden newWritten newSofar  -- | Run a transaction for one step.-stepTrans :: Monad n => Fixed n r -> STMAction n r -> CTVarId -> n (STMAction n r, n (), CTVarId, [CTVarId], [CTVarId])-stepTrans fixed act newctvid = case act of+stepTrans :: Monad n => Fixed n r -> STMAction n r -> IdSource -> n (STMAction n r, n (), IdSource, [TVarId], [TVarId], TAction)+stepTrans fixed act idsource = case act of   SCatch  h stm c -> stepCatch h stm c   SRead   ref c   -> stepRead ref c   SWrite  ref a c -> stepWrite ref a c-  SNew    a c     -> stepNew a c+  SNew    n a c   -> stepNew n a c   SOrElse a b c   -> stepOrElse a b c   SLift   na      -> stepLift na -  halt -> return (halt, nothing, newctvid, [], [])+  SThrow e -> return (SThrow e, nothing, idsource, [], [], TThrow)+  SRetry   -> return (SRetry,   nothing, idsource, [], [], TRetry)+  SStop    -> return (SStop,    nothing, idsource, [], [], TStop)    where     nothing = return () -    stepCatch h stm c = onFailure stm c-      (\readen -> return (SRetry, nothing, newctvid, readen, []))-      (\exc    -> case fromException exc of-        Just exc' -> transaction (h exc') c-        Nothing   -> return (SThrow exc, nothing, newctvid, [], []))+    stepCatch h stm c = cases TCatch stm c+      (\trace readen -> return (SRetry, nothing, idsource, readen, [], TCatch trace Nothing))+      (\trace exc    -> case fromException exc of+        Just exc' -> transaction (TCatch trace . Just) (h exc') c+        Nothing   -> return (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing)) -    stepRead (CTVar (ctvid, ref)) c = do+    stepRead (TVar (tvid, ref)) c = do       val <- readRef fixed ref-      return (c val, nothing, newctvid, [ctvid], [])+      return (c val, nothing, idsource, [tvid], [], TRead tvid) -    stepWrite (CTVar (ctvid, ref)) a c = do+    stepWrite (TVar (tvid, ref)) a c = do       old <- readRef fixed ref       writeRef fixed ref a-      return (c, writeRef fixed ref old, newctvid, [], [ctvid])+      return (c, writeRef fixed ref old, idsource, [], [tvid], TWrite tvid) -    stepNew a c = do-      let newctvid' = newctvid + 1+    stepNew n a c = do+      let (idsource', tvid) = nextTVId n idsource       ref <- newRef fixed a-      let ctvar = CTVar (newctvid, ref)-      return (c ctvar, nothing, newctvid', [], [newctvid])+      let tvar = TVar (tvid, ref)+      return (c tvar, nothing, idsource', [], [tvid], TNew) -    stepOrElse a b c = onFailure a c-      (\_   -> transaction b c)-      (\exc -> return (SThrow exc, nothing, newctvid, [], []))+    stepOrElse a b c = cases TOrElse a c+      (\trace _   -> transaction (TOrElse trace . Just) b c)+      (\trace exc -> return (SThrow exc, nothing, idsource, [], [], TOrElse trace Nothing))      stepLift na = do       a <- na-      return (a, nothing, newctvid, [], [])+      return (a, nothing, idsource, [], [], TLift) -    onFailure stm onSuccess onRetry onException = do-      (res, undo, newctvid') <- doTransaction fixed stm newctvid+    cases tact stm onSuccess onRetry onException = do+      (res, undo, idsource', trace) <- doTransaction fixed stm idsource       case res of-        Success readen written val -> return (onSuccess val, undo, newctvid', readen, written)-        Retry readen  -> onRetry readen-        Exception exc -> onException exc+        Success readen written val -> return (onSuccess val, undo, idsource', readen, written, tact trace Nothing)+        Retry readen  -> onRetry     trace readen+        Exception exc -> onException trace exc -    transaction stm onSuccess = onFailure stm onSuccess-      (\readen -> return (SRetry, nothing, newctvid, readen, []))-      (\exc    -> return (SThrow exc, nothing, newctvid, [], []))+    transaction tact stm onSuccess = cases (\t _ -> tact t) stm onSuccess+      (\trace readen -> return (SRetry, nothing, idsource, readen, [], tact trace))+      (\trace exc    -> return (SThrow exc, nothing, idsource, [], [], tact trace))

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             0.2.0.0+version:             0.3.0.0 synopsis:            Overloadable primitives for testable, potentially non-deterministic, concurrency.  description:@@ -75,20 +75,28 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      0.1.0.0+  tag:      dejafu-0.3.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+                     , Control.Concurrent.Classy+                     , Control.Concurrent.Classy.Chan+                     , Control.Concurrent.Classy.CRef+                     , Control.Concurrent.Classy.MVar+                     , Control.Concurrent.Classy.QSem+                     , Control.Concurrent.Classy.QSemN+                     , Control.Concurrent.Classy.STM+                     , Control.Concurrent.Classy.STM.TVar+                     , Control.Concurrent.Classy.STM.TMVar+                     , Control.Concurrent.Classy.STM.TChan+                     , Control.Concurrent.Classy.STM.TQueue+                     , Control.Concurrent.Classy.STM.TBQueue+                     , Control.Concurrent.Classy.STM.TArray                       , Test.DejaFu                      , Test.DejaFu.Deterministic-                     , Test.DejaFu.Deterministic.Schedule                      , Test.DejaFu.SCT                      , Test.DejaFu.STM @@ -97,22 +105,25 @@                      , Test.DejaFu.Deterministic.Internal.Memory                      , Test.DejaFu.Deterministic.Internal.Threading                      , Test.DejaFu.Internal-                     , Test.DejaFu.SCT.Internal                      , Test.DejaFu.STM.Internal-                     , Data.List.Extra    -- other-modules:          -- other-extensions:       build-depends:       base >=4.5 && <5+                     , array                      , atomic-primops                      , containers+                     , dpor                      , deepseq                      , exceptions >=0.7+                     , monad-control                      , monad-loops                      , mtl-                     , random+                     , semigroups                      , stm+                     , template-haskell                      , transformers+                     , transformers-base   -- hs-source-dirs:         default-language:    Haskell2010   ghc-options:         -Wall