diff --git a/Control/Concurrent/Classy.hs b/Control/Concurrent/Classy.hs deleted file mode 100644 --- a/Control/Concurrent/Classy.hs +++ /dev/null @@ -1,40 +0,0 @@ --- | --- Module : Control.Concurrent.Classy --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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) #-} diff --git a/Control/Concurrent/Classy/CRef.hs b/Control/Concurrent/Classy/CRef.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/CRef.hs +++ /dev/null @@ -1,114 +0,0 @@ --- | --- Module : Control.Concurrent.Classy.CRef --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 diff --git a/Control/Concurrent/Classy/Chan.hs b/Control/Concurrent/Classy/Chan.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/Chan.hs +++ /dev/null @@ -1,79 +0,0 @@ --- | --- Module : Control.Concurrent.Classy.Chan --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 diff --git a/Control/Concurrent/Classy/MVar.hs b/Control/Concurrent/Classy/MVar.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/MVar.hs +++ /dev/null @@ -1,128 +0,0 @@ --- | --- Module : Control.Concurrent.Classy.MVar --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 diff --git a/Control/Concurrent/Classy/QSem.hs b/Control/Concurrent/Classy/QSem.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/QSem.hs +++ /dev/null @@ -1,45 +0,0 @@ --- | --- Module : Control.Concurrent.Classy.QSem --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 diff --git a/Control/Concurrent/Classy/QSemN.hs b/Control/Concurrent/Classy/QSemN.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/QSemN.hs +++ /dev/null @@ -1,97 +0,0 @@ --- | --- Module : Control.Concurrent.Classy.QSemN --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 diff --git a/Control/Concurrent/Classy/STM.hs b/Control/Concurrent/Classy/STM.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/STM.hs +++ /dev/null @@ -1,28 +0,0 @@ --- | --- Module : Control.Concurrent.Classy.STM --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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) #-} diff --git a/Control/Concurrent/Classy/STM/TArray.hs b/Control/Concurrent/Classy/STM/TArray.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/STM/TArray.hs +++ /dev/null @@ -1,56 +0,0 @@ -{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-} - --- | --- Module : Control.Concurrent.Classy.STM. --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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) diff --git a/Control/Concurrent/Classy/STM/TBQueue.hs b/Control/Concurrent/Classy/STM/TBQueue.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/STM/TBQueue.hs +++ /dev/null @@ -1,146 +0,0 @@ --- | --- Module : Control.Concurrent.Classy.STM.TBQueue --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 diff --git a/Control/Concurrent/Classy/STM/TChan.hs b/Control/Concurrent/Classy/STM/TChan.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/STM/TChan.hs +++ /dev/null @@ -1,135 +0,0 @@ --- | --- Module : Control.Concurrent.Classy.STM.TChan --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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) diff --git a/Control/Concurrent/Classy/STM/TMVar.hs b/Control/Concurrent/Classy/STM/TMVar.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/STM/TMVar.hs +++ /dev/null @@ -1,118 +0,0 @@ --- | --- Module : Control.Concurrent.Classy.STM.TMVar --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 diff --git a/Control/Concurrent/Classy/STM/TQueue.hs b/Control/Concurrent/Classy/STM/TQueue.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/STM/TQueue.hs +++ /dev/null @@ -1,113 +0,0 @@ --- | --- Module : Control.Concurrent.Classy.STM.TQueue --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 diff --git a/Control/Concurrent/Classy/STM/TVar.hs b/Control/Concurrent/Classy/STM/TVar.hs deleted file mode 100644 --- a/Control/Concurrent/Classy/STM/TVar.hs +++ /dev/null @@ -1,62 +0,0 @@ --- | --- Module : Control.Concurrent.Classy.STM.TVar --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 diff --git a/Control/Monad/Conc/Class.hs b/Control/Monad/Conc/Class.hs deleted file mode 100644 --- a/Control/Monad/Conc/Class.hs +++ /dev/null @@ -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 --- 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)) diff --git a/Control/Monad/STM/Class.hs b/Control/Monad/STM/Class.hs deleted file mode 100644 --- a/Control/Monad/STM/Class.hs +++ /dev/null @@ -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 --- 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' diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs --- a/Test/DejaFu.hs +++ b/Test/DejaFu.hs @@ -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 diff --git a/Test/DejaFu/Common.hs b/Test/DejaFu/Common.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Common.hs @@ -0,0 +1,746 @@ +-- | +-- Module : Test.DejaFu.Common +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- 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) diff --git a/Test/DejaFu/Conc.hs b/Test/DejaFu/Conc.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Conc.hs @@ -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 +-- 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) diff --git a/Test/DejaFu/Conc/Internal.hs b/Test/DejaFu/Conc/Internal.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Conc/Internal.hs @@ -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 +-- 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 diff --git a/Test/DejaFu/Conc/Internal/Common.hs b/Test/DejaFu/Conc/Internal/Common.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Conc/Internal/Common.hs @@ -0,0 +1,172 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE RankNTypes #-} + +-- | +-- Module : Test.DejaFu.Conc.Internal.Common +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- 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] diff --git a/Test/DejaFu/Conc/Internal/Memory.hs b/Test/DejaFu/Conc/Internal/Memory.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Conc/Internal/Memory.hs @@ -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 +-- 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, []) diff --git a/Test/DejaFu/Conc/Internal/Threading.hs b/Test/DejaFu/Conc/Internal/Threading.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Conc/Internal/Threading.hs @@ -0,0 +1,143 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE RankNTypes #-} + +-- | +-- Module : Test.DejaFu.Conc.Internal.Threading +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- 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 diff --git a/Test/DejaFu/Deterministic.hs b/Test/DejaFu/Deterministic.hs deleted file mode 100644 --- a/Test/DejaFu/Deterministic.hs +++ /dev/null @@ -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 --- 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 --- --- --- __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) diff --git a/Test/DejaFu/Deterministic/Internal.hs b/Test/DejaFu/Deterministic/Internal.hs deleted file mode 100644 --- a/Test/DejaFu/Deterministic/Internal.hs +++ /dev/null @@ -1,475 +0,0 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} - --- | --- Module : Test.DejaFu.Deterministic.Internal --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 diff --git a/Test/DejaFu/Deterministic/Internal/Common.hs b/Test/DejaFu/Deterministic/Internal/Common.hs deleted file mode 100644 --- a/Test/DejaFu/Deterministic/Internal/Common.hs +++ /dev/null @@ -1,873 +0,0 @@ -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE RankNTypes #-} - --- | --- Module : Test.DejaFu.Deterministic.Internal.Common --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 diff --git a/Test/DejaFu/Deterministic/Internal/Memory.hs b/Test/DejaFu/Deterministic/Internal/Memory.hs deleted file mode 100644 --- a/Test/DejaFu/Deterministic/Internal/Memory.hs +++ /dev/null @@ -1,208 +0,0 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE GADTs #-} - --- | --- Module : Test.DejaFu.Deterministic.Internal.Memory --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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, []) diff --git a/Test/DejaFu/Deterministic/Internal/Threading.hs b/Test/DejaFu/Deterministic/Internal/Threading.hs deleted file mode 100644 --- a/Test/DejaFu/Deterministic/Internal/Threading.hs +++ /dev/null @@ -1,200 +0,0 @@ -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE RankNTypes #-} - --- | --- Module : Test.DejaFu.Deterministic.Internal.Threading --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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!" diff --git a/Test/DejaFu/Internal.hs b/Test/DejaFu/Internal.hs deleted file mode 100644 --- a/Test/DejaFu/Internal.hs +++ /dev/null @@ -1,43 +0,0 @@ -{-# LANGUAGE RankNTypes #-} - --- | --- Module : Test.DejaFu.Internal --- Copyright : (c) 2016 Michael Walker --- License : MIT --- Maintainer : Michael Walker --- 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 - } diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -1,5 +1,4 @@ {-# LANGUAGE CPP #-} -{-# LANGUAGE RankNTypes #-} -- | -- Module : Test.DejaFu.SCT @@ -7,7 +6,7 @@ -- License : MIT -- Maintainer : Michael Walker -- 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 ( 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 diff --git a/Test/DejaFu/STM.hs b/Test/DejaFu/STM.hs --- a/Test/DejaFu/STM.hs +++ b/Test/DejaFu/STM.hs @@ -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) diff --git a/Test/DejaFu/STM/Internal.hs b/Test/DejaFu/STM/Internal.hs --- a/Test/DejaFu/STM/Internal.hs +++ b/Test/DejaFu/STM/Internal.hs @@ -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 diff --git a/dejafu.cabal b/dejafu.cabal --- a/dejafu.cabal +++ b/dejafu.cabal @@ -2,8 +2,8 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu -version: 0.3.2.1 -synopsis: Overloadable primitives for testable, potentially non-deterministic, concurrency. +version: 0.4.0.0 +synopsis: Systematic testing for Haskell concurrency. description: /[Déjà Fu is] A martial art in which the user's limbs move in time as well as space, […] It is best described as "the feeling that you have been kicked in the head this way before"/ -- Terry Pratchett, Thief of Time @@ -14,18 +14,17 @@ provides deterministic parallelism, but sometimes we can tolerate a bit of nondeterminism. . - This package provides a class of monads for potentially - nondeterministic concurrency, with an interface in the spirit of - GHC's normal concurrency abstraction. + This package builds on the + + package by enabling you to systematically and deterministically test + your concurrent programs. . - == @MonadConc@ with 'IO': + == Déjà Fu with 'IO': . - The intention of the @MonadConc@ class is to provide concurrency - where any apparent nondeterminism arises purely from the scheduling - behaviour. To put it another way, a given computation, parametrised - with a fixed set of scheduling decisions, is deterministic. This - assumption is used by the testing functionality provided by - Test.DejaFu. + The core assumption underlying Déjà Fu is that any apparent + nondeterminism arises purely from the scheduling behaviour. To put + it another way, a given computation, parametrised with a fixed set + of scheduling decisions, is deterministic. . Whilst this assumption may not hold in general when 'IO' is involved, you should strive to produce test cases where it does. @@ -75,53 +74,33 @@ source-repository this type: git location: https://github.com/barrucadu/dejafu.git - tag: dejafu-0.3.2.1 + tag: dejafu-0.4.0.0 library - exposed-modules: Control.Monad.Conc.Class - , Control.Monad.STM.Class - - , Control.Concurrent.Classy - , Control.Concurrent.Classy.Chan - , Control.Concurrent.Classy.CRef - , Control.Concurrent.Classy.MVar - , Control.Concurrent.Classy.QSem - , Control.Concurrent.Classy.QSemN - , Control.Concurrent.Classy.STM - , Control.Concurrent.Classy.STM.TVar - , Control.Concurrent.Classy.STM.TMVar - , Control.Concurrent.Classy.STM.TChan - , Control.Concurrent.Classy.STM.TQueue - , Control.Concurrent.Classy.STM.TBQueue - , Control.Concurrent.Classy.STM.TArray - - , Test.DejaFu - , Test.DejaFu.Deterministic + exposed-modules: Test.DejaFu + , Test.DejaFu.Conc + , Test.DejaFu.Common , Test.DejaFu.SCT , Test.DejaFu.STM - , Test.DejaFu.Deterministic.Internal - , Test.DejaFu.Deterministic.Internal.Common - , Test.DejaFu.Deterministic.Internal.Memory - , Test.DejaFu.Deterministic.Internal.Threading - , Test.DejaFu.Internal + , Test.DejaFu.Conc.Internal + , Test.DejaFu.Conc.Internal.Common + , Test.DejaFu.Conc.Internal.Memory + , Test.DejaFu.Conc.Internal.Threading , Test.DejaFu.STM.Internal -- other-modules: -- other-extensions: build-depends: base >=4.8 && <5 - , array >=0.5 && <0.6 - , atomic-primops >=0.8 && <0.9 + , concurrency >=1.0 && <1.1 , containers >=0.5 && <0.6 - , dpor >=0.1 && <0.3 , deepseq >=1.3 && <1.5 + , dpor >=0.1 && <0.3 , exceptions >=0.7 && <0.9 - , monad-control >=1.0 && <1.1 , monad-loops >=0.4 && <0.5 , mtl >=2.2 && <2.3 + , ref-fd >=0.4 && <0.5 , semigroups >=0.16 && <0.19 - , stm >=2.4 && <2.5 - , template-haskell >=2.10 && <2.12 , transformers >=0.4 && <0.6 , transformers-base >=0.4 && <0.5 -- hs-source-dirs: