dejafu 0.3.2.1 → 0.4.0.0

raw patch · 32 files changed

+2016/−4328 lines, 32 filesdep +concurrencydep +ref-fddep −arraydep −atomic-primopsdep −monad-controlPVP ok

version bump matches the API change (PVP)

Dependencies added: concurrency, ref-fd

Dependencies removed: array, atomic-primops, monad-control, stm, template-haskell

API changes (from Hackage documentation)

Files

• Control/Concurrent/Classy.hs +0/−40
• Control/Concurrent/Classy/CRef.hs +0/−114
• Control/Concurrent/Classy/Chan.hs +0/−79
• Control/Concurrent/Classy/MVar.hs +0/−128
• Control/Concurrent/Classy/QSem.hs +0/−45
• Control/Concurrent/Classy/QSemN.hs +0/−97
• Control/Concurrent/Classy/STM.hs +0/−28
• Control/Concurrent/Classy/STM/TArray.hs +0/−56
• Control/Concurrent/Classy/STM/TBQueue.hs +0/−146
• Control/Concurrent/Classy/STM/TChan.hs +0/−135
• Control/Concurrent/Classy/STM/TMVar.hs +0/−118
• Control/Concurrent/Classy/STM/TQueue.hs +0/−113
• Control/Concurrent/Classy/STM/TVar.hs +0/−62
• Control/Monad/Conc/Class.hs +0/−736
• Control/Monad/STM/Class.hs +0/−195
• Test/DejaFu.hs +56/−45
• Test/DejaFu/Common.hs +746/−0
• Test/DejaFu/Conc.hs +200/−0
• Test/DejaFu/Conc/Internal.hs +385/−0
• Test/DejaFu/Conc/Internal/Common.hs +172/−0
• Test/DejaFu/Conc/Internal/Memory.hs +211/−0
• Test/DejaFu/Conc/Internal/Threading.hs +143/−0
• Test/DejaFu/Deterministic.hs +0/−209
• Test/DejaFu/Deterministic/Internal.hs +0/−475
• Test/DejaFu/Deterministic/Internal/Common.hs +0/−873
• Test/DejaFu/Deterministic/Internal/Memory.hs +0/−208
• Test/DejaFu/Deterministic/Internal/Threading.hs +0/−200
• Test/DejaFu/Internal.hs +0/−43
• Test/DejaFu/SCT.hs +34/−82
• Test/DejaFu/STM.hs +14/−29
• Test/DejaFu/STM/Internal.hs +33/−29
• dejafu.cabal +22/−43

@@ -1,40 +0,0 @@--- |--- Module      : Control.Concurrent.Classy--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : experimental--- Portability : non-portable------ 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) #-}

@@ -1,114 +0,0 @@--- |--- Module      : Control.Concurrent.Classy.CRef--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : stable--- Portability : portable------ 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

@@ -1,79 +0,0 @@--- |--- Module      : Control.Concurrent.Classy.Chan--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : stable--- Portability : portable------ 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

@@ -1,128 +0,0 @@--- |--- Module      : Control.Concurrent.Classy.MVar--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : stable--- Portability : portable------ 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

@@ -1,45 +0,0 @@--- |--- Module      : Control.Concurrent.Classy.QSem--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : stable--- Portability : portable------ 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

@@ -1,97 +0,0 @@--- |--- Module      : Control.Concurrent.Classy.QSemN--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : stable--- Portability : portable------ 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

@@ -1,28 +0,0 @@--- |--- Module      : Control.Concurrent.Classy.STM--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : experimental--- Portability : non-portable------ 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) #-}

@@ -1,56 +0,0 @@-{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}---- |--- Module      : Control.Concurrent.Classy.STM.--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : stable--- Portability : 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)

@@ -1,146 +0,0 @@--- |--- Module      : Control.Concurrent.Classy.STM.TBQueue--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : stable--- Portability : portable------ '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

@@ -1,135 +0,0 @@--- |--- Module      : Control.Concurrent.Classy.STM.TChan--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : stable--- Portability : portable------ 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)

@@ -1,118 +0,0 @@--- |--- Module      : Control.Concurrent.Classy.STM.TMVar--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : stable--- Portability : portable------ 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

@@ -1,113 +0,0 @@--- |--- Module      : Control.Concurrent.Classy.STM.TQueue--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : stable--- Portability : portable------ 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

@@ -1,62 +0,0 @@--- |--- Module      : Control.Concurrent.Classy.STM.TVar--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : stable--- Portability : portable------ 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,736 +0,0 @@-{-# LANGUAGE CPP              #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE RankNTypes       #-}-{-# LANGUAGE TemplateHaskell  #-}-{-# LANGUAGE TypeFamilies     #-}---- |--- Module      : Control.Monad.Conc.Class--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : experimental--- Portability : CPP, FlexibleContexts, RankNTypes, TemplateHaskell, 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(..)--  -- * Threads-  , spawn-  , forkFinally-  , killThread--  -- ** 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---- for the class and utilities-import Control.Exception (Exception, AsyncException(ThreadKilled), SomeException)-import Control.Monad.Catch (MonadCatch, MonadThrow, MonadMask)-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.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--{-# 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--- terms of how they can operate on shared state and in the presence--- of exceptions.------ Every @MonadConc@ has an associated 'MonadSTM', transactions of--- which can be run atomically.-class ( Applicative m, Monad m-      , MonadCatch m, MonadThrow m, MonadMask m-      , MonadSTM (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 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\"-  -- @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@, @atomicModifyCRef@, and @atomicWriteCRef@ are used.-  type CRef m :: * -> *--  -- | When performing compare-and-swap operations on @CRef@s, a-  -- @Ticket@ is a proof that a thread observed a specific previous-  -- value.-  type Ticket m :: * -> *--  -- | An abstract handle to a thread.-  type ThreadId m :: *--  -- | Fork a computation to happen concurrently. Communication may-  -- happen over @MVar@s.-  ---  -- > fork ma = forkWithUnmask (\_ -> ma)-  fork :: m () -> m (ThreadId m)-  fork ma = forkWithUnmask (\_ -> ma)--  -- | 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-  -- implementation dependent. The int is interpreted modulo to the-  -- total number of capabilities as returned by 'getNumCapabilities'.-  ---  -- > forkOn c ma = forkOnWithUnmask c (\_ -> ma)-  forkOn :: Int -> m () -> m (ThreadId m)-  forkOn c ma = forkOnWithUnmask c (\_ -> ma)--  -- | 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--  -- | Set the number of Haskell threads that can run simultaneously.-  setNumCapabilities :: Int -> m ()--  -- | Get the @ThreadId@ of the current thread.-  myThreadId :: m (ThreadId m)--  -- | Allows a context-switch to any other currently runnable thread-  -- (if any).-  yield :: m ()--  -- | 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--  -- | 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.-  putMVar :: MVar m a -> a -> m ()--  -- | Attempt to put a value in a @MVar@ non-blockingly, returning-  -- 'True' (and filling the @MVar@) if there was nothing there,-  -- otherwise returning 'False'.-  tryPutMVar :: MVar m a -> a -> m Bool--  -- | 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.-  readMVar :: MVar m a -> m a--  -- | 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 @MVar@ already, until one has been put.-  takeMVar :: MVar m a -> m a--  -- | 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'.-  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-  readCRef :: CRef m a -> m a-  readCRef cref = readForCAS cref >>= peekTicket--  -- | Atomically modify the value stored in a reference. This imposes-  -- a full memory barrier.-  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 'atomicModifyCRef' has.-  ---  -- > atomicWriteCRef r a = atomicModifyCRef r $ const (a, ())-  atomicWriteCRef :: CRef m a -> a -> m ()-  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.-  readForCAS :: CRef m a -> m (Ticket m a)--  -- | Extract the actual Haskell value from a @Ticket@.-  ---  -- This shouldn't need to do any monadic computation, the @m@-  -- appears in the result type because of the need for injectivity in-  -- the @Ticket@ type family, which can't be expressed currently.-  peekTicket :: Ticket m a -> m a--  -- | Perform a machine-level compare-and-swap (CAS) operation on a-  -- @CRef@. Returns an indication of success and a @Ticket@ for the-  -- most current value in the @CRef@.-  ---  -- This is strict in the \"new\" value argument.-  casCRef :: CRef m a -> Ticket m a -> a -> m (Bool, Ticket m a)--  -- | 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--  -- | A variant of 'modifyCRefCAS' which doesn't return a result.-  ---  -- > modifyCRefCAS_ cref f = modifyCRefCAS cref (\a -> (f a, ()))-  modifyCRefCAS_ :: CRef m a -> (a -> a) -> m ()-  modifyCRefCAS_ cref f = modifyCRefCAS cref (\a -> (f a, ()))--  -- | Perform an STM transaction atomically.-  atomically :: STM m a -> m a--  -- | Read the current value stored in a @TVar@. This may be-  -- implemented differently for speed.-  ---  -- > 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 ()--  -- | Does nothing.-  ---  -- This function is purely for testing purposes, and indicates that-  -- 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 _ = pure ()-  _concKnowsAbout :: Either (MVar m a) (TVar (STM m) a) -> m ()-  _concKnowsAbout _ = pure ()--  -- | Does nothing.-  ---  -- The counterpart to '_concKnowsAbout'. Indicates that the-  -- referenced variable will never be touched again by the current-  -- thread.-  ---  -- Note that inappropriate use of @_concForgets@ can result in false-  -- positives! Be very sure that the current thread will /never/-  -- refer to the variable again, for instance when leaving its scope.-  ---  -- > _concForgets _ = pure ()-  _concForgets :: Either (MVar m a) (TVar (STM m) a) -> m ()-  _concForgets _ = pure ()--  -- | Does nothing.-  ---  -- Indicates to the test runner that all variables which have been-  -- passed in to this thread have been recorded by calls to-  -- '_concKnowsAbout'. If every thread has called '_concAllKnown',-  -- then detection of nonglobal deadlock is turned on.-  ---  -- If a thread receives references to @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 = pure ()-  _concAllKnown :: m ()-  _concAllKnown = pure ()--  -- | Does nothing.-  ---  -- During testing, records a message which shows up in the trace.-  ---  -- > _concMessage _ = pure ()-  _concMessage :: Typeable a => a -> m ()-  _concMessage _ = pure ()------------------------------------------------------------------------------------ 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 @MVar@ which can be used to query the result.-spawn :: MonadConc m => m a -> m (MVar m a)-spawn ma = do-  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--- function is called with asynchronous exceptions masked.------ This function is useful for informing the parent when a child--- terminates, for example.-forkFinally :: MonadConc m => m a -> (Either SomeException a -> m ()) -> m (ThreadId m)-forkFinally action and_then =-  mask $ \restore ->-    fork $ Ca.try (restore action) >>= and_then---- | Raise the 'ThreadKilled' exception in the target thread. Note--- that if the thread is prepared to catch this exception, it won't--- actually kill it.-killThread :: MonadConc m => ThreadId m -> m ()-killThread tid = throwTo tid ThreadKilled---- | 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 = pure False---- Exceptions---- | 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---- | 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---- | 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---- | 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---- Mutable Variables---- | 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---- | 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---- | 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'--  pure (suc, a')------------------------------------------------------------------------------------ Concrete instances--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   = IO.forkIO-  forkOn = IO.forkOn--  forkWithUnmask   = IO.forkIOWithUnmask-  forkOnWithUnmask = IO.forkOnWithUnmask--  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------------------------------------------------------------------------------------ Transformer instances--#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                        }--INSTANCE(ReaderT r, MonadConc m, id)--INSTANCE(IdentityT, MonadConc m, id)--INSTANCE(WL.WriterT w, (MonadConc m, Monoid w), fst)-INSTANCE(WS.WriterT w, (MonadConc m, Monoid w), fst)--INSTANCE(SL.StateT s, MonadConc m, fst)-INSTANCE(SS.StateT s, MonadConc m, fst)--INSTANCE(RL.RWST r w s, (MonadConc m, Monoid w), (\(a,_,_) -> a))-INSTANCE(RS.RWST r w s, (MonadConc m, Monoid w), (\(a,_,_) -> a))--#undef INSTANCE------------------------------------------------------------------------------------- | 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-#if MIN_VERSION_template_haskell(2,11,0)-    -- template-haskell-2.11.0.0 drops the 'Fixity' value from 'VarI'-    VarI _ (ForallT _ _ (AppT (AppT ArrowT (AppT (AppT (ConT _) t) _)) _)) _ ->-#else-    VarI _ (ForallT _ _ (AppT (AppT ArrowT (AppT (AppT (ConT _) t) _)) _)) _ _ ->-#endif-      [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--          fork   = liftedF $(varE unstN) fork-          forkOn = liftedF $(varE unstN) . forkOn--          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)--          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--          _concKnowsAbout = lift . _concKnowsAbout-          _concForgets    = lift . _concForgets-          _concAllKnown   = lift _concAllKnown-          _concMessage    = lift . _concMessage-      |]-    _ -> fail "Expected a value of type (forall a -> StT t a -> a)"---- | 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)---- | 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,195 +0,0 @@-{-# LANGUAGE CPP             #-}-{-# LANGUAGE RankNTypes      #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeFamilies    #-}---- |--- Module      : Control.Monad.STM.Class--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : experimental--- Portability : CPP, RankNTypes, TemplateHaskell, TypeFamilies------ This module provides an abstraction over 'STM', which can be used--- with 'MonadConc'.------ 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--  -- * Utilities for instance writers-  , makeTransSTM-  , liftedOrElse-  ) where--import Control.Exception (Exception)-import Control.Monad (unless)-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.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---- | @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.-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 TVar stm :: * -> *--  -- | Retry execution of this transaction because it has seen values-  -- 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 :: 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 :: stm a -> stm a -> stm a--  -- | Create a new @TVar@ containing the given value.-  ---  -- > newTVar = newTVarN ""-  newTVar :: a -> stm (TVar stm a)-  newTVar = newTVarN ""--  -- | 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 @TVar@.-  readTVar :: TVar stm a -> stm a--  -- | Write the supplied value into the @TVar@.-  writeTVar :: TVar stm a -> a -> stm ()---- | Check whether a condition is true and, if not, call @retry@.-check :: MonadSTM stm => Bool -> stm ()-check b = unless b retry---- | Throw an exception. This aborts the transaction and propagates--- the exception.-throwSTM :: (MonadSTM stm, Exception e) => e -> stm a-throwSTM = Ca.throwM---- | Handling exceptions from 'throwSTM'.-catchSTM :: (MonadSTM stm, Exception e) => stm a -> (e -> stm a) -> stm a-catchSTM = Ca.catch--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--#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(ReaderT r, MonadSTM stm, id)--INSTANCE(IdentityT, MonadSTM stm, id)--INSTANCE(WL.WriterT w, (MonadSTM stm, Monoid w), fst)-INSTANCE(WS.WriterT w, (MonadSTM stm, Monoid w), fst)--INSTANCE(SL.StateT s, MonadSTM stm, fst)-INSTANCE(SS.StateT s, MonadSTM stm, fst)--INSTANCE(RL.RWST r w s, (MonadSTM stm, Monoid w), (\(a,_,_) -> a))-INSTANCE(RS.RWST r w s, (MonadSTM stm, Monoid w), (\(a,_,_) -> a))--#undef INSTANCE------------------------------------------------------------------------------------- | 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-#if MIN_VERSION_template_haskell(2,11,0)-    -- template-haskell-2.11.0.0 drops the 'Fixity' value from 'VarI'-    VarI _ (ForallT _ _ (AppT (AppT ArrowT (AppT (AppT (ConT _) t) _)) _)) _ ->-#else-    VarI _ (ForallT _ _ (AppT (AppT ArrowT (AppT (AppT (ConT _) t) _)) _)) _ _ ->-#endif-      [d|-        instance (MonadSTM stm, MonadTransControl $(pure t)) => MonadSTM ($(pure t) stm) where-          type TVar ($(pure t) stm) = TVar stm--          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)"---- | 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,3 +1,4 @@+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-}  -- |@@ -44,22 +45,25 @@ -- Here is what Deja Fu has to say about it: -- -- > > autocheck example1--- > [fail] Never Deadlocks (checked: 2)--- >         [deadlock] S0---------S1--P2---S1---- > [pass] No Exceptions (checked: 11)--- > [fail] Consistent Result (checked: 10)--- >         0 S0---------S1---------------S0--S2---------------S0------- >         [deadlock] S0---------S1--P2---S1-+-- > [fail] Never Deadlocks (checked: 5)+-- >         [deadlock] S0------------S1-P2--S1-+-- > [pass] No Exceptions (checked: 12)+-- > [fail] Consistent Result (checked: 11)+-- >         0 S0------------S2-----------------S1-----------------S0----+-- >+-- >         [deadlock] S0------------S1-P2--S1- -- > False -- -- It identifies the deadlock, and also the possible results the -- computation can produce, and displays a simplified trace leading to--- each failing outcome. It also returns @False@ as there are test--- failures. The automatic testing functionality is good enough if you--- only want to check your computation is deterministic, but if you--- have more specific requirements (or have some expected and--- tolerated level of nondeterminism), you can write tests yourself--- using the @dejafu*@ functions.+-- each failing outcome. The trace contains thread numbers, and the+-- names (which can be set by the programmer) are displayed beneath.+-- It also returns @False@ as there are test failures. The automatic+-- testing functionality is good enough if you only want to check your+-- computation is deterministic, but if you have more specific+-- requirements (or have some expected and tolerated level of+-- nondeterminism), you can write tests yourself using the @dejafu*@+-- functions. -- -- __Warning:__ If your computation under test does @IO@, the @IO@ -- will be executed lots of times! Be sure that it is deterministic@@ -199,8 +203,8 @@   , Failure(..)   , runTest   , runTest'-  , runTestIO-  , runTestIO'+  , runTestM+  , runTestM'    -- * Predicates @@ -238,12 +242,14 @@ import Control.Arrow (first) import Control.DeepSeq (NFData(..)) import Control.Monad (when, unless)+import Control.Monad.Ref (MonadRef)+import Control.Monad.ST (runST) import Data.Function (on) 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.Common+import Test.DejaFu.Conc import Test.DejaFu.SCT  -- | The default memory model: @TotalStoreOrder@@@ -260,25 +266,38 @@   => (forall t. ConcST t a)   -- ^ The computation to test   -> IO Bool-autocheck = autocheck' defaultMemType+autocheck = autocheck' defaultMemType defaultBounds --- | Variant of 'autocheck' which tests a computation under a given--- memory model.+-- | Variant of 'autocheck' which takes a memor model and schedule+-- bounds.+--+-- Schedule bounding is used to filter the large number of possible+-- schedules, and can be iteratively increased for further coverage+-- guarantees. Empirical studies (/Concurrency Testing Using Schedule+-- Bounding: an Empirical Study/, P. Thompson, A. Donaldson, and+-- A. Betts) have found that many concurrency bugs can be exhibited+-- with as few as two threads and two pre-emptions, which is part of+-- what 'dejafus' uses.+--+-- __Warning:__ Using largers bounds will almost certainly+-- significantly increase the time taken to test! autocheck' :: (Eq a, Show a)   => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -> Bounds+  -- ^ The schedule bounds   -> (forall t. ConcST t a)   -- ^ The computation to test   -> IO Bool-autocheck' memtype conc = dejafus' memtype defaultBounds conc autocheckCases+autocheck' memtype cb conc = dejafus' memtype cb conc autocheckCases  -- | Variant of 'autocheck' for computations which do 'IO'. autocheckIO :: (Eq a, Show a) => ConcIO a -> IO Bool-autocheckIO = autocheckIO' defaultMemType+autocheckIO = autocheckIO' defaultMemType defaultBounds  -- | Variant of 'autocheck'' for computations which do 'IO'.-autocheckIO' :: (Eq a, Show a) => MemType -> ConcIO a -> IO Bool-autocheckIO' memtype concio = dejafusIO' memtype defaultBounds concio autocheckCases+autocheckIO' :: (Eq a, Show a) => MemType -> Bounds -> ConcIO a -> IO Bool+autocheckIO' memtype cb concio = dejafusIO' memtype cb concio autocheckCases  -- | Predicates for the various autocheck functions. autocheckCases :: (Eq a, Show a) => [(String, Predicate a)]@@ -300,17 +319,6 @@  -- | Variant of 'dejafu'' which takes a memory model and schedule -- bounds.------ Schedule bounding is used to filter the large number of possible--- schedules, and can be iteratively increased for further coverage--- guarantees. Empirical studies (/Concurrency Testing Using Schedule--- Bounding: an Empirical Study/, P. Thompson, A. Donaldson, and--- A. Betts) have found that many concurrency bugs can be exhibited--- with as few as two threads and two pre-emptions, which is part of--- what 'dejafus' uses.------ __Warning:__ Using largers bounds will almost certainly--- significantly increase the time taken to test! dejafu' :: Show a   => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.@@ -346,7 +354,7 @@   -- ^ The list of predicates (with names) to check   -> IO Bool dejafus' memtype cb conc tests = do-  let traces = sctBound memtype cb conc+  let traces = runST (sctBound memtype cb conc)   results <- mapM (\(name, test) -> doTest name $ test traces) tests   return $ and results @@ -365,7 +373,7 @@ -- | Variant of 'dejafus'' for computations which do 'IO'. dejafusIO' :: Show a => MemType -> Bounds -> ConcIO a -> [(String, Predicate a)] -> IO Bool dejafusIO' memtype cb concio tests = do-  traces  <- sctBoundIO memtype cb concio+  traces  <- sctBound memtype cb concio   results <- mapM (\(name, test) -> doTest name $ test traces) tests   return $ and results @@ -409,7 +417,7 @@   -> (forall t. ConcST t a)   -- ^ The computation to test   -> Result a-runTest = runTest' defaultMemType defaultBounds+runTest test conc = runST (runTestM test conc)  -- | Variant of 'runTest' which takes a memory model and schedule -- bounds.@@ -423,15 +431,18 @@   -> (forall t. ConcST t a)   -- ^ The computation to test   -> Result a-runTest' memtype cb predicate conc = predicate $ sctBound memtype cb conc+runTest' memtype cb predicate conc =+  runST (runTestM' memtype cb predicate conc) --- | Variant of 'runTest' for computations which do 'IO'.-runTestIO :: Predicate a -> ConcIO a -> IO (Result a)-runTestIO = runTestIO' defaultMemType defaultBounds+-- | Monad-polymorphic variant of 'runTest'.+runTestM :: MonadRef r n+         => Predicate a -> Conc n r a -> n (Result a)+runTestM = runTestM' defaultMemType defaultBounds --- | Variant of 'runTest'' for computations which do 'IO'.-runTestIO' :: MemType -> Bounds -> Predicate a -> ConcIO a -> IO (Result a)-runTestIO' memtype cb predicate conc = predicate <$> sctBoundIO memtype cb conc+-- | Monad-polymorphic variant of 'runTest''.+runTestM' :: MonadRef r n+          => MemType -> Bounds -> Predicate a -> Conc n r a -> n (Result a)+runTestM' memtype cb predicate conc = predicate <$> sctBound memtype cb conc  -- * Predicates 

@@ -0,0 +1,746 @@+-- |+-- Module      : Test.DejaFu.Common+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : experimental+-- Portability : portable+--+-- Common types and functions used throughout DejaFu. This module is+-- NOT considered to form part of the public interface of this+-- library.+module Test.DejaFu.Common+  ( -- * Identifiers+    ThreadId(..)+  , CRefId(..)+  , MVarId(..)+  , TVarId(..)+  , initialThread+  -- ** Identifier source+  , IdSource(..)+  , nextCRId+  , nextMVId+  , nextTVId+  , nextTId+  , initialIdSource++  -- * Actions+  -- ** Thread actions+  , ThreadAction(..)+  , isBlock+  , tvarsOf+  -- ** Lookahead+  , Lookahead(..)+  , rewind+  , willRelease+  -- ** Simplified actions+  , ActionType(..)+  , isBarrier+  , isCommit+  , synchronises+  , crefOf+  , mvarOf+  , simplifyAction+  , simplifyLookahead+  -- ** STM actions+  , TTrace+  , TAction(..)++  -- * Traces+  , Trace+  , Decision(..)+  , showTrace+  , preEmpCount++  -- * Failures+  , Failure(..)+  , showFail++  -- * Memory models+  , MemType(..)+  ) where++import Control.DeepSeq (NFData(..))+import Control.Exception (MaskingState(..))+import Data.Dynamic (Dynamic)+import Data.List (sort, nub, intercalate)+import Data.Maybe (fromMaybe, mapMaybe)+import Data.Set (Set)+import qualified Data.Set as S+import Test.DPOR (Decision(..), Trace)++-------------------------------------------------------------------------------+-- Identifiers++-- | Every live thread has a unique identitifer.+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 (Just n) _) = n+  show (ThreadId Nothing  i) = show i++instance NFData ThreadId where+  rnf (ThreadId 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 (Just n) _) = n+  show (CRefId Nothing  i) = show i++instance NFData CRefId where+  rnf (CRefId n i) = rnf (n, i)++-- | 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 @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 ID of the initial thread.+initialThread :: ThreadId+initialThread = ThreadId (Just "main") 0++---------------------------------------+-- Identifier source++-- | The number of ID parameters was getting a bit unwieldy, so this+-- hides them all away.+data IdSource = Id+  { _nextCRId  :: Int+  , _nextMVId  :: Int+  , _nextTVId  :: Int+  , _nextTId   :: Int+  , _usedCRNames :: [String]+  , _usedMVNames :: [String]+  , _usedTVNames :: [String]+  , _usedTNames  :: [String]+  }++-- | Get the next free 'CRefId'.+nextCRId :: String -> IdSource -> (IdSource, CRefId)+nextCRId name idsource = (newIdSource, newCRId) where+  newIdSource = idsource { _nextCRId = newId, _usedCRNames = newUsed }+  newCRId     = CRefId newName newId+  newId       = _nextCRId idsource + 1+  (newName, newUsed) = nextId name (_usedCRNames idsource)++-- | Get the next free 'MVarId'.+nextMVId :: String -> IdSource -> (IdSource, MVarId)+nextMVId name idsource = (newIdSource, newMVId) where+  newIdSource = idsource { _nextMVId = newId, _usedMVNames = newUsed }+  newMVId     = MVarId newName newId+  newId       = _nextMVId idsource + 1+  (newName, newUsed) = nextId name (_usedMVNames idsource)++-- | Get the next free 'TVarId'.+nextTVId :: String -> IdSource -> (IdSource, TVarId)+nextTVId name idsource = (newIdSource, newTVId) where+  newIdSource = idsource { _nextTVId = newId, _usedTVNames = newUsed }+  newTVId     = TVarId newName newId+  newId       = _nextTVId idsource + 1+  (newName, newUsed) = nextId name (_usedTVNames idsource)++-- | Get the next free 'ThreadId'.+nextTId :: String -> IdSource -> (IdSource, ThreadId)+nextTId name idsource = (newIdSource, newTId) where+  newIdSource = idsource { _nextTId = newId, _usedTNames = newUsed }+  newTId      = ThreadId newName newId+  newId       = _nextTId idsource + 1+  (newName, newUsed) = nextId name (_usedTNames idsource)++-- | The initial ID source.+initialIdSource :: IdSource+initialIdSource = Id 0 0 0 0 [] [] [] []++-------------------------------------------------------------------------------+-- Actions++---------------------------------------+-- Thread actions++-- | All the actions that a thread can perform.+data ThreadAction =+    Fork ThreadId+  -- ^ Start a new thread.+  | MyThreadId+  -- ^ Get the 'ThreadId' of the current thread.+  | GetNumCapabilities Int+  -- ^ Get the number of Haskell threads that can run simultaneously.+  | SetNumCapabilities Int+  -- ^ Set the number of Haskell threads that can run simultaneously.+  | Yield+  -- ^ Yield the current thread.+  | 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 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 MVarId [ThreadId]+  -- ^ Take from a 'MVar', possibly waking up some threads.+  | BlockedTakeVar MVarId+  -- ^ Get blocked on a take.+  | TryTakeVar MVarId Bool [ThreadId]+  -- ^ Try to take from a 'MVar', possibly waking up some threads.+  | NewRef CRefId+  -- ^ Create a new 'CRef'.+  | ReadRef CRefId+  -- ^ Read from a 'CRef'.+  | ReadRefCas CRefId+  -- ^ Read from a 'CRef' for a future compare-and-swap.+  | ModRef CRefId+  -- ^ Modify a 'CRef'.+  | ModRefCas CRefId+  -- ^ Modify a 'CRef' using a compare-and-swap.+  | WriteRef CRefId+  -- ^ Write to a 'CRef' without synchronising.+  | CasRef CRefId Bool+  -- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising+  -- it.+  | 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 TTrace [ThreadId]+  -- ^ An STM transaction was executed, possibly waking up some+  -- threads.+  | BlockedSTM TTrace+  -- ^ Got blocked in an STM transaction.+  | Catching+  -- ^ Register a new exception handler+  | PopCatching+  -- ^ Pop the innermost exception handler from the stack.+  | Throw+  -- ^ Throw an exception.+  | ThrowTo ThreadId+  -- ^ Throw an exception to a thread.+  | BlockedThrowTo ThreadId+  -- ^ Get blocked on a 'throwTo'.+  | Killed+  -- ^ Killed by an uncaught exception.+  | SetMasking Bool MaskingState+  -- ^ Set the masking state. If 'True', this is being used to set the+  -- masking state to the original state in the argument passed to a+  -- 'mask'ed function.+  | ResetMasking Bool MaskingState+  -- ^ Return to an earlier masking state.  If 'True', this is being+  -- used to return to the state of the masked block in the argument+  -- passed to a 'mask'ed function.+  | LiftIO+  -- ^ Lift an IO action. Note that this can only happen with+  -- 'ConcIO'.+  | Return+  -- ^ A 'return' or 'pure' action was executed.+  | Message Dynamic+  -- ^ A '_concMessage' annotation was processed.+  | Stop+  -- ^ Cease execution and terminate.+  deriving Show++instance NFData ThreadAction where+  rnf (Fork t) = rnf t+  rnf (GetNumCapabilities i) = rnf i+  rnf (SetNumCapabilities i) = rnf i+  rnf (NewVar c) = rnf c+  rnf (PutVar c ts) = rnf (c, ts)+  rnf (BlockedPutVar c) = rnf c+  rnf (TryPutVar c b ts) = rnf (c, b, ts)+  rnf (ReadVar c) = rnf c+  rnf (BlockedReadVar c) = rnf c+  rnf (TakeVar c ts) = rnf (c, ts)+  rnf (BlockedTakeVar c) = rnf c+  rnf (TryTakeVar c b ts) = rnf (c, b, ts)+  rnf (NewRef c) = rnf c+  rnf (ReadRef c) = rnf c+  rnf (ReadRefCas c) = rnf c+  rnf (ModRef c) = rnf c+  rnf (ModRefCas c) = rnf c+  rnf (WriteRef c) = rnf c+  rnf (CasRef c b) = rnf (c, b)+  rnf (CommitRef t c) = rnf (t, c)+  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++-- | Get the @TVar@s affected by a @ThreadAction@.+tvarsOf :: ThreadAction -> Set TVarId+tvarsOf act = S.fromList $ case act of+  STM trc _ -> concatMap tvarsOf' trc+  BlockedSTM trc -> concatMap tvarsOf' trc+  _ -> []++  where+    tvarsOf' (TRead  tv) = [tv]+    tvarsOf' (TWrite tv) = [tv]+    tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)+    tvarsOf' (TCatch  ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)+    tvarsOf' _ = []++---------------------------------------+-- Lookahead++-- | A one-step look-ahead at what a thread will do next.+data Lookahead =+    WillFork+  -- ^ Will start a new thread.+  | WillMyThreadId+  -- ^ Will get the 'ThreadId'.+  | WillGetNumCapabilities+  -- ^ Will get the number of Haskell threads that can run+  -- simultaneously.+  | WillSetNumCapabilities Int+  -- ^ Will set the number of Haskell threads that can run+  -- simultaneously.+  | WillYield+  -- ^ Will yield the current thread.+  | WillNewVar+  -- ^ 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+  -- ^ Will read from a 'CRef'.+  | WillReadRefCas CRefId+  -- ^ Will read from a 'CRef' for a future compare-and-swap.+  | WillModRef CRefId+  -- ^ Will modify a 'CRef'.+  | WillModRefCas CRefId+  -- ^ Will nodify a 'CRef' using a compare-and-swap.+  | WillWriteRef CRefId+  -- ^ Will write to a 'CRef' without synchronising.+  | WillCasRef CRefId+  -- ^ Will attempt to to a 'CRef' using a compare-and-swap,+  -- synchronising it.+  | WillCommitRef ThreadId CRefId+  -- ^ Will commit the last write by the given thread to the 'CRef'.+  | WillSTM+  -- ^ Will execute an STM transaction, possibly waking up some+  -- threads.+  | WillCatching+  -- ^ Will register a new exception handler+  | WillPopCatching+  -- ^ Will pop the innermost exception handler from the stack.+  | WillThrow+  -- ^ Will throw an exception.+  | WillThrowTo ThreadId+  -- ^ Will throw an exception to a thread.+  | WillSetMasking Bool MaskingState+  -- ^ Will set the masking state. If 'True', this is being used to+  -- set the masking state to the original state in the argument+  -- passed to a 'mask'ed function.+  | WillResetMasking Bool MaskingState+  -- ^ Will return to an earlier masking state.  If 'True', this is+  -- being used to return to the state of the masked block in the+  -- argument passed to a 'mask'ed function.+  | WillLiftIO+  -- ^ Will lift an IO action. Note that this can only happen with+  -- 'ConcIO'.+  | WillReturn+  -- ^ Will execute a 'return' or 'pure' action.+  | WillMessage Dynamic+  -- ^ Will process a _concMessage' annotation.+  | WillStop+  -- ^ Will cease execution and terminate.+  deriving Show++instance NFData Lookahead where+  rnf (WillSetNumCapabilities i) = rnf i+  rnf (WillPutVar c) = rnf c+  rnf (WillTryPutVar c) = rnf c+  rnf (WillReadVar c) = rnf c+  rnf (WillTakeVar c) = rnf c+  rnf (WillTryTakeVar c) = rnf c+  rnf (WillReadRef c) = rnf c+  rnf (WillReadRefCas c) = rnf c+  rnf (WillModRef c) = rnf c+  rnf (WillModRefCas c) = rnf c+  rnf (WillWriteRef c) = rnf c+  rnf (WillCasRef c) = rnf c+  rnf (WillCommitRef t c) = rnf (t, c)+  rnf (WillThrowTo t) = rnf t+  rnf (WillSetMasking b m) = b `seq` m `seq` ()+  rnf (WillResetMasking b m) = b `seq` m `seq` ()+  rnf (WillMessage m) = m `seq` ()+  rnf l = l `seq` ()++-- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has+-- happened. 'Killed' has no 'Lookahead' counterpart.+rewind :: ThreadAction -> Maybe Lookahead+rewind (Fork _) = Just WillFork+rewind MyThreadId = Just WillMyThreadId+rewind (GetNumCapabilities _) = Just WillGetNumCapabilities+rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i)+rewind Yield = Just WillYield+rewind (NewVar _) = Just WillNewVar+rewind (PutVar c _) = Just (WillPutVar c)+rewind (BlockedPutVar c) = Just (WillPutVar c)+rewind (TryPutVar c _ _) = Just (WillTryPutVar c)+rewind (ReadVar c) = Just (WillReadVar c)+rewind (BlockedReadVar c) = Just (WillReadVar c)+rewind (TakeVar c _) = Just (WillTakeVar c)+rewind (BlockedTakeVar c) = Just (WillTakeVar c)+rewind (TryTakeVar c _ _) = Just (WillTryTakeVar c)+rewind (NewRef _) = Just WillNewRef+rewind (ReadRef c) = Just (WillReadRef c)+rewind (ReadRefCas c) = Just (WillReadRefCas c)+rewind (ModRef c) = Just (WillModRef c)+rewind (ModRefCas c) = Just (WillModRefCas c)+rewind (WriteRef c) = Just (WillWriteRef c)+rewind (CasRef c _) = Just (WillCasRef c)+rewind (CommitRef t c) = Just (WillCommitRef t c)+rewind (STM _ _) = Just WillSTM+rewind (BlockedSTM _) = Just WillSTM+rewind Catching = Just WillCatching+rewind PopCatching = Just WillPopCatching+rewind Throw = Just WillThrow+rewind (ThrowTo t) = Just (WillThrowTo t)+rewind (BlockedThrowTo t) = Just (WillThrowTo t)+rewind Killed = Nothing+rewind (SetMasking b m) = Just (WillSetMasking b m)+rewind (ResetMasking b m) = Just (WillResetMasking b m)+rewind LiftIO = Just WillLiftIO+rewind Return = Just WillReturn+rewind (Message m) = Just (WillMessage m)+rewind Stop = Just WillStop++-- | Check if an operation could enable another thread.+willRelease :: Lookahead -> Bool+willRelease WillFork = True+willRelease WillYield = True+willRelease (WillPutVar _) = True+willRelease (WillTryPutVar _) = True+willRelease (WillReadVar _) = True+willRelease (WillTakeVar _) = True+willRelease (WillTryTakeVar _) = True+willRelease WillSTM = True+willRelease WillThrow = True+willRelease (WillSetMasking _ _) = True+willRelease (WillResetMasking _ _) = True+willRelease WillStop = True+willRelease _ = False++---------------------------------------+-- Simplified actions++-- | A simplified view of the possible actions a thread can perform.+data ActionType =+    UnsynchronisedRead  CRefId+  -- ^ A 'readCRef' or a 'readForCAS'.+  | UnsynchronisedWrite CRefId+  -- ^ A 'writeCRef'.+  | UnsynchronisedOther+  -- ^ Some other action which doesn't require cross-thread+  -- communication.+  | PartiallySynchronisedCommit CRefId+  -- ^ A commit.+  | PartiallySynchronisedWrite  CRefId+  -- ^ A 'casCRef'+  | PartiallySynchronisedModify CRefId+  -- ^ A 'modifyCRefCAS'+  | SynchronisedModify  CRefId+  -- ^ An 'atomicModifyCRef'.+  | SynchronisedRead    MVarId+  -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants).+  | SynchronisedWrite   MVarId+  -- ^ A 'putMVar' (or @try@/@blocked@ variant).+  | SynchronisedOther+  -- ^ Some other action which does require cross-thread+  -- communication.+  deriving (Eq, Show)++instance NFData ActionType where+  rnf (UnsynchronisedRead  r) = rnf r+  rnf (UnsynchronisedWrite r) = rnf r+  rnf (PartiallySynchronisedCommit r) = rnf r+  rnf (PartiallySynchronisedWrite  r) = rnf r+  rnf (PartiallySynchronisedModify  r) = rnf r+  rnf (SynchronisedModify  r) = rnf r+  rnf (SynchronisedRead    c) = rnf c+  rnf (SynchronisedWrite   c) = rnf c+  rnf a = a `seq` ()++-- | Check if an action imposes a write barrier.+isBarrier :: ActionType -> Bool+isBarrier (SynchronisedModify _) = True+isBarrier (SynchronisedRead   _) = True+isBarrier (SynchronisedWrite  _) = True+isBarrier SynchronisedOther = True+isBarrier _ = False++-- | Check if an action commits a given 'CRef'.+isCommit :: ActionType -> CRefId -> Bool+isCommit (PartiallySynchronisedCommit c) r = c == r+isCommit (PartiallySynchronisedWrite  c) r = c == r+isCommit (PartiallySynchronisedModify c) r = c == r+isCommit _ _ = False++-- | Check if an action synchronises a given 'CRef'.+synchronises :: ActionType -> CRefId -> Bool+synchronises a r = isCommit a r || isBarrier a++-- | Get the 'CRef' affected.+crefOf :: ActionType -> Maybe CRefId+crefOf (UnsynchronisedRead  r) = Just r+crefOf (UnsynchronisedWrite r) = Just r+crefOf (SynchronisedModify  r) = Just r+crefOf (PartiallySynchronisedCommit r) = Just r+crefOf (PartiallySynchronisedWrite  r) = Just r+crefOf (PartiallySynchronisedModify r) = Just r+crefOf _ = Nothing++-- | Get the 'MVar' affected.+mvarOf :: ActionType -> Maybe MVarId+mvarOf (SynchronisedRead  c) = Just c+mvarOf (SynchronisedWrite c) = Just c+mvarOf _ = Nothing++-- | Throw away information from a 'ThreadAction' and give a+-- simplified view of what is happening.+--+-- This is used in the SCT code to help determine interesting+-- alternative scheduling decisions.+simplifyAction :: ThreadAction -> ActionType+simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind++-- | Variant of 'simplifyAction' that takes a 'Lookahead'.+simplifyLookahead :: Lookahead -> ActionType+simplifyLookahead (WillPutVar c)     = SynchronisedWrite c+simplifyLookahead (WillTryPutVar c)  = SynchronisedWrite c+simplifyLookahead (WillReadVar c)    = SynchronisedRead c+simplifyLookahead (WillTakeVar c)    = SynchronisedRead c+simplifyLookahead (WillTryTakeVar c) = SynchronisedRead c+simplifyLookahead (WillReadRef r)     = UnsynchronisedRead r+simplifyLookahead (WillReadRefCas r)  = UnsynchronisedRead r+simplifyLookahead (WillModRef r)      = SynchronisedModify r+simplifyLookahead (WillModRefCas r)   = PartiallySynchronisedModify r+simplifyLookahead (WillWriteRef r)    = UnsynchronisedWrite r+simplifyLookahead (WillCasRef r)      = PartiallySynchronisedWrite r+simplifyLookahead (WillCommitRef _ r) = PartiallySynchronisedCommit r+simplifyLookahead WillSTM         = SynchronisedOther+simplifyLookahead (WillThrowTo _) = SynchronisedOther+simplifyLookahead _ = UnsynchronisedOther++---------------------------------------+-- STM actions++-- | 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.+  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` ()++-------------------------------------------------------------------------------+-- Traces++-- | Pretty-print a trace, including a key of the thread IDs (not+-- including thread 0). Each line of the key is indented by two+-- spaces.+showTrace :: Trace ThreadId ThreadAction Lookahead -> String+showTrace trc = intercalate "\n" $ concatMap go trc : strkey where+  go (_,_,CommitRef _ _) = "C-"+  go (Start    (ThreadId _ i),_,_) = "S" ++ show i ++ "-"+  go (SwitchTo (ThreadId _ i),_,_) = "P" ++ show i ++ "-"+  go (Continue,_,_) = "-"++  strkey = ["  " ++ show i ++ ": " ++ name | (i, name) <- key]++  key = sort . nub $ mapMaybe toKey trc where+    toKey (Start (ThreadId (Just name) i), _, _)+      | i > 0 = Just (i, name)+    toKey _ = Nothing++-- | Count the number of pre-emptions in a schedule prefix.+--+-- Commit threads complicate this a bit. Conceptually, commits are+-- happening truly in parallel, nondeterministically. The commit+-- thread implementation is just there to unify the two sources of+-- nondeterminism: commit timing and thread scheduling.+--+-- SO, we don't count a switch TO a commit thread as a+-- preemption. HOWEVER, the switch FROM a commit thread counts as a+-- preemption if it is not to the thread that the commit interrupted.+preEmpCount :: [(Decision ThreadId, ThreadAction)]+            -> (Decision ThreadId, Lookahead)+            -> Int+preEmpCount ts (d, _) = go initialThread Nothing ts where+  go _ (Just Yield) ((SwitchTo t, a):rest) = go t (Just a) rest+  go tid prior ((SwitchTo t, a):rest)+    | isCommitThread t = go tid prior (skip rest)+    | otherwise = 1 + go t (Just a) rest+  go _   _ ((Start t,  a):rest) = go t   (Just a) rest+  go tid _ ((Continue, a):rest) = go tid (Just a) rest+  go _ prior [] = case (prior, d) of+    (Just Yield, SwitchTo _) -> 0+    (_, SwitchTo _) -> 1+    _ -> 0++  -- Commit threads have negative thread IDs for easy identification.+  isCommitThread = (< initialThread)++  -- Skip until the next context switch.+  skip = dropWhile (not . isContextSwitch . fst)+  isContextSwitch Continue = False+  isContextSwitch _ = True++-------------------------------------------------------------------------------+-- Failures+++-- | An indication of how a concurrent computation failed.+data Failure =+    InternalError+  -- ^ Will be raised if the scheduler does something bad. This should+  -- never arise unless you write your own, faulty, scheduler! If it+  -- does, please file a bug report.+  | Abort+  -- ^ The scheduler chose to abort execution. This will be produced+  -- if, for example, all possible decisions exceed the specified+  -- bounds (there have been too many pre-emptions, the computation+  -- has executed for too long, or there have been too many yields).+  | Deadlock+  -- ^ The computation became blocked indefinitely on @MVar@s.+  | STMDeadlock+  -- ^ 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)++instance NFData Failure where+  rnf f = f `seq` ()++-- | Pretty-print a failure+showFail :: Failure -> String+showFail Abort             = "[abort]"+showFail Deadlock          = "[deadlock]"+showFail STMDeadlock       = "[stm-deadlock]"+showFail InternalError     = "[internal-error]"+showFail UncaughtException = "[exception]"++-------------------------------------------------------------------------------+-- Memory Models++-- | The memory model to use for non-synchronised 'CRef' operations.+data MemType =+    SequentialConsistency+  -- ^ The most intuitive model: a program behaves as a simple+  -- interleaving of the actions in different threads. When a 'CRef'+  -- is written to, that write is immediately visible to all threads.+  | TotalStoreOrder+  -- ^ Each thread has a write buffer. A thread sees its writes+  -- immediately, but other threads will only see writes when they are+  -- committed, which may happen later. Writes are committed in the+  -- same order that they are created.+  | PartialStoreOrder+  -- ^ Each 'CRef' has a write buffer. A thread sees its writes+  -- immediately, but other threads will only see writes when they are+  -- committed, which may happen later. Writes to different 'CRef's+  -- are not necessarily committed in the same order that they are+  -- created.+  deriving (Eq, Show, Read, Ord, Enum, Bounded)++instance NFData MemType where+  rnf m = m `seq` ()++-------------------------------------------------------------------------------+-- Utilities++-- | Helper for @next*@+nextId :: String -> [String] -> (Maybe String, [String])+nextId name used = (newName, newUsed) where+  newName+    | null name = Nothing+    | occurrences > 0 = Just (name ++ "-" ++ show occurrences)+    | otherwise = Just name+  newUsed+    | null name = used+    | otherwise = name : used+  occurrences = length (filter (==name) used)

@@ -0,0 +1,200 @@+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE RankNTypes                 #-}+{-# LANGUAGE TypeFamilies               #-}+{-# LANGUAGE TypeSynonymInstances       #-}++-- |+-- Module      : Test.DejaFu.Conc+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : experimental+-- Portability : FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, RankNTypes, TypeFamilies, TypeSynonymInstances+--+-- Deterministic traced execution of concurrent computations.+--+-- This works by executing the computation on a single thread, calling+-- out to the supplied scheduler after each step to determine which+-- thread runs next.+module Test.DejaFu.Conc+  ( -- * The @Conc@ Monad+    Conc+  , ConcST+  , ConcIO++  -- * Executing computations+  , Failure(..)+  , MemType(..)+  , runConcurrent++  -- * Execution traces+  , Trace+  , Decision(..)+  , ThreadId(..)+  , ThreadAction(..)+  , Lookahead(..)+  , MVarId+  , CRefId+  , MaskingState(..)+  , showTrace+  , showFail++  -- * Scheduling+  , module Test.DPOR.Schedule+  ) where++import Control.Exception (MaskingState(..))+import qualified Control.Monad.Base as Ba+import qualified Control.Monad.Catch as Ca+import qualified Control.Monad.IO.Class as IO+import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef)+import Control.Monad.ST (ST)+import Data.Dynamic (toDyn)+import Data.IORef (IORef)+import qualified Data.Map.Strict as M+import Data.Maybe (fromJust)+import Data.STRef (STRef)+import Test.DPOR.Schedule++import qualified Control.Monad.Conc.Class as C+import Test.DejaFu.Common+import Test.DejaFu.Conc.Internal+import Test.DejaFu.Conc.Internal.Common+import Test.DejaFu.Conc.Internal.Threading+import Test.DejaFu.STM++{-# ANN module ("HLint: ignore Avoid lambda" :: String) #-}+{-# ANN module ("HLint: ignore Use const"    :: String) #-}++newtype Conc n r a = C { unC :: M n r (STMLike n r) a } deriving (Functor, Applicative, Monad)++-- | A 'MonadConc' implementation using @ST@, this should be preferred+-- if you do not need 'liftIO'.+type ConcST t = Conc (ST t) (STRef t)++-- | A 'MonadConc' implementation using @IO@.+type ConcIO = Conc IO IORef++toConc :: ((a -> Action n r (STMLike n r)) -> Action n r (STMLike n r)) -> Conc n r a+toConc = C . cont++wrap :: (M n r (STMLike n r) a -> M n r (STMLike n r) a) -> Conc n r a -> Conc n r a+wrap f = C . f . unC++instance IO.MonadIO ConcIO where+  liftIO ma = toConc (\c -> ALift (fmap c ma))++instance Ba.MonadBase IO ConcIO where+  liftBase = IO.liftIO++instance Ca.MonadCatch (Conc n r) where+  catch ma h = toConc (ACatching (unC . h) (unC ma))++instance Ca.MonadThrow (Conc n r) where+  throwM e = toConc (\_ -> AThrow e)++instance Ca.MonadMask (Conc n r) where+  mask                mb = toConc (AMasking MaskedInterruptible   (\f -> unC $ mb $ wrap f))+  uninterruptibleMask mb = toConc (AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f))++instance Monad n => C.MonadConc (Conc n r) where+  type MVar     (Conc n r) = MVar r+  type CRef     (Conc n r) = CRef r+  type Ticket   (Conc n r) = Ticket+  type STM      (Conc n r) = STMLike n r+  type ThreadId (Conc n r) = ThreadId++  -- ----------++  forkWithUnmaskN   n ma = toConc (AFork n (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop (pure ()))))+  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,+  -- so it seems a sane choice.+  getNumCapabilities      = toConc AGetNumCapabilities+  setNumCapabilities caps = toConc (\c -> ASetNumCapabilities caps (c ()))++  myThreadId = toConc AMyTId++  yield = toConc (\c -> AYield (c ()))++  -- ----------++  newCRefN n a = toConc (\c -> ANewRef n a c)++  readCRef   ref = toConc (AReadRef    ref)+  readForCAS ref = toConc (AReadRefCas ref)++  peekTicket' _ = _ticketVal++  writeCRef ref      a = toConc (\c -> AWriteRef ref a (c ()))+  casCRef   ref tick a = toConc (ACasRef ref tick a)++  atomicModifyCRef ref f = toConc (AModRef    ref f)+  modifyCRefCAS    ref f = toConc (AModRefCas ref f)++  -- ----------++  newEmptyMVarN n = toConc (\c -> ANewVar n c)++  putMVar  var a = toConc (\c -> APutVar var a (c ()))+  readMVar var   = toConc (AReadVar var)+  takeMVar var   = toConc (ATakeVar var)++  tryPutMVar  var a = toConc (ATryPutVar  var a)+  tryTakeMVar var   = toConc (ATryTakeVar var)++  -- ----------++  throwTo tid e = toConc (\c -> AThrowTo tid e (c ()))++  -- ----------++  atomically = toConc . AAtom++  -- ----------++  _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.+--+-- __Warning:__ Blocking on the action of another thread in 'liftIO'+-- cannot be detected! So if you perform some potentially blocking+-- action in a 'liftIO' the entire collection of threads may deadlock!+-- You should therefore keep @IO@ blocks small, and only perform+-- blocking operations with the supplied primitives, insofar as+-- possible.+--+-- __Note:__ In order to prevent computation from hanging, the runtime+-- will assume that a deadlock situation has arisen if the scheduler+-- attempts to (a) schedule a blocked thread, or (b) schedule a+-- nonexistent thread. In either of those cases, the computation will+-- be halted.+runConcurrent :: MonadRef r n+              => Scheduler ThreadId ThreadAction Lookahead s+              -> MemType+              -> s+              -> Conc n r a+              -> n (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)+runConcurrent sched memtype s (C conc) = do+  ref <- newRef Nothing++  let c = runCont conc (AStop . writeRef ref . Just . Right)+  let threads = launch' Unmasked initialThread (const c) M.empty++  (s', trace) <- runThreads runTransaction+                           sched+                           memtype+                           s+                           threads+                           initialIdSource+                           ref++  out <- readRef ref++  pure (fromJust out, s', reverse trace)

@@ -0,0 +1,385 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- |+-- Module      : Test.DejaFu.Conc.Internal+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : experimental+-- Portability : RankNTypes, ScopedTypeVariables+--+-- Concurrent monads with a fixed scheduler: internal types and+-- functions. This module is NOT considered to form part of the public+-- interface of this library.+module Test.DejaFu.Conc.Internal where++import Control.Exception (MaskingState(..), toException)+import Control.Monad.Ref (MonadRef, newRef, writeRef)+import Data.Functor (void)+import Data.List (sort)+import Data.List.NonEmpty (NonEmpty(..), fromList)+import qualified Data.Map.Strict as M+import Data.Maybe (fromJust, isJust, isNothing, listToMaybe)+import Test.DPOR (Scheduler)++import Test.DejaFu.Common+import Test.DejaFu.Conc.Internal.Common+import Test.DejaFu.Conc.Internal.Memory+import Test.DejaFu.Conc.Internal.Threading+import Test.DejaFu.STM (Result(..))++{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}+{-# ANN module ("HLint: ignore Use const"           :: String) #-}++--------------------------------------------------------------------------------+-- * Execution++-- | Run a collection of threads, until there are no threads left.+--+-- Note: this returns the trace in reverse order, because it's more+-- efficient to prepend to a list than append. As this function isn't+-- exposed to users of the library, this is just an internal gotcha to+-- watch out for.+runThreads :: MonadRef r n => (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, Trace ThreadId ThreadAction Lookahead)+runThreads 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+    | isDeadlocked  = die g Deadlock+    | isSTMLocked   = die g STMDeadlock+    | isAborted     = die g' Abort+    | isNonexistant = die g' InternalError+    | isBlocked     = die g' InternalError+    | otherwise = do+      stepped <- stepThread runstm memtype (_continuation $ fromJust thread) idSource chosen threads wb caps+      case stepped of+        Right (threads', idSource', act, wb', caps') -> loop threads' idSource' act wb' caps'++        Left UncaughtException+          | chosen == initialThread -> die g' UncaughtException+          | otherwise -> loop (kill chosen threads) idSource Killed wb caps++        Left failure -> die g' failure++    where+      (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+      thread        = M.lookup chosen threadsc+      threadsc      = addCommitThreads wb threads+      isAborted     = isNothing choice+      isBlocked     = isJust . _blocking $ fromJust thread+      isNonexistant = isNothing thread+      isTerminated  = initialThread `notElem` M.keys threads+      isDeadlocked  = M.null (M.filter (isNothing . _blocking) 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 = M.null (M.filter (isNothing . _blocking) threads) &&+        ((~=  OnTVar []) <$> M.lookup initialThread threads) == Just True++      unblockWaitingOn tid = fmap unblock where+        unblock thrd = case _blocking thrd of+          Just (OnMask t) | t == tid -> thrd { _blocking = Nothing }+          _ -> thrd++      decision+        | Just chosen == prior = Continue+        | prior `notElem` map (Just . fst) runnable' = Start chosen+        | otherwise = SwitchTo chosen++      nextActions t = lookahead . _continuation . fromJust $ M.lookup t threadsc++      stop outg = pure (outg, sofar)+      die  outg reason = writeRef ref (Just $ Left reason) >> stop outg++      loop threads' idSource' act wb' =+        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'++--------------------------------------------------------------------------------+-- * Single-step execution++-- | Run a single thread one step, by dispatching on the type of+-- 'Action'.+stepThread :: forall n r s. MonadRef r n+  => (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))+  -- ^ Run a 'MonadSTM' transaction atomically.+  -> MemType+  -- ^ The memory model+  -> Action n r s+  -- ^ Action to step+  -> IdSource+  -- ^ Source of fresh IDs+  -> ThreadId+  -- ^ ID of the current thread+  -> Threads n r s+  -- ^ Current state of threads+  -> WriteBuffer r+  -- ^ @CRef@ write buffer+  -> Int+  -- ^ The number of capabilities+  -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))+stepThread runstm memtype action idSource tid threads wb caps = case action of+  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  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  n a c   -> stepNewRef      n a c+  AReadRef ref c   -> stepReadRef     ref c+  AReadRefCas ref c -> stepReadRefCas ref c+  AModRef  ref f c -> stepModRef      ref f c+  AModRefCas ref f c -> stepModRefCas ref f c+  AWriteRef ref a c -> stepWriteRef   ref a c+  ACasRef ref tick a c -> stepCasRef ref tick a c+  ACommit  t c     -> stepCommit      t c+  AAtom    stm c   -> stepAtom        stm c+  ALift    na      -> stepLift        na+  AThrow   e       -> stepThrow       e+  AThrowTo t e c   -> stepThrowTo     t e c+  ACatching h ma c -> stepCatching    h ma c+  APopCatching a   -> stepPopCatching a+  AMasking m ma c  -> stepMasking     m ma c+  AResetMask b1 b2 m c -> stepResetMask b1 b2 m c+  AReturn     c    -> stepReturn c+  AMessage    m c  -> stepMessage m c+  AStop       na   -> stepStop na++  where+    -- | Start a new thread, assigning it the next 'ThreadId'+    --+    -- Explicit type signature needed for GHC 8. Looks like the+    -- impredicative polymorphism checks got stronger.+    stepFork :: String+             -> ((forall b. M n r s b -> M n r s b) -> Action n r s)+             -> (ThreadId -> Action n r s)+             -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))+    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 n idSource++    -- | Get the 'ThreadId' of the current thread+    stepMyTId c = simple (goto (c tid) tid threads) MyThreadId++    -- | Get the number of capabilities+    stepGetNumCapabilities c = simple (goto (c caps) tid threads) $ GetNumCapabilities caps++    -- | Set the number of capabilities+    stepSetNumCapabilities i c = return $ Right (goto c tid threads, idSource, SetNumCapabilities i, wb, i)++    -- | Yield the current thread+    stepYield c = simple (goto c tid threads) Yield++    -- | Put a value into a @MVar@, blocking the thread until it's+    -- empty.+    stepPutVar cvar@(MVar cvid _) a c = synchronised $ do+      (success, threads', woken) <- putIntoMVar cvar a c tid threads+      simple threads' $ if success then PutVar cvid woken else BlockedPutVar cvid++    -- | 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 tid threads+      simple threads' $ TryPutVar cvid success woken++    -- | Get the value from a @MVar@, without emptying, blocking the+    -- thread until it's full.+    stepReadVar cvar@(MVar cvid _) c = synchronised $ do+      (success, threads', _) <- readFromMVar cvar c tid threads+      simple threads' $ if success then ReadVar cvid else BlockedReadVar cvid++    -- | Take the value from a @MVar@, blocking the thread until it's+    -- full.+    stepTakeVar cvar@(MVar cvid _) c = synchronised $ do+      (success, threads', woken) <- takeFromMVar cvar c tid threads+      simple threads' $ if success then TakeVar cvid woken else BlockedTakeVar cvid++    -- | Try to take the value from a @MVar@, without blocking.+    stepTryTakeVar cvar@(MVar cvid _) c = synchronised $ do+      (success, threads', woken) <- tryTakeFromMVar cvar c tid threads+      simple threads' $ TryTakeVar cvid success woken++    -- | Read from a @CRef@.+    stepReadRef cref@(CRef crid _) c = do+      val <- readCRef 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+      tick <- readForTicket cref tid+      simple (goto (c tick) tid threads) $ ReadRefCas crid++    -- | Modify a @CRef@.+    stepModRef cref@(CRef crid _) f c = synchronised $ do+      (new, val) <- f <$> readCRef cref tid+      writeImmediate 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 cref tid+      let (new, val) = f old+      void $ casCRef 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+      -- Write immediately.+      SequentialConsistency -> do+        writeImmediate cref a+        simple (goto c tid threads) $ WriteRef crid++      -- Add to buffer using thread id.+      TotalStoreOrder -> do+        wb' <- bufferWrite wb (tid, Nothing) cref a+        return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps)++      -- Add to buffer using both thread id and cref id+      PartialStoreOrder -> do+        wb' <- bufferWrite 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+      (suc, tick') <- casCRef cref tid tick a+      simple (goto (c (suc, tick')) tid threads) $ CasRef crid suc++    -- | Commit a @CRef@ write+    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 wb (t, Nothing)++        -- Commit using the cref id.+        PartialStoreOrder -> commitWrite wb (t, Just c)++      return $ Right (threads, idSource, CommitRef t c, wb', caps)++    -- | Run a STM transaction atomically.+    stepAtom stm c = synchronised $ do+      (res, idSource', trace) <- runstm stm idSource+      case res of+        Success _ written val ->+          let (threads', woken) = wake (OnTVar written) threads+          in return $ Right (goto (c val) tid threads', idSource', STM trace woken, wb, caps)+        Retry touched ->+          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+      a     = runCont ma      (APopCatching . c)+      e exc = runCont (h exc) (APopCatching . c)++      threads' = goto a tid (catching e tid threads)++    -- | Pop the top exception handler from the thread's stack.+    stepPopCatching a = simple threads' PopCatching where+      threads' = goto a tid (uncatching tid threads)++    -- | Throw an exception, and propagate it to the appropriate+    -- handler.+    stepThrow e =+      case propagate (toException e) tid threads of+        Just threads' -> simple threads' Throw+        Nothing -> return $ Left UncaughtException++    -- | Throw an exception to the target thread, and propagate it to+    -- the appropriate handler.+    stepThrowTo t e c = synchronised $+      let threads' = goto c tid threads+          blocked  = block (OnMask t) tid threads+      in case M.lookup t threads of+           Just thread+             | interruptible thread -> case propagate (toException e) t threads' of+               Just threads'' -> simple threads'' $ ThrowTo t+               Nothing+                 | t == initialThread -> return $ Left UncaughtException+                 | otherwise -> simple (kill t threads') $ ThrowTo t+             | otherwise -> simple blocked $ BlockedThrowTo t+           Nothing -> simple threads' $ ThrowTo t++    -- | Execute a subcomputation with a new masking state, and give+    -- it a function to run a computation with the current masking+    -- state.+    --+    -- Explicit type sig necessary for checking in the prescence of+    -- 'umask', sadly.+    stepMasking :: MaskingState+                -> ((forall b. M n r s b -> M n r s b) -> M n r s a)+                -> (a -> Action n r s)+                -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))+    stepMasking m ma c = simple threads' $ SetMasking False m where+      a = runCont (ma umask) (AResetMask False False m' . c)++      m' = _masking . fromJust $ M.lookup tid threads+      umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> return b+      resetMask typ ms = cont $ \k -> AResetMask typ True ms $ k ()++      threads' = goto a tid (mask m tid threads)++    -- | Reset the masking thread of the state.+    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 @MVar@, using the next 'MVarId'.+    stepNewVar n c = do+      let (idSource', newmvid) = nextMVId n idSource+      ref <- newRef Nothing+      let mvar = MVar newmvid ref+      return $ Right (goto (c mvar) tid threads, idSource', NewVar newmvid, wb, caps)++    -- | Create a new @CRef@, using the next 'CRefId'.+    stepNewRef n a c = do+      let (idSource', newcrid) = nextCRId n idSource+      ref <- newRef (M.empty, 0, a)+      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@+    -- computation.+    stepLift na = do+      a <- na+      simple (goto a tid threads) LiftIO++    -- | Execute a 'return' or 'pure'.+    stepReturn c = simple (goto c tid threads) Return++    -- | Add a message to the trace.+    stepMessage m c = simple (goto c tid threads) (Message m)++    -- | Kill the current thread.+    stepStop na = na >> simple (kill tid threads) Stop++    -- | Helper for actions which don't touch the 'IdSource' or+    -- 'WriteBuffer'+    simple threads' act = return $ Right (threads', idSource, act, wb, caps)++    -- | Helper for actions impose a write barrier.+    synchronised ma = do+      writeBarrier wb+      res <- ma++      return $ case res of+        Right (threads', idSource', act', _, caps') -> Right (threads', idSource', act', emptyBuffer, caps')+        _ -> res

@@ -0,0 +1,172 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE RankNTypes                #-}++-- |+-- Module      : Test.DejaFu.Conc.Internal.Common+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : experimental+-- Portability : ExistentialQuantification, RankNTypes+--+-- Common types and utility functions for deterministic execution of+-- 'MonadConc' implementations. This module is NOT considered to form+module Test.DejaFu.Conc.Internal.Common where++import Control.Exception (Exception, MaskingState(..))+import Data.Dynamic (Dynamic)+import Data.Map.Strict (Map)+import Data.List.NonEmpty (NonEmpty, fromList)+import Test.DejaFu.Common++{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}++--------------------------------------------------------------------------------+-- * The @Conc@ Monad++-- | 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+-- @AStop@ actions having their parameter. 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+    fmap f m = M $ \ c -> runM m (c . f)++instance Applicative (M n r s) where+    pure x  = M $ \c -> AReturn $ c x+    f <*> v = M $ \c -> runM f (\g -> runM v (c . g))++instance Monad (M n r s) where+    return  = pure+    m >>= k = M $ \c -> runM m (\x -> runM (k x) c)++-- | 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 @MVar@+-- wakes up all threads blocked on reading it, and it is up to the+-- scheduler which one runs next. Taking from a @MVar@ behaves+-- analogously.+data MVar r a = MVar+  { _cvarId   :: MVarId+  , _cvarVal  :: r (Maybe a)+  }++-- | The mutable non-blocking reference type. These are like 'IORef's.+--+-- @CRef@s are represented as a unique numeric identifier and a+-- reference containing (a) any thread-local non-synchronised writes+-- (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.+data CRef r a = CRef+  { _crefId   :: CRefId+  , _crefVal  :: r (Map ThreadId a, Integer, a)+  }++-- | The compare-and-swap proof type.+--+-- @Ticket@s are represented as just a wrapper around the identifier+-- of the 'CRef' it came from, the commit count at the time it was+-- 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.+data Ticket a = Ticket+  { _ticketCRef   :: CRefId+  , _ticketWrites :: Integer+  , _ticketVal    :: a+  }++-- | Construct a continuation-passing operation from a function.+cont :: ((a -> Action n r s) -> Action n r s) -> M n r s a+cont = M++-- | Run a CPS computation with the given final computation.+runCont :: M n r s a -> (a -> Action n r s) -> Action n r s+runCont = runM++--------------------------------------------------------------------------------+-- * Primitive Actions++-- | Scheduling is done in terms of a trace of 'Action's. Blocking can+-- only occur as a result of an action, and they cover (most of) the+-- primitives of the concurrency. 'spawn' is absent as it is+-- implemented in terms of 'newEmptyMVar', 'fork', and 'putMVar'.+data 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 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 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 b. AModRef     (CRef r a) (a -> (a, b)) (b -> Action n r s)+  | forall a b. AModRefCas  (CRef r a) (a -> (a, b)) (b -> Action n r s)+  | forall a.   AWriteRef   (CRef r a) a (Action n r s)+  | forall a.   ACasRef     (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r s)++  | forall e.   Exception e => AThrow e+  | forall e.   Exception e => AThrowTo ThreadId e (Action n r s)+  | forall a e. Exception e => ACatching (e -> M n r s a) (M n r s a) (a -> Action n r s)+  | APopCatching (Action n r s)+  | forall a. AMasking MaskingState ((forall b. M n r s b -> M n r s b) -> M n r s a) (a -> Action n r s)+  | AResetMask Bool Bool MaskingState (Action n r s)++  | AMessage    Dynamic (Action n r s)++  | forall a. AAtom (s a) (a -> Action n r s)+  | ALift (n (Action n r s))+  | AYield  (Action n r s)+  | AReturn (Action n r s)+  | ACommit ThreadId CRefId+  | AStop (n ())++--------------------------------------------------------------------------------+-- * Scheduling & Traces++-- | Look as far ahead in the given continuation as possible.+lookahead :: Action n r s -> NonEmpty Lookahead+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 (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' (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]+  lookahead' (AThrowTo tid _ k)      = WillThrowTo tid : lookahead' k+  lookahead' (ACatching _ _ _)       = [WillCatching]+  lookahead' (APopCatching k)        = WillPopCatching : lookahead' k+  lookahead' (AMasking ms _ _)       = [WillSetMasking False ms]+  lookahead' (AResetMask b1 b2 ms k) = (if b1 then WillSetMasking else WillResetMasking) b2 ms : lookahead' k+  lookahead' (ALift _)               = [WillLiftIO]+  lookahead' (AMessage m k)          = WillMessage m : lookahead' k+  lookahead' (AYield k)              = WillYield : lookahead' k+  lookahead' (AReturn k)             = WillReturn : lookahead' k+  lookahead' (AStop _)               = [WillStop]

@@ -0,0 +1,211 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE GADTs        #-}+{-# LANGUAGE MultiParamTypeClasses #-}++-- |+-- Module      : Test.DejaFu.Conc.Internal.Memory+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : experimental+-- Portability : BangPatterns, GADTs+--+-- Operations over @CRef@s and @MVar@s. This module is NOT considered+-- to form part of the public interface of this library.+--+-- 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.Conc.Internal.Memory where++import Control.Monad (when)+import Control.Monad.Ref (MonadRef, readRef, writeRef)+import Data.Map.Strict (Map)+import Data.Maybe (isJust, fromJust)+import Data.Monoid ((<>))+import Data.Sequence (Seq, ViewL(..), (><), singleton, viewl)++import Test.DejaFu.Common+import Test.DejaFu.Conc.Internal.Common+import Test.DejaFu.Conc.Internal.Threading++import qualified Data.Map.Strict as M++--------------------------------------------------------------------------------+-- * Manipulating @CRef@s++-- | In non-sequentially-consistent memory models, non-synchronised+-- writes get buffered.+--+-- 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+-- thing which can be done with it is to write it to the reference.+data BufferedWrite r where+  BufferedWrite :: ThreadId -> CRef r a -> a -> BufferedWrite r++-- | An empty write buffer.+emptyBuffer :: WriteBuffer r+emptyBuffer = WriteBuffer M.empty++-- | Add a new write to the end of a buffer.+bufferWrite :: MonadRef r n => WriteBuffer r -> (ThreadId, Maybe CRefId) -> CRef r a -> a -> n (WriteBuffer r)+bufferWrite (WriteBuffer wb) k@(tid, _) cref@(CRef _ ref) new = do+  -- Construct the new write buffer+  let write = singleton $ BufferedWrite tid cref new+  let buffer' = M.insertWith (flip (><)) k write wb++  -- Write the thread-local value to the @CRef@'s update map.+  (locals, count, def) <- readRef ref+  writeRef ref (M.insert tid new locals, count, def)++  return $ WriteBuffer buffer'++-- | Commit the write at the head of a buffer.+commitWrite :: MonadRef r n => WriteBuffer r -> (ThreadId, Maybe CRefId) -> n (WriteBuffer r)+commitWrite w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of+  BufferedWrite _ cref a :< rest -> do+    writeImmediate cref a+    return . WriteBuffer $ M.insert k rest wb++  EmptyL -> return w++-- | Read from a @CRef@, returning a newer thread-local non-committed+-- write if there is one.+readCRef :: MonadRef r n => CRef r a -> ThreadId -> n a+readCRef cref tid = do+  (val, _) <- readCRefPrim cref tid+  return val++-- | Read from a @CRef@, returning a @Ticket@ representing the current+-- view of the thread.+readForTicket :: MonadRef r n => CRef r a -> ThreadId -> n (Ticket a)+readForTicket cref@(CRef crid _) tid = do+  (val, count) <- readCRefPrim cref tid+  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 :: MonadRef r n => CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a)+casCRef cref tid (Ticket _ cc _) !new = do+  tick'@(Ticket _ cc' _) <- readForTicket cref tid++  if cc == cc'+  then do+    writeImmediate cref new+    tick'' <- readForTicket cref tid+    return (True, tick'')+  else return (False, tick')++-- | Read the local state of a @CRef@.+readCRefPrim :: MonadRef r n => CRef r a -> ThreadId -> n (a, Integer)+readCRefPrim (CRef _ ref) tid = do+  (vals, count, def) <- readRef ref++  return (M.findWithDefault def tid vals, count)++-- | Write and commit to a @CRef@ immediately, clearing the update map+-- and incrementing the write count.+writeImmediate :: MonadRef r n => CRef r a -> a -> n ()+writeImmediate (CRef _ ref) a = do+  (_, count, _) <- readRef ref+  writeRef ref (M.empty, count + 1, a)++-- | Flush all writes in the buffer.+writeBarrier :: MonadRef r n => WriteBuffer r -> n ()+writeBarrier (WriteBuffer wb) = mapM_ flush $ M.elems wb where+  flush = mapM_ $ \(BufferedWrite _ cref a) -> writeImmediate 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 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 >= initialThread++--------------------------------------------------------------------------------+-- * Manipulating @MVar@s++-- | Put into a @MVar@, blocking if full.+putIntoMVar :: MonadRef r n => MVar r a -> a -> Action n r s+            -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+putIntoMVar cvar a c = mutMVar True cvar a (const c)++-- | Try to put into a @MVar@, not blocking if full.+tryPutIntoMVar :: MonadRef r n => MVar r a -> a -> (Bool -> Action n r s)+               -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+tryPutIntoMVar = mutMVar False++-- | Read from a @MVar@, blocking if empty.+readFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r s)+            -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+readFromMVar cvar c = seeMVar False True cvar (c . fromJust)++-- | Take from a @MVar@, blocking if empty.+takeFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r s)+             -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+takeFromMVar cvar c = seeMVar True True cvar (c . fromJust)++-- | Try to take from a @MVar@, not blocking if empty.+tryTakeFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r s)+                -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+tryTakeFromMVar = seeMVar True False++-- | Mutate a @MVar@, in either a blocking or nonblocking way.+mutMVar :: MonadRef r n+        => Bool -> MVar r a -> a -> (Bool -> Action n r s)+        -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+mutMVar blocking (MVar cvid ref) a c threadid threads = do+  val <- readRef ref++  case val of+    Just _+      | blocking ->+        let threads' = block (OnMVarEmpty cvid) threadid threads+        in return (False, threads', [])++      | otherwise ->+        return (False, goto (c False) threadid threads, [])++    Nothing -> do+      writeRef ref $ Just a+      let (threads', woken) = wake (OnMVarFull cvid) threads+      return (True, goto (c True) threadid threads', woken)++-- | Read a @MVar@, in either a blocking or nonblocking+-- way.+seeMVar :: MonadRef r n+        => Bool -> Bool -> MVar r a -> (Maybe a -> Action n r s)+        -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+seeMVar emptying blocking (MVar cvid ref) c threadid threads = do+  val <- readRef ref++  case val of+    Just _ -> do+      when emptying $ writeRef ref Nothing+      let (threads', woken) = wake (OnMVarEmpty cvid) threads+      return (True, goto (c val) threadid threads', woken)++    Nothing+      | blocking ->+        let threads' = block (OnMVarFull cvid) threadid threads+        in return (False, threads', [])++      | otherwise ->+        return (False, goto (c Nothing) threadid threads, [])

@@ -0,0 +1,143 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE RankNTypes                #-}++-- |+-- Module      : Test.DejaFu.Conc.Internal.Threading+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : experimental+-- Portability : ExistentialQuantification, RankNTypes+--+-- Operations and types for threads. This module is NOT considered to+-- form part of the public interface of this library.+module Test.DejaFu.Conc.Internal.Threading where++import Control.Exception (Exception, MaskingState(..), SomeException, fromException)+import Data.List (intersect)+import Data.Map.Strict (Map)+import Data.Maybe (fromMaybe, isJust)++import Test.DejaFu.Common+import Test.DejaFu.Conc.Internal.Common++import qualified Data.Map.Strict as M++--------------------------------------------------------------------------------+-- * Threads++-- | Threads are stored in a map index by 'ThreadId'.+type Threads n r s = Map ThreadId (Thread n r s)++-- | All the state of a thread.+data Thread n r s = Thread+  { _continuation :: Action n r s+  -- ^ The next action to execute.+  , _blocking     :: Maybe BlockedOn+  -- ^ The state of any blocks.+  , _handlers     :: [Handler n r s]+  -- ^ Stack of exception handlers+  , _masking      :: MaskingState+  -- ^ The exception masking state.+  }++-- | Construct a thread with just one action+mkthread :: Action n r s -> Thread n r s+mkthread c = Thread c Nothing [] Unmasked++--------------------------------------------------------------------------------+-- * Blocking++-- | A @BlockedOn@ is used to determine what sort of variable a thread+-- is blocked on.+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 (OnMVarFull  _), OnMVarFull  _) -> True+  (Just (OnMVarEmpty _), OnMVarEmpty _) -> True+  (Just (OnTVar      _), OnTVar      _) -> True+  (Just (OnMask      _), OnMask      _) -> True+  _ -> False++--------------------------------------------------------------------------------+-- * Exceptions++-- | An exception handler.+data Handler n r s = forall e. Exception e => Handler (e -> Action n r s)++-- | Propagate an exception upwards, finding the closest handler+-- which can deal with it.+propagate :: SomeException -> ThreadId -> Threads n r s -> Maybe (Threads n r s)+propagate e tid threads = case M.lookup tid threads >>= go . _handlers of+  Just (act, hs) -> Just $ except act hs tid threads+  Nothing -> Nothing++  where+    go [] = Nothing+    go (Handler h:hs) = maybe (go hs) (\act -> Just (act, hs)) $ h <$> fromException e++-- | Check if a thread can be interrupted by an exception.+interruptible :: Thread n r s -> Bool+interruptible thread = _masking thread == Unmasked || (_masking thread == MaskedInterruptible && isJust (_blocking thread))++-- | Register a new exception handler.+catching :: Exception e => (e -> Action n r s) -> ThreadId -> Threads n r s -> Threads n r s+catching h = M.alter $ \(Just thread) -> Just $ thread { _handlers = Handler h : _handlers thread }++-- | Remove the most recent exception handler.+uncatching :: ThreadId -> Threads n r s -> Threads n r s+uncatching = M.alter $ \(Just thread) -> Just $ thread { _handlers = tail $ _handlers thread }++-- | Raise an exception in a thread.+except :: Action n r s -> [Handler n r s] -> ThreadId -> Threads n r s -> Threads n r s+except act hs = M.alter $ \(Just thread) -> Just $ thread { _continuation = act, _handlers = hs, _blocking = Nothing }++-- | Set the masking state of a thread.+mask :: MaskingState -> ThreadId -> Threads n r s -> Threads n r s+mask ms = M.alter $ \(Just thread) -> Just $ thread { _masking = ms }++--------------------------------------------------------------------------------+-- * Manipulating threads++-- | Replace the @Action@ of a thread.+goto :: Action n r s -> ThreadId -> Threads n r s -> Threads n r s+goto a = M.alter $ \(Just thread) -> Just (thread { _continuation = a })++-- | Start a thread with the given ID, inheriting the masking state+-- from the parent thread. This ID must not already be in use!+launch :: ThreadId -> ThreadId -> ((forall b. M n r s b -> M n r s b) -> Action n r s) -> Threads n r s -> Threads n r s+launch parent tid a threads = launch' 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' ms tid a = M.insert tid thread where+  thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = ms }++  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.+kill :: ThreadId -> Threads n r s -> Threads n r s+kill = M.delete++-- | Block a thread.+block :: BlockedOn -> ThreadId -> Threads n r s -> Threads n r s+block blockedOn = M.alter doBlock where+  doBlock (Just thread) = Just $ thread { _blocking = Just blockedOn }+  doBlock _ = error "Invariant failure in 'block': thread does NOT exist!"++-- | Unblock all threads waiting on the appropriate block. For 'TVar'+-- blocks, this will wake all threads waiting on at least one of the+-- 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+    | isBlocked thread = thread { _blocking = Nothing }+    | otherwise = thread++  isBlocked thread = case (_blocking thread, blockedOn) of+    (Just (OnTVar tvids), OnTVar blockedOn') -> tvids `intersect` blockedOn' /= []+    (theblock, _) -> theblock == Just blockedOn

@@ -1,209 +0,0 @@-{-# LANGUAGE FlexibleInstances          #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE MultiParamTypeClasses      #-}-{-# LANGUAGE RankNTypes                 #-}-{-# LANGUAGE TypeFamilies               #-}-{-# LANGUAGE TypeSynonymInstances       #-}---- |--- Module      : Test.DejaFu.Deterministic--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : experimental--- Portability : FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, RankNTypes, TypeFamilies, TypeSynonymInstances------ Deterministic traced execution of concurrent computations.------ This works by executing the computation on a single thread, calling--- out to the supplied scheduler after each step to determine which--- thread runs next.-module Test.DejaFu.Deterministic-  ( -- * The @Conc@ Monad-    Conc-  , ConcST-  , ConcIO--  -- * Executing computations-  , Failure(..)-  , MemType(..)-  , runConcST-  , runConcIO--  -- * Execution traces-  , Trace-  , Decision(..)-  , ThreadId(..)-  , ThreadAction(..)-  , Lookahead(..)-  , MVarId-  , CRefId-  , MaskingState(..)-  , showTrace-  , showFail--  -- * Scheduling-  , 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.Internal (refST, refIO)-import Test.DejaFu.STM (STMLike, STMIO, STMST, runTransactionIO, runTransactionST)-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--{-# ANN module ("HLint: ignore Avoid lambda" :: String) #-}-{-# ANN module ("HLint: ignore Use const"    :: String) #-}--newtype Conc n r s a = C { unC :: M n r s a } deriving (Functor, Applicative, Monad)---- | A 'MonadConc' implementation using @ST@, this should be preferred--- if you do not need 'liftIO'.-type ConcST t = Conc (ST t) (STRef t) (STMST t)---- | A 'MonadConc' implementation using @IO@.-type ConcIO = Conc IO IORef STMIO--toConc :: ((a -> Action n r s) -> Action n r s) -> Conc n r s a-toConc = C . cont--wrap :: (M n r s a -> M n r s a) -> Conc n r s a -> Conc n r s a-wrap f = C . f . unC--instance IO.MonadIO ConcIO where-  liftIO ma = toConc (\c -> ALift (fmap c ma))--instance Ba.MonadBase IO ConcIO where-  liftBase = IO.liftIO--instance Ca.MonadCatch (Conc n r s) where-  catch ma h = toConc (ACatching (unC . h) (unC ma))--instance Ca.MonadThrow (Conc n r s) where-  throwM e = toConc (\_ -> AThrow e)--instance Ca.MonadMask (Conc n r s) where-  mask                mb = toConc (AMasking MaskedInterruptible   (\f -> unC $ mb $ wrap f))-  uninterruptibleMask mb = toConc (AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f))--instance Monad n => C.MonadConc (Conc n r (STMLike n r)) where-  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 STM      (Conc n r (STMLike n r)) = STMLike n r-  type ThreadId (Conc n r (STMLike n r)) = ThreadId--  -- ------------  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,-  -- so it seems a sane choice.-  getNumCapabilities      = toConc AGetNumCapabilities-  setNumCapabilities caps = toConc (\c -> ASetNumCapabilities caps (c ()))--  myThreadId = toConc AMyTId--  yield = toConc (\c -> AYield (c ()))--  -- ------------  newCRefN n a = toConc (\c -> ANewRef n a c)--  readCRef   ref = toConc (AReadRef    ref)-  readForCAS ref = toConc (AReadRefCas ref)--  peekTicket tick = toConc (APeekTicket tick)--  writeCRef ref      a = toConc (\c -> AWriteRef ref a (c ()))-  casCRef   ref tick a = toConc (ACasRef ref tick a)--  atomicModifyCRef ref f = toConc (AModRef    ref f)-  modifyCRefCAS    ref f = toConc (AModRefCas ref f)--  -- ------------  newEmptyMVarN n = toConc (\c -> ANewVar n c)--  putMVar  var a = toConc (\c -> APutVar var a (c ()))-  readMVar var   = toConc (AReadVar var)-  takeMVar var   = toConc (ATakeVar var)--  tryPutMVar  var a = toConc (ATryPutVar  var a)-  tryTakeMVar var   = toConc (ATryTakeVar var)--  -- ------------  throwTo tid e = toConc (\c -> AThrowTo tid e (c ()))--  -- ------------  atomically = toConc . AAtom--  -- ------------  _concKnowsAbout (Left  (MVar cvarid  _)) = toConc (\c -> AKnowsAbout (Left  cvarid)  (c ()))-  _concKnowsAbout (Right (TVar (ctvarid, _))) = toConc (\c -> AKnowsAbout (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.------ 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 () 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>------ __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--- 'Scheduler' and initial state, returning a failure reason on--- error. Also returned is the final state of the scheduler, and an--- execution trace.------ __Warning:__ Blocking on the action of another thread in 'liftIO'--- cannot be detected! So if you perform some potentially blocking--- action in a 'liftIO' the entire collection of threads may deadlock!--- You should therefore keep @IO@ blocks small, and only perform--- blocking operations with the supplied primitives, insofar as--- possible.------ __Note:__ In order to prevent computation from hanging, the runtime--- will assume that a deadlock situation has arisen if the scheduler--- attempts to (a) schedule a blocked thread, or (b) schedule a--- nonexistent thread. In either of those cases, the computation will--- be halted.-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,475 +0,0 @@-{-# LANGUAGE RankNTypes          #-}-{-# LANGUAGE ScopedTypeVariables #-}---- |--- Module      : Test.DejaFu.Deterministic.Internal--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : experimental--- Portability : RankNTypes, ScopedTypeVariables------ Concurrent monads with a fixed scheduler: internal types and--- functions. This module is NOT considered to form part of the public--- interface of this library.-module Test.DejaFu.Deterministic.Internal- ( -- * Execution-   runFixed- , runFixed'-- -- * The @Conc@ Monad- , M(..)- , MVar(..)- , CRef(..)- , Ticket(..)- , Fixed- , cont- , runCont-- -- * Primitive Actions- , Action(..)-- -- * Identifiers- , ThreadId(..)- , MVarId(..)- , CRefId(..)- , initialThread-- -- * Memory Models- , MemType(..)-- -- * Scheduling & Traces- , Scheduler- , Trace- , Decision(..)- , ThreadAction(..)- , Lookahead(..)- , isBlock- , lookahead- , rewind- , willRelease- , preEmpCount- , showTrace- , showFail- , tvarsOf-- -- * Synchronised and Unsynchronised Actions- , ActionType(..)- , isBarrier- , isCommit- , synchronises- , crefOf- , cvarOf- , simplify- , simplify'-- -- * Failures- , Failure(..)- ) where--import Control.Exception (MaskingState(..), toException)-import Data.Functor (void)-import Data.List (sort)-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--{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}-{-# ANN module ("HLint: ignore Use const"           :: String) #-}------------------------------------------------------------------------------------- * Execution---- | Run a concurrent computation with a given 'Scheduler' and initial--- state, returning a 'Just' if it terminates, and 'Nothing' if a--- deadlock is detected. Also returned is the final state of the--- scheduler, and an execution trace.-runFixed :: (Functor n, Monad n) => Fixed n r s -> (forall x. s 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 -> 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 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--  return (fromJust out, s', idSource', reverse trace)---- | Run a collection of threads, until there are no threads left.------ Note: this returns the trace in reverse order, because it's more--- efficient to prepend to a list than append. As this function isn't--- exposed to users of the library, this is just an internal gotcha to--- watch out for.-runThreads :: (Functor n, Monad n) => Fixed n r s -> (forall x. s 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-    | isDeadlocked  = die g Deadlock-    | isSTMLocked   = die g STMDeadlock-    | isAborted     = die g' Abort-    | isNonexistant = die g' InternalError-    | isBlocked     = die g' InternalError-    | otherwise = do-      stepped <- stepThread fixed runstm memtype (_continuation $ fromJust thread) idSource chosen threads wb caps-      case stepped of-        Right (threads', idSource', act, wb', caps') -> loop threads' idSource' act wb' caps'--        Left UncaughtException-          | chosen == initialThread -> die g' UncaughtException-          | otherwise -> loop (kill chosen threads) idSource Killed wb caps--        Left failure -> die g' failure--    where-      (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-      thread        = M.lookup chosen threadsc-      threadsc      = addCommitThreads wb threads-      isAborted     = isNothing choice-      isBlocked     = isJust . _blocking $ fromJust thread-      isNonexistant = isNothing thread-      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-          Just (OnMask t) | t == tid -> thrd { _blocking = Nothing }-          _ -> thrd--      decision-        | Just chosen == prior = Continue-        | prior `notElem` map (Just . fst) runnable' = Start chosen-        | otherwise = SwitchTo chosen--      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, 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'------------------------------------------------------------------------------------- * Single-step execution---- | Run a single thread one step, by dispatching on the type of--- 'Action'.-stepThread :: forall n r s. (Functor n, Monad n) => Fixed n r s-  -> (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))-  -- ^ Run a 'MonadSTM' transaction atomically.-  -> MemType-  -- ^ The memory model-  -> Action n r s-  -- ^ Action to step-  -> IdSource-  -- ^ Source of fresh IDs-  -> ThreadId-  -- ^ ID of the current thread-  -> Threads n r s-  -- ^ Current state of threads-  -> WriteBuffer r-  -- ^ @CRef@ write buffer-  -> Int-  -- ^ 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    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  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  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-  AModRef  ref f c -> stepModRef      ref f c-  AModRefCas ref f c -> stepModRefCas ref f c-  AWriteRef ref a c -> stepWriteRef   ref a c-  ACasRef ref tick a c -> stepCasRef ref tick a c-  ACommit  t c     -> stepCommit      t c-  AAtom    stm c   -> stepAtom        stm c-  ALift    na      -> stepLift        na-  AThrow   e       -> stepThrow       e-  AThrowTo t e c   -> stepThrowTo     t e c-  ACatching h ma c -> stepCatching    h ma c-  APopCatching a   -> stepPopCatching a-  AMasking m ma c  -> stepMasking     m ma c-  AResetMask b1 b2 m c -> stepResetMask b1 b2 m c-  AReturn     c    -> stepReturn c-  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'-    ---    -- Explicit type signature needed for GHC 8. Looks like the-    -- impredicative polymorphism checks got stronger.-    stepFork :: String-             -> ((forall b. M n r s b -> M n r s b) -> Action n r s)-             -> (ThreadId -> Action n r s)-             -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))-    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 n idSource--    -- | Get the 'ThreadId' of the current thread-    stepMyTId c = simple (goto (c tid) tid threads) MyThreadId--    -- | Get the number of capabilities-    stepGetNumCapabilities c = simple (goto (c caps) tid threads) $ GetNumCapabilities caps--    -- | Set the number of capabilities-    stepSetNumCapabilities i c = return $ Right (goto c tid threads, idSource, SetNumCapabilities i, wb, i)--    -- | Yield the current thread-    stepYield c = simple (goto c tid threads) Yield--    -- | Put a value into a @MVar@, blocking the thread until it's-    -- empty.-    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 @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 @MVar@, without emptying, blocking the-    -- thread until it's full.-    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 @MVar@, blocking the thread until it's-    -- full.-    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 @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-      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-      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--    -- | Modify a @CRef@.-    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-      let (new, val) = f old-      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-      -- Write immediately.-      SequentialConsistency -> do-        writeImmediate fixed cref a-        simple (goto c tid threads) $ WriteRef crid--      -- Add to buffer using thread id.-      TotalStoreOrder -> do-        wb' <- bufferWrite fixed wb (tid, Nothing) cref a-        return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps)--      -- Add to buffer using both thread id and cref id-      PartialStoreOrder -> do-        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-      (suc, tick') <- casCRef fixed cref tid tick a-      simple (goto (c (suc, tick')) tid threads) $ CasRef crid suc--    -- | Commit a @CRef@ write-    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, Nothing)--        -- Commit using the cref id.-        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-      (res, idSource', trace) <- runstm stm idSource-      case res of-        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 (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-      a     = runCont ma      (APopCatching . c)-      e exc = runCont (h exc) (APopCatching . c)--      threads' = goto a tid (catching e tid threads)--    -- | Pop the top exception handler from the thread's stack.-    stepPopCatching a = simple threads' PopCatching where-      threads' = goto a tid (uncatching tid threads)--    -- | Throw an exception, and propagate it to the appropriate-    -- handler.-    stepThrow e =-      case propagate (toException e) tid threads of-        Just threads' -> simple threads' Throw-        Nothing -> return $ Left UncaughtException--    -- | Throw an exception to the target thread, and propagate it to-    -- the appropriate handler.-    stepThrowTo t e c = synchronised $-      let threads' = goto c tid threads-          blocked  = block (OnMask t) tid threads-      in case M.lookup t threads of-           Just thread-             | interruptible thread -> case propagate (toException e) t threads' of-               Just threads'' -> simple threads'' $ ThrowTo t-               Nothing-                 | t == initialThread -> return $ Left UncaughtException-                 | otherwise -> simple (kill t threads') $ ThrowTo t-             | otherwise -> simple blocked $ BlockedThrowTo t-           Nothing -> simple threads' $ ThrowTo t--    -- | Execute a subcomputation with a new masking state, and give-    -- it a function to run a computation with the current masking-    -- state.-    ---    -- Explicit type sig necessary for checking in the prescence of-    -- 'umask', sadly.-    stepMasking :: MaskingState-                -> ((forall b. M n r s b -> M n r s b) -> M n r s a)-                -> (a -> Action n r s)-                -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))-    stepMasking m ma c = simple threads' $ SetMasking False m where-      a = runCont (ma umask) (AResetMask False False m' . c)--      m' = _masking . fromJust $ M.lookup tid threads-      umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> return b-      resetMask typ ms = cont $ \k -> AResetMask typ True ms $ k ()--      threads' = goto a tid (mask m tid threads)--    -- | Reset the masking thread of the state.-    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 @MVar@, using the next 'MVarId'.-    stepNewVar n c = do-      let (idSource', newcvid) = nextCVId n idSource-      ref <- newRef fixed Nothing-      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 n a c = do-      let (idSource', newcrid) = nextCRId n idSource-      ref <- newRef fixed (M.empty, 0, a)-      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@-    -- computation.-    stepLift na = do-      a <- na-      simple (goto a tid threads) Lift--    -- | Execute a 'return' or 'pure'.-    stepReturn c = simple (goto c tid threads) Return--    -- | Record that a variable is known about.-    stepKnowsAbout v c = simple (knows [v] tid $ goto c tid threads) KnowsAbout--    -- | Record that a variable will never be touched again.-    stepForgets v c = simple (forgets [v] tid $ goto c tid threads) Forgets--    -- | 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--    -- | Helper for actions which don't touch the 'IdSource' or-    -- 'WriteBuffer'-    simple threads' act = return $ Right (threads', idSource, act, wb, caps)--    -- | Helper for actions impose a write barrier.-    synchronised ma = do-      writeBarrier fixed wb-      res <- ma--      return $ case res of-        Right (threads', idSource', act', _, caps') -> Right (threads', idSource', act', emptyBuffer, caps')-        _ -> res

@@ -1,873 +0,0 @@-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE RankNTypes                #-}---- |--- Module      : Test.DejaFu.Deterministic.Internal.Common--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : experimental--- Portability : ExistentialQuantification, RankNTypes------ Common types and utility functions for deterministic execution of--- 'MonadConc' implementations. This module is NOT considered to form--- part of the public interface of this library.-module Test.DejaFu.Deterministic.Internal.Common where--import Control.DeepSeq (NFData(..))-import Control.Exception (Exception, MaskingState(..))-import Data.Dynamic (Dynamic)-import Data.Map.Strict (Map)-import Data.Maybe (fromMaybe, mapMaybe)-import Data.List (sort, nub, intercalate)-import Data.List.NonEmpty (NonEmpty, fromList)-import Data.Set (Set)-import qualified Data.Set as S-import Test.DejaFu.Internal-import Test.DPOR (Decision(..), Trace)--{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}------------------------------------------------------------------------------------- * The @Conc@ Monad---- | 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-    fmap f m = M $ \ c -> runM m (c . f)--instance Applicative (M n r s) where-    pure x  = M $ \c -> AReturn $ c x-    f <*> v = M $ \c -> runM f (\g -> runM v (c . g))--instance Monad (M n r s) where-    return  = pure-    m >>= k = M $ \c -> runM m (\x -> runM (k x) c)---- | 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 @MVar@--- wakes up all threads blocked on reading it, and it is up to the--- scheduler which one runs next. Taking from a @MVar@ behaves--- analogously.-data MVar r a = MVar-  { _cvarId   :: MVarId-  , _cvarVal  :: r (Maybe a)-  }---- | The mutable non-blocking reference type. These are like 'IORef's.------ @CRef@s are represented as a unique numeric identifier and a--- reference containing (a) any thread-local non-synchronised writes--- (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.-data CRef r a = CRef-  { _crefId   :: CRefId-  , _crefVal  :: r (Map ThreadId a, Integer, a)-  }---- | The compare-and-swap proof type.------ @Ticket@s are represented as just a wrapper around the identifier--- of the 'CRef' it came from, the commit count at the time it was--- 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.-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)---- | Construct a continuation-passing operation from a function.-cont :: ((a -> Action n r s) -> Action n r s) -> M n r s a-cont = M---- | Run a CPS computation with the given final computation.-runCont :: M n r s a -> (a -> Action n r s) -> Action n r s-runCont = runM------------------------------------------------------------------------------------- * Primitive Actions---- | Scheduling is done in terms of a trace of 'Action's. Blocking can--- only occur as a result of an action, and they cover (most of) the--- primitives of the concurrency. 'spawn' is absent as it is--- implemented in terms of 'newEmptyMVar', 'fork', and 'putMVar'.-data 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 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 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)-  | forall a b. AModRef     (CRef r a) (a -> (a, b)) (b -> Action n r s)-  | forall a b. AModRefCas  (CRef r a) (a -> (a, b)) (b -> Action n r s)-  | forall a.   AWriteRef   (CRef r a) a (Action n r s)-  | forall a.   ACasRef     (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r s)--  | forall e.   Exception e => AThrow e-  | forall e.   Exception e => AThrowTo ThreadId e (Action n r s)-  | forall a e. Exception e => ACatching (e -> M n r s a) (M n r s a) (a -> Action n r s)-  | APopCatching (Action n r s)-  | forall a. AMasking MaskingState ((forall b. M n r s b -> M n r s b) -> M n r s a) (a -> Action n r s)-  | AResetMask Bool Bool MaskingState (Action n r s)--  | AKnowsAbout (Either 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))-  | AYield  (Action n r s)-  | AReturn (Action n r s)-  | ACommit ThreadId CRefId-  | AStop------------------------------------------------------------------------------------- * Identifiers---- | Every live thread has a unique identitifer.-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 (Just n) _) = n-  show (ThreadId Nothing  i) = show i--instance NFData ThreadId where-  rnf (ThreadId n i) = rnf (n, i)---- | The ID of the initial thread.-initialThread :: ThreadId-initialThread = ThreadId (Just "main") 0---- | 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 (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  :: Int-  , _nextCVId  :: Int-  , _nextTVId  :: Int-  , _nextTId   :: Int-  , _usedCRNames :: [String]-  , _usedCVNames :: [String]-  , _usedTVNames :: [String]-  , _usedTNames  :: [String] }---- | Get the next free 'CRefId'.-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 '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 '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 :: 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 [] [] [] []------------------------------------------------------------------------------------- * Scheduling & Traces---- | 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 '-'--  toKey (Start (ThreadId (Just name) i), _, _) = Just $ show i ++ ": " ++ name-  toKey _ = Nothing---- | All the actions that a thread can perform.-data ThreadAction =-    Fork ThreadId-  -- ^ Start a new thread.-  | MyThreadId-  -- ^ Get the 'ThreadId' of the current thread.-  | GetNumCapabilities Int-  -- ^ Get the number of Haskell threads that can run simultaneously.-  | SetNumCapabilities Int-  -- ^ Set the number of Haskell threads that can run simultaneously.-  | Yield-  -- ^ Yield the current thread.-  | 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 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 MVarId [ThreadId]-  -- ^ Take from a 'MVar', possibly waking up some threads.-  | BlockedTakeVar MVarId-  -- ^ Get blocked on a take.-  | TryTakeVar MVarId Bool [ThreadId]-  -- ^ Try to take from a 'MVar', possibly waking up some threads.-  | NewRef CRefId-  -- ^ Create a new 'CRef'.-  | ReadRef CRefId-  -- ^ Read from a 'CRef'.-  | ReadRefCas CRefId-  -- ^ Read from a 'CRef' for a future compare-and-swap.-  | PeekTicket CRefId-  -- ^ Extract the value from a 'Ticket'.-  | ModRef CRefId-  -- ^ Modify a 'CRef'.-  | ModRefCas CRefId-  -- ^ Modify a 'CRef' using a compare-and-swap.-  | WriteRef CRefId-  -- ^ Write to a 'CRef' without synchronising.-  | CasRef CRefId Bool-  -- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising-  -- it.-  | 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 TTrace [ThreadId]-  -- ^ An STM transaction was executed, possibly waking up some-  -- threads.-  | BlockedSTM TTrace-  -- ^ Got blocked in an STM transaction.-  | Catching-  -- ^ Register a new exception handler-  | PopCatching-  -- ^ Pop the innermost exception handler from the stack.-  | Throw-  -- ^ Throw an exception.-  | ThrowTo ThreadId-  -- ^ Throw an exception to a thread.-  | BlockedThrowTo ThreadId-  -- ^ Get blocked on a 'throwTo'.-  | Killed-  -- ^ Killed by an uncaught exception.-  | SetMasking Bool MaskingState-  -- ^ Set the masking state. If 'True', this is being used to set the-  -- masking state to the original state in the argument passed to a-  -- 'mask'ed function.-  | ResetMasking Bool MaskingState-  -- ^ Return to an earlier masking state.  If 'True', this is being-  -- used to return to the state of the masked block in the argument-  -- passed to a 'mask'ed function.-  | Lift-  -- ^ Lift an action from the underlying monad. Note that the-  -- penultimate action in a trace will always be a @Lift@, this is an-  -- artefact of how the runner works.-  | Return-  -- ^ A 'return' or 'pure' action was executed.-  | KnowsAbout-  -- ^ A '_concKnowsAbout' annotation was processed.-  | Forgets-  -- ^ A '_concForgets' annotation was processed.-  | AllKnown-  -- ^ A '_concALlKnown' annotation was processed.-  | Message Dynamic-  -- ^ A '_concMessage' annotation was processed.-  | Stop-  -- ^ Cease execution and terminate.-  deriving Show--instance NFData ThreadAction where-  rnf (Fork t) = rnf t-  rnf (GetNumCapabilities i) = rnf i-  rnf (SetNumCapabilities i) = rnf i-  rnf (NewVar c) = rnf c-  rnf (PutVar c ts) = rnf (c, ts)-  rnf (BlockedPutVar c) = rnf c-  rnf (TryPutVar c b ts) = rnf (c, b, ts)-  rnf (ReadVar c) = rnf c-  rnf (BlockedReadVar c) = rnf c-  rnf (TakeVar c ts) = rnf (c, ts)-  rnf (BlockedTakeVar c) = rnf c-  rnf (TryTakeVar c b ts) = rnf (c, b, ts)-  rnf (NewRef c) = rnf c-  rnf (ReadRef c) = rnf c-  rnf (ReadRefCas c) = rnf c-  rnf (PeekTicket c) = rnf c-  rnf (ModRef c) = rnf c-  rnf (ModRefCas c) = rnf c-  rnf (WriteRef c) = rnf c-  rnf (CasRef c b) = rnf (c, b)-  rnf (CommitRef t c) = rnf (t, c)-  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-  -- ^ Will start a new thread.-  | WillMyThreadId-  -- ^ Will get the 'ThreadId'.-  | WillGetNumCapabilities-  -- ^ Will get the number of Haskell threads that can run-  -- simultaneously.-  | WillSetNumCapabilities Int-  -- ^ Will set the number of Haskell threads that can run-  -- simultaneously.-  | WillYield-  -- ^ Will yield the current thread.-  | WillNewVar-  -- ^ 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-  -- ^ Will read from a 'CRef'.-  | WillPeekTicket CRefId-  -- ^ Will extract the value from a 'Ticket'.-  | WillReadRefCas CRefId-  -- ^ Will read from a 'CRef' for a future compare-and-swap.-  | WillModRef CRefId-  -- ^ Will modify a 'CRef'.-  | WillModRefCas CRefId-  -- ^ Will nodify a 'CRef' using a compare-and-swap.-  | WillWriteRef CRefId-  -- ^ Will write to a 'CRef' without synchronising.-  | WillCasRef CRefId-  -- ^ Will attempt to to a 'CRef' using a compare-and-swap,-  -- synchronising it.-  | WillCommitRef ThreadId CRefId-  -- ^ Will commit the last write by the given thread to the 'CRef'.-  | WillSTM-  -- ^ Will execute an STM transaction, possibly waking up some-  -- threads.-  | WillCatching-  -- ^ Will register a new exception handler-  | WillPopCatching-  -- ^ Will pop the innermost exception handler from the stack.-  | WillThrow-  -- ^ Will throw an exception.-  | WillThrowTo ThreadId-  -- ^ Will throw an exception to a thread.-  | WillSetMasking Bool MaskingState-  -- ^ Will set the masking state. If 'True', this is being used to-  -- set the masking state to the original state in the argument-  -- passed to a 'mask'ed function.-  | WillResetMasking Bool MaskingState-  -- ^ Will return to an earlier masking state.  If 'True', this is-  -- being used to return to the state of the masked block in the-  -- argument passed to a 'mask'ed function.-  | WillLift-  -- ^ Will lift an action from the underlying monad. Note that the-  -- penultimate action in a trace will always be a @Lift@, this is an-  -- artefact of how the runner works.-  | WillReturn-  -- ^ Will execute a 'return' or 'pure' action.-  | WillKnowsAbout-  -- ^ Will process a '_concKnowsAbout' annotation.-  | WillForgets-  -- ^ 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 Show--instance NFData Lookahead where-  rnf (WillSetNumCapabilities i) = rnf i-  rnf (WillPutVar c) = rnf c-  rnf (WillTryPutVar c) = rnf c-  rnf (WillReadVar c) = rnf c-  rnf (WillTakeVar c) = rnf c-  rnf (WillTryTakeVar c) = rnf c-  rnf (WillReadRef c) = rnf c-  rnf (WillReadRefCas c) = rnf c-  rnf (WillPeekTicket c) = rnf c-  rnf (WillModRef c) = rnf c-  rnf (WillModRefCas c) = rnf c-  rnf (WillWriteRef c) = rnf c-  rnf (WillCasRef c) = rnf c-  rnf (WillCommitRef t c) = rnf (t, c)-  rnf (WillThrowTo t) = rnf t-  rnf (WillSetMasking b m) = b `seq` m `seq` ()-  rnf (WillResetMasking b m) = b `seq` m `seq` ()-  rnf (WillMessage m) = m `seq` ()-  rnf l = l `seq` ()---- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has--- happened. 'Killed' has no 'Lookahead' counterpart.-rewind :: ThreadAction -> Maybe Lookahead-rewind (Fork _) = Just WillFork-rewind MyThreadId = Just WillMyThreadId-rewind (GetNumCapabilities _) = Just WillGetNumCapabilities-rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i)-rewind Yield = Just WillYield-rewind (NewVar _) = Just WillNewVar-rewind (PutVar c _) = Just (WillPutVar c)-rewind (BlockedPutVar c) = Just (WillPutVar c)-rewind (TryPutVar c _ _) = Just (WillTryPutVar c)-rewind (ReadVar c) = Just (WillReadVar c)-rewind (BlockedReadVar c) = Just (WillReadVar c)-rewind (TakeVar c _) = Just (WillTakeVar c)-rewind (BlockedTakeVar c) = Just (WillTakeVar c)-rewind (TryTakeVar c _ _) = Just (WillTryTakeVar c)-rewind (NewRef _) = Just WillNewRef-rewind (ReadRef c) = Just (WillReadRef c)-rewind (ReadRefCas c) = Just (WillReadRefCas c)-rewind (PeekTicket c) = Just (WillPeekTicket c)-rewind (ModRef c) = Just (WillModRef c)-rewind (ModRefCas c) = Just (WillModRefCas c)-rewind (WriteRef c) = Just (WillWriteRef c)-rewind (CasRef c _) = Just (WillCasRef c)-rewind (CommitRef t c) = Just (WillCommitRef t c)-rewind (STM _ _) = Just WillSTM-rewind (BlockedSTM _) = Just WillSTM-rewind Catching = Just WillCatching-rewind PopCatching = Just WillPopCatching-rewind Throw = Just WillThrow-rewind (ThrowTo t) = Just (WillThrowTo t)-rewind (BlockedThrowTo t) = Just (WillThrowTo t)-rewind Killed = Nothing-rewind (SetMasking b m) = Just (WillSetMasking b m)-rewind (ResetMasking b m) = Just (WillResetMasking b m)-rewind Lift = Just WillLift-rewind Return = Just WillReturn-rewind KnowsAbout = Just WillKnowsAbout-rewind Forgets = Just WillForgets-rewind AllKnown = Just WillAllKnown-rewind (Message m) = Just (WillMessage m)-rewind Stop = Just WillStop---- | Look as far ahead in the given continuation as possible.-lookahead :: Action n r s -> NonEmpty Lookahead-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 (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]-  lookahead' (AThrowTo tid _ k)      = WillThrowTo tid : lookahead' k-  lookahead' (ACatching _ _ _)       = [WillCatching]-  lookahead' (APopCatching k)        = WillPopCatching : lookahead' k-  lookahead' (AMasking ms _ _)       = [WillSetMasking False ms]-  lookahead' (AResetMask b1 b2 ms k) = (if b1 then WillSetMasking else WillResetMasking) b2 ms : lookahead' k-  lookahead' (ALift _)               = [WillLift]-  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]---- | Check if an operation could enable another thread.-willRelease :: Lookahead -> Bool-willRelease WillFork = True-willRelease WillYield = True-willRelease (WillPutVar _) = True-willRelease (WillTryPutVar _) = True-willRelease (WillReadVar _) = True-willRelease (WillTakeVar _) = True-willRelease (WillTryTakeVar _) = True-willRelease WillSTM = True-willRelease WillThrow = True-willRelease (WillSetMasking _ _) = True-willRelease (WillResetMasking _ _) = True-willRelease WillStop = True-willRelease _ = False---- Count the number of pre-emptions in a schedule prefix.------ Commit threads complicate this a bit. Conceptually, commits are--- happening truly in parallel, nondeterministically. The commit--- thread implementation is just there to unify the two sources of--- nondeterminism: commit timing and thread scheduling.------ SO, we don't count a switch TO a commit thread as a--- preemption. HOWEVER, the switch FROM a commit thread counts as a--- preemption if it is not to the thread that the commit interrupted.-preEmpCount :: [(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Int-preEmpCount ts (d, _) = go initialThread Nothing ts where-  go _ (Just Yield) ((SwitchTo t, a):rest) = go t (Just a) rest-  go tid prior ((SwitchTo t, a):rest)-    | isCommitThread t = go tid prior (skip rest)-    | otherwise = 1 + go t (Just a) rest-  go _   _ ((Start t,  a):rest) = go t   (Just a) rest-  go tid _ ((Continue, a):rest) = go tid (Just a) rest-  go _ prior [] = case (prior, d) of-    (Just Yield, SwitchTo _) -> 0-    (_, SwitchTo _) -> 1-    _ -> 0--  -- Commit threads have negative thread IDs for easy identification.-  isCommitThread = (< initialThread)--  -- Skip until the next context switch.-  skip = dropWhile (not . isContextSwitch . fst)-  isContextSwitch Continue = False-  isContextSwitch _ = True---- | A simplified view of the possible actions a thread can perform.-data ActionType =-    UnsynchronisedRead  CRefId-  -- ^ A 'readCRef' or a 'readForCAS'.-  | UnsynchronisedWrite CRefId-  -- ^ A 'writeCRef'.-  | UnsynchronisedOther-  -- ^ Some other action which doesn't require cross-thread-  -- communication.-  | PartiallySynchronisedCommit CRefId-  -- ^ A commit.-  | PartiallySynchronisedWrite  CRefId-  -- ^ A 'casCRef'-  | PartiallySynchronisedModify CRefId-  -- ^ A 'modifyCRefCAS'-  | SynchronisedModify  CRefId-  -- ^ An 'atomicModifyCRef'.-  | SynchronisedRead    MVarId-  -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants).-  | SynchronisedWrite   MVarId-  -- ^ A 'putMVar' (or @try@/@blocked@ variant).-  | SynchronisedOther-  -- ^ Some other action which does require cross-thread-  -- communication.-  deriving (Eq, Show)--instance NFData ActionType where-  rnf (UnsynchronisedRead  r) = rnf r-  rnf (UnsynchronisedWrite r) = rnf r-  rnf (PartiallySynchronisedCommit r) = rnf r-  rnf (PartiallySynchronisedWrite  r) = rnf r-  rnf (PartiallySynchronisedModify  r) = rnf r-  rnf (SynchronisedModify  r) = rnf r-  rnf (SynchronisedRead    c) = rnf c-  rnf (SynchronisedWrite   c) = rnf c-  rnf a = a `seq` ()---- | Check if an action imposes a write barrier.-isBarrier :: ActionType -> Bool-isBarrier (SynchronisedModify _) = True-isBarrier (SynchronisedRead   _) = True-isBarrier (SynchronisedWrite  _) = True-isBarrier SynchronisedOther = True-isBarrier _ = False---- | Check if an action commits a given 'CRef'.-isCommit :: ActionType -> CRefId -> Bool-isCommit (PartiallySynchronisedCommit c) r = c == r-isCommit (PartiallySynchronisedWrite  c) r = c == r-isCommit (PartiallySynchronisedModify c) r = c == r-isCommit _ _ = False---- | Check if an action synchronises a given 'CRef'.-synchronises :: ActionType -> CRefId -> Bool-synchronises a r = isCommit a r || isBarrier a---- | Get the 'CRef' affected.-crefOf :: ActionType -> Maybe CRefId-crefOf (UnsynchronisedRead  r) = Just r-crefOf (UnsynchronisedWrite r) = Just r-crefOf (SynchronisedModify  r) = Just r-crefOf (PartiallySynchronisedCommit r) = Just r-crefOf (PartiallySynchronisedWrite  r) = Just r-crefOf (PartiallySynchronisedModify r) = Just r-crefOf _ = Nothing---- | Get the 'MVar' affected.-cvarOf :: ActionType -> Maybe MVarId-cvarOf (SynchronisedRead  c) = Just c-cvarOf (SynchronisedWrite c) = Just c-cvarOf _ = Nothing---- | Get the 'TVar's affected.-tvarsOf :: ThreadAction -> Set TVarId-tvarsOf act = S.fromList $ case act of-  STM trc _ -> concatMap tvarsOf' trc-  BlockedSTM trc -> concatMap tvarsOf' trc-  _ -> []--  where-    tvarsOf' (TRead  tv) = [tv]-    tvarsOf' (TWrite tv) = [tv]-    tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)-    tvarsOf' (TCatch  ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb)-    tvarsOf' _ = []---- | Throw away information from a 'ThreadAction' and give a--- simplified view of what is happening.------ This is used in the SCT code to help determine interesting--- alternative scheduling decisions.-simplify :: ThreadAction -> ActionType-simplify = maybe UnsynchronisedOther simplify' . rewind---- | Variant of 'simplify' that takes a 'Lookahead'.-simplify' :: Lookahead -> ActionType-simplify' (WillPutVar c)     = SynchronisedWrite c-simplify' (WillTryPutVar c)  = SynchronisedWrite c-simplify' (WillReadVar c)    = SynchronisedRead c-simplify' (WillTakeVar c)    = SynchronisedRead c-simplify' (WillTryTakeVar c) = SynchronisedRead c-simplify' (WillReadRef r)     = UnsynchronisedRead r-simplify' (WillReadRefCas r)  = UnsynchronisedRead r-simplify' (WillModRef r)      = SynchronisedModify r-simplify' (WillModRefCas r)   = PartiallySynchronisedModify r-simplify' (WillWriteRef r)    = UnsynchronisedWrite r-simplify' (WillCasRef r)      = PartiallySynchronisedWrite r-simplify' (WillCommitRef _ r) = PartiallySynchronisedCommit r-simplify' WillSTM         = SynchronisedOther-simplify' (WillThrowTo _) = SynchronisedOther-simplify' _ = UnsynchronisedOther------------------------------------------------------------------------------------- * Failures---- | An indication of how a concurrent computation failed.-data Failure =-    InternalError-  -- ^ Will be raised if the scheduler does something bad. This should-  -- never arise unless you write your own, faulty, scheduler! If it-  -- does, please file a bug report.-  | Abort-  -- ^ The scheduler chose to abort execution. This will be produced-  -- if, for example, all possible decisions exceed the specified-  -- bounds (there have been too many pre-emptions, the computation-  -- has executed for too long, or there have been too many yields).-  | Deadlock-  -- ^ The computation became blocked indefinitely on @MVar@s.-  | STMDeadlock-  -- ^ 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)--instance NFData Failure where-  rnf f = f `seq` () -- WHNF == NF---- | Pretty-print a failure-showFail :: Failure -> String-showFail Abort = "[abort]"-showFail Deadlock = "[deadlock]"-showFail STMDeadlock = "[stm-deadlock]"-showFail InternalError = "[internal-error]"-showFail UncaughtException = "[exception]"------------------------------------------------------------------------------------- * Memory Models---- | The memory model to use for non-synchronised 'CRef' operations.-data MemType =-    SequentialConsistency-  -- ^ The most intuitive model: a program behaves as a simple-  -- interleaving of the actions in different threads. When a 'CRef'-  -- is written to, that write is immediately visible to all threads.-  | TotalStoreOrder-  -- ^ Each thread has a write buffer. A thread sees its writes-  -- immediately, but other threads will only see writes when they are-  -- committed, which may happen later. Writes are committed in the-  -- same order that they are created.-  | PartialStoreOrder-  -- ^ Each 'CRef' has a write buffer. A thread sees its writes-  -- immediately, but other threads will only see writes when they are-  -- committed, which may happen later. Writes to different 'CRef's-  -- are not necessarily committed in the same order that they are-  -- created.-  deriving (Eq, Show, Read, Ord, Enum, Bounded)--instance NFData MemType where-  rnf m = m `seq` () -- WHNF == NF

@@ -1,208 +0,0 @@-{-# LANGUAGE BangPatterns #-}-{-# LANGUAGE GADTs        #-}---- |--- Module      : Test.DejaFu.Deterministic.Internal.Memory--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : experimental--- Portability : BangPatterns, GADTs------ Operations over @CRef@s and @MVar@s. This module is NOT considered--- to form part of the public interface of this library.------ 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.Map.Strict (Map)-import Data.Maybe (isJust, fromJust)-import Data.Monoid ((<>))-import Data.Sequence (Seq, ViewL(..), (><), singleton, viewl)-import Test.DejaFu.Deterministic.Internal.Common-import Test.DejaFu.Deterministic.Internal.Threading-import Test.DejaFu.Internal--import qualified Data.Map.Strict as M------------------------------------------------------------------------------------- * Manipulating @CRef@s---- | In non-sequentially-consistent memory models, non-synchronised--- writes get buffered.------ 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--- thing which can be done with it is to write it to the reference.-data BufferedWrite r where-  BufferedWrite :: ThreadId -> CRef r a -> a -> BufferedWrite r---- | An empty write buffer.-emptyBuffer :: WriteBuffer r-emptyBuffer = WriteBuffer M.empty---- | Add a new write to the end of a buffer.-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' = M.insertWith (flip (><)) k write wb--  -- Write the thread-local value to the @CRef@'s update map.-  (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 -> (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 $ M.insert k rest wb--  EmptyL -> return w---- | Read from a @CRef@, returning a newer thread-local non-committed--- write if there is one.-readCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n a-readCRef fixed cref tid = do-  (val, _) <- readCRefPrim fixed cref tid-  return val---- | 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-  (val, count) <- readCRefPrim fixed cref tid-  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--  if cc == cc'-  then do-    writeImmediate fixed cref new-    tick'' <- readForTicket fixed cref tid-    return (True, tick'')-  else return (False, tick')---- | 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-  (vals, count, def) <- readRef fixed ref--  return (M.findWithDefault def tid vals, count)---- | 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-  (_, 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 $ 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 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 >= initialThread------------------------------------------------------------------------------------- * Manipulating @MVar@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])-putIntoMVar cvar a c = mutMVar True cvar a (const c)---- | 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])-tryPutIntoMVar = mutMVar False---- | 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])-readFromMVar cvar c = seeMVar False True cvar (c . fromJust)---- | 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])-takeFromMVar cvar c = seeMVar True True cvar (c . fromJust)---- | 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])-tryTakeFromMVar = seeMVar True False---- | 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])-mutMVar blocking (MVar cvid ref) a c fixed threadid threads = do-  val <- readRef fixed ref--  case val of-    Just _-      | blocking ->-        let threads' = block (OnMVarEmpty cvid) threadid threads-        in return (False, threads', [])--      | otherwise ->-        return (False, goto (c False) threadid threads, [])--    Nothing -> do-      writeRef fixed ref $ Just a-      let (threads', woken) = wake (OnMVarFull cvid) threads-      return (True, goto (c True) threadid threads', woken)---- | Read a @MVar@, in either a blocking or nonblocking--- way.-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])-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 (OnMVarEmpty cvid) threads-      return (True, goto (c val) threadid threads', woken)--    Nothing-      | blocking ->-        let threads' = block (OnMVarFull cvid) threadid threads-        in return (False, threads', [])--      | otherwise ->-        return (False, goto (c Nothing) threadid threads, [])

@@ -1,200 +0,0 @@-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE RankNTypes                #-}---- |--- Module      : Test.DejaFu.Deterministic.Internal.Threading--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : experimental--- Portability : ExistentialQuantification, RankNTypes------ Operations and types for threads. This module is NOT considered to--- form part of the public interface of this library.-module Test.DejaFu.Deterministic.Internal.Threading where--import Control.Exception (Exception, MaskingState(..), SomeException, fromException)-import Data.List (intersect, nub)-import Data.Map.Strict (Map)-import Data.Maybe (fromMaybe, isJust, isNothing)-import Test.DejaFu.Deterministic.Internal.Common--import qualified Data.Map.Strict as M------------------------------------------------------------------------------------- * Threads---- | Threads are stored in a map index by 'ThreadId'.-type Threads n r s = Map ThreadId (Thread n r s)---- | All the state of a thread.-data Thread n r s = Thread-  { _continuation :: Action n r s-  -- ^ The next action to execute.-  , _blocking     :: Maybe BlockedOn-  -- ^ The state of any blocks.-  , _handlers     :: [Handler n r s]-  -- ^ Stack of exception handlers-  , _masking      :: MaskingState-  -- ^ The exception masking state.-  , _known        :: [Either MVarId TVarId]-  -- ^ Shared variables the thread knows about.-  , _fullknown    :: Bool-  -- ^ Whether the referenced variables of the thread are completely-  -- known. If every thread has _fullknown == True, then turn on-  -- detection of nonglobal deadlock.-  }---- | Construct a thread with just one action-mkthread :: Action n r s -> Thread n r s-mkthread c = Thread c Nothing [] Unmasked [] False------------------------------------------------------------------------------------- * Blocking---- | A @BlockedOn@ is used to determine what sort of variable a thread--- is blocked on.-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 (OnMVarFull  _), OnMVarFull  _) -> True-  (Just (OnMVarEmpty _), OnMVarEmpty _) -> True-  (Just (OnTVar      _), OnTVar      _) -> True-  (Just (OnMask      _), OnMask      _) -> True-  _ -> False---- | Determine if a thread is deadlocked. If at least one thread is--- not in a fully-known state, this will only check for global--- deadlock.-isLocked :: ThreadId -> Threads n r a -> Bool-isLocked tid ts-  | allKnown = case M.lookup tid ts of-    Just thread -> noRefs $ _blocking thread-    Nothing -> False-  | otherwise = M.null $ M.filter (isNothing . _blocking) ts--  where-    -- | Check if all threads are in a fully-known state.-    allKnown = all _fullknown $ M.elems ts--    -- | Check if no other runnable thread has a reference to anything-    -- the block references.-    noRefs (Just (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 '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 '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.-    check lookingfor thetid thethread-      | thetid == tid = False-      | otherwise     = (not . null $ lookingfor `intersect` _known thethread) && isNothing (_blocking thethread)------------------------------------------------------------------------------------- * Exceptions---- | An exception handler.-data Handler n r s = forall e. Exception e => Handler (e -> Action n r s)---- | Propagate an exception upwards, finding the closest handler--- which can deal with it.-propagate :: SomeException -> ThreadId -> Threads n r s -> Maybe (Threads n r s)-propagate e tid threads = case M.lookup tid threads >>= go . _handlers of-  Just (act, hs) -> Just $ except act hs tid threads-  Nothing -> Nothing--  where-    go [] = Nothing-    go (Handler h:hs) = maybe (go hs) (\act -> Just (act, hs)) $ h <$> fromException e---- | Check if a thread can be interrupted by an exception.-interruptible :: Thread n r s -> Bool-interruptible thread = _masking thread == Unmasked || (_masking thread == MaskedInterruptible && isJust (_blocking thread))---- | Register a new exception handler.-catching :: Exception e => (e -> Action n r s) -> ThreadId -> Threads n r s -> Threads n r s-catching h = M.alter $ \(Just thread) -> Just $ thread { _handlers = Handler h : _handlers thread }---- | Remove the most recent exception handler.-uncatching :: ThreadId -> Threads n r s -> Threads n r s-uncatching = M.alter $ \(Just thread) -> Just $ thread { _handlers = tail $ _handlers thread }---- | Raise an exception in a thread.-except :: Action n r s -> [Handler n r s] -> ThreadId -> Threads n r s -> Threads n r s-except act hs = M.alter $ \(Just thread) -> Just $ thread { _continuation = act, _handlers = hs, _blocking = Nothing }---- | Set the masking state of a thread.-mask :: MaskingState -> ThreadId -> Threads n r s -> Threads n r s-mask ms = M.alter $ \(Just thread) -> Just $ thread { _masking = ms }------------------------------------------------------------------------------------- * Manipulating threads---- | Replace the @Action@ of a thread.-goto :: Action n r s -> ThreadId -> Threads n r s -> Threads n r s-goto a = M.alter $ \(Just thread) -> Just (thread { _continuation = a })---- | Start a thread with the given ID, inheriting the masking state--- from the parent thread. This ID must not already be in use!-launch :: ThreadId -> ThreadId -> ((forall b. M n r s b -> M n r s b) -> Action n r s) -> Threads n r s -> Threads n r s-launch parent tid a threads = launch' 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' 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 ms >> return b-  resetMask typ m = cont $ \k -> AResetMask typ True m $ k ()---- | Kill a thread.-kill :: ThreadId -> Threads n r s -> Threads n r s-kill = M.delete---- | Block a thread.-block :: BlockedOn -> ThreadId -> Threads n r s -> Threads n r s-block blockedOn = M.alter doBlock where-  doBlock (Just thread) = Just $ thread { _blocking = Just blockedOn }-  doBlock _ = error "Invariant failure in 'block': thread does NOT exist!"---- | Unblock all threads waiting on the appropriate block. For 'TVar'--- blocks, this will wake all threads waiting on at least one of the--- 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-    | isBlocked thread = thread { _blocking = Nothing }-    | otherwise = thread--  isBlocked thread = case (_blocking thread, blockedOn) of-    (Just (OnTVar tvids), OnTVar blockedOn') -> tvids `intersect` blockedOn' /= []-    (theblock, _) -> theblock == Just blockedOn---- | Record that a thread knows about a shared variable.-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 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!"---- | Record that a thread's shared variable state is fully known.-fullknown :: ThreadId -> Threads n r s -> Threads n r s-fullknown = M.alter go where-  go (Just thread) = Just $ thread { _fullknown = True }-  go _ = error "Invariant failure in 'fullknown': thread does NOT exist!"

@@ -1,43 +0,0 @@-{-# LANGUAGE RankNTypes #-}---- |--- Module      : Test.DejaFu.Internal--- Copyright   : (c) 2016 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : experimental--- Portability : RankNTypes------ Dealing with mutable state. This module is NOT considered to form--- part of the public interface of this library.-module Test.DejaFu.Internal where--import Control.Monad.ST (ST)-import Data.IORef (IORef, newIORef, readIORef, writeIORef)-import Data.STRef (STRef, newSTRef, readSTRef, writeSTRef)---- | Mutable references.-data Ref n r m = Ref-  { newRef   :: forall a. a -> n (r a)-  , readRef  :: forall a. r a -> n a-  , writeRef :: forall a. r a -> a -> n ()-  , liftN    :: forall a. n a -> m a-  }---- | Method dict for 'ST'.-refST :: (forall a. ST t a -> m a) -> Ref (ST t) (STRef t) m-refST lftN = Ref-  { newRef   = newSTRef-  , readRef  = readSTRef-  , writeRef = writeSTRef-  , liftN    = lftN-  }---- | Method dict for 'IO'.-refIO :: (forall a. IO a -> m a) -> Ref IO IORef m-refIO lftN = Ref-  { newRef   = newIORef-  , readRef  = readIORef-  , writeRef = writeIORef-  , liftN    = lftN-  }

@@ -1,5 +1,4 @@ {-# LANGUAGE CPP #-}-{-# LANGUAGE RankNTypes #-}  -- | -- Module      : Test.DejaFu.SCT@@ -7,7 +6,7 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : CPP, RankNTypes+-- Portability : CPP -- -- Systematic testing for concurrent computations. module Test.DejaFu.SCT@@ -32,7 +31,6 @@   -- K. McKinley for more details.      sctBounded-  , sctBoundedIO    -- * Combination Bounds @@ -51,7 +49,6 @@   , noBounds    , sctBound-  , sctBoundIO    -- * Individual Bounds @@ -67,7 +64,6 @@   , PreemptionBound(..)   , defaultPreemptionBound   , sctPreBound-  , sctPreBoundIO   , pBacktrack   , pBound @@ -82,7 +78,6 @@   , FairBound(..)   , defaultFairBound   , sctFairBound-  , sctFairBoundIO   , fBacktrack   , fBound @@ -94,7 +89,6 @@   , LengthBound(..)   , defaultLengthBound   , sctLengthBound-  , sctLengthBoundIO    -- * Backtracking @@ -103,8 +97,7 @@   ) where  import Control.DeepSeq (NFData(..))-import Control.Exception (MaskingState(..))-import Data.Functor.Identity (Identity(..), runIdentity)+import Control.Monad.Ref (MonadRef) import Data.Map.Strict (Map) import qualified Data.Map.Strict as M import Data.Maybe (isJust, fromJust)@@ -117,8 +110,8 @@                  , LengthBound(..), defaultLengthBound, lenBound, lenBacktrack                  ) -import Test.DejaFu.Deterministic (ConcIO, ConcST, runConcIO, runConcST)-import Test.DejaFu.Deterministic.Internal+import Test.DejaFu.Common+import Test.DejaFu.Conc  ------------------------------------------------------------------------------- -- Combined Bounds@@ -148,22 +141,16 @@   }  -- | An SCT runner using a bounded scheduler-sctBound :: MemType+sctBound :: MonadRef r n+  => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> Bounds   -- ^ The combined bounds.-  -> (forall t. ConcST t a)+  -> Conc n r a   -- ^ The computation to run many times-  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]+  -> n [(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 ThreadId ThreadAction Lookahead)]-sctBoundIO memtype cb = sctBoundedIO memtype (cBound cb) (cBacktrack cb)- -- | Combination bound function cBound :: Bounds -> BoundFunc ThreadId ThreadAction Lookahead cBound (Bounds pb fb lb) = maybe trueBound pBound pb &+& maybe trueBound fBound fb &+& maybe trueBound lenBound lb@@ -183,23 +170,17 @@ -- Pre-emption bounding  -- | An SCT runner using a pre-emption bounding scheduler.-sctPreBound :: MemType+sctPreBound :: MonadRef r n+  => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> PreemptionBound   -- ^ The maximum number of pre-emptions to allow in a single   -- execution-  -> (forall t. ConcST t a)+  -> Conc n r a   -- ^ The computation to run many times-  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]+  -> n [(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 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@@ -217,23 +198,17 @@ -- Fair bounding  -- | An SCT runner using a fair bounding scheduler.-sctFairBound :: MemType+sctFairBound :: MonadRef r n+  => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> FairBound   -- ^ The maximum difference between the number of yield operations   -- performed by different threads.-  -> (forall t. ConcST t a)+  -> Conc n r a   -- ^ The computation to run many times-  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]+  -> n [(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 ThreadId ThreadAction Lookahead)]-sctFairBoundIO memtype fb = sctBoundedIO memtype (fBound fb) fBacktrack- -- | Fair bound function fBound :: FairBound -> BoundFunc ThreadId ThreadAction Lookahead fBound = fairBound didYield willYield (\act -> case act of Fork t -> [t]; _ -> [])@@ -247,23 +222,17 @@ -- Length bounding  -- | An SCT runner using a length bounding scheduler.-sctLengthBound :: MemType+sctLengthBound :: MonadRef r n+  => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> LengthBound   -- ^ The maximum length of a schedule, in terms of primitive   -- actions.-  -> (forall t. ConcST t a)+  -> Conc n r a   -- ^ The computation to run many times-  -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]+  -> n [(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 ThreadId ThreadAction Lookahead)]-sctLengthBoundIO memtype lb = sctBoundedIO memtype (lenBound lb) lenBacktrack- ------------------------------------------------------------------------------- -- DPOR @@ -279,7 +248,8 @@ -- Note that unlike with non-bounded partial-order reduction, this may -- do some redundant work as the introduction of a bound can make -- previously non-interfering events interfere with each other.-sctBounded :: MemType+sctBounded :: MonadRef r n+  => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.   -> BoundFunc ThreadId ThreadAction Lookahead   -- ^ Check if a prefix trace is within the bound@@ -288,27 +258,9 @@   -- 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 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---- | Variant of 'sctBounded' for computations which do 'IO'.-sctBoundedIO :: MemType-  -> BoundFunc ThreadId ThreadAction Lookahead-  -> BacktrackFunc ThreadId ThreadAction Lookahead DepState-  -> 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---- | Generic SCT runner.-sctBoundedM :: Monad m-  => MemType-  -> ([(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Bool)-  -> BacktrackFunc ThreadId ThreadAction Lookahead DepState-  -> (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 ThreadId ThreadAction Lookahead)]-sctBoundedM memtype bf backtrack run =+  -> Conc n r a+  -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]+sctBounded memtype bf backtrack conc =   dpor didYield        willYield        initialDepState@@ -324,7 +276,7 @@        bf        backtrack        pruneCommits-       (run memtype)+       (\sched s -> runConcurrent sched memtype s conc)  ------------------------------------------------------------------------------- -- Post-processing@@ -345,7 +297,7 @@     onlycommits = all (<initialThread) . M.keys $ dporTodo bpor     alldonesync = all barrier . M.elems $ dporDone bpor -    barrier = isBarrier . simplify . fromJust . dporAction+    barrier = isBarrier . simplifyAction . fromJust . dporAction  ------------------------------------------------------------------------------- -- Dependency function@@ -381,9 +333,9 @@   Just l2     | isSTM a1 && isSTM a2       -> not . S.null $ tvarsOf a1 `S.intersection` tvarsOf a2-    | not (isBlock a1 && isBarrier (simplify' l2)) ->+    | not (isBlock a1 && isBarrier (simplifyLookahead l2)) ->       dependent' memtype ds (t1, a1) (t2, l2)-  _ -> dependentActions memtype ds (simplify a1) (simplify a2)+  _ -> dependentActions memtype ds (simplifyAction a1) (simplifyAction a2)    where     isSTM (STM _ _) = True@@ -403,7 +355,7 @@ #endif    -- Worst-case assumption: all IO is dependent.-  (Lift, WillLift) -> True+  (LiftIO, WillLiftIO) -> True    -- Throwing an exception is only dependent with actions in that   -- thread and if the actions can be interrupted. We can also@@ -429,8 +381,8 @@   -- anyway so there's no point pre-empting the action UNLESS the   -- pre-emption would possibly allow for a different relaxed memory   -- stage.-  _ | isBlock a1 && isBarrier (simplify' l2) -> False-    | otherwise -> dependentActions memtype ds (simplify a1) (simplify' l2)+  _ | isBlock a1 && isBarrier (simplifyLookahead l2) -> False+    | otherwise -> dependentActions memtype ds (simplifyAction a1) (simplifyLookahead l2)  -- | Check if two 'ActionType's are dependent. Note that this is not -- sufficient to know if two 'ThreadAction's are dependent, without@@ -460,7 +412,7 @@     -- 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+    | same mvarOf -> True    _ -> False @@ -508,7 +460,7 @@ updateCRState (CommitRef _ r) = M.delete r updateCRState (WriteRef    r) = M.insert r True updateCRState ta-  | isBarrier $ simplify ta = const M.empty+  | isBarrier $ simplifyAction ta = const M.empty   | otherwise = id  -- | Update the thread masking state with the action that has just

@@ -23,23 +23,20 @@   , TTrace   , TAction(..)   , TVarId-  , runTransactionST-  , runTransactionIO+  , runTransaction   ) where -import Control.Monad (liftM)+import Control.Monad (unless) import Control.Monad.Catch (MonadCatch(..), MonadThrow(..)) import Control.Monad.Cont (cont)+import Control.Monad.Ref (MonadRef) 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--{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}+import Test.DejaFu.Common+import Test.DejaFu.STM.Internal  newtype STMLike n r a = S { runSTM :: M n r a } deriving (Functor, Applicative, Monad) @@ -82,26 +79,14 @@    writeTVar tvar a = toSTM (\c -> SWrite tvar a (c ())) --- | Run a transaction in the 'ST' monad, returning the result and new--- 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 '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, returning the result and new initial+-- 'TVarId'. If the transaction ended by calling 'retry', any 'TVar'+-- modifications are undone.+runTransaction :: MonadRef r n+               => STMLike n r a -> IdSource -> n (Result a, IdSource, TTrace)+runTransaction ma tvid = do+  (res, undo, tvid', trace) <- doTransaction (runSTM ma) tvid --- | Run a transaction in an arbitrary monad.-runTransactionM :: Monad n-  => 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+  unless (isSTMSuccess res) undo -  case res of-    Success _ _ _ -> return (res, tvid', trace)-    _ -> undo >> return (res, tvid, trace)+  pure (res, tvid', trace)

@@ -1,5 +1,6 @@ {-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE RankNTypes                #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}  -- | -- Module      : Test.DejaFu.STM.Internal@@ -16,10 +17,13 @@  import Control.Exception (Exception, SomeException, fromException, toException) import Control.Monad.Cont (Cont, runCont)+import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef) import Data.List (nub)-import Test.DejaFu.Deterministic.Internal.Common (TVarId, IdSource, TAction(..), TTrace, nextTVId)-import Test.DejaFu.Internal +import Test.DejaFu.Common++{-# ANN module ("HLint: ignore Use record patterns" :: String) #-}+ -------------------------------------------------------------------------------- -- The @STMLike@ monad @@ -27,9 +31,6 @@ -- actions. type M n r a = Cont (STMAction n r) a --- | Dict of methods for implementations to override.-type Fixed n r = Ref n r (Cont (STMAction n r))- -------------------------------------------------------------------------------- -- * Primitive actions @@ -41,10 +42,9 @@   | 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 String a (TVar r a -> STMAction n r)-  | SLift (n (STMAction n r))   | forall e. Exception e => SThrow e   | SRetry-  | SStop+  | SStop (n ())  -------------------------------------------------------------------------------- -- * @TVar@s@@ -71,6 +71,11 @@   -- ^ The transaction aborted by throwing an exception.   deriving Show +-- | Check if a 'Result' is a @Success@.+isSTMSuccess :: Result a -> Bool+isSTMSuccess (Success _ _ _) = True+isSTMSuccess _ = False+ instance Functor Result where   fmap f (Success rs ws a) = Success rs ws $ f a   fmap _ (Retry rs)    = Retry rs@@ -84,15 +89,15 @@ -- * Execution  -- | Run a STM transaction, returning an action to undo its effects.-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+doTransaction :: MonadRef r n => M n r a -> IdSource -> n (Result a, n (), IdSource, TTrace)+doTransaction ma idsource = do+  ref <- newRef Nothing -  let c = runCont (ma >>= liftN fixed . writeRef fixed ref . Just . Right) $ const SStop+  let c = runCont ma (SStop . writeRef ref . Just . Right)    (idsource', undo, readen, written, trace) <- go ref c (return ()) idsource [] [] [] -  res <- readRef fixed ref+  res <- readRef ref    case res of     Just (Right val) -> return (Success (nub readen) (nub written) val, undo, idsource', reverse trace)@@ -102,7 +107,7 @@    where     go ref act undo nidsrc readen written sofar = do-      (act', undo', nidsrc', readen', written', tact) <- stepTrans fixed act nidsrc+      (act', undo', nidsrc', readen', written', tact) <- stepTrans act nidsrc        let newIDSource = nidsrc'           newAct = act'@@ -113,25 +118,24 @@        case tact of         TStop  -> return (newIDSource, newUndo, newReaden, newWritten, TStop:newSofar)-        TRetry -> writeRef fixed ref Nothing+        TRetry -> writeRef ref Nothing           >> return (newIDSource, newUndo, newReaden, newWritten, TRetry:newSofar)-        TThrow -> writeRef fixed ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)+        TThrow -> writeRef 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 -> IdSource -> n (STMAction n r, n (), IdSource, [TVarId], [TVarId], TAction)-stepTrans fixed act idsource = case act of+stepTrans :: MonadRef r n => STMAction n r -> IdSource -> n (STMAction n r, n (), IdSource, [TVarId], [TVarId], TAction)+stepTrans act idsource = case act of   SCatch  h stm c -> stepCatch h stm c   SRead   ref c   -> stepRead ref c   SWrite  ref a c -> stepWrite ref a c   SNew    n a c   -> stepNew n a c   SOrElse a b c   -> stepOrElse a b c-  SLift   na      -> stepLift na+  SStop   na      -> stepStop na    SThrow e -> return (SThrow e, nothing, idsource, [], [], TThrow)   SRetry   -> return (SRetry,   nothing, idsource, [], [], TRetry)-  SStop    -> return (SStop,    nothing, idsource, [], [], TStop)    where     nothing = return ()@@ -143,17 +147,17 @@         Nothing   -> return (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing))      stepRead (TVar (tvid, ref)) c = do-      val <- readRef fixed ref+      val <- readRef ref       return (c val, nothing, idsource, [tvid], [], TRead tvid)      stepWrite (TVar (tvid, ref)) a c = do-      old <- readRef fixed ref-      writeRef fixed ref a-      return (c, writeRef fixed ref old, idsource, [], [tvid], TWrite tvid)+      old <- readRef ref+      writeRef ref a+      return (c, writeRef ref old, idsource, [], [tvid], TWrite tvid)      stepNew n a c = do       let (idsource', tvid) = nextTVId n idsource-      ref <- newRef fixed a+      ref <- newRef a       let tvar = TVar (tvid, ref)       return (c tvar, nothing, idsource', [], [tvid], TNew) @@ -161,12 +165,12 @@       (\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, idsource, [], [], TLift)+    stepStop na = do+      na+      return (SStop na, nothing, idsource, [], [], TStop)      cases tact stm onSuccess onRetry onException = do-      (res, undo, idsource', trace) <- doTransaction fixed stm idsource+      (res, undo, idsource', trace) <- doTransaction stm idsource       case res of         Success readen written val -> return (onSuccess val, undo, idsource', readen, written, tact trace Nothing)         Retry readen -> do