diff --git a/Control/Concurrent/CVar.hs b/Control/Concurrent/CVar.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CVar.hs @@ -0,0 +1,123 @@ +-- | Combinators using @CVar@s. These provide many of the helpful +-- functions found in Control.Concurrent.MVar, but for @CVar@s. +module Control.Concurrent.CVar + ( -- *@CVar@s + CVar + , newEmptyCVar + , newCVar + , takeCVar + , putCVar + , readCVar + , swapCVar + , tryTakeCVar + , tryPutCVar + , isEmptyCVar + , withCVar + , withCVarMasked + , modifyCVar_ + , modifyCVar + , modifyCVarMasked_ + , modifyCVarMasked + + -- * Binary semaphores + -- | A common use of @CVar@s is in making binary semaphores to + -- control mutual exclusion over a resource, so a couple of helper + -- functions are provided. + , lock + , unlock + ) where + +import Control.Monad (liftM) +import Control.Monad.Catch (mask_, onException) +import Control.Monad.Conc.Class + +-- | Create a new @CVar@ containing a value. +newCVar :: MonadConc m => a -> m (CVar m a) +newCVar a = do + cvar <- newEmptyCVar + putCVar cvar a + return cvar + +-- | Swap the contents of a @CVar@, and return the value taken. This +-- function is atomic only if there are no other producers fro this +-- @CVar@. +swapCVar :: MonadConc m => CVar m a -> a -> m a +swapCVar cvar a = mask_ $ do + old <- takeCVar cvar + putCVar cvar a + return old + +-- | Check if a @CVar@ is empty. +isEmptyCVar :: MonadConc m => CVar m a -> m Bool +isEmptyCVar cvar = do + val <- tryTakeCVar cvar + case val of + Just val' -> putCVar cvar val' >> return True + Nothing -> return False + +-- | Operate on the contents of a @CVar@, replacing the contents after +-- finishing. This operation is exception-safe: it will replace the +-- original contents of the @CVar@ if an exception is raised. However, +-- it is only atomic if there are no other producers for this @CVar@. +{-# INLINE withCVar #-} +withCVar :: MonadConc m => CVar m a -> (a -> m b) -> m b +withCVar cvar f = mask $ \restore -> do + val <- takeCVar cvar + out <- restore (f val) `onException` putCVar cvar val + putCVar cvar val + + return out + +-- | Like 'withCVar', but the @IO@ action in the second argument is +-- executed with asynchronous exceptions masked. +{-# INLINE withCVarMasked #-} +withCVarMasked :: MonadConc m => CVar m a -> (a -> m b) -> m b +withCVarMasked cvar f = mask_ $ do + val <- takeCVar cvar + out <- f val `onException` putCVar cvar val + putCVar cvar val + + return out + +-- | An exception-safe wrapper for modifying the contents of a @CVar@. +-- Like 'withCVar', 'modifyCVar' will replace the original contents of +-- the @CVar@ if an exception is raised during the operation. This +-- function is only atomic if there are no other producers for this +-- @CVar@. +{-# INLINE modifyCVar_ #-} +modifyCVar_ :: MonadConc m => CVar m a -> (a -> m a) -> m () +modifyCVar_ cvar f = modifyCVar cvar $ liftM (\a -> (a,())) . f + +-- | A slight variation on 'modifyCVar_' that allows a value to be +-- returned (@b@) in addition to the modified value of the @CVar@. +{-# INLINE modifyCVar #-} +modifyCVar :: MonadConc m => CVar m a -> (a -> m (a, b)) -> m b +modifyCVar cvar f = mask $ \restore -> do + val <- takeCVar cvar + (val', out) <- restore (f val) `onException` putCVar cvar val + putCVar cvar val' + return out + +-- | Like 'modifyCVar_', but the @IO@ action in the second argument is +-- executed with asynchronous exceptions masked. +{-# INLINE modifyCVarMasked_ #-} +modifyCVarMasked_ :: MonadConc m => CVar m a -> (a -> m a) -> m () +modifyCVarMasked_ cvar f = modifyCVarMasked cvar $ liftM (\a -> (a,())) . f + +-- | Like 'modifyCVar', but the @IO@ action in the second argument is +-- executed with asynchronous exceptions masked. +{-# INLINE modifyCVarMasked #-} +modifyCVarMasked :: MonadConc m => CVar m a -> (a -> m (a, b)) -> m b +modifyCVarMasked cvar f = mask_ $ do + val <- takeCVar cvar + (val', out) <- f val `onException` putCVar cvar val + putCVar cvar val' + return out + +-- | Put a @()@ into a @CVar@, claiming the lock. This is atomic. +lock :: MonadConc m => CVar m () -> m () +lock = flip putCVar () + +-- | Empty a @CVar@, releasing the lock. This is atomic. +unlock :: MonadConc m => CVar m () -> m () +unlock = takeCVar diff --git a/Control/Concurrent/CVar/Strict.hs b/Control/Concurrent/CVar/Strict.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CVar/Strict.hs @@ -0,0 +1,97 @@ +-- | Strict alternatives to the functions in +-- Control.Monad.Conc.CVar. Specifically, values are evaluated to +-- normal form before being put into a @CVar@. +module Control.Concurrent.CVar.Strict + ( -- *@CVar@s + CVar + , newEmptyCVar + , newCVar + , takeCVar + , putCVar + , readCVar + , swapCVar + , tryTakeCVar + , tryPutCVar + , isEmptyCVar + , withCVar + , withCVarMasked + , modifyCVar_ + , modifyCVar + , modifyCVarMasked_ + , modifyCVarMasked + + -- * Binary semaphores + -- | A common use of @CVar@s is in making binary semaphores to + -- control mutual exclusion over a resource, so a couple of helper + -- functions are provided. + , lock + , unlock + ) where + +import Control.Concurrent.CVar (isEmptyCVar, withCVar, withCVarMasked, lock, unlock) +import Control.DeepSeq (NFData, force) +import Control.Monad (liftM) +import Control.Monad.Catch (mask_, onException) +import Control.Monad.Conc.Class hiding (newEmptyCVar, putCVar, tryPutCVar) + +import qualified Control.Concurrent.CVar as V +import qualified Control.Monad.Conc.Class as C + +-- | Create a new empty @CVar@. +newEmptyCVar :: (MonadConc m, NFData a) => m (CVar m a) +newEmptyCVar = C.newEmptyCVar + +-- | Create a new @CVar@ containing a value. +newCVar :: (MonadConc m, NFData a) => a -> m (CVar m a) +newCVar = V.newCVar . force + +-- | Swap the contents of a @CVar@, and return the value taken. +swapCVar :: (MonadConc m, NFData a) => CVar m a -> a -> m a +swapCVar cvar = V.swapCVar cvar . force + +-- | Put a value into a @CVar@. If there is already a value there, +-- this will block until that value has been taken, at which point the +-- value will be stored. +putCVar :: (MonadConc m, NFData a) => CVar m a -> a -> m () +putCVar cvar = C.putCVar cvar . force + +-- | Attempt to put a value in a @CVar@, returning 'True' (and filling +-- the @CVar@) if there was nothing there, otherwise returning +-- 'False'. +tryPutCVar :: (MonadConc m, NFData a) => CVar m a -> a -> m Bool +tryPutCVar cvar = C.tryPutCVar cvar . force + +-- | An exception-safe wrapper for modifying the contents of a @CVar@. +-- Like 'withCVar', 'modifyCVar' will replace the original contents of +-- the @CVar@ if an exception is raised during the operation. This +-- function is only atomic if there are no other producers for this +-- @CVar@. +{-# INLINE modifyCVar_ #-} +modifyCVar_ :: (MonadConc m, NFData a) => CVar m a -> (a -> m a) -> m () +modifyCVar_ cvar f = modifyCVar cvar $ liftM (\a -> (a,())) . f + +-- | A slight variation on 'modifyCVar_' that allows a value to be +-- returned (@b@) in addition to the modified value of the @CVar@. +{-# INLINE modifyCVar #-} +modifyCVar :: (MonadConc m, NFData a) => CVar m a -> (a -> m (a, b)) -> m b +modifyCVar cvar f = mask $ \restore -> do + val <- takeCVar cvar + (val', out) <- restore (f val) `onException` putCVar cvar val + putCVar cvar val' + return out + +-- | Like 'modifyCVar_', but the @IO@ action in the second argument is +-- executed with asynchronous exceptions masked. +{-# INLINE modifyCVarMasked_ #-} +modifyCVarMasked_ :: (MonadConc m, NFData a) => CVar m a -> (a -> m a) -> m () +modifyCVarMasked_ cvar f = modifyCVarMasked cvar $ liftM (\a -> (a,())) . f + +-- | Like 'modifyCVar', but the @IO@ action in the second argument is +-- executed with asynchronous exceptions masked. +{-# INLINE modifyCVarMasked #-} +modifyCVarMasked :: (MonadConc m, NFData a) => CVar m a -> (a -> m (a, b)) -> m b +modifyCVarMasked cvar f = mask_ $ do + val <- takeCVar cvar + (val', out) <- f val `onException` putCVar cvar val + putCVar cvar val' + return out diff --git a/Control/Concurrent/STM/CTMVar.hs b/Control/Concurrent/STM/CTMVar.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/STM/CTMVar.hs @@ -0,0 +1,86 @@ +-- | Transactional @CVar@s, for use with 'MonadSTM'. +module Control.Concurrent.STM.CTMVar + ( -- * @CTMVar@s + CTMVar + , newCTMVar + , newEmptyCTMVar + , takeCTMVar + , putCTMVar + , readCTMVar + , tryTakeCTMVar + , tryPutCTMVar + , tryReadCTMVar + , isEmptyCTMVar + , swapCTMVar + ) where + +import Control.Monad (liftM, when, unless) +import Control.Monad.STM.Class +import Data.Maybe (isJust, isNothing) + +-- | A @CTMVar@ is like an @MVar@ or a @CVar@, but using transactional +-- memory. As transactions are atomic, this makes dealing with +-- multiple @CTMVar@s easier than wrangling multiple @CVar@s. +newtype CTMVar m a = CTMVar (CTVar m (Maybe a)) + +-- | Create a 'CTMVar' containing the given value. +newCTMVar :: MonadSTM m => a -> m (CTMVar m a) +newCTMVar a = do + ctvar <- newCTVar $ Just a + return $ CTMVar ctvar + +-- | Create a new empty 'CTMVar'. +newEmptyCTMVar :: MonadSTM m => m (CTMVar m a) +newEmptyCTMVar = do + ctvar <- newCTVar Nothing + return $ CTMVar ctvar + +-- | Take the contents of a 'CTMVar', or 'retry' if it is empty. +takeCTMVar :: MonadSTM m => CTMVar m a -> m a +takeCTMVar ctmvar = do + taken <- tryTakeCTMVar ctmvar + maybe retry return taken + +-- | Write to a 'CTMVar', or 'retry' if it is full. +putCTMVar :: MonadSTM m => CTMVar m a -> a -> m () +putCTMVar ctmvar a = do + putted <- tryPutCTMVar ctmvar a + unless putted retry + +-- | Read from a 'CTMVar' without emptying, or 'retry' if it is empty. +readCTMVar :: MonadSTM m => CTMVar m a -> m a +readCTMVar ctmvar = do + readed <- tryReadCTMVar ctmvar + maybe retry return readed + +-- | Try to take the contents of a 'CTMVar', returning 'Nothing' if it +-- is empty. +tryTakeCTMVar :: MonadSTM m => CTMVar m a -> m (Maybe a) +tryTakeCTMVar (CTMVar ctvar) = do + val <- readCTVar ctvar + when (isJust val) $ writeCTVar ctvar Nothing + return val + +-- | Try to write to a 'CTMVar', returning 'False' if it is full. +tryPutCTMVar :: MonadSTM m => CTMVar m a -> a -> m Bool +tryPutCTMVar (CTMVar ctvar) a = do + val <- readCTVar ctvar + when (isNothing val) $ writeCTVar ctvar (Just a) + return $ isNothing val + +-- | Try to read from a 'CTMVar' without emptying, returning 'Nothing' +-- if it is empty. +tryReadCTMVar :: MonadSTM m => CTMVar m a -> m (Maybe a) +tryReadCTMVar (CTMVar ctvar) = readCTVar ctvar + +-- | Check if a 'CTMVar' is empty or not. +isEmptyCTMVar :: MonadSTM m => CTMVar m a -> m Bool +isEmptyCTMVar ctmvar = isNothing `liftM` tryReadCTMVar ctmvar + +-- | Swap the contents of a 'CTMVar' returning the old contents, or +-- 'retry' if it is empty. +swapCTMVar :: MonadSTM m => CTMVar m a -> a -> m a +swapCTMVar ctmvar a = do + val <- takeCTMVar ctmvar + putCTMVar ctmvar a + return val diff --git a/Control/Concurrent/STM/CTVar.hs b/Control/Concurrent/STM/CTVar.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/STM/CTVar.hs @@ -0,0 +1,34 @@ +-- | Transactional variables, for use with 'MonadSTM'. +module Control.Concurrent.STM.CTVar + ( -- * @CTVar@s + CTVar + , newCTVar + , readCTVar + , writeCTVar + , modifyCTVar + , modifyCTVar' + , swapCTVar + ) where + +import Control.Monad.STM.Class + +-- * @CTVar@s + +-- | Mutate the contents of a 'CTVar'. This is non-strict. +modifyCTVar :: MonadSTM m => CTVar m a -> (a -> a) -> m () +modifyCTVar ctvar f = do + a <- readCTVar ctvar + writeCTVar ctvar $ f a + +-- | Mutate the contents of a 'CTVar' strictly. +modifyCTVar' :: MonadSTM m => CTVar m a -> (a -> a) -> m () +modifyCTVar' ctvar f = do + a <- readCTVar ctvar + writeCTVar ctvar $! f a + +-- | Swap the contents of a 'CTVar', returning the old value. +swapCTVar :: MonadSTM m => CTVar m a -> a -> m a +swapCTVar ctvar a = do + old <- readCTVar ctvar + writeCTVar ctvar a + return old diff --git a/Control/Monad/Conc/Class.hs b/Control/Monad/Conc/Class.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Conc/Class.hs @@ -0,0 +1,536 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} + +-- | This module captures in a typeclass the interface of concurrency +-- monads. +module Control.Monad.Conc.Class + ( MonadConc(..) + -- * Utilities + , spawn + , forkFinally + , killThread + ) where + +import Control.Concurrent (forkIO) +import Control.Concurrent.MVar (MVar, readMVar, newEmptyMVar, putMVar, tryPutMVar, takeMVar, tryTakeMVar) +import Control.Exception (Exception, AsyncException(ThreadKilled), SomeException) +import Control.Monad (liftM) +import Control.Monad.Catch (MonadCatch, MonadThrow, MonadMask) +import Control.Monad.Reader (ReaderT(..), runReaderT) +import Control.Monad.STM (STM) +import Control.Monad.STM.Class (MonadSTM, CTVar) +import Control.Monad.Trans (lift) +import Data.IORef (IORef, atomicModifyIORef, newIORef, readIORef) + +import qualified Control.Concurrent as C +import qualified Control.Monad.Catch as Ca +import qualified Control.Monad.RWS.Lazy as RL +import qualified Control.Monad.RWS.Strict as RS +import qualified Control.Monad.STM as S +import qualified Control.Monad.State.Lazy as SL +import qualified Control.Monad.State.Strict as SS +import qualified Control.Monad.Writer.Lazy as WL +import qualified Control.Monad.Writer.Strict as WS + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative (Applicative) +import Data.Monoid (Monoid, mempty) +#endif + +-- | @MonadConc@ is an abstraction over GHC's typical concurrency +-- abstraction. It captures the interface of concurrency monads in +-- terms of how they can operate on shared state and in the presence +-- of exceptions. +-- +-- There are a few notable differences between this and the @Par@ +-- monad approach: firstly, @Par@ imposes 'NFData' constraints on +-- everything, as it achieves its speed-up by forcing evaluation in +-- separate threads. @MonadConc@ doesn't do that, and so you need to +-- be careful about where evaluation occurs, just like with +-- 'MVar's. Secondly, this builds on @Par@'s futures by allowing +-- @CVar@s which threads can read from and write to, possibly multiple +-- times, whereas with the @Par@ monads it is illegal to write +-- multiple times to the same @IVar@ (or to non-blockingly read from +-- it) which, when there are no exceptions, removes the possibility of +-- data races. +-- +-- Every @MonadConc@ has an associated 'MonadSTM', transactions of +-- which can be run atomically. +class ( Applicative m, Monad m + , MonadCatch m, MonadThrow m, MonadMask m + , MonadSTM (STMLike m) + , Eq (ThreadId m), Show (ThreadId m)) => MonadConc m where + -- | The associated 'MonadSTM' for this class. + type STMLike m :: * -> * + + -- | The mutable reference type, like 'MVar's. This may contain one + -- value at a time, attempting to read or take from an \"empty\" + -- @CVar@ will block until it is full, and attempting to put to a + -- \"full\" @CVar@ will block until it is empty. + type CVar m :: * -> * + + -- | The mutable non-blocking reference type. These are like + -- 'IORef's, but don't have the potential re-ordering problem + -- mentioned in Data.IORef. + type CRef m :: * -> * + + -- | An abstract handle to a thread. + type ThreadId m :: * + + -- | Fork a computation to happen concurrently. Communication may + -- happen over @CVar@s. + fork :: m () -> m (ThreadId m) + + -- | Like 'fork', but the child thread is passed a function that can + -- be used to unmask asynchronous exceptions. This function should + -- not be used within a 'mask' or 'uninterruptibleMask'. + forkWithUnmask :: ((forall a. m a -> m a) -> m ()) -> m (ThreadId m) + + -- | Fork a computation to happen on a specific processor. The + -- specified int is the /capability number/, typically capabilities + -- correspond to physical processors or cores but this is + -- implementation dependent. The int is interpreted modulo to the + -- total number of capabilities as returned by 'getNumCapabilities'. + forkOn :: Int -> m () -> m (ThreadId m) + + -- | Get the number of Haskell threads that can run simultaneously. + getNumCapabilities :: m Int + + -- | Get the @ThreadId@ of the current thread. + myThreadId :: m (ThreadId m) + + -- | Create a new empty @CVar@. + newEmptyCVar :: m (CVar m a) + + -- | Put a value into a @CVar@. If there is already a value there, + -- this will block until that value has been taken, at which point + -- the value will be stored. + putCVar :: CVar m a -> a -> m () + + -- | Attempt to put a value in a @CVar@ non-blockingly, returning + -- 'True' (and filling the @CVar@) if there was nothing there, + -- otherwise returning 'False'. + tryPutCVar :: CVar m a -> a -> m Bool + + -- | Block until a value is present in the @CVar@, and then return + -- it. As with 'readMVar', this does not \"remove\" the value, + -- multiple reads are possible. + readCVar :: CVar m a -> m a + + -- | Take a value from a @CVar@. This \"empties\" the @CVar@, + -- allowing a new value to be put in. This will block if there is no + -- value in the @CVar@ already, until one has been put. + takeCVar :: CVar m a -> m a + + -- | Attempt to take a value from a @CVar@ non-blockingly, returning + -- a 'Just' (and emptying the @CVar@) if there was something there, + -- otherwise returning 'Nothing'. + tryTakeCVar :: CVar m a -> m (Maybe a) + + -- | Create a new reference. + newCRef :: a -> m (CRef m a) + + -- | Read the current value stored in a reference. + readCRef :: CRef m a -> m a + + -- | Atomically modify the value stored in a reference. + modifyCRef :: CRef m a -> (a -> (a, b)) -> m b + + -- | Replace the value stored in a reference. + -- + -- > writeCRef r a = modifyCRef r $ const (a, ()) + writeCRef :: CRef m a -> a -> m () + writeCRef r a = modifyCRef r $ const (a, ()) + + -- | Perform an STM transaction atomically. + atomically :: STMLike m a -> m a + + -- | Throw an exception. This will \"bubble up\" looking for an + -- exception handler capable of dealing with it and, if one is not + -- found, the thread is killed. + -- + -- > throw = Control.Monad.Catch.throwM + throw :: Exception e => e -> m a + throw = Ca.throwM + + -- | Catch an exception. This is only required to be able to catch + -- exceptions raised by 'throw', unlike the more general + -- Control.Exception.catch function. If you need to be able to catch + -- /all/ errors, you will have to use 'IO'. + -- + -- > catch = Control.Monad.Catch.catch + catch :: Exception e => m a -> (e -> m a) -> m a + catch = Ca.catch + + -- | Throw an exception to the target thread. This blocks until the + -- exception is delivered, and it is just as if the target thread + -- had raised it with 'throw'. This can interrupt a blocked action. + throwTo :: Exception e => ThreadId m -> e -> m () + + -- | Executes a computation with asynchronous exceptions + -- /masked/. That is, any thread which attempts to raise an + -- exception in the current thread with 'throwTo' will be blocked + -- until asynchronous exceptions are unmasked again. + -- + -- The argument passed to mask is a function that takes as its + -- argument another function, which can be used to restore the + -- prevailing masking state within the context of the masked + -- computation. This function should not be used within an + -- 'uninterruptibleMask'. + -- + -- > mask = Control.Monad.Catch.mask + mask :: ((forall a. m a -> m a) -> m b) -> m b + mask = Ca.mask + + -- | Like 'mask', but the masked computation is not + -- interruptible. THIS SHOULD BE USED WITH GREAT CARE, because if a + -- thread executing in 'uninterruptibleMask' blocks for any reason, + -- then the thread (and possibly the program, if this is the main + -- thread) will be unresponsive and unkillable. This function should + -- only be necessary if you need to mask exceptions around an + -- interruptible operation, and you can guarantee that the + -- interruptible operation will only block for a short period of + -- time. The supplied unmasking function should not be used within a + -- 'mask'. + -- + -- > uninterruptibleMask = Control.Monad.Catch.uninterruptibleMask + uninterruptibleMask :: ((forall a. m a -> m a) -> m b) -> m b + uninterruptibleMask = Ca.uninterruptibleMask + + -- | Runs its argument, just as if the @_concNoTest@ weren't there. + -- + -- This function is purely for testing purposes, and indicates that + -- it's not worth considering more than one schedule here. This is + -- useful if you have some larger computation built up out of + -- subcomputations which you have already got tests for: you only + -- want to consider what's unique to the large component. + -- + -- The test runner will report a failure if the argument fails. + -- + -- Note that inappropriate use of @_concNoTest@ can actually + -- /suppress/ bugs! For this reason it is recommended to use it only + -- for things which don't make use of any state from a larger + -- scope. As a rule-of-thumb: if you can't define it as a top-level + -- function taking no @CVRef@, @CVar@, or @CTVar@ arguments, you + -- probably shouldn't @_concNoTest@ it. + -- + -- > _concNoTest x = x + _concNoTest :: m a -> m a + _concNoTest = id + + -- | Does nothing. + -- + -- This function is purely for testing purposes, and indicates that + -- the thread has a reference to the provided @CVar@ or + -- @CTVar@. This function may be called multiple times, to add new + -- knowledge to the system. It does not need to be called when + -- @CVar@s or @CTVar@s are created, these get recorded + -- automatically. + -- + -- Gathering this information allows detection of cases where the + -- main thread is blocked on a variable no runnable thread has a + -- reference to, which is a deadlock situation. + -- + -- > _concKnowsAbout _ = return () + _concKnowsAbout :: Either (CVar m a) (CTVar (STMLike m) a) -> m () + _concKnowsAbout _ = return () + + -- | Does nothing. + -- + -- The counterpart to '_concKnowsAbout'. Indicates that the + -- referenced variable will never be touched again by the current + -- thread. + -- + -- Note that inappropriate use of @_concForgets@ can result in false + -- positives! Be very sure that the current thread will /never/ + -- refer to the variable again, for instance when leaving its scope. + -- + -- > _concForgets _ = return () + _concForgets :: Either (CVar m a) (CTVar (STMLike m) a) -> m () + _concForgets _ = return () + + -- | Does nothing. + -- + -- Indicates to the test runner that all variables which have been + -- passed in to this thread have been recorded by calls to + -- '_concKnowsAbout'. If every thread has called '_concAllKnown', + -- then detection of nonglobal deadlock is turned on. + -- + -- If a thread receives references to @CVar@s or @CTVar@s in the + -- future (for instance, if one was sent over a channel), then + -- '_concKnowsAbout' should be called immediately, otherwise there + -- is a risk of identifying false positives. + -- + -- > _concAllKnown = return () + _concAllKnown :: m () + _concAllKnown = return () + +instance MonadConc IO where + type STMLike IO = STM + type CVar IO = MVar + type CRef IO = IORef + type ThreadId IO = C.ThreadId + + readCVar = readMVar + fork = forkIO + forkWithUnmask = C.forkIOWithUnmask + forkOn = C.forkOn + getNumCapabilities = C.getNumCapabilities + myThreadId = C.myThreadId + throwTo = C.throwTo + newEmptyCVar = newEmptyMVar + putCVar = putMVar + tryPutCVar = tryPutMVar + takeCVar = takeMVar + tryTakeCVar = tryTakeMVar + newCRef = newIORef + readCRef = readIORef + modifyCRef = atomicModifyIORef + atomically = S.atomically + +-- | Create a concurrent computation for the provided action, and +-- return a @CVar@ which can be used to query the result. +spawn :: MonadConc m => m a -> m (CVar m a) +spawn ma = do + cvar <- newEmptyCVar + _ <- fork $ _concKnowsAbout (Left cvar) >> ma >>= putCVar cvar + return cvar + +-- | Fork a thread and call the supplied function when the thread is +-- about to terminate, with an exception or a returned value. The +-- function is called with asynchronous exceptions masked. +-- +-- This function is useful for informing the parent when a child +-- terminates, for example. +forkFinally :: MonadConc m => m a -> (Either SomeException a -> m ()) -> m (ThreadId m) +forkFinally action and_then = + mask $ \restore -> + fork $ Ca.try (restore action) >>= and_then + +-- | Raise the 'ThreadKilled' exception in the target thread. Note +-- that if the thread is prepared to catch this exception, it won't +-- actually kill it. +killThread :: MonadConc m => ThreadId m -> m () +killThread tid = throwTo tid ThreadKilled + +------------------------------------------------------------------------------- +-- Transformer instances + +instance MonadConc m => MonadConc (ReaderT r m) where + type STMLike (ReaderT r m) = STMLike m + type CVar (ReaderT r m) = CVar m + type CRef (ReaderT r m) = CRef m + type ThreadId (ReaderT r m) = ThreadId m + + fork = reader fork + forkOn i = reader (forkOn i) + forkWithUnmask ma = ReaderT $ \r -> forkWithUnmask (\f -> runReaderT (ma $ reader f) r) + _concNoTest = reader _concNoTest + + getNumCapabilities = lift getNumCapabilities + myThreadId = lift myThreadId + throwTo t = lift . throwTo t + newEmptyCVar = lift newEmptyCVar + readCVar = lift . readCVar + putCVar v = lift . putCVar v + tryPutCVar v = lift . tryPutCVar v + takeCVar = lift . takeCVar + tryTakeCVar = lift . tryTakeCVar + newCRef = lift . newCRef + readCRef = lift . readCRef + modifyCRef r = lift . modifyCRef r + atomically = lift . atomically + _concKnowsAbout = lift . _concKnowsAbout + _concForgets = lift . _concForgets + _concAllKnown = lift _concAllKnown + +reader :: Monad m => (m a -> m b) -> ReaderT r m a -> ReaderT r m b +reader f ma = ReaderT $ \r -> f (runReaderT ma r) + +instance (MonadConc m, Monoid w) => MonadConc (WL.WriterT w m) where + type STMLike (WL.WriterT w m) = STMLike m + type CVar (WL.WriterT w m) = CVar m + type CRef (WL.WriterT w m) = CRef m + type ThreadId (WL.WriterT w m) = ThreadId m + + fork = writerlazy fork + forkOn i = writerlazy (forkOn i) + forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WL.runWriterT (ma $ writerlazy f)) + _concNoTest = writerlazy _concNoTest + + getNumCapabilities = lift getNumCapabilities + myThreadId = lift myThreadId + throwTo t = lift . throwTo t + newEmptyCVar = lift newEmptyCVar + readCVar = lift . readCVar + putCVar v = lift . putCVar v + tryPutCVar v = lift . tryPutCVar v + takeCVar = lift . takeCVar + tryTakeCVar = lift . tryTakeCVar + newCRef = lift . newCRef + readCRef = lift . readCRef + modifyCRef r = lift . modifyCRef r + atomically = lift . atomically + _concKnowsAbout = lift . _concKnowsAbout + _concForgets = lift . _concForgets + _concAllKnown = lift _concAllKnown + +writerlazy :: (Monad m, Monoid w) => (m a -> m b) -> WL.WriterT w m a -> WL.WriterT w m b +writerlazy f ma = lift . f $ fst `liftM` WL.runWriterT ma + +instance (MonadConc m, Monoid w) => MonadConc (WS.WriterT w m) where + type STMLike (WS.WriterT w m) = STMLike m + type CVar (WS.WriterT w m) = CVar m + type CRef (WS.WriterT w m) = CRef m + type ThreadId (WS.WriterT w m) = ThreadId m + + fork = writerstrict fork + forkOn i = writerstrict (forkOn i) + forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WS.runWriterT (ma $ writerstrict f)) + _concNoTest = writerstrict _concNoTest + + getNumCapabilities = lift getNumCapabilities + myThreadId = lift myThreadId + throwTo t = lift . throwTo t + newEmptyCVar = lift newEmptyCVar + readCVar = lift . readCVar + putCVar v = lift . putCVar v + tryPutCVar v = lift . tryPutCVar v + takeCVar = lift . takeCVar + tryTakeCVar = lift . tryTakeCVar + newCRef = lift . newCRef + readCRef = lift . readCRef + modifyCRef r = lift . modifyCRef r + atomically = lift . atomically + _concKnowsAbout = lift . _concKnowsAbout + _concForgets = lift . _concForgets + _concAllKnown = lift _concAllKnown + +writerstrict :: (Monad m, Monoid w) => (m a -> m b) -> WS.WriterT w m a -> WS.WriterT w m b +writerstrict f ma = lift . f $ fst `liftM` WS.runWriterT ma + +instance MonadConc m => MonadConc (SL.StateT s m) where + type STMLike (SL.StateT s m) = STMLike m + type CVar (SL.StateT s m) = CVar m + type CRef (SL.StateT s m) = CRef m + type ThreadId (SL.StateT s m) = ThreadId m + + fork = statelazy fork + forkOn i = statelazy (forkOn i) + forkWithUnmask ma = SL.StateT $ \s -> (\a -> (a,s)) `liftM` forkWithUnmask (\f -> SL.evalStateT (ma $ statelazy f) s) + _concNoTest = statelazy _concNoTest + + getNumCapabilities = lift getNumCapabilities + myThreadId = lift myThreadId + throwTo t = lift . throwTo t + newEmptyCVar = lift newEmptyCVar + readCVar = lift . readCVar + putCVar v = lift . putCVar v + tryPutCVar v = lift . tryPutCVar v + takeCVar = lift . takeCVar + tryTakeCVar = lift . tryTakeCVar + newCRef = lift . newCRef + readCRef = lift . readCRef + modifyCRef r = lift . modifyCRef r + atomically = lift . atomically + _concKnowsAbout = lift . _concKnowsAbout + _concForgets = lift . _concForgets + _concAllKnown = lift _concAllKnown + +statelazy :: Monad m => (m a -> m b) -> SL.StateT s m a -> SL.StateT s m b +statelazy f ma = SL.StateT $ \s -> (\b -> (b,s)) `liftM` f (SL.evalStateT ma s) + +instance MonadConc m => MonadConc (SS.StateT s m) where + type STMLike (SS.StateT s m) = STMLike m + type CVar (SS.StateT s m) = CVar m + type CRef (SS.StateT s m) = CRef m + type ThreadId (SS.StateT s m) = ThreadId m + + fork = statestrict fork + forkOn i = statestrict (forkOn i) + forkWithUnmask ma = SS.StateT $ \s -> (\a -> (a,s)) `liftM` forkWithUnmask (\f -> SS.evalStateT (ma $ statestrict f) s) + _concNoTest = statestrict _concNoTest + + getNumCapabilities = lift getNumCapabilities + myThreadId = lift myThreadId + throwTo t = lift . throwTo t + newEmptyCVar = lift newEmptyCVar + readCVar = lift . readCVar + putCVar v = lift . putCVar v + tryPutCVar v = lift . tryPutCVar v + takeCVar = lift . takeCVar + tryTakeCVar = lift . tryTakeCVar + newCRef = lift . newCRef + readCRef = lift . readCRef + modifyCRef r = lift . modifyCRef r + atomically = lift . atomically + _concKnowsAbout = lift . _concKnowsAbout + _concForgets = lift . _concForgets + _concAllKnown = lift _concAllKnown + +statestrict :: Monad m => (m a -> m b) -> SS.StateT s m a -> SS.StateT s m b +statestrict f ma = SS.StateT $ \s -> (\b -> (b,s)) `liftM` f (SS.evalStateT ma s) + +instance (MonadConc m, Monoid w) => MonadConc (RL.RWST r w s m) where + type STMLike (RL.RWST r w s m) = STMLike m + type CVar (RL.RWST r w s m) = CVar m + type CRef (RL.RWST r w s m) = CRef m + type ThreadId (RL.RWST r w s m) = ThreadId m + + fork = rwslazy fork + forkOn i = rwslazy (forkOn i) + forkWithUnmask ma = RL.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkWithUnmask (\f -> fst `liftM` RL.evalRWST (ma $ rwslazy f) r s) + _concNoTest = rwslazy _concNoTest + + getNumCapabilities = lift getNumCapabilities + myThreadId = lift myThreadId + throwTo t = lift . throwTo t + newEmptyCVar = lift newEmptyCVar + readCVar = lift . readCVar + putCVar v = lift . putCVar v + tryPutCVar v = lift . tryPutCVar v + takeCVar = lift . takeCVar + tryTakeCVar = lift . tryTakeCVar + newCRef = lift . newCRef + readCRef = lift . readCRef + modifyCRef r = lift . modifyCRef r + atomically = lift . atomically + _concKnowsAbout = lift . _concKnowsAbout + _concForgets = lift . _concForgets + _concAllKnown = lift _concAllKnown + +rwslazy :: (Monad m, Monoid w) => (m a -> m b) -> RL.RWST r w s m a -> RL.RWST r w s m b +rwslazy f ma = RL.RWST $ \r s -> (\b -> (b,s,mempty)) `liftM` f (fst `liftM` RL.evalRWST ma r s) + +instance (MonadConc m, Monoid w) => MonadConc (RS.RWST r w s m) where + type STMLike (RS.RWST r w s m) = STMLike m + type CVar (RS.RWST r w s m) = CVar m + type CRef (RS.RWST r w s m) = CRef m + type ThreadId (RS.RWST r w s m) = ThreadId m + + fork = rwsstrict fork + forkOn i = rwsstrict (forkOn i) + forkWithUnmask ma = RS.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkWithUnmask (\f -> fst `liftM` RS.evalRWST (ma $ rwsstrict f) r s) + _concNoTest = rwsstrict _concNoTest + + getNumCapabilities = lift getNumCapabilities + myThreadId = lift myThreadId + throwTo t = lift . throwTo t + newEmptyCVar = lift newEmptyCVar + readCVar = lift . readCVar + putCVar v = lift . putCVar v + tryPutCVar v = lift . tryPutCVar v + takeCVar = lift . takeCVar + tryTakeCVar = lift . tryTakeCVar + newCRef = lift . newCRef + readCRef = lift . readCRef + modifyCRef r = lift . modifyCRef r + atomically = lift . atomically + _concKnowsAbout = lift . _concKnowsAbout + _concForgets = lift . _concForgets + _concAllKnown = lift _concAllKnown + +rwsstrict :: (Monad m, Monoid w) => (m a -> m b) -> RS.RWST r w s m a -> RS.RWST r w s m b +rwsstrict f ma = RS.RWST $ \r s -> (\b -> (b,s,mempty)) `liftM` f (fst `liftM` RS.evalRWST ma r s) diff --git a/Control/Monad/STM/Class.hs b/Control/Monad/STM/Class.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/STM/Class.hs @@ -0,0 +1,163 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE TypeFamilies #-} + +-- | This module provides an abstraction over 'STM', which can be used +-- with 'MonadConc'. +module Control.Monad.STM.Class where + +import Control.Concurrent.STM (STM) +import Control.Concurrent.STM.TVar (TVar, newTVar, readTVar, writeTVar) +import Control.Exception (Exception) +import Control.Monad (unless) +import Control.Monad.Catch (MonadCatch, MonadThrow, throwM, catch) +import Control.Monad.Reader (ReaderT(..), runReaderT) +import Control.Monad.Trans (lift) + +import qualified Control.Monad.RWS.Lazy as RL +import qualified Control.Monad.RWS.Strict as RS +import qualified Control.Monad.STM as S +import qualified Control.Monad.State.Lazy as SL +import qualified Control.Monad.State.Strict as SS +import qualified Control.Monad.Writer.Lazy as WL +import qualified Control.Monad.Writer.Strict as WS + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative (Applicative) +import Data.Monoid (Monoid) +#endif + +-- | @MonadSTM@ is an abstraction over 'STM'. +-- +-- This class does not provide any way to run transactions, rather +-- each 'MonadConc' has an associated @MonadSTM@ from which it can +-- atomically run a transaction. +-- +-- A minimal implementation consists of 'retry', 'orElse', 'newCTVar', +-- 'readCTVar', and 'writeCTVar'. +class (Applicative m, Monad m, MonadCatch m, MonadThrow m) => MonadSTM m where + -- | The mutable reference type. These behave like 'TVar's, in that + -- they always contain a value and updates are non-blocking and + -- synchronised. + type CTVar m :: * -> * + + -- | Retry execution of this transaction because it has seen values + -- in @CTVar@s that it shouldn't have. This will result in the + -- thread running the transaction being blocked until any @CTVar@s + -- referenced in it have been mutated. + retry :: m a + + -- | Run the first transaction and, if it @retry@s, run the second + -- instead. If the monad is an instance of + -- 'Alternative'/'MonadPlus', 'orElse' should be the '(<|>)'/'mplus' + -- function. + orElse :: m a -> m a -> m a + + -- | Check whether a condition is true and, if not, call @retry@. + -- + -- > check b = unless b retry + check :: Bool -> m () + check b = unless b retry + + -- | Create a new @CTVar@ containing the given value. + newCTVar :: a -> m (CTVar m a) + + -- | Return the current value stored in a @CTVar@. + readCTVar :: CTVar m a -> m a + + -- | Write the supplied value into the @CTVar@. + writeCTVar :: CTVar m a -> a -> m () + + -- | Throw an exception. This aborts the transaction and propagates + -- the exception. + -- + -- > throwSTM = Control.Monad.Catch.throwM + throwSTM :: Exception e => e -> m a + throwSTM = throwM + + -- | Handling exceptions from 'throwSTM'. + -- + -- > catchSTM = Control.Monad.Catch.catch + catchSTM :: Exception e => m a -> (e -> m a) -> m a + catchSTM = Control.Monad.Catch.catch + +instance MonadSTM STM where + type CTVar STM = TVar + + retry = S.retry + orElse = S.orElse + newCTVar = newTVar + readCTVar = readTVar + writeCTVar = writeTVar + +------------------------------------------------------------------------------- +-- Transformer instances + +instance MonadSTM m => MonadSTM (ReaderT r m) where + type CTVar (ReaderT r m) = CTVar m + + retry = lift retry + orElse ma mb = ReaderT $ \r -> orElse (runReaderT ma r) (runReaderT mb r) + check = lift . check + newCTVar = lift . newCTVar + readCTVar = lift . readCTVar + writeCTVar v = lift . writeCTVar v + +instance (MonadSTM m, Monoid w) => MonadSTM (WL.WriterT w m) where + type CTVar (WL.WriterT w m) = CTVar m + + retry = lift retry + orElse ma mb = WL.WriterT $ orElse (WL.runWriterT ma) (WL.runWriterT mb) + check = lift . check + newCTVar = lift . newCTVar + readCTVar = lift . readCTVar + writeCTVar v = lift . writeCTVar v + +instance (MonadSTM m, Monoid w) => MonadSTM (WS.WriterT w m) where + type CTVar (WS.WriterT w m) = CTVar m + + retry = lift retry + orElse ma mb = WS.WriterT $ orElse (WS.runWriterT ma) (WS.runWriterT mb) + check = lift . check + newCTVar = lift . newCTVar + readCTVar = lift . readCTVar + writeCTVar v = lift . writeCTVar v + +instance MonadSTM m => MonadSTM (SL.StateT s m) where + type CTVar (SL.StateT s m) = CTVar m + + retry = lift retry + orElse ma mb = SL.StateT $ \s -> orElse (SL.runStateT ma s) (SL.runStateT mb s) + check = lift . check + newCTVar = lift . newCTVar + readCTVar = lift . readCTVar + writeCTVar v = lift . writeCTVar v + +instance MonadSTM m => MonadSTM (SS.StateT s m) where + type CTVar (SS.StateT s m) = CTVar m + + retry = lift retry + orElse ma mb = SS.StateT $ \s -> orElse (SS.runStateT ma s) (SS.runStateT mb s) + check = lift . check + newCTVar = lift . newCTVar + readCTVar = lift . readCTVar + writeCTVar v = lift . writeCTVar v + +instance (MonadSTM m, Monoid w) => MonadSTM (RL.RWST r w s m) where + type CTVar (RL.RWST r w s m) = CTVar m + + retry = lift retry + orElse ma mb = RL.RWST $ \r s -> orElse (RL.runRWST ma r s) (RL.runRWST mb r s) + check = lift . check + newCTVar = lift . newCTVar + readCTVar = lift . readCTVar + writeCTVar v = lift . writeCTVar v + +instance (MonadSTM m, Monoid w) => MonadSTM (RS.RWST r w s m) where + type CTVar (RS.RWST r w s m) = CTVar m + + retry = lift retry + orElse ma mb = RS.RWST $ \r s -> orElse (RS.runRWST ma r s) (RS.runRWST mb r s) + check = lift . check + newCTVar = lift . newCTVar + readCTVar = lift . readCTVar + writeCTVar v = lift . writeCTVar v diff --git a/Data/List/Extra.hs b/Data/List/Extra.hs new file mode 100644 --- /dev/null +++ b/Data/List/Extra.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE CPP #-} +-- | Extra list functions and list-like types. +module Data.List.Extra where + +import Control.DeepSeq (NFData(..)) +import Data.Traversable (fmapDefault, foldMapDefault) + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative ((<$>), (<*>)) +import Data.Foldable (Foldable(..)) +import Data.Traversable (Traversable(..)) +#else +-- Why does this give a redundancy warning? It's necessary in order to +-- define the toList function in the Foldable instance for NonEmpty! +import Data.Foldable (toList) +#endif + +-- * Regular lists + +-- | Check if a list has more than some number of elements. +moreThan :: [a] -> Int -> Bool +moreThan [] n = n < 0 +moreThan _ 0 = True +moreThan (_:xs) n = moreThan xs (n-1) + +-- * Non-empty lists + +-- This gets exposed to users of the library, so it has a bunch of +-- classes which aren't actually used in the rest of the code to make +-- it more friendly to further use. + +-- | The type of non-empty lists. +data NonEmpty a = a :| [a] deriving (Eq, Ord, Read, Show) + +instance Functor NonEmpty where + fmap = fmapDefault + +instance Foldable NonEmpty where + foldMap = foldMapDefault + +#if __GLASGOW_HASKELL__ >= 710 + -- toList isn't in Foldable until GHC 7.10 + toList (a :| as) = a : as +#endif + +instance Traversable NonEmpty where + traverse f (a:|as) = (:|) <$> f a <*> traverse f as + +instance NFData a => NFData (NonEmpty a) where + rnf (x:|xs) = rnf (x, xs) + +-- | Convert a 'NonEmpty' to a regular non-empty list. +toList :: NonEmpty a -> [a] +toList (a :| as) = a : as + +-- | Convert a regular non-empty list to a 'NonEmpty'. This is +-- necessarily partial. +unsafeToNonEmpty :: [a] -> NonEmpty a +unsafeToNonEmpty (a:as) = a :| as +unsafeToNonEmpty [] = error "Cannot convert [] to NonEmpty!" diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2015, Michael Walker + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be +included in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu.hs @@ -0,0 +1,387 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE RankNTypes #-} + +-- | Deterministic testing for concurrent computations. +-- +-- As an example, consider this program, which has two locks and a +-- shared variable. Two threads are spawned, which claim the locks, +-- update the shared variable, and release the locks. The main thread +-- waits for them both to terminate, and returns the final result. +-- +-- > bad :: MonadConc m => m Int +-- > bad = do +-- > a <- newEmptyCVar +-- > b <- newEmptyCVar +-- > +-- > c <- newCVar 0 +-- > +-- > j1 <- spawn $ lock a >> lock b >> modifyCVar_ c (return . succ) >> unlock b >> unlock a +-- > j2 <- spawn $ lock b >> lock a >> modifyCVar_ c (return . pred) >> unlock a >> unlock b +-- > +-- > takeCVar j1 +-- > takeCVar j2 +-- > +-- > takeCVar c +-- +-- The correct result is 0, as it starts out as 0 and is incremented +-- and decremented by threads 1 and 2, respectively. However, note the +-- order of acquisition of the locks in the two threads. If thread 2 +-- pre-empts thread 1 between the acquisition of the locks (or if +-- thread 1 pre-empts thread 2), a deadlock situation will arise, as +-- thread 1 will have lock @a@ and be waiting on @b@, and thread 2 +-- will have @b@ and be waiting on @a@. +-- +-- Here is what Deja Fu has to say about it: +-- +-- > > autocheck bad +-- > [fail] Never Deadlocks (checked: 2) +-- > [deadlock] S0---------S1--P2---S1- +-- > [pass] No Exceptions (checked: 11) +-- > [fail] Consistent Result (checked: 10) +-- > 0 S0---------S1---------------S0--S2---------------S0---- +-- > [deadlock] S0---------S1--P2---S1- +-- > False +-- +-- It identifies the deadlock, and also the possible results the +-- computation can produce, and displays a simplified trace leading to +-- each failing outcome. It also returns @False@ as there are test +-- failures. The automatic testing functionality is good enough if you +-- only want to check your computation is deterministic, but if you +-- have more specific requirements (or have some expected and +-- tolerated level of nondeterminism), you can write tests yourself +-- using the @dejafu*@ functions. +-- +-- __Warning:__ If your computation under test does @IO@, the @IO@ +-- will be executed lots of times! Be sure that it is deterministic +-- enough not to invalidate your test results. Mocking may be useful +-- where possible. +module Test.DejaFu + ( -- * Testing + + -- | Testing in Deja Fu is similar to unit testing, the programmer + -- produces a self-contained monadic action to execute under + -- different schedules, and supplies a list of predicates to apply + -- to the list of results produced. + -- + -- If you simply wish to check that something is deterministic, see + -- the 'autocheck' and 'autocheckIO' functions. + + autocheck + , dejafu + , dejafus + , dejafus' + , autocheckIO + , dejafuIO + , dejafusIO + , dejafusIO' + + -- * Results + + -- | The results of a test can be pretty-printed to the console, as + -- with the above functions, or used in their original, much richer, + -- form for debugging purposes. These functions provide full access + -- to this data type which, most usefully, contains a detailed trace + -- of execution, showing what each thread did at each point. + + , Result(..) + , Failure(..) + , runTest + , runTest' + , runTestIO + , runTestIO' + + -- * Predicates + + -- | Predicates evaluate a list of results of execution and decide + -- whether some test case has passed or failed. They can be lazy and + -- make use of short-circuit evaluation to avoid needing to examine + -- the entire list of results, and can check any property which can + -- be defined for the return type of your monadic action. + -- + -- A collection of common predicates are provided, along with the + -- helper functions 'alwaysTrue', 'alwaysTrue2' and 'somewhereTrue' + -- to lfit predicates over a single result to over a collection of + -- results. + + , Predicate + , deadlocksNever + , deadlocksAlways + , deadlocksSometimes + , exceptionsNever + , exceptionsAlways + , exceptionsSometimes + , alwaysSame + , notAlwaysSame + , alwaysTrue + , alwaysTrue2 + , somewhereTrue + ) where + +import Control.Arrow (first) +import Control.DeepSeq (NFData(..)) +import Control.Monad (when) +import Data.List.Extra +import Test.DejaFu.Deterministic +import Test.DejaFu.Deterministic.IO (ConcIO) +import Test.DejaFu.SCT + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative ((<$>)) +import Data.Foldable (Foldable(..)) +#endif + +-- | Automatically test a computation. In particular, look for +-- deadlocks, uncaught exceptions, and multiple return values. +-- +-- This uses the 'Conc' monad for testing, which is an instance of +-- 'MonadConc'. If you need to test something which also uses +-- 'MonadIO', use 'autocheckIO'. +autocheck :: (Eq a, Show a) + => (forall t. Conc t a) + -- ^ The computation to test + -> IO Bool +autocheck conc = dejafus conc cases where + cases = [ ("Never Deadlocks", deadlocksNever) + , ("No Exceptions", exceptionsNever) + , ("Consistent Result", alwaysSame) + ] + +-- | Variant of 'autocheck' for computations which do 'IO'. +autocheckIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> IO Bool +autocheckIO concio = dejafusIO concio cases where + cases = [ ("Never Deadlocks", deadlocksNever) + , ("No Exceptions", exceptionsNever) + , ("Consistent Result", alwaysSame) + ] + +-- | Check a predicate and print the result to stdout, return 'True' +-- if it passes. +dejafu :: (Eq a, Show a) + => (forall t. Conc t a) + -- ^ The computation to test + -> (String, Predicate a) + -- ^ The predicate (with a name) to check + -> IO Bool +dejafu conc test = dejafus conc [test] + +-- | Variant of 'dejafu' which takes a collection of predicates to +-- test, returning 'True' if all pass. +dejafus :: (Eq a, Show a) + => (forall t. Conc t a) + -- ^ The computation to test + -> [(String, Predicate a)] + -- ^ The list of predicates (with names) to check + -> IO Bool +dejafus = dejafus' 2 + +-- | Variant of 'dejafus' which takes a pre-emption bound. +-- +-- Pre-emption bounding is used to filter the large number of possible +-- schedules, and can be iteratively increased for further coverage +-- guarantees. Empirical studies (/Concurrency Testing Using Schedule Bounding: an Empirical Study/, +-- P. Thompson, A. Donaldson, and A. Betts) have found that many +-- concurrency bugs can be exhibited with as few as two threads and +-- two pre-emptions, which is what 'dejafus' uses. +-- +-- __Warning:__ Using a larger pre-emption bound will almost certainly +-- significantly increase the time taken to test! +dejafus' :: (Eq a, Show a) + => Int + -- ^ The maximum number of pre-emptions to allow in a single + -- execution + -> (forall t. Conc t a) + -- ^ The computation to test + -> [(String, Predicate a)] + -- ^ The list of predicates (with names) to check + -> IO Bool +dejafus' pb conc tests = do + let traces = sctPreBound pb conc + results <- mapM (\(name, test) -> doTest name $ test traces) tests + return $ and results + +-- | Variant of 'dejafu' for computations which do 'IO'. +dejafuIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> (String, Predicate a) -> IO Bool +dejafuIO concio test = dejafusIO concio [test] + +-- | Variant of 'dejafus' for computations which do 'IO'. +dejafusIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> [(String, Predicate a)] -> IO Bool +dejafusIO = dejafusIO' 2 + +-- | Variant of 'dejafus'' for computations which do 'IO'. +dejafusIO' :: (Eq a, Show a) => Int -> (forall t. ConcIO t a) -> [(String, Predicate a)] -> IO Bool +dejafusIO' pb concio tests = do + traces <- sctPreBoundIO pb concio + results <- mapM (\(name, test) -> doTest name $ test traces) tests + return $ and results + +-- * Test cases + +-- | The results of a test, including the number of cases checked to +-- determine the final boolean outcome. +data Result a = Result + { _pass :: Bool + -- ^ Whether the test passed or not. + , _casesChecked :: Int + -- ^ The number of cases checked. + , _failures :: [(Either Failure a, Trace)] + -- ^ The failing cases, if any. + } deriving (Show, Eq) + +instance NFData a => NFData (Result a) where + rnf r = rnf (_pass r, _casesChecked r, _failures r) + +instance Functor Result where + fmap f r = r { _failures = map (first $ fmap f) $ _failures r } + +instance Foldable Result where + foldMap f r = foldMap f [a | (Right a, _) <- _failures r] + +-- | Run a predicate over all executions with two or fewer +-- pre-emptions. +runTest :: + Predicate a + -- ^ The predicate to check + -> (forall t. Conc t a) + -- ^ The computation to test + -> Result a +runTest = runTest' 2 + +-- | Variant of 'runTest' which takes a pre-emption bound. +runTest' :: + Int + -- ^ The maximum number of pre-emptions to allow in a single + -- execution + -> Predicate a + -- ^ The predicate to check + -> (forall t. Conc t a) + -- ^ The computation to test + -> Result a +runTest' pb predicate conc = predicate $ sctPreBound pb conc + +-- | Variant of 'runTest' for computations which do 'IO'. +runTestIO :: Predicate a -> (forall t. ConcIO t a) -> IO (Result a) +runTestIO = runTestIO' 2 + +-- | Variant of 'runTest'' for computations which do 'IO'. +runTestIO' :: Int -> Predicate a -> (forall t. ConcIO t a) -> IO (Result a) +runTestIO' pb predicate conc = predicate <$> sctPreBoundIO pb conc + +-- * Predicates + +-- | A @Predicate@ is a function which collapses a list of results +-- into a 'Result'. +type Predicate a = [(Either Failure a, Trace)] -> Result a + +-- | Check that a computation never deadlocks. +deadlocksNever :: Predicate a +deadlocksNever = alwaysTrue (not . either (`elem` [Deadlock, STMDeadlock]) (const False)) + +-- | Check that a computation always deadlocks. +deadlocksAlways :: Predicate a +deadlocksAlways = alwaysTrue $ either (`elem` [Deadlock, STMDeadlock]) (const False) + +-- | Check that a computation deadlocks at least once. +deadlocksSometimes :: Predicate a +deadlocksSometimes = somewhereTrue $ either (`elem` [Deadlock, STMDeadlock]) (const False) + +-- | Check that a computation never fails with an uncaught exception. +exceptionsNever :: Predicate a +exceptionsNever = alwaysTrue (not . either (==UncaughtException) (const False)) + +-- | Check that a computation always fails with an uncaught exception. +exceptionsAlways :: Predicate a +exceptionsAlways = alwaysTrue $ either (==UncaughtException) (const False) + +-- | Check that a computation fails with an uncaught exception at least once. +exceptionsSometimes :: Predicate a +exceptionsSometimes = somewhereTrue $ either (==UncaughtException) (const False) + +-- | Check that the result of a computation is always the same. In +-- particular this means either: (a) it always fails in the same way, +-- or (b) it never fails and the values returned are all equal. +alwaysSame :: Eq a => Predicate a +alwaysSame = alwaysTrue2 (==) + +-- | Check that the result of a computation is not always the same. +notAlwaysSame :: Eq a => Predicate a +notAlwaysSame [x] = Result { _pass = False, _casesChecked = 1, _failures = [x] } +notAlwaysSame xs = go xs Result { _pass = False, _casesChecked = 0, _failures = [] } where + go [y1,y2] res + | fst y1 /= fst y2 = incCC res { _pass = True } + | otherwise = incCC res { _failures = y1 : y2 : _failures res } + go (y1:y2:ys) res + | fst y1 /= fst y2 = go (y2:ys) . incCC $ res { _pass = True } + | otherwise = go (y2:ys) . incCC $ res { _failures = y1 : y2 : _failures res } + go _ res = res + +-- | Check that the result of a unary boolean predicate is always +-- true. +alwaysTrue :: (Either Failure a -> Bool) -> Predicate a +alwaysTrue p xs = go xs Result { _pass = True, _casesChecked = 0, _failures = filter (not . p . fst) xs } where + go (y:ys) res + | p (fst y) = go ys . incCC $ res + | otherwise = incCC $ res { _pass = False } + go [] res = res + +-- | Check that the result of a binary boolean predicate is true +-- between all pairs of results. Only properties which are transitive +-- and symmetric should be used here. +-- +-- If the predicate fails, /both/ (result,trace) tuples will be added +-- to the failures list. +alwaysTrue2 :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a +alwaysTrue2 _ [_] = Result { _pass = True, _casesChecked = 1, _failures = [] } +alwaysTrue2 p xs = go xs Result { _pass = True, _casesChecked = 0, _failures = failures xs } where + go [y1,y2] res + | p (fst y1) (fst y2) = incCC res + | otherwise = incCC res { _pass = False } + go (y1:y2:ys) res + | p (fst y1) (fst y2) = go (y2:ys) . incCC $ res + | otherwise = go (y2:ys) . incCC $ res { _pass = False } + go _ res = res + + failures (y1:y2:ys) + | p (fst y1) (fst y2) = failures (y2:ys) + | otherwise = y1 : if null ys then [y2] else failures (y2:ys) + failures _ = [] + +-- | Check that the result of a unary boolean predicate is true at +-- least once. +somewhereTrue :: (Either Failure a -> Bool) -> Predicate a +somewhereTrue p xs = go xs Result { _pass = False, _casesChecked = 0, _failures = filter (not . p . fst) xs } where + go (y:ys) res + | p (fst y) = incCC $ res { _pass = True } + | otherwise = go ys . incCC $ res { _failures = y : _failures res } + go [] res = res + +-- * Internal + +-- | Run a test and print to stdout +doTest :: (Eq a, Show a) => String -> Result a -> IO Bool +doTest name result = do + if _pass result + then + -- Display a pass message. + putStrLn $ "\27[32m[pass]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")" + else do + -- Display a failure message, and the first 5 (simplified) failed traces + putStrLn ("\27[31m[fail]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")") + + let failures = _failures result + mapM_ (\(r, t) -> putStrLn $ "\t" ++ either showfail show r ++ " " ++ showTrace t) $ take 5 failures + when (moreThan failures 5) $ + putStrLn "\t..." + + return $ _pass result + +-- | Increment the cases +incCC :: Result a -> Result a +incCC r = r { _casesChecked = _casesChecked r + 1 } + +-- | Pretty-print a failure +showfail :: Failure -> String +showfail Deadlock = "[deadlock]" +showfail STMDeadlock = "[stm-deadlock]" +showfail InternalError = "[internal-error]" +showfail FailureInNoTest = "[_concNoTest]" +showfail UncaughtException = "[exception]" diff --git a/Test/DejaFu/Deterministic.hs b/Test/DejaFu/Deterministic.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Deterministic.hs @@ -0,0 +1,345 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} + +-- | Deterministic traced execution of concurrent computations which +-- don't do @IO@. +-- +-- This works by executing the computation on a single thread, calling +-- out to the supplied scheduler after each step to determine which +-- thread runs next. +module Test.DejaFu.Deterministic + ( -- * The @Conc@ Monad + Conc + , Failure(..) + , runConc + , runConc' + + -- * Concurrency + , fork + , forkFinally + , forkWithUnmask + , forkOn + , getNumCapabilities + , myThreadId + , spawn + , atomically + , throw + , throwTo + , killThread + , Test.DejaFu.Deterministic.catch + , mask + , uninterruptibleMask + + -- * @CVar@s + , CVar + , newEmptyCVar + , putCVar + , tryPutCVar + , readCVar + , takeCVar + , tryTakeCVar + + -- * @CRef@s + , CRef + , newCRef + , readCRef + , writeCRef + , modifyCRef + + -- * Testing + , _concNoTest + , _concKnowsAbout + , _concForgets + , _concAllKnown + + -- * Execution traces + , Trace + , Trace' + , Decision(..) + , ThreadAction(..) + , Lookahead(..) + , CVarId + , CRefId + , MaskingState(..) + , showTrace + , toTrace + + -- * Scheduling + , module Test.DejaFu.Deterministic.Schedule + ) where + +import Control.Exception (Exception, MaskingState(..), SomeException(..)) +import Control.Monad.Cont (cont, runCont) +import Control.Monad.ST (ST, runST) +import Data.STRef (STRef, newSTRef) +import Test.DejaFu.Deterministic.Internal +import Test.DejaFu.Deterministic.Schedule +import Test.DejaFu.Internal (refST) +import Test.DejaFu.STM (STMLike, runTransactionST) +import Test.DejaFu.STM.Internal (CTVar(..)) + +import qualified Control.Monad.Catch as Ca +import qualified Control.Monad.Conc.Class as C + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative (Applicative(..), (<$>)) +#endif + +{-# ANN module ("HLint: ignore Avoid lambda" :: String) #-} + +-- | The @Conc@ monad itself. This uses the same +-- universally-quantified indexing state trick as used by 'ST' and +-- 'STRef's to prevent mutable references from leaking out of the +-- monad. +newtype Conc t a = C { unC :: M (ST t) (STRef t) (STMLike t) a } deriving (Functor, Applicative, Monad) + +wrap :: (M (ST t) (STRef t) (STMLike t) a -> M (ST t) (STRef t) (STMLike t) a) -> Conc t a -> Conc t a +wrap f = C . f . unC + +instance Ca.MonadCatch (Conc t) where + catch = Test.DejaFu.Deterministic.catch + +instance Ca.MonadThrow (Conc t) where + throwM = throw + +instance Ca.MonadMask (Conc t) where + mask = mask + uninterruptibleMask = uninterruptibleMask + +instance C.MonadConc (Conc t) where + type CVar (Conc t) = CVar t + type CRef (Conc t) = CRef t + type STMLike (Conc t) = STMLike t (ST t) (STRef t) + type ThreadId (Conc t) = Int + + fork = fork + forkWithUnmask = forkWithUnmask + forkOn = forkOn + getNumCapabilities = getNumCapabilities + myThreadId = myThreadId + throwTo = throwTo + newEmptyCVar = newEmptyCVar + putCVar = putCVar + tryPutCVar = tryPutCVar + readCVar = readCVar + takeCVar = takeCVar + tryTakeCVar = tryTakeCVar + newCRef = newCRef + readCRef = readCRef + writeCRef = writeCRef + modifyCRef = modifyCRef + atomically = atomically + _concNoTest = _concNoTest + _concKnowsAbout = _concKnowsAbout + _concForgets = _concForgets + _concAllKnown = _concAllKnown + +fixed :: Fixed (ST t) (STRef t) (STMLike t) +fixed = refST $ \ma -> cont (\c -> ALift $ c <$> ma) + +-- | The concurrent variable type used with the 'Conc' monad. One +-- notable difference between these and 'MVar's is that 'MVar's are +-- single-wakeup, and wake up in a FIFO order. Writing to a @CVar@ +-- wakes up all threads blocked on reading it, and it is up to the +-- scheduler which one runs next. Taking from a @CVar@ behaves +-- analogously. +newtype CVar t a = Var { unV :: V (STRef t) a } deriving Eq + +-- | The mutable non-blocking reference type. These are like 'IORef's, +-- but don't have the potential re-ordering problem mentioned in +-- Data.IORef. +newtype CRef t a = Ref { unR :: R (STRef t) a } deriving Eq + +-- | Run the provided computation concurrently, returning the result. +spawn :: Conc t a -> Conc t (CVar t a) +spawn = C.spawn + +-- | Block on a 'CVar' until it is full, then read from it (without +-- emptying). +readCVar :: CVar t a -> Conc t a +readCVar cvar = C $ cont $ AGet $ unV cvar + +-- | Run the provided computation concurrently. +fork :: Conc t () -> Conc t ThreadId +fork (C ma) = C $ cont $ AFork (const' $ runCont ma $ const AStop) + +-- | Get the 'ThreadId' of the current thread. +myThreadId :: Conc t ThreadId +myThreadId = C $ cont AMyTId + +-- | Run the provided 'MonadSTM' transaction atomically. If 'retry' is +-- called, it will be blocked until any of the touched 'CTVar's have +-- been written to. +atomically :: STMLike t (ST t) (STRef t) a -> Conc t a +atomically stm = C $ cont $ AAtom stm + +-- | Create a new empty 'CVar'. +newEmptyCVar :: Conc t (CVar t a) +newEmptyCVar = C $ cont lifted where + lifted c = ANew $ \cvid -> c <$> newEmptyCVar' cvid + newEmptyCVar' cvid = (\ref -> Var (cvid, ref)) <$> newSTRef Nothing + +-- | Block on a 'CVar' until it is empty, then write to it. +putCVar :: CVar t a -> a -> Conc t () +putCVar cvar a = C $ cont $ \c -> APut (unV cvar) a $ c () + +-- | Put a value into a 'CVar' if there isn't one, without blocking. +tryPutCVar :: CVar t a -> a -> Conc t Bool +tryPutCVar cvar a = C $ cont $ ATryPut (unV cvar) a + +-- | Block on a 'CVar' until it is full, then read from it (with +-- emptying). +takeCVar :: CVar t a -> Conc t a +takeCVar cvar = C $ cont $ ATake $ unV cvar + +-- | Read a value from a 'CVar' if there is one, without blocking. +tryTakeCVar :: CVar t a -> Conc t (Maybe a) +tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar + +-- | Create a new 'CRef'. +newCRef :: a -> Conc t (CRef t a) +newCRef a = C $ cont lifted where + lifted c = ANewRef $ \crid -> c <$> newCRef' crid + newCRef' crid = (\ref -> Ref (crid, ref)) <$> newSTRef a + +-- | Read the value from a 'CRef'. +readCRef :: CRef t a -> Conc t a +readCRef ref = C $ cont $ AReadRef $ unR ref + +-- | Atomically modify the value inside a 'CRef'. +modifyCRef :: CRef t a -> (a -> (a, b)) -> Conc t b +modifyCRef ref f = C $ cont $ AModRef (unR ref) f + +-- | Replace the value stored inside a 'CRef'. +writeCRef :: CRef t a -> a -> Conc t () +writeCRef ref a = modifyCRef ref $ const (a, ()) + +-- | Raise an exception in the 'Conc' monad. The exception is raised +-- when the action is run, not when it is applied. It short-citcuits +-- the rest of the computation: +-- +-- > throw e >> x == throw e +throw :: Exception e => e -> Conc t a +throw e = C $ cont $ \_ -> AThrow (SomeException e) + +-- | Throw an exception to the target thread. This blocks until the +-- exception is delivered, and it is just as if the target thread had +-- raised it with 'throw'. This can interrupt a blocked action. +throwTo :: Exception e => ThreadId -> e -> Conc t () +throwTo tid e = C $ cont $ \c -> AThrowTo tid (SomeException e) $ c () + +-- | Raise the 'ThreadKilled' exception in the target thread. Note +-- that if the thread is prepared to catch this exception, it won't +-- actually kill it. +killThread :: ThreadId -> Conc t () +killThread = C.killThread + +-- | Catch an exception raised by 'throw'. This __cannot__ catch +-- errors, such as evaluating 'undefined', or division by zero. If you +-- need that, use Control.Exception.catch and 'ConcIO'. +catch :: Exception e => Conc t a -> (e -> Conc t a) -> Conc t a +catch ma h = C $ cont $ ACatching (unC . h) (unC ma) + +-- | Fork a thread and call the supplied function when the thread is +-- about to terminate, with an exception or a returned value. The +-- function is called with asynchronous exceptions masked. +-- +-- This function is useful for informing the parent when a child +-- terminates, for example. +forkFinally :: Conc t a -> (Either SomeException a -> Conc t ()) -> Conc t ThreadId +forkFinally action and_then = mask $ \restore -> + fork $ Ca.try (restore action) >>= and_then + +-- | Like 'fork', but the child thread is passed a function that can +-- be used to unmask asynchronous exceptions. This function should not +-- be used within a 'mask' or 'uninterruptibleMask'. +forkWithUnmask :: ((forall a. Conc t a -> Conc t a) -> Conc t ()) -> Conc t ThreadId +forkWithUnmask ma = C $ cont $ + AFork (\umask -> runCont (unC $ ma $ wrap umask) $ const AStop) + +-- | Executes a computation with asynchronous exceptions +-- /masked/. That is, any thread which attempts to raise an exception +-- in the current thread with 'throwTo' will be blocked until +-- asynchronous exceptions are unmasked again. +-- +-- The argument passed to mask is a function that takes as its +-- argument another function, which can be used to restore the +-- prevailing masking state within the context of the masked +-- computation. This function should not be used within an +-- 'uninterruptibleMask'. +mask :: ((forall a. Conc t a -> Conc t a) -> Conc t b) -> Conc t b +-- Can't avoid the lambda here (and in uninterruptibleMask and in +-- ConcIO) because higher-ranked type inference is scary. +mask mb = C $ cont $ AMasking MaskedInterruptible (\f -> unC $ mb $ wrap f) + +-- | Like 'mask', but the masked computation is not +-- interruptible. THIS SHOULD BE USED WITH GREAT CARE, because if a +-- thread executing in 'uninterruptibleMask' blocks for any reason, +-- then the thread (and possibly the program, if this is the main +-- thread) will be unresponsive and unkillable. This function should +-- only be necessary if you need to mask exceptions around an +-- interruptible operation, and you can guarantee that the +-- interruptible operation will only block for a short period of +-- time. The supplied unmasking function should not be used within a +-- 'mask'. +uninterruptibleMask :: ((forall a. Conc t a -> Conc t a) -> Conc t b) -> Conc t b +uninterruptibleMask mb = C $ cont $ + AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f) + +-- | Fork a computation to happen on a specific processor. This +-- implementation only has a single processor. +forkOn :: Int -> Conc t () -> Conc t ThreadId +forkOn _ = fork + +-- | Get the number of Haskell threads that can run +-- simultaneously. This implementation lies and always returns +-- 2. There is no way to verify in the computation that this is a lie, +-- and will potentially avoid special-case behaviour for 1 capability, +-- so it seems a sane choice. +getNumCapabilities :: Conc t Int +getNumCapabilities = return 2 + +-- | Run the argument in one step. If the argument fails, the whole +-- computation will fail. +_concNoTest :: Conc t a -> Conc t a +_concNoTest ma = C $ cont $ \c -> ANoTest (unC ma) c + +-- | Record that the referenced variable is known by the current thread. +_concKnowsAbout :: Either (CVar t a) (CTVar t (STRef t) a) -> Conc t () +_concKnowsAbout (Left (Var (cvarid, _))) = C $ cont $ \c -> AKnowsAbout (Left cvarid) (c ()) +_concKnowsAbout (Right (V (ctvarid, _))) = C $ cont $ \c -> AKnowsAbout (Right ctvarid) (c ()) + +-- | Record that the referenced variable will never be touched by the +-- current thread. +_concForgets :: Either (CVar t a) (CTVar t (STRef t) a) -> Conc t () +_concForgets (Left (Var (cvarid, _))) = C $ cont $ \c -> AForgets (Left cvarid) (c ()) +_concForgets (Right (V (ctvarid, _))) = C $ cont $ \c -> AForgets (Right ctvarid) (c ()) + +-- | Record that all 'CVar's and 'CTVar's known by the current thread +-- have been passed to '_concKnowsAbout'. +_concAllKnown :: Conc t () +_concAllKnown = C $ cont $ \c -> AAllKnown (c ()) + +-- | Run a concurrent computation with a given 'Scheduler' and initial +-- state, returning a failure reason on error. Also returned is the +-- final state of the scheduler, and an execution trace. +-- +-- Note how the @t@ in 'Conc' is universally quantified, what this +-- means in practice is that you can't do something like this: +-- +-- > runConc roundRobinSched () newEmptyCVar +-- +-- So mutable references cannot leak out of the 'Conc' computation. If +-- this is making your head hurt, check out the \"How @runST@ works\" +-- section of +-- +runConc :: Scheduler s -> s -> (forall t. Conc t a) -> (Either Failure a, s, Trace) +runConc sched s ma = + let (r, s', t') = runConc' sched s ma + in (r, s', toTrace t') + +-- | Variant of 'runConc' which produces a 'Trace''. +runConc' :: Scheduler s -> s -> (forall t. Conc t a) -> (Either Failure a, s, Trace') +runConc' sched s ma = runST $ runFixed fixed runTransactionST sched s $ unC ma diff --git a/Test/DejaFu/Deterministic/IO.hs b/Test/DejaFu/Deterministic/IO.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Deterministic/IO.hs @@ -0,0 +1,337 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} + +-- | Deterministic traced execution of concurrent computations which +-- may do @IO@. +-- +-- __Warning:__ Blocking on the action of another thread in 'liftIO' +-- cannot be detected! So if you perform some potentially blocking +-- action in a 'liftIO' the entire collection of threads may deadlock! +-- You should therefore keep @IO@ blocks small, and only perform +-- blocking operations with the supplied primitives, insofar as +-- possible. +module Test.DejaFu.Deterministic.IO + ( -- * The @ConcIO@ Monad + ConcIO + , Failure(..) + , runConcIO + , runConcIO' + , liftIO + + -- * Concurrency + , fork + , forkFinally + , forkWithUnmask + , forkOn + , getNumCapabilities + , myThreadId + , spawn + , atomically + , throw + , throwTo + , killThread + , Test.DejaFu.Deterministic.IO.catch + , mask + , uninterruptibleMask + + -- * @CVar@s + , CVar + , newEmptyCVar + , putCVar + , tryPutCVar + , readCVar + , takeCVar + , tryTakeCVar + + -- * @CRef@s + , CRef + , newCRef + , readCRef + , writeCRef + , modifyCRef + + -- * Testing + , _concNoTest + , _concKnowsAbout + , _concForgets + , _concAllKnown + + -- * Execution traces + , Trace + , Trace' + , Decision(..) + , ThreadAction(..) + , Lookahead(..) + , CVarId + , MaskingState(..) + , showTrace + , toTrace + + -- * Scheduling + , module Test.DejaFu.Deterministic.Schedule + ) where + +import Control.Exception (Exception, MaskingState(..), SomeException(..)) +import Control.Monad.Cont (cont, runCont) +import Data.IORef (IORef, newIORef) +import Test.DejaFu.Deterministic.Internal +import Test.DejaFu.Deterministic.Schedule +import Test.DejaFu.Internal (refIO) +import Test.DejaFu.STM (STMLike, runTransactionIO) +import Test.DejaFu.STM.Internal (CTVar(..)) + +import qualified Control.Monad.Catch as Ca +import qualified Control.Monad.Conc.Class as C +import qualified Control.Monad.IO.Class as IO + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative (Applicative(..), (<$>)) +#endif + +{-# ANN module ("HLint: ignore Avoid lambda" :: String) #-} + +-- | The 'IO' variant of Test.DejaFu.Deterministic's +-- 'Test.DejaFu.Deterministic.Conc' monad. +newtype ConcIO t a = C { unC :: M IO IORef (STMLike t) a } deriving (Functor, Applicative, Monad) + +wrap :: (M IO IORef (STMLike t) a -> M IO IORef (STMLike t) a) -> ConcIO t a -> ConcIO t a +wrap f = C . f . unC + +instance Ca.MonadCatch (ConcIO t) where + catch = Test.DejaFu.Deterministic.IO.catch + +instance Ca.MonadThrow (ConcIO t) where + throwM = throw + +instance Ca.MonadMask (ConcIO t) where + mask = mask + uninterruptibleMask = uninterruptibleMask + +instance IO.MonadIO (ConcIO t) where + liftIO = liftIO + +instance C.MonadConc (ConcIO t) where + type CVar (ConcIO t) = CVar t + type CRef (ConcIO t) = CRef t + type STMLike (ConcIO t) = STMLike t IO IORef + type ThreadId (ConcIO t) = Int + + fork = fork + forkWithUnmask = forkWithUnmask + forkOn = forkOn + getNumCapabilities = getNumCapabilities + myThreadId = myThreadId + throwTo = throwTo + newEmptyCVar = newEmptyCVar + putCVar = putCVar + tryPutCVar = tryPutCVar + readCVar = readCVar + takeCVar = takeCVar + tryTakeCVar = tryTakeCVar + newCRef = newCRef + readCRef = readCRef + writeCRef = writeCRef + modifyCRef = modifyCRef + atomically = atomically + _concNoTest = _concNoTest + _concKnowsAbout = _concKnowsAbout + _concForgets = _concForgets + _concAllKnown = _concAllKnown + +fixed :: Fixed IO IORef (STMLike t) +fixed = refIO $ unC . liftIO + +-- | The concurrent variable type used with the 'ConcIO' monad. These +-- behave the same as @Conc@'s @CVar@s +newtype CVar t a = Var { unV :: V IORef a } deriving Eq + +-- | The mutable non-blocking reference type. These behave the same as +-- @Conc@'s @CRef@s +newtype CRef t a = Ref { unR :: R IORef a } deriving Eq + +-- | Lift an 'IO' action into the 'ConcIO' monad. +liftIO :: IO a -> ConcIO t a +liftIO ma = C $ cont lifted where + lifted c = ALift $ c <$> ma + +-- | Run the provided computation concurrently, returning the result. +spawn :: ConcIO t a -> ConcIO t (CVar t a) +spawn = C.spawn + +-- | Block on a 'CVar' until it is full, then read from it (without +-- emptying). +readCVar :: CVar t a -> ConcIO t a +readCVar cvar = C $ cont $ AGet $ unV cvar + +-- | Run the provided computation concurrently. +fork :: ConcIO t () -> ConcIO t ThreadId +fork (C ma) = C $ cont $ AFork (const' $ runCont ma $ const AStop) + +-- | Get the 'ThreadId' of the current thread. +myThreadId :: ConcIO t ThreadId +myThreadId = C $ cont AMyTId + +-- | Run the provided 'MonadSTM' transaction atomically. If 'retry' is +-- called, it will be blocked until any of the touched 'CTVar's have +-- been written to. +atomically :: STMLike t IO IORef a -> ConcIO t a +atomically stm = C $ cont $ AAtom stm + +-- | Create a new empty 'CVar'. +newEmptyCVar :: ConcIO t (CVar t a) +newEmptyCVar = C $ cont lifted where + lifted c = ANew $ \cvid -> c <$> newEmptyCVar' cvid + newEmptyCVar' cvid = (\ref -> Var (cvid, ref)) <$> newIORef Nothing + +-- | Block on a 'CVar' until it is empty, then write to it. +putCVar :: CVar t a -> a -> ConcIO t () +putCVar cvar a = C $ cont $ \c -> APut (unV cvar) a $ c () + +-- | Put a value into a 'CVar' if there isn't one, without blocking. +tryPutCVar :: CVar t a -> a -> ConcIO t Bool +tryPutCVar cvar a = C $ cont $ ATryPut (unV cvar) a + +-- | Block on a 'CVar' until it is full, then read from it (with +-- emptying). +takeCVar :: CVar t a -> ConcIO t a +takeCVar cvar = C $ cont $ ATake $ unV cvar + +-- | Read a value from a 'CVar' if there is one, without blocking. +tryTakeCVar :: CVar t a -> ConcIO t (Maybe a) +tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar + +-- | Create a new 'CRef'. +newCRef :: a -> ConcIO t (CRef t a) +newCRef a = C $ cont lifted where + lifted c = ANewRef $ \crid -> c <$> newCRef' crid + newCRef' crid = (\ref -> Ref (crid, ref)) <$> newIORef a + +-- | Read the value from a 'CRef'. +readCRef :: CRef t a -> ConcIO t a +readCRef ref = C $ cont $ AReadRef $ unR ref + +-- | Atomically modify the value inside a 'CRef'. +modifyCRef :: CRef t a -> (a -> (a, b)) -> ConcIO t b +modifyCRef ref f = C $ cont $ AModRef (unR ref) f + +-- | Replace the value stored inside a 'CRef'. +writeCRef :: CRef t a -> a -> ConcIO t () +writeCRef ref a = modifyCRef ref $ const (a, ()) + +-- | Raise an exception in the 'ConcIO' monad. The exception is raised +-- when the action is run, not when it is applied. It short-citcuits +-- the rest of the computation: +-- +-- > throw e >> x == throw e +throw :: Exception e => e -> ConcIO t a +throw e = C $ cont $ \_ -> AThrow (SomeException e) + +-- | Throw an exception to the target thread. This blocks until the +-- exception is delivered, and it is just as if the target thread had +-- raised it with 'throw'. This can interrupt a blocked action. +throwTo :: Exception e => ThreadId -> e -> ConcIO t () +throwTo tid e = C $ cont $ \c -> AThrowTo tid (SomeException e) $ c () + +-- | Raise the 'ThreadKilled' exception in the target thread. Note +-- that if the thread is prepared to catch this exception, it won't +-- actually kill it. +killThread :: ThreadId -> ConcIO t () +killThread = C.killThread + +-- | Catch an exception raised by 'throw'. This __cannot__ catch +-- errors, such as evaluating 'undefined', or division by zero. If you +-- need that, use Control.Exception.catch and 'liftIO'. +catch :: Exception e => ConcIO t a -> (e -> ConcIO t a) -> ConcIO t a +catch ma h = C $ cont $ ACatching (unC . h) (unC ma) + +-- | Fork a thread and call the supplied function when the thread is +-- about to terminate, with an exception or a returned value. The +-- function is called with asynchronous exceptions masked. +-- +-- This function is useful for informing the parent when a child +-- terminates, for example. +forkFinally :: ConcIO t a -> (Either SomeException a -> ConcIO t ()) -> ConcIO t ThreadId +forkFinally action and_then = mask $ \restore -> + fork $ Ca.try (restore action) >>= and_then + +-- | Like 'fork', but the child thread is passed a function that can +-- be used to unmask asynchronous exceptions. This function should not +-- be used within a 'mask' or 'uninterruptibleMask'. +forkWithUnmask :: ((forall a. ConcIO t a -> ConcIO t a) -> ConcIO t ()) -> ConcIO t ThreadId +forkWithUnmask ma = C $ cont $ + AFork (\umask -> runCont (unC $ ma $ wrap umask) $ const AStop) + +-- | Executes a computation with asynchronous exceptions +-- /masked/. That is, any thread which attempts to raise an exception +-- in the current thread with 'throwTo' will be blocked until +-- asynchronous exceptions are unmasked again. +-- +-- The argument passed to mask is a function that takes as its +-- argument another function, which can be used to restore the +-- prevailing masking state within the context of the masked +-- computation. This function should not be used within an +-- 'uninterruptibleMask'. +mask :: ((forall a. ConcIO t a -> ConcIO t a) -> ConcIO t b) -> ConcIO t b +mask mb = C $ cont $ AMasking MaskedInterruptible (\f -> unC $ mb $ wrap f) + +-- | Like 'mask', but the masked computation is not +-- interruptible. THIS SHOULD BE USED WITH GREAT CARE, because if a +-- thread executing in 'uninterruptibleMask' blocks for any reason, +-- then the thread (and possibly the program, if this is the main +-- thread) will be unresponsive and unkillable. This function should +-- only be necessary if you need to mask exceptions around an +-- interruptible operation, and you can guarantee that the +-- interruptible operation will only block for a short period of +-- time. The supplied unmasking function should not be used within a +-- 'mask'. +uninterruptibleMask :: ((forall a. ConcIO t a -> ConcIO t a) -> ConcIO t b) -> ConcIO t b +uninterruptibleMask mb = C $ cont $ + AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f) + +-- | Fork a computation to happen on a specific processor. This +-- implementation only has a single processor. +forkOn :: Int -> ConcIO t () -> ConcIO t ThreadId +forkOn _ = fork + +-- | Get the number of Haskell threads that can run +-- simultaneously. This implementation lies and always returns +-- 2. There is no way to verify in the computation that this is a lie, +-- and will potentially avoid special-case behaviour for 1 capability, +-- so it seems a sane choice. +getNumCapabilities :: ConcIO t Int +getNumCapabilities = return 2 + +-- | Run the argument in one step. If the argument fails, the whole +-- computation will fail. +_concNoTest :: ConcIO t a -> ConcIO t a +_concNoTest ma = C $ cont $ \c -> ANoTest (unC ma) c + +-- | Record that the referenced variable is known by the current thread. +_concKnowsAbout :: Either (CVar t a) (CTVar t IORef a) -> ConcIO t () +_concKnowsAbout (Left (Var (cvarid, _))) = C $ cont $ \c -> AKnowsAbout (Left cvarid) (c ()) +_concKnowsAbout (Right (V (ctvarid, _))) = C $ cont $ \c -> AKnowsAbout (Right ctvarid) (c ()) + +-- | Record that the referenced variable will never be touched by the +-- current thread. +_concForgets :: Either (CVar t a) (CTVar t IORef a) -> ConcIO t () +_concForgets (Left (Var (cvarid, _))) = C $ cont $ \c -> AForgets (Left cvarid) (c ()) +_concForgets (Right (V (ctvarid, _))) = C $ cont $ \c -> AForgets (Right ctvarid) (c ()) + +-- | Record that all 'CVar's and 'CTVar's known by the current thread +-- have been passed to '_concKnowsAbout'. +_concAllKnown :: ConcIO t () +_concAllKnown = C $ cont $ \c -> AAllKnown (c ()) + +-- | Run a concurrent computation with a given 'Scheduler' and initial +-- state, returning an failure reason on error. Also returned is the +-- final state of the scheduler, and an execution trace. +runConcIO :: Scheduler s -> s -> (forall t. ConcIO t a) -> IO (Either Failure a, s, Trace) +runConcIO sched s ma = do + (r, s', t') <- runConcIO' sched s ma + return (r, s', toTrace t') + +-- | Variant of 'runConcIO' which produces a 'Trace''. +runConcIO' :: Scheduler s -> s -> (forall t. ConcIO t a) -> IO (Either Failure a, s, Trace') +runConcIO' sched s ma = runFixed fixed runTransactionIO sched s $ unC ma diff --git a/Test/DejaFu/Deterministic/Internal.hs b/Test/DejaFu/Deterministic/Internal.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Deterministic/Internal.hs @@ -0,0 +1,390 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + +#if __GLASGOW_HASKELL__ < 710 +-- ImpredicativeTypes are needed for the const' function, as the +-- type-checker can't otherwise unify the higher-ranked application. + +{-# LANGUAGE ImpredicativeTypes #-} +#endif + +-- | Concurrent monads with a fixed scheduler: internal types and +-- functions. +module Test.DejaFu.Deterministic.Internal + ( -- * Execution + runFixed + , runFixed' + + -- * The @Conc@ Monad + , M + , V + , R + , Fixed + + -- * Primitive Actions + , Action(..) + + -- * Identifiers + , ThreadId + , CVarId + , CRefId + + -- * Scheduling & Traces + , Scheduler + , Trace + , Decision(..) + , ThreadAction(..) + , Lookahead(..) + , Trace' + , showTrace + , toTrace + + -- * Failures + , Failure(..) + + -- * Utils + , const' + ) where + +import Control.Exception (MaskingState(..)) +import Control.Monad.Cont (cont, runCont) +import Data.List (sort) +import Data.List.Extra +import Data.Maybe (fromJust, isJust, isNothing, listToMaybe) +import Test.DejaFu.STM (CTVarId, Result(..)) +import Test.DejaFu.Internal +import Test.DejaFu.Deterministic.Internal.Common +import Test.DejaFu.Deterministic.Internal.CVar +import Test.DejaFu.Deterministic.Internal.Threading + +import qualified Data.Map as M + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative ((<$>), (<*>)) +#endif + +{-# ANN module ("HLint: ignore Use record patterns" :: String) #-} + +const' :: a -> (forall b. M n r s b -> M n r s b) -> a +const' = const + +-------------------------------------------------------------------------------- +-- * Execution + +-- | Run a concurrent computation with a given 'Scheduler' and initial +-- state, returning a 'Just' if it terminates, and 'Nothing' if a +-- deadlock is detected. Also returned is the final state of the +-- scheduler, and an execution trace. +runFixed :: (Functor n, Monad n) => Fixed n r s -> (forall x. s n r x -> CTVarId -> n (Result x, CTVarId)) + -> Scheduler g -> g -> M n r s a -> n (Either Failure a, g, Trace') +runFixed fixed runstm sched s ma = (\(e,g,_,t) -> (e,g,t)) <$> runFixed' fixed runstm sched s initialIdSource ma + +-- | Same as 'runFixed', be parametrised by an 'IdSource'. +runFixed' :: forall n r s g a. (Functor n, Monad n) + => Fixed n r s -> (forall x. s n r x -> CTVarId -> n (Result x, CTVarId)) + -> Scheduler g -> g -> IdSource -> M n r s a -> n (Either Failure a, g, IdSource, Trace') +runFixed' fixed runstm sched s idSource ma = do + ref <- newRef fixed Nothing + + let c = ma >>= liftN fixed . writeRef fixed ref . Just . Right + let threads = launch' Unmasked 0 (const' $ runCont c $ const AStop) M.empty + + (s', idSource', trace) <- runThreads fixed runstm sched s threads idSource ref + out <- readRef fixed ref + + return (fromJust out, s', idSource', reverse trace) + +-- | Run a collection of threads, until there are no threads left. +-- +-- Note: this returns the trace in reverse order, because it's more +-- efficient to prepend to a list than append. As this function isn't +-- exposed to users of the library, this is just an internal gotcha to +-- watch out for. +runThreads :: (Functor n, Monad n) => Fixed n r s -> (forall x. s n r x -> CTVarId -> n (Result x, CTVarId)) + -> Scheduler g -> g -> Threads n r s -> IdSource -> r (Maybe (Either Failure a)) -> n (g, IdSource, Trace') +runThreads fixed runstm sched origg origthreads idsrc ref = go idsrc [] Nothing origg origthreads where + go idSource sofar prior g threads + | isTerminated = return (g, idSource, sofar) + | isDeadlocked = writeRef fixed ref (Just $ Left Deadlock) >> return (g, idSource, sofar) + | isSTMLocked = writeRef fixed ref (Just $ Left STMDeadlock) >> return (g, idSource, sofar) + | isNonexistant = writeRef fixed ref (Just $ Left InternalError) >> return (g, idSource, sofar) + | isBlocked = writeRef fixed ref (Just $ Left InternalError) >> return (g, idSource, sofar) + | otherwise = do + stepped <- stepThread fixed runconc runstm (_continuation $ fromJust thread) idSource chosen threads + case stepped of + Right (threads', idSource', act) -> + let sofar' = (decision, alternatives, act) : sofar + threads'' = if (interruptible <$> M.lookup chosen threads') == Just True then unblockWaitingOn chosen threads' else threads' + in go idSource' sofar' (Just chosen) g' threads'' + + Left UncaughtException + | chosen == 0 -> writeRef fixed ref (Just $ Left UncaughtException) >> return (g, idSource, sofar) + | otherwise -> + let sofar' = (decision, alternatives, Killed) : sofar + threads' = unblockWaitingOn chosen $ kill chosen threads + in go idSource sofar' (Just chosen) g' threads' + + Left failure -> writeRef fixed ref (Just $ Left failure) >> return (g, idSource, sofar) + + where + (chosen, g') = sched g ((\p (_,_,a) -> (p,a)) <$> prior <*> listToMaybe sofar) $ unsafeToNonEmpty runnable' + runnable' = [(t, nextActions t) | t <- sort $ M.keys runnable] + runnable = M.filter (isNothing . _blocking) threads + thread = M.lookup chosen threads + isBlocked = isJust . _blocking $ fromJust thread + isNonexistant = isNothing thread + isTerminated = 0 `notElem` M.keys threads + isDeadlocked = isLocked 0 threads && (((~= OnCVarFull undefined) <$> M.lookup 0 threads) == Just True || + ((~= OnCVarEmpty undefined) <$> M.lookup 0 threads) == Just True || + ((~= OnMask undefined) <$> M.lookup 0 threads) == Just True) + isSTMLocked = isLocked 0 threads && ((~= OnCTVar []) <$> M.lookup 0 threads) == Just True + + runconc ma i = do { (a,_,i',_) <- runFixed' fixed runstm sched g i ma; return (a,i') } + + unblockWaitingOn tid = M.map unblock where + unblock thrd = case _blocking thrd of + Just (OnMask t) | t == tid -> thrd { _blocking = Nothing } + _ -> thrd + + decision + | Just chosen == prior = Continue + | prior `notElem` map (Just . fst) runnable' = Start chosen + | otherwise = SwitchTo chosen + + alternatives + | Just chosen == prior = [(SwitchTo t, na) | (t, na) <- runnable', Just t /= prior] + | prior `notElem` map (Just . fst) runnable' = [(Start t, na) | (t, na) <- runnable', t /= chosen] + | otherwise = [(if Just t == prior then Continue else SwitchTo t, na) | (t, na) <- runnable', t /= chosen] + + nextActions t = unsafeToNonEmpty . nextActions' . _continuation . fromJust $ M.lookup t threads + nextActions' (AFork _ _) = [WillFork] + nextActions' (AMyTId _) = [WillMyThreadId] + nextActions' (ANew _) = [WillNew] + nextActions' (APut (c, _) _ k) = WillPut c : nextActions' k + nextActions' (ATryPut (c, _) _ _) = [WillTryPut c] + nextActions' (AGet (c, _) _) = [WillRead c] + nextActions' (ATake (c, _) _) = [WillTake c] + nextActions' (ATryTake (c, _) _) = [WillTryTake c] + nextActions' (ANewRef _) = [WillNewRef] + nextActions' (AReadRef (r, _) _) = [WillReadRef r] + nextActions' (AModRef (r, _) _ _) = [WillModRef r] + nextActions' (AAtom _ _) = [WillSTM] + nextActions' (AThrow _) = [WillThrow] + nextActions' (AThrowTo tid _ k) = WillThrowTo tid : nextActions' k + nextActions' (ACatching _ _ _) = [WillCatching] + nextActions' (APopCatching k) = WillPopCatching : nextActions' k + nextActions' (AMasking ms _ _) = [WillSetMasking False ms] + nextActions' (AResetMask b1 b2 ms k) = (if b1 then WillSetMasking else WillResetMasking) b2 ms : nextActions' k + nextActions' (ALift _) = [WillLift] + nextActions' (ANoTest _ _) = [WillNoTest] + nextActions' (AKnowsAbout _ k) = WillKnowsAbout : nextActions' k + nextActions' (AForgets _ k) = WillForgets : nextActions' k + nextActions' (AAllKnown k) = WillAllKnown : nextActions' k + nextActions' (AStop) = [WillStop] + +-------------------------------------------------------------------------------- +-- * Single-step execution + +-- | Run a single thread one step, by dispatching on the type of +-- 'Action'. +stepThread :: forall n r s. (Functor n, Monad n) => Fixed n r s + -> (forall x. M n r s x -> IdSource -> n (Either Failure x, IdSource)) + -- ^ Run a 'MonadConc' computation atomically. + -> (forall x. s n r x -> CTVarId -> n (Result x, CTVarId)) + -- ^ Run a 'MonadSTM' transaction atomically. + -> Action n r s + -- ^ Action to step + -> IdSource + -- ^ Source of fresh IDs + -> ThreadId + -- ^ ID of the current thread + -> Threads n r s + -- ^ Current state of threads + -> n (Either Failure (Threads n r s, IdSource, ThreadAction)) +stepThread fixed runconc runstm action idSource tid threads = case action of + AFork a b -> stepFork a b + AMyTId c -> stepMyTId c + APut ref a c -> stepPut ref a c + ATryPut ref a c -> stepTryPut ref a c + AGet ref c -> stepGet ref c + ATake ref c -> stepTake ref c + ATryTake ref c -> stepTryTake ref c + AReadRef ref c -> stepReadRef ref c + AModRef ref f c -> stepModRef ref f c + AAtom stm c -> stepAtom stm c + ANew na -> stepNew na + ANewRef na -> stepNewRef na + ALift na -> stepLift na + AThrow e -> stepThrow e + AThrowTo t e c -> stepThrowTo t e c + ACatching h ma c -> stepCatching h ma c + APopCatching a -> stepPopCatching a + AMasking m ma c -> stepMasking m ma c + AResetMask b1 b2 m c -> stepResetMask b1 b2 m c + ANoTest ma a -> stepNoTest ma a + AKnowsAbout v c -> stepKnowsAbout v c + AForgets v c -> stepForgets v c + AAllKnown c -> stepAllKnown c + AStop -> stepStop + + where + -- | Start a new thread, assigning it the next 'ThreadId' + stepFork a b = return $ Right (goto (b newtid) tid threads', idSource', Fork newtid) where + threads' = launch tid newtid a threads + (idSource', newtid) = nextTId idSource + + -- | Get the 'ThreadId' of the current thread + stepMyTId c = return $ Right (goto (c tid) tid threads, idSource, MyThreadId) + + -- | Put a value into a @CVar@, blocking the thread until it's + -- empty. + stepPut cvar@(cvid, _) a c = do + (success, threads', woken) <- putIntoCVar True cvar a (const c) fixed tid threads + return $ Right (threads', idSource, if success then Put cvid woken else BlockedPut cvid) + + -- | Try to put a value into a @CVar@, without blocking. + stepTryPut cvar@(cvid, _) a c = do + (success, threads', woken) <- putIntoCVar False cvar a c fixed tid threads + return $ Right (threads', idSource, TryPut cvid success woken) + + -- | Get the value from a @CVar@, without emptying, blocking the + -- thread until it's full. + stepGet cvar@(cvid, _) c = do + (success, threads', _) <- readFromCVar False True cvar (c . fromJust) fixed tid threads + return $ Right (threads', idSource, if success then Read cvid else BlockedRead cvid) + + -- | Take the value from a @CVar@, blocking the thread until it's + -- full. + stepTake cvar@(cvid, _) c = do + (success, threads', woken) <- readFromCVar True True cvar (c . fromJust) fixed tid threads + return $ Right (threads', idSource, if success then Take cvid woken else BlockedTake cvid) + + -- | Try to take the value from a @CVar@, without blocking. + stepTryTake cvar@(cvid, _) c = do + (success, threads', woken) <- readFromCVar True False cvar c fixed tid threads + return $ Right (threads', idSource, TryTake cvid success woken) + + -- | Read from a @CRef@. + stepReadRef (crid, ref) c = do + val <- readRef fixed ref + return $ Right (goto (c val) tid threads, idSource, ReadRef crid) + + -- | Modify a @CRef@. + stepModRef (crid, ref) f c = do + (new, val) <- f <$> readRef fixed ref + writeRef fixed ref new + return $ Right (goto (c val) tid threads, idSource, ModRef crid) + + -- | Run a STM transaction atomically. + stepAtom stm c = do + let oldctvid = _nextCTVId idSource + (res, newctvid) <- runstm stm oldctvid + case res of + Success readen written val + | any ( + let (threads', woken) = wake (OnCTVar written) threads + in return $ Right (knows (map Right written) tid $ goto (c val) tid threads', idSource { _nextCTVId = newctvid }, STM woken) + | otherwise -> + return $ Right (knows (map Right written) tid $ goto (c val) tid threads, idSource { _nextCTVId = newctvid }, FreshSTM) + Retry touched -> + let threads' = block (OnCTVar touched) tid threads + in return $ Right (threads', idSource { _nextCTVId = newctvid }, BlockedSTM) + Exception e -> stepThrow e + + -- | Run a subcomputation in an exception-catching context. + stepCatching h ma c = return $ Right (threads', idSource, Catching) where + a = runCont ma (APopCatching . c) + e exc = runCont (h exc) (APopCatching . c) + + threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = a, _handlers = Handler e : _handlers thread }) tid threads + + -- | Pop the top exception handler from the thread's stack. + stepPopCatching a = return $ Right (threads', idSource, PopCatching) where + threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = a, _handlers = tail $_handlers thread }) tid threads + + -- | Throw an exception, and propagate it to the appropriate + -- handler. + stepThrow e = return $ + case propagate e . _handlers . fromJust $ M.lookup tid threads of + Just (act, hs) -> + let threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = act, _handlers = hs }) tid threads + in Right (threads', idSource, Throw) + Nothing -> Left UncaughtException + + -- | Throw an exception to the target thread, and propagate it to + -- the appropriate handler. + stepThrowTo t e c = return $ + let threads' = goto c tid threads + blocked = M.alter (\(Just thread) -> Just $ thread { _blocking = Just (OnMask t) }) tid threads + interrupted act hs = M.alter (\(Just thread) -> Just $ thread { _continuation = act, _blocking = Nothing, _handlers = hs }) t + in case M.lookup t threads of + Just thread + | interruptible thread -> case propagate e $ _handlers thread of + Just (act, hs) -> Right (interrupted act hs threads', idSource, ThrowTo t) + Nothing + | t == 0 -> Left UncaughtException + | otherwise -> Right (kill t threads', idSource, ThrowTo t) + | otherwise -> Right (blocked, idSource, BlockedThrowTo t) + Nothing -> Right (threads', idSource, ThrowTo t) + + -- | Execute a subcomputation with a new masking state, and give + -- it a function to run a computation with the current masking + -- state. + -- + -- Explicit type sig necessary for checking in the prescence of + -- 'umask', sadly. + stepMasking :: MaskingState + -> ((forall b. M n r s b -> M n r s b) -> M n r s a) + -> (a -> Action n r s) + -> n (Either Failure (Threads n r s, IdSource, ThreadAction)) + stepMasking m ma c = return $ Right (threads', idSource, SetMasking False m) where + a = runCont (ma umask) (AResetMask False False m' . c) + + m' = _masking . fromJust $ M.lookup tid threads + umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> return b + resetMask typ mask = cont $ \k -> AResetMask typ True mask $ k () + + threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = a, _masking = m }) tid threads + + -- | Reset the masking thread of the state. + stepResetMask b1 b2 m c = return $ Right (threads', idSource, (if b1 then SetMasking else ResetMasking) b2 m) where + threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = c, _masking = m }) tid threads + + -- | Create a new @CVar@, using the next 'CVarId'. + stepNew na = do + let (idSource', newcvid) = nextCVId idSource + a <- na newcvid + return $ Right (knows [Left newcvid] tid $ goto a tid threads, idSource', New newcvid) + + -- | Create a new @CRef@, using the next 'CRefId'. + stepNewRef na = do + let (idSource', newcrid) = nextCRId idSource + a <- na newcrid + return $ Right (goto a tid threads, idSource', NewRef newcrid) + + -- | Lift an action from the underlying monad into the @Conc@ + -- computation. + stepLift na = do + a <- na + return $ Right (goto a tid threads, idSource, Lift) + + -- | Run a computation atomically. If this fails, the entire thing fails. + stepNoTest ma c = do + (a, idSource') <- runconc ma idSource + return $ + case a of + Right a' -> Right (goto (c a') tid threads, idSource', NoTest) + _ -> Left FailureInNoTest + + -- | Record that a variable is known about. + stepKnowsAbout v c = return $ Right (knows [v] tid $ goto c tid threads, idSource, KnowsAbout) + + -- | Record that a variable will never be touched again. + stepForgets v c = return $ Right (forgets [v] tid $ goto c tid threads, idSource, Forgets) + + -- | Record that all shared variables are known. + stepAllKnown c = return $ Right (fullknown tid $ goto c tid threads, idSource, AllKnown) + + -- | Kill the current thread. + stepStop = return $ Right (kill tid threads, idSource, Stop) diff --git a/Test/DejaFu/Deterministic/Internal/CVar.hs b/Test/DejaFu/Deterministic/Internal/CVar.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Deterministic/Internal/CVar.hs @@ -0,0 +1,54 @@ +-- | Operations over @CVar@s +module Test.DejaFu.Deterministic.Internal.CVar where + +import Control.Monad (when) +import Test.DejaFu.Internal +import Test.DejaFu.Deterministic.Internal.Common +import Test.DejaFu.Deterministic.Internal.Threading + +-------------------------------------------------------------------------------- +-- * Manipulating @CVar@s + +-- | Put a value into a @CVar@, in either a blocking or nonblocking +-- way. +putIntoCVar :: Monad n + => Bool -> V r a -> a -> (Bool -> Action n r s) + -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId]) +putIntoCVar blocking (cvid, ref) a c fixed threadid threads = do + val <- readRef fixed ref + + case val of + Just _ + | blocking -> + let threads' = block (OnCVarEmpty cvid) threadid threads + in return (False, threads', []) + + | otherwise -> + return (False, goto (c False) threadid threads, []) + + Nothing -> do + writeRef fixed ref $ Just a + let (threads', woken) = wake (OnCVarFull cvid) threads + return (True, goto (c True) threadid threads', woken) + +-- | Take a value from a @CVar@, in either a blocking or nonblocking +-- way. +readFromCVar :: Monad n + => Bool -> Bool -> V r a -> (Maybe a -> Action n r s) + -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId]) +readFromCVar emptying blocking (cvid, ref) c fixed threadid threads = do + val <- readRef fixed ref + + case val of + Just _ -> do + when emptying $ writeRef fixed ref Nothing + let (threads', woken) = wake (OnCVarEmpty cvid) threads + return (True, goto (c val) threadid threads', woken) + + Nothing + | blocking -> + let threads' = block (OnCVarFull cvid) threadid threads + in return (False, threads', []) + + | otherwise -> + return (False, goto (c Nothing) threadid threads, []) diff --git a/Test/DejaFu/Deterministic/Internal/Common.hs b/Test/DejaFu/Deterministic/Internal/Common.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Deterministic/Internal/Common.hs @@ -0,0 +1,345 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE RankNTypes #-} + +-- | Common types and utility functions for deterministic execution of +-- 'MonadConc' implementations. +module Test.DejaFu.Deterministic.Internal.Common where + +import Control.DeepSeq (NFData(..)) +import Control.Exception (Exception, MaskingState(..), SomeException(..)) +import Control.Monad.Cont (Cont) +import Data.List.Extra +import Test.DejaFu.Internal +import Test.DejaFu.STM (CTVarId) + +-------------------------------------------------------------------------------- +-- * The @Conc@ Monad + +-- | The underlying monad is based on continuations over Actions. +type M n r s a = Cont (Action n r s) a + +-- | CVars are represented as a unique numeric identifier, and a +-- reference containing a Maybe value. +type V r a = (CVarId, r (Maybe a)) + +-- | CRefs are represented as a unique numeric identifier, and a +-- reference containing a value. +type R r a = (CRefId, r a) + +-- | Dict of methods for implementations to override. +type Fixed n r s = Ref n r (Cont (Action n r s)) + +-------------------------------------------------------------------------------- +-- * Primitive Actions + +-- | Scheduling is done in terms of a trace of 'Action's. Blocking can +-- only occur as a result of an action, and they cover (most of) the +-- primitives of the concurrency. 'spawn' is absent as it is +-- implemented in terms of 'newEmptyCVar', 'fork', and 'putCVar'. +data Action n r s = + AFork ((forall b. M n r s b -> M n r s b) -> Action n r s) (ThreadId -> Action n r s) + | AMyTId (ThreadId -> Action n r s) + | forall a. APut (V r a) a (Action n r s) + | forall a. ATryPut (V r a) a (Bool -> Action n r s) + | forall a. AGet (V r a) (a -> Action n r s) + | forall a. ATake (V r a) (a -> Action n r s) + | forall a. ATryTake (V r a) (Maybe a -> Action n r s) + | forall a. AReadRef (R r a) (a -> Action n r s) + | forall a b. AModRef (R r a) (a -> (a, b)) (b -> Action n r s) + | forall a. ANoTest (M n r s a) (a -> Action n r s) + | forall a. AAtom (s n r a) (a -> Action n r s) + | ANew (CVarId -> n (Action n r s)) + | ANewRef (CRefId -> n (Action n r s)) + | ALift (n (Action n r s)) + | AThrow SomeException + | AThrowTo ThreadId SomeException (Action n r s) + | forall a e. Exception e => ACatching (e -> M n r s a) (M n r s a) (a -> Action n r s) + | APopCatching (Action n r s) + | forall a. AMasking MaskingState ((forall b. M n r s b -> M n r s b) -> M n r s a) (a -> Action n r s) + | AResetMask Bool Bool MaskingState (Action n r s) + | AKnowsAbout (Either CVarId CTVarId) (Action n r s) + | AForgets (Either CVarId CTVarId) (Action n r s) + | AAllKnown (Action n r s) + | AStop + +-------------------------------------------------------------------------------- +-- * Identifiers + +-- | Every live thread has a unique identitifer. +type ThreadId = Int + +-- | Every 'CVar' has a unique identifier. +type CVarId = Int + +-- | Every 'CRef' has a unique identifier. +type CRefId = Int + +-- | The number of ID parameters was getting a bit unwieldy, so this +-- hides them all away. +data IdSource = Id { _nextCRId :: CRefId, _nextCVId :: CVarId, _nextCTVId :: CTVarId, _nextTId :: ThreadId } + +-- | Get the next free 'CRefId'. +nextCRId :: IdSource -> (IdSource, CRefId) +nextCRId idsource = let newid = _nextCRId idsource + 1 in (idsource { _nextCRId = newid }, newid) + +-- | Get the next free 'CVarId'. +nextCVId :: IdSource -> (IdSource, CVarId) +nextCVId idsource = let newid = _nextCVId idsource + 1 in (idsource { _nextCVId = newid }, newid) + +-- | Get the next free 'CTVarId'. +nextCTVId :: IdSource -> (IdSource, CTVarId) +nextCTVId idsource = let newid = _nextCTVId idsource + 1 in (idsource { _nextCTVId = newid }, newid) + +-- | Get the next free 'ThreadId'. +nextTId :: IdSource -> (IdSource, ThreadId) +nextTId idsource = let newid = _nextTId idsource + 1 in (idsource { _nextTId = newid }, newid) + +-- | The initial ID source. +initialIdSource :: IdSource +initialIdSource = Id 0 0 0 0 + +-------------------------------------------------------------------------------- +-- * Scheduling & Traces + +-- | A @Scheduler@ maintains some internal state, @s@, takes the +-- 'ThreadId' of the last thread scheduled, or 'Nothing' if this is +-- the first decision, and the list of runnable threads along with +-- what each will do in the next steps (as far as can be +-- determined). It produces a 'ThreadId' to schedule, and a new state. +-- +-- __Note:__ In order to prevent computation from hanging, the runtime +-- will assume that a deadlock situation has arisen if the scheduler +-- attempts to (a) schedule a blocked thread, or (b) schedule a +-- nonexistent thread. In either of those cases, the computation will +-- be halted. +type Scheduler s = s -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, NonEmpty Lookahead) -> (ThreadId, s) + +-- | One of the outputs of the runner is a @Trace@, which is a log of +-- decisions made, alternative decisions (including what action would +-- have been performed had that decision been taken), and the action a +-- thread took in its step. +type Trace = [(Decision, [(Decision, Lookahead)], ThreadAction)] + +-- | Like a 'Trace', but gives more lookahead (where possible) for +-- alternative decisions. +type Trace' = [(Decision, [(Decision, NonEmpty Lookahead)], ThreadAction)] + +-- | Throw away information from a 'Trace'' to get just a 'Trace'. +toTrace :: Trace' -> Trace +toTrace = map go where + go (dec, alters, act) = (dec, map (\(d, a:|_) -> (d, a)) alters, act) + +-- | Pretty-print a trace. +showTrace :: Trace -> String +showTrace = trace "" 0 where + trace prefix num ((Start tid,_,_):ds) = thread prefix num ++ trace ("S" ++ show tid) 1 ds + trace prefix num ((SwitchTo tid,_,_):ds) = thread prefix num ++ trace ("P" ++ show tid) 1 ds + trace prefix num ((Continue,_,_):ds) = trace prefix (num + 1) ds + trace prefix num [] = thread prefix num + + thread prefix num = prefix ++ replicate num '-' + +-- | Scheduling decisions are based on the state of the running +-- program, and so we can capture some of that state in recording what +-- specific decision we made. +data Decision = + Start ThreadId + -- ^ Start a new thread, because the last was blocked (or it's the + -- start of computation). + | Continue + -- ^ Continue running the last thread for another step. + | SwitchTo ThreadId + -- ^ Pre-empt the running thread, and switch to another. + deriving (Eq, Show) + +instance NFData Decision where + rnf (Start tid) = rnf tid + rnf (SwitchTo tid) = rnf tid + rnf Continue = () + +-- | All the actions that a thread can perform. +data ThreadAction = + Fork ThreadId + -- ^ Start a new thread. + | MyThreadId + -- ^ Get the 'ThreadId' of the current thread. + | New CVarId + -- ^ Create a new 'CVar'. + | Put CVarId [ThreadId] + -- ^ Put into a 'CVar', possibly waking up some threads. + | BlockedPut CVarId + -- ^ Get blocked on a put. + | TryPut CVarId Bool [ThreadId] + -- ^ Try to put into a 'CVar', possibly waking up some threads. + | Read CVarId + -- ^ Read from a 'CVar'. + | BlockedRead CVarId + -- ^ Get blocked on a read. + | Take CVarId [ThreadId] + -- ^ Take from a 'CVar', possibly waking up some threads. + | BlockedTake CVarId + -- ^ Get blocked on a take. + | TryTake CVarId Bool [ThreadId] + -- ^ Try to take from a 'CVar', possibly waking up some threads. + | NewRef CRefId + -- ^ Create a new 'CRef'. + | ReadRef CRefId + -- ^ Read from a 'CRef'. + | ModRef CRefId + -- ^ Modify a 'CRef'. + | STM [ThreadId] + -- ^ An STM transaction was executed, possibly waking up some + -- threads. + | FreshSTM + -- ^ An STM transaction was executed, and all it did was create and + -- write to new 'CTVar's, no existing 'CTVar's were touched. + | BlockedSTM + -- ^ Got blocked in an STM transaction. + | Catching + -- ^ Register a new exception handler + | PopCatching + -- ^ Pop the innermost exception handler from the stack. + | Throw + -- ^ Throw an exception. + | ThrowTo ThreadId + -- ^ Throw an exception to a thread. + | BlockedThrowTo ThreadId + -- ^ Get blocked on a 'throwTo'. + | Killed + -- ^ Killed by an uncaught exception. + | SetMasking Bool MaskingState + -- ^ Set the masking state. If 'True', this is being used to set the + -- masking state to the original state in the argument passed to a + -- 'mask'ed function. + | ResetMasking Bool MaskingState + -- ^ Return to an earlier masking state. If 'True', this is being + -- used to return to the state of the masked block in the argument + -- passed to a 'mask'ed function. + | Lift + -- ^ Lift an action from the underlying monad. Note that the + -- penultimate action in a trace will always be a @Lift@, this is an + -- artefact of how the runner works. + | NoTest + -- ^ A computation annotated with '_concNoTest' was executed in a + -- single step. + | KnowsAbout + -- ^ A '_concKnowsAbout' annotation was processed. + | Forgets + -- ^ A '_concForgets' annotation was processed. + | AllKnown + -- ^ A '_concALlKnown' annotation was processed. + | Stop + -- ^ Cease execution and terminate. + deriving (Eq, Show) + +instance NFData ThreadAction where + rnf (TryTake c b tids) = rnf (c, b, tids) + rnf (TryPut c b tids) = rnf (c, b, tids) + rnf (SetMasking b m) = m `seq` b `seq` () + rnf (ResetMasking b m) = m `seq` b `seq` () + rnf (BlockedRead c) = rnf c + rnf (BlockedTake c) = rnf c + rnf (BlockedPut c) = rnf c + rnf (ThrowTo tid) = rnf tid + rnf (Take c tids) = rnf (c, tids) + rnf (Put c tids) = rnf (c, tids) + rnf (STM tids) = rnf tids + rnf (Fork tid) = rnf tid + rnf (New c) = rnf c + rnf (Read c) = rnf c + rnf ta = ta `seq` () + +-- | A one-step look-ahead at what a thread will do next. +data Lookahead = + WillFork + -- ^ Will start a new thread. + | WillMyThreadId + -- ^ Will get the 'ThreadId'. + | WillNew + -- ^ Will create a new 'CVar'. + | WillPut CVarId + -- ^ Will put into a 'CVar', possibly waking up some threads. + | WillTryPut CVarId + -- ^ Will try to put into a 'CVar', possibly waking up some threads. + | WillRead CVarId + -- ^ Will read from a 'CVar'. + | WillTake CVarId + -- ^ Will take from a 'CVar', possibly waking up some threads. + | WillTryTake CVarId + -- ^ Will try to take from a 'CVar', possibly waking up some threads. + | WillNewRef + -- ^ Will create a new 'CRef'. + | WillReadRef CRefId + -- ^ Will read from a 'CRef'. + | WillModRef CRefId + -- ^ Will modify a 'CRef'. + | WillSTM + -- ^ Will execute an STM transaction, possibly waking up some + -- threads. + | WillCatching + -- ^ Will register a new exception handler + | WillPopCatching + -- ^ Will pop the innermost exception handler from the stack. + | WillThrow + -- ^ Will throw an exception. + | WillThrowTo ThreadId + -- ^ Will throw an exception to a thread. + | WillSetMasking Bool MaskingState + -- ^ Will set the masking state. If 'True', this is being used to + -- set the masking state to the original state in the argument + -- passed to a 'mask'ed function. + | WillResetMasking Bool MaskingState + -- ^ Will return to an earlier masking state. If 'True', this is + -- being used to return to the state of the masked block in the + -- argument passed to a 'mask'ed function. + | WillLift + -- ^ Will lift an action from the underlying monad. Note that the + -- penultimate action in a trace will always be a @Lift@, this is an + -- artefact of how the runner works. + | WillNoTest + -- ^ Will execute a computation annotated with '_concNoTest' in a + -- single step. + | WillKnowsAbout + -- ^ Will process a '_concKnowsAbout' annotation. + | WillForgets + -- ^ Will process a '_concForgets' annotation. + | WillAllKnown + -- ^ Will process a '_concALlKnown' annotation. + | WillStop + -- ^ Will cease execution and terminate. + deriving (Eq, Show) + +instance NFData Lookahead where + rnf (WillSetMasking b ms) = b `seq` ms `seq` () + rnf (WillResetMasking b ms) = b `seq` ms `seq` () + rnf (WillPut c) = rnf c + rnf (WillTryPut c) = rnf c + rnf (WillRead c) = rnf c + rnf (WillTake c) = rnf c + rnf (WillTryTake c) = rnf c + rnf (WillReadRef c) = rnf c + rnf (WillModRef c) = rnf c + rnf ta = ta `seq` () + +-------------------------------------------------------------------------------- +-- * Failures + +-- | An indication of how a concurrent computation failed. +data Failure = + InternalError + -- ^ Will be raised if the scheduler does something bad. This should + -- never arise unless you write your own, faulty, scheduler! If it + -- does, please file a bug report. + | Deadlock + -- ^ The computation became blocked indefinitely on @CVar@s. + | STMDeadlock + -- ^ The computation became blocked indefinitely on @CTVar@s. + | UncaughtException + -- ^ An uncaught exception bubbled to the top of the computation. + | FailureInNoTest + -- ^ A computation annotated with '_concNoTest' produced a failure, + -- rather than a result. + deriving (Eq, Show) + +instance NFData Failure where + rnf f = f `seq` () -- WHNF == NF diff --git a/Test/DejaFu/Deterministic/Internal/Threading.hs b/Test/DejaFu/Deterministic/Internal/Threading.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Deterministic/Internal/Threading.hs @@ -0,0 +1,174 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE RankNTypes #-} + +-- | Operations and types for threads. +module Test.DejaFu.Deterministic.Internal.Threading where + +import Control.Exception (Exception, MaskingState(..), SomeException(..), fromException) +import Control.Monad.Cont (cont) +import Data.List (intersect, nub) +import Data.Map (Map) +import Data.Maybe (fromMaybe, isJust, isNothing) +import Test.DejaFu.STM (CTVarId) +import Test.DejaFu.Deterministic.Internal.Common + +import qualified Data.Map as M + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative ((<$>)) +#endif + +-------------------------------------------------------------------------------- +-- * Threads + +-- | Threads are stored in a map index by 'ThreadId'. +type Threads n r s = Map ThreadId (Thread n r s) + +-- | All the state of a thread. +data Thread n r s = Thread + { _continuation :: Action n r s + -- ^ The next action to execute. + , _blocking :: Maybe BlockedOn + -- ^ The state of any blocks. + , _handlers :: [Handler n r s] + -- ^ Stack of exception handlers + , _masking :: MaskingState + -- ^ The exception masking state. + , _known :: [Either CVarId CTVarId] + -- ^ Shared variables the thread knows about. + , _fullknown :: Bool + -- ^ Whether the referenced variables of the thread are completely + -- known. If every thread has _fullknown == True, then turn on + -- detection of nonglobal deadlock. + } + +-------------------------------------------------------------------------------- +-- * Blocking + +-- | A @BlockedOn@ is used to determine what sort of variable a thread +-- is blocked on. +data BlockedOn = OnCVarFull CVarId | OnCVarEmpty CVarId | OnCTVar [CTVarId] | OnMask ThreadId deriving Eq + +-- | Determine if a thread is blocked in a certain way. +(~=) :: Thread n r s -> BlockedOn -> Bool +thread ~= theblock = case (_blocking thread, theblock) of + (Just (OnCVarFull _), OnCVarFull _) -> True + (Just (OnCVarEmpty _), OnCVarEmpty _) -> True + (Just (OnCTVar _), OnCTVar _) -> True + (Just (OnMask _), OnMask _) -> True + _ -> False + +-- | Determine if a thread is deadlocked. If at least one thread is +-- not in a fully-known state, this will only check for global +-- deadlock. +isLocked :: ThreadId -> Threads n r a -> Bool +isLocked tid ts + | allKnown = case M.lookup tid ts of + Just thread -> noRefs $ _blocking thread + Nothing -> False + | otherwise = M.null $ M.filter (isNothing . _blocking) ts + + where + -- | Check if all threads are in a fully-known state. + allKnown = all _fullknown $ M.elems ts + + -- | Check if no other runnable thread has a reference to anything + -- the block references. + noRefs (Just (OnCVarFull cvarid)) = null $ findCVar cvarid + noRefs (Just (OnCVarEmpty cvarid)) = null $ findCVar cvarid + noRefs (Just (OnCTVar ctvids)) = null $ findCTVars ctvids + noRefs _ = True + + -- | Get IDs of all threads (other than the one under + -- consideration) which reference a 'CVar'. + findCVar cvarid = M.keys $ M.filterWithKey (check [Left cvarid]) ts + + -- | Get IDs of all runnable threads (other than the one under + -- consideration) which reference some 'CTVar's. + findCTVars ctvids = M.keys $ M.filterWithKey (check (map Right ctvids)) ts + + -- | Check if a thread references a variable, and if it's not the + -- thread under consideration. + check lookingfor thetid thethread + | thetid == tid = False + | otherwise = (not . null $ lookingfor `intersect` _known thethread) && isNothing (_blocking thethread) + +-------------------------------------------------------------------------------- +-- * Exceptions + +-- | An exception handler. +data Handler n r s = forall e. Exception e => Handler (e -> Action n r s) + +-- | Propagate an exception upwards, finding the closest handler +-- which can deal with it. +propagate :: SomeException -> [Handler n r s] -> Maybe (Action n r s, [Handler n r s]) +propagate _ [] = Nothing +propagate e (Handler h:hs) = maybe (propagate e hs) (\act -> Just (act, hs)) $ h <$> e' where + e' = fromException e + +-- | Check if a thread can be interrupted by an exception. +interruptible :: Thread n r s -> Bool +interruptible thread = _masking thread == Unmasked || (_masking thread == MaskedInterruptible && isJust (_blocking thread)) + +-------------------------------------------------------------------------------- +-- * Manipulating threads + +-- | Replace the @Action@ of a thread. +goto :: Action n r s -> ThreadId -> Threads n r s -> Threads n r s +goto a = M.alter $ \(Just thread) -> Just (thread { _continuation = a }) + +-- | Start a thread with the given ID, inheriting the masking state +-- from the parent thread. This ID must not already be in use! +launch :: ThreadId -> ThreadId -> ((forall b. M n r s b -> M n r s b) -> Action n r s) -> Threads n r s -> Threads n r s +launch parent tid a threads = launch' mask tid a threads where + mask = fromMaybe Unmasked $ _masking <$> M.lookup parent threads + +-- | Start a thread with the given ID and masking state. This must not already be in use! +launch' :: MaskingState -> ThreadId -> ((forall b. M n r s b -> M n r s b) -> Action n r s) -> Threads n r s -> Threads n r s +launch' mask tid a = M.insert tid thread where + thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = mask, _known = [], _fullknown = False } + + umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False mask >> return b + resetMask typ m = cont $ \k -> AResetMask typ True m $ k () + +-- | Kill a thread. +kill :: ThreadId -> Threads n r s -> Threads n r s +kill = M.delete + +-- | Block a thread. +block :: BlockedOn -> ThreadId -> Threads n r s -> Threads n r s +block blockedOn = M.alter doBlock where + doBlock (Just thread) = Just $ thread { _blocking = Just blockedOn } + doBlock _ = error "Invariant failure in 'block': thread does NOT exist!" + +-- | Unblock all threads waiting on the appropriate block. For 'CTVar' +-- blocks, this will wake all threads waiting on at least one of the +-- given 'CTVar's. +wake :: BlockedOn -> Threads n r s -> (Threads n r s, [ThreadId]) +wake blockedOn threads = (M.map unblock threads, M.keys $ M.filter isBlocked threads) where + unblock thread + | isBlocked thread = thread { _blocking = Nothing } + | otherwise = thread + + isBlocked thread = case (_blocking thread, blockedOn) of + (Just (OnCTVar ctvids), OnCTVar blockedOn') -> ctvids `intersect` blockedOn' /= [] + (theblock, _) -> theblock == Just blockedOn + +-- | Record that a thread knows about a shared variable. +knows :: [Either CVarId CTVarId] -> ThreadId -> Threads n r s -> Threads n r s +knows theids = M.alter go where + go (Just thread) = Just $ thread { _known = nub $ theids ++ _known thread } + go _ = error "Invariant failure in 'knows': thread does NOT exist!" + +-- | Forget about a shared variable. +forgets :: [Either CVarId CTVarId] -> ThreadId -> Threads n r s -> Threads n r s +forgets theids = M.alter go where + go (Just thread) = Just $ thread { _known = filter (`notElem` theids) $ _known thread } + go _ = error "Invariant failure in 'forgets': thread does NOT exist!" + +-- | Record that a thread's shared variable state is fully known. +fullknown :: ThreadId -> Threads n r s -> Threads n r s +fullknown = M.alter go where + go (Just thread) = Just $ thread { _fullknown = True } + go _ = error "Invariant failure in 'fullknown': thread does NOT exist!" diff --git a/Test/DejaFu/Deterministic/Schedule.hs b/Test/DejaFu/Deterministic/Schedule.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Deterministic/Schedule.hs @@ -0,0 +1,57 @@ +-- | Deterministic scheduling for concurrent computations. +module Test.DejaFu.Deterministic.Schedule + ( Scheduler + , ThreadId + , NonEmpty(..) + -- * Pre-emptive + , randomSched + , roundRobinSched + -- * Non pre-emptive + , randomSchedNP + , roundRobinSchedNP + -- * Utilities + , makeNP + , toList + ) where + +import Data.List.Extra +import System.Random (RandomGen, randomR) +import Test.DejaFu.Deterministic.Internal + +-- | A simple random scheduler which, at every step, picks a random +-- thread to run. +randomSched :: RandomGen g => Scheduler g +randomSched g _ threads = (threads' !! choice, g') where + (choice, g') = randomR (0, length threads' - 1) g + threads' = map fst $ toList threads + +-- | A random scheduler which doesn't pre-empt the running +-- thread. That is, if the last thread scheduled is still runnable, +-- run that, otherwise schedule randomly. +randomSchedNP :: RandomGen g => Scheduler g +randomSchedNP = makeNP randomSched + +-- | A round-robin scheduler which, at every step, schedules the +-- thread with the next 'ThreadId'. +roundRobinSched :: Scheduler () +roundRobinSched _ Nothing _ = (0, ()) +roundRobinSched _ (Just (prior, _)) threads + | prior >= maximum threads' = (minimum threads', ()) + | otherwise = (minimum $ filter (>prior) threads', ()) + + where + threads' = map fst $ toList threads + +-- | A round-robin scheduler which doesn't pre-empt the running +-- thread. +roundRobinSchedNP :: Scheduler () +roundRobinSchedNP = makeNP roundRobinSched + +-- | Turn a potentially pre-emptive scheduler into a non-preemptive +-- one. +makeNP :: Scheduler s -> Scheduler s +makeNP sched = newsched where + newsched s p@(Just (prior, _)) threads + | prior `elem` map fst (toList threads) = (prior, s) + | otherwise = sched s p threads + newsched s Nothing threads = sched s Nothing threads diff --git a/Test/DejaFu/Internal.hs b/Test/DejaFu/Internal.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Internal.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE RankNTypes #-} + +-- | Dealing with mutable state. +module Test.DejaFu.Internal where + +import Control.Monad.ST (ST) +import Data.IORef (IORef, newIORef, readIORef, writeIORef) +import Data.STRef (STRef, newSTRef, readSTRef, writeSTRef) + +-- | Mutable references. +data Ref n r m = Ref + { newRef :: forall a. a -> n (r a) + , readRef :: forall a. r a -> n a + , writeRef :: forall a. r a -> a -> n () + , liftN :: forall a. n a -> m a + } + +-- | Method dict for 'ST'. +refST :: (forall a. ST t a -> m a) -> Ref (ST t) (STRef t) m +refST lftN = Ref + { newRef = newSTRef + , readRef = readSTRef + , writeRef = writeSTRef + , liftN = lftN + } + +-- | Method dict for 'IO'. +refIO :: (forall a. IO a -> m a) -> Ref IO IORef m +refIO lftN = Ref + { newRef = newIORef + , readRef = readIORef + , writeRef = writeIORef + , liftN = lftN + } diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/SCT.hs @@ -0,0 +1,239 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE RankNTypes #-} + +-- | Systematic testing for concurrent computations. +module Test.DejaFu.SCT + ( -- * Bounded Partial-order Reduction + + -- | We can characterise the state of a concurrent computation by + -- considering the ordering of dependent events. This is a partial + -- order: independent events can be performed in any order without + -- affecting the result, and so are /not/ ordered. + -- + -- Partial-order reduction is a technique for computing these + -- partial orders, and only testing one total order for each partial + -- order. This cuts down the amount of work to be done + -- significantly. /Bounded/ partial-order reduction is a further + -- optimisation, which only considers schedules within some bound. + -- + -- This module provides both a generic function for BPOR, and also a + -- pre-emption bounding BPOR runner, which is used by the + -- "Test.DejaFu" module. + -- + -- See /Bounded partial-order reduction/, K. Coons, M. Musuvathi, + -- K. McKinley for more details. + + BacktrackStep(..) + , sctBounded + , sctBoundedIO + + -- * Pre-emption Bounding + + -- | BPOR using pre-emption bounding. This adds conservative + -- backtracking points at the prior context switch whenever a + -- non-conervative backtracking point is added, as alternative + -- decisions can influence the reachability of different states. + -- + -- See the BPOR paper for more details. + + , sctPreBound + , sctPreBoundIO + + -- * Utilities + + , tidOf + , decisionOf + , activeTid + , preEmpCount + , initialCVState + , updateCVState + , willBlock + , willBlockSafely + ) where + +import Control.DeepSeq (force) +import Data.Functor.Identity (Identity(..), runIdentity) +import Data.IntMap.Strict (IntMap) +import Data.Sequence (Seq, (|>)) +import Data.Maybe (maybeToList, isNothing) +import Test.DejaFu.Deterministic +import Test.DejaFu.Deterministic.IO (ConcIO, runConcIO') +import Test.DejaFu.SCT.Internal + +import qualified Data.IntMap.Strict as I +import qualified Data.Set as S +import qualified Data.Sequence as Sq + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative ((<$>), (<*>)) +#endif + +-- * Pre-emption bounding + +-- | An SCT runner using a pre-emption bounding scheduler. +sctPreBound :: + Int + -- ^ The maximum number of pre-emptions to allow in a single + -- execution + -> (forall t. Conc t a) + -- ^ The computation to run many times + -> [(Either Failure a, Trace)] +sctPreBound pb = sctBounded (pbBv pb) pbBacktrack pbInitialise + +-- | Variant of 'sctPreBound' for computations which do 'IO'. +sctPreBoundIO :: Int -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)] +sctPreBoundIO pb = sctBoundedIO (pbBv pb) pbBacktrack pbInitialise + +-- | Check if a schedule is in the bound. +pbBv :: Int -> [Decision] -> Bool +pbBv pb ds = preEmpCount ds <= pb + +-- | Add a backtrack point, and also conservatively add one prior to +-- the most recent transition before that point. This may result in +-- the same state being reached multiple times, but is needed because +-- of the artificial dependency imposed by the bound. +pbBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep] +pbBacktrack bs i tid = maybe id (\j' b -> backtrack True b j' tid) j $ backtrack False bs i tid where + -- Index of the conservative point + j = goJ . reverse . pairs $ zip [0..i-1] bs where + goJ (((_,b1), (j',b2)):rest) + | _threadid b1 /= _threadid b2 = Just j' + | otherwise = goJ rest + goJ [] = Nothing + + {-# INLINE pairs #-} + pairs = zip <*> tail + + -- Add a backtracking point. If the thread isn't runnable, add all + -- runnable threads. + backtrack c bx@(b:rest) 0 t + -- If the backtracking point is already present, don't re-add it, + -- UNLESS this would force it to backtrack (it's conservative) + -- where before it might not. + | t `S.member` _runnable b = + let val = I.lookup t $ _backtrack b + in if isNothing val || (val == Just False && c) + then b { _backtrack = I.insert t c $ _backtrack b } : rest + else bx + + -- Otherwise just backtrack to everything runnable. + | otherwise = b { _backtrack = I.fromList [ (t',c) | t' <- S.toList $ _runnable b ] } : rest + + backtrack c (b:rest) n t = b : backtrack c rest (n-1) t + backtrack _ [] _ _ = error "Ran out of schedule whilst backtracking!" + +-- | Pick a new thread to run. Choose the current thread if available, +-- otherwise add all runnable threads. +pbInitialise :: Maybe (ThreadId, a) -> NonEmpty (ThreadId, b) -> NonEmpty ThreadId +pbInitialise prior threads@((nextTid, _):|rest) = case prior of + Just (tid, _) + | any (\(t, _) -> t == tid) $ toList threads -> tid:|[] + _ -> nextTid:|map fst rest + +-- * BPOR + +-- | SCT via BPOR. +-- +-- Schedules are generated by running the computation with a +-- deterministic scheduler with some initial list of decisions, after +-- which the supplied function is called. At each step of execution, +-- possible-conflicting actions are looked for, if any are found, +-- \"backtracking points\" are added, to cause the events to happen in +-- a different order in a future execution. +-- +-- Note that unlike with non-bounded partial-order reduction, this may +-- do some redundant work as the introduction of a bound can make +-- previously non-interfering events interfere with each other. +sctBounded :: ([Decision] -> Bool) + -- ^ Check if a prefix trace is within the bound. + -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) + -- ^ Add a new backtrack point, this takes the history of + -- the execution so far, the index to insert the + -- backtracking point, and the thread to backtrack to. This + -- may insert more than one backtracking point. + -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId) + -- ^ Produce possible scheduling decisions, all will be + -- tried. + -> (forall t. Conc t a) -> [(Either Failure a, Trace)] +sctBounded bv backtrack initialise c = runIdentity $ sctBoundedM bv backtrack initialise run where + run sched s = Identity $ runConc' sched s c + +-- | Variant of 'sctBounded' for computations which do 'IO'. +sctBoundedIO :: ([Decision] -> Bool) + -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) + -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId) + -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)] +sctBoundedIO bv backtrack initialise c = sctBoundedM bv backtrack initialise run where + run sched s = runConcIO' sched s c + +-- | Generic SCT runner. +sctBoundedM :: (Functor m, Monad m) + => ([Decision] -> Bool) + -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) + -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId) + -> (Scheduler SchedState -> SchedState -> m (Either Failure a, SchedState, Trace')) + -- ^ Monadic runner, with computation fixed. + -> m [(Either Failure a, Trace)] +sctBoundedM bv backtrack initialise run = go initialState where + go bpor = case next bpor of + Just (sched, conservative, bpor') -> do + (res, s, trace) <- run (bporSched initialise) (initialSchedState sched) + + let bpoints = findBacktrack backtrack (_sbpoints s) trace + let bpor'' = grow conservative trace bpor' + let bpor''' = todo bv bpoints bpor'' + + ((res, toTrace trace):) <$> go bpor''' + + Nothing -> return [] + +-- * BPOR Scheduler + +-- | The scheduler state +data SchedState = SchedState + { _sprefix :: [ThreadId] + -- ^ Decisions still to make + , _sbpoints :: Seq (NonEmpty (ThreadId, Lookahead), [ThreadId]) + -- ^ Which threads are runnable at each step, and the alternative + -- decisions still to make. + , _scvstate :: IntMap Bool + -- ^ The 'CVar' block state. + } + +-- | Initial scheduler state for a given prefix +initialSchedState :: [ThreadId] -> SchedState +initialSchedState prefix = SchedState + { _sprefix = prefix + , _sbpoints = Sq.empty + , _scvstate = initialCVState + } + +-- | BPOR scheduler: takes a list of decisions, and maintains a trace +-- including the runnable threads, and the alternative choices allowed +-- by the bound-specific initialise function. +bporSched :: (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId) + -> Scheduler SchedState +bporSched initialise = force $ \s prior threads -> case _sprefix s of + -- If there is a decision available, make it + (d:ds) -> + let threads' = fmap (\(t,a:|_) -> (t,a)) threads + cvstate' = maybe (_scvstate s) (updateCVState (_scvstate s) . snd) prior + in (d, s { _sprefix = ds, _sbpoints = _sbpoints s |> (threads', []), _scvstate = cvstate' }) + + -- Otherwise query the initialise function for a list of possible + -- choices, and make one of them arbitrarily (recording the others). + [] -> + let threads' = fmap (\(t,a:|_) -> (t,a)) threads + choices = initialise prior threads' + cvstate' = maybe (_scvstate s) (updateCVState (_scvstate s) . snd) prior + choices' = [t + | t <- toList choices + , as <- maybeToList $ lookup t (toList threads) + , not . willBlockSafely cvstate' $ toList as + ] + in case choices' of + (nextTid:rest) -> (nextTid, s { _sbpoints = _sbpoints s |> (threads', rest), _scvstate = cvstate' }) + + -- TODO: abort the execution here. + [] -> case choices of + (nextTid:|_) -> (nextTid, s { _sbpoints = _sbpoints s |> (threads', []), _scvstate = cvstate' }) diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/SCT/Internal.hs @@ -0,0 +1,334 @@ +{-# LANGUAGE CPP #-} + +-- | Internal utilities and types for BPOR. +module Test.DejaFu.SCT.Internal where + +import Control.DeepSeq (NFData(..)) +import Data.IntMap.Strict (IntMap) +import Data.List (foldl', partition, maximumBy) +import Data.Maybe (mapMaybe, fromJust) +import Data.Ord (comparing) +import Data.Sequence (Seq, ViewL(..)) +import Data.Set (Set) +import Test.DejaFu.Deterministic + +import qualified Data.IntMap.Strict as I +import qualified Data.Sequence as Sq +import qualified Data.Set as S + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative ((<$>), (<*>)) +#endif + +-- * BPOR state + +-- | One step of the execution, including information for backtracking +-- purposes. This backtracking information is used to generate new +-- schedules. +data BacktrackStep = BacktrackStep + { _threadid :: ThreadId + -- ^ The thread running at this step + , _decision :: (Decision, ThreadAction) + -- ^ What happened at this step. + , _runnable :: Set ThreadId + -- ^ The threads runnable at this step + , _backtrack :: IntMap Bool + -- ^ The list of alternative threads to run, and whether those + -- alternatives were added conservatively due to the bound. + } deriving (Eq, Show) + +instance NFData BacktrackStep where + rnf b = rnf (_threadid b, _decision b, _runnable b, _backtrack b) + +-- | BPOR execution is represented as a tree of states, characterised +-- by the decisions that lead to that state. +data BPOR = BPOR + { _brunnable :: Set ThreadId + -- ^ What threads are runnable at this step. + , _btodo :: IntMap Bool + -- ^ Follow-on decisions still to make, and whether that decision + -- was added conservatively due to the bound. + , _bignore :: Set ThreadId + -- ^ Follow-on decisions never to make, because they will result in + -- the chosen thread immediately blocking without achieving + -- anything, which can't have any effect on the result of the + -- program. + , _bdone :: IntMap BPOR + -- ^ Follow-on decisions that have been made. + , _bsleep :: IntMap ThreadAction + -- ^ Transitions to ignore (in this node and children) until a + -- dependent transition happens. + , _btaken :: IntMap ThreadAction + -- ^ Transitions which have been taken, excluding + -- conservatively-added ones, in the (reverse) order that they were + -- taken, as the 'Map' doesn't preserve insertion order. This is + -- used in implementing sleep sets. + } + +-- | Initial BPOR state. +initialState :: BPOR +initialState = BPOR + { _brunnable = S.singleton 0 + , _btodo = I.singleton 0 False + , _bignore = S.empty + , _bdone = I.empty + , _bsleep = I.empty + , _btaken = I.empty + } + +-- | Produce a new schedule from a BPOR tree. If there are no new +-- schedules remaining, return 'Nothing'. Also returns whether the +-- decision made was added conservatively. +-- +-- This returns the longest prefix, on the assumption that this will +-- lead to lots of backtracking points being identified before +-- higher-up decisions are reconsidered, so enlarging the sleep sets. +next :: BPOR -> Maybe ([ThreadId], Bool, BPOR) +next = go 0 where + go tid bpor = + -- All the possible prefix traces from this point, with + -- updated BPOR subtrees if taken from the done list. + let prefixes = mapMaybe go' (I.toList $ _bdone bpor) ++ [Left t | t <- I.toList $ _btodo bpor] + -- Sort by number of preemptions, in descending order. + cmp = comparing $ preEmps tid bpor . either (\(a,_) -> [a]) (\(a,_,_) -> a) + + in if null prefixes + then Nothing + else case maximumBy cmp prefixes of + -- If the prefix with the most preemptions is from the done list, update that. + Right (ts@(t:_), c, b) -> Just (ts, c, bpor { _bdone = I.insert t b $ _bdone bpor }) + Right ([], _, _) -> error "Invariant failure in 'next': empty done prefix!" + + -- If from the todo list, remove it. + Left (t,c) -> Just ([t], c, bpor { _btodo = I.delete t $ _btodo bpor }) + + go' (tid, bpor) = (\(ts,c,b) -> Right (tid:ts, c, b)) <$> go tid bpor + + preEmps tid bpor (t:ts) = + let rest = preEmps t (fromJust . I.lookup t $ _bdone bpor) ts + in if tid /= t && tid `S.member` _brunnable bpor then 1 + rest else rest + preEmps _ _ [] = 0::Int + +-- | Produce a list of new backtracking points from an execution +-- trace. +findBacktrack :: ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) + -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId]) + -> Trace' + -> [BacktrackStep] +findBacktrack backtrack = go S.empty 0 [] . Sq.viewl where + go allThreads tid bs ((e,i): (i', False)) i + } + bs' = doBacktrack allThreads (toList e) bs + allThreads' = allThreads `S.union` _runnable this + in go allThreads' tid' (bs' ++ [this]) (Sq.viewl is) ts + go _ _ bs _ _ = bs + + doBacktrack allThreads enabledThreads bs = + let tagged = reverse $ zip [0..] bs + idxs = [ (head is, u) + | (u, n) <- enabledThreads + , v <- S.toList allThreads + , u /= v + , let is = [ i + | (i, b) <- tagged + , _threadid b == v + , dependent' (snd $ _decision b) (u, n) + ] + , not $ null is] :: [(Int, ThreadId)] + in foldl' (\b (i, u) -> backtrack b i u) bs idxs + +-- | Add a new trace to the tree, creating a new subtree. +grow :: Bool -> Trace' -> BPOR -> BPOR +grow conservative = grow' initialCVState 0 where + grow' cvstate tid trc@((d, _, a):rest) bpor = + let tid' = tidOf tid d + cvstate' = updateCVState cvstate a + in case I.lookup tid' $ _bdone bpor of + Just bpor' -> bpor { _bdone = I.insert tid' (grow' cvstate' tid' rest bpor') $ _bdone bpor } + Nothing -> bpor { _btaken = if conservative then _btaken bpor else I.insert tid' a $ _btaken bpor + , _bdone = I.insert tid' (subtree cvstate' tid' (_bsleep bpor `I.union` _btaken bpor) trc) $ _bdone bpor } + grow' _ _ [] bpor = bpor + + subtree cvstate tid sleep ((d, ts, a):rest) = + let cvstate' = updateCVState cvstate a + sleep' = I.filterWithKey (\t a' -> not $ dependent a (t,a')) sleep + in BPOR + { _brunnable = S.fromList $ tids tid d a ts + , _btodo = I.empty + , _bignore = S.fromList [tidOf tid d' | (d',as) <- ts, willBlockSafely cvstate' $ toList as] + , _bdone = I.fromList $ case rest of + ((d', _, _):_) -> + let tid' = tidOf tid d' + in [(tid', subtree cvstate' tid' sleep' rest)] + [] -> [] + , _bsleep = sleep' + , _btaken = case rest of + ((d', _, a'):_) -> I.singleton (tidOf tid d') a' + [] -> I.empty + } + subtree _ _ _ [] = error "Invariant failure in 'subtree': suffix empty!" + + tids tid d (Fork t) ts = tidOf tid d : t : map (tidOf tid . fst) ts + tids tid _ (BlockedPut _) ts = map (tidOf tid . fst) ts + tids tid _ (BlockedRead _) ts = map (tidOf tid . fst) ts + tids tid _ (BlockedTake _) ts = map (tidOf tid . fst) ts + tids tid _ BlockedSTM ts = map (tidOf tid . fst) ts + tids tid _ (BlockedThrowTo _) ts = map (tidOf tid . fst) ts + tids tid _ Stop ts = map (tidOf tid . fst) ts + tids tid d _ ts = tidOf tid d : map (tidOf tid . fst) ts + +-- | Add new backtracking points, if they have not already been +-- visited, fit into the bound, and aren't in the sleep set. +todo :: ([Decision] -> Bool) -> [BacktrackStep] -> BPOR -> BPOR +todo bv = step where + step bs bpor = + let (bpor', bs') = go 0 [] Nothing bs bpor + in if all (I.null . _backtrack) bs' + then bpor' + else step bs' bpor' + + go tid pref lastb (b:bs) bpor = + let (bpor', blocked) = backtrack pref b bpor + tid' = tidOf tid . fst $ _decision b + (child, blocked') = go tid' (pref++[fst $ _decision b]) (Just b) bs . fromJust $ I.lookup tid' (_bdone bpor) + bpor'' = bpor' { _bdone = I.insert tid' child $ _bdone bpor' } + in case lastb of + Just b' -> (bpor'', b' { _backtrack = blocked } : blocked') + Nothing -> (bpor'', blocked') + + go _ _ (Just b') _ bpor = (bpor, [b' { _backtrack = I.empty }]) + go _ _ Nothing _ bpor = (bpor, []) + + backtrack pref b bpor = + let todo' = [ x + | x@(t,c) <- I.toList $ _backtrack b + , bv $ pref ++ [decisionOf (Just $ activeTid pref) (_brunnable bpor) t] + , t `notElem` I.keys (_bdone bpor) + , c || I.notMember t (_bsleep bpor) + ] + (blocked, nxt) = partition (\(t,_) -> t `S.member` _bignore bpor) todo' + in (bpor { _btodo = _btodo bpor `I.union` I.fromList nxt }, I.fromList blocked) + +-- * Utilities + +-- | Get the resultant 'ThreadId' of a 'Decision', with a default case +-- for 'Continue'. +tidOf :: ThreadId -> Decision -> ThreadId +tidOf _ (Start t) = t +tidOf _ (SwitchTo t) = t +tidOf tid Continue = tid + +-- | Get the 'Decision' that would have resulted in this 'ThreadId', +-- given a prior 'ThreadId' (if any) and list of runnable threads. +decisionOf :: Maybe ThreadId -> Set ThreadId -> ThreadId -> Decision +decisionOf prior runnable chosen + | prior == Just chosen = Continue + | prior `S.member` S.map Just runnable = SwitchTo chosen + | otherwise = Start chosen + +-- | Get the tid of the currently active thread after executing a +-- series of decisions. The list MUST begin with a 'Start'. +activeTid :: [Decision] -> ThreadId +activeTid = foldl' go 0 where + go _ (Start t) = t + go _ (SwitchTo t) = t + go t Continue = t + +-- | Count the number of pre-emptions in a schedule +preEmpCount :: [Decision] -> Int +preEmpCount (SwitchTo _:ds) = 1 + preEmpCount ds +preEmpCount (_:ds) = preEmpCount ds +preEmpCount [] = 0 + +-- | Check if an action is dependent on another, assumes the actions +-- are from different threads (two actions in the same thread are +-- always dependent). +dependent :: ThreadAction -> (ThreadId, ThreadAction) -> Bool +dependent Lift (_, Lift) = True +dependent (ThrowTo t) (t2, _) = t == t2 +dependent d1 (_, d2) = cref || cvar || ctvar where + cref = Just True == ((\(r1, w1) (r2, w2) -> r1 == r2 && (w1 || w2)) <$> cref' d1 <*> cref' d2) + cref' (ReadRef r) = Just (r, False) + cref' (ModRef r) = Just (r, True) + cref' _ = Nothing + + cvar = Just True == ((==) <$> cvar' d1 <*> cvar' d2) + cvar' (TryPut c _ _) = Just c + cvar' (TryTake c _ _) = Just c + cvar' (Put c _) = Just c + cvar' (Read c) = Just c + cvar' (Take c _) = Just c + cvar' _ = Nothing + + ctvar = ctvar' d1 && ctvar' d2 + ctvar' (STM _) = True + ctvar' _ = False + +-- | Variant of 'dependent' to handle 'ThreadAction''s +dependent' :: ThreadAction -> (ThreadId, Lookahead) -> Bool +dependent' Lift (_, WillLift) = True +dependent' (ThrowTo t) (t2, _) = t == t2 +dependent' d1 (_, d2) = cref || cvar || ctvar where + cref = Just True == ((\(r1, w1) (r2, w2) -> r1 == r2 && (w1 || w2)) <$> cref' d1 <*> cref'' d2) + cref' (ReadRef r) = Just (r, False) + cref' (ModRef r) = Just (r, True) + cref' _ = Nothing + cref'' (WillReadRef r) = Just (r, False) + cref'' (WillModRef r) = Just (r, True) + cref'' _ = Nothing + + cvar = Just True == ((==) <$> cvar' d1 <*> cvar'' d2) + cvar' (TryPut c _ _) = Just c + cvar' (TryTake c _ _) = Just c + cvar' (Put c _) = Just c + cvar' (Read c) = Just c + cvar' (Take c _) = Just c + cvar' _ = Nothing + cvar'' (WillTryPut c) = Just c + cvar'' (WillTryTake c) = Just c + cvar'' (WillPut c) = Just c + cvar'' (WillRead c) = Just c + cvar'' (WillTake c) = Just c + cvar'' _ = Nothing + + ctvar = ctvar' d1 && ctvar'' d2 + ctvar' (STM _) = True + ctvar' _ = False + ctvar'' WillSTM = True + ctvar'' _ = False + +-- * Keeping track of 'CVar' full/empty states + +-- | Initial global 'CVar' state +initialCVState :: IntMap Bool +initialCVState = I.empty + +-- | Update the 'CVar' state with the action that has just happened. +updateCVState :: IntMap Bool -> ThreadAction -> IntMap Bool +updateCVState cvstate (Put c _) = I.insert c True cvstate +updateCVState cvstate (Take c _) = I.insert c False cvstate +updateCVState cvstate (TryPut c True _) = I.insert c True cvstate +updateCVState cvstate (TryTake c True _) = I.insert c False cvstate +updateCVState cvstate _ = cvstate + +-- | Check if an action will block. +willBlock :: IntMap Bool -> Lookahead -> Bool +willBlock cvstate (WillPut c) = I.lookup c cvstate == Just True +willBlock cvstate (WillTake c) = I.lookup c cvstate == Just False +willBlock _ _ = False + +-- | Check if a list of actions will block safely (without modifying +-- any global state). This allows further lookahead at, say, the +-- 'spawn' of a thread (which always starts with 'KnowsAbout'). +willBlockSafely :: IntMap Bool -> [Lookahead] -> Bool +willBlockSafely cvstate (WillKnowsAbout:as) = willBlockSafely cvstate as +willBlockSafely cvstate (WillForgets:as) = willBlockSafely cvstate as +willBlockSafely cvstate (WillAllKnown:as) = willBlockSafely cvstate as +willBlockSafely cvstate (WillPut c:_) = willBlock cvstate (WillPut c) +willBlockSafely cvstate (WillTake c:_) = willBlock cvstate (WillTake c) +willBlockSafely _ _ = False diff --git a/Test/DejaFu/STM.hs b/Test/DejaFu/STM.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/STM.hs @@ -0,0 +1,145 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} + +-- | A 'MonadSTM' implementation, which can be run on top of 'IO' or +-- 'ST'. +module Test.DejaFu.STM + ( -- * The @STMLike@ Monad + STMLike + , STMST + , STMIO + , Result(..) + , runTransaction + , runTransactionST + , runTransactionIO + + -- * Software Transactional Memory + , retry + , orElse + , check + , throwSTM + , catchSTM + + -- * @CTVar@s + , CTVar + , CTVarId + , newCTVar + , readCTVar + , writeCTVar + ) where + +import Control.Exception (Exception, SomeException(..)) +import Control.Monad (liftM) +import Control.Monad.Catch (MonadCatch(..), MonadThrow(..)) +import Control.Monad.Cont (cont) +import Control.Monad.ST (ST, runST) +import Data.IORef (IORef) +import Data.STRef (STRef) +import Test.DejaFu.Internal +import Test.DejaFu.STM.Internal + +import qualified Control.Monad.STM.Class as C + +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative (Applicative) +#endif + +{-# ANN module ("HLint: ignore Use record patterns" :: String) #-} + +-- | The 'MonadSTM' implementation, it encapsulates a single atomic +-- transaction. The environment, that is, the collection of defined +-- 'CTVar's is implicit, there is no list of them, they exist purely +-- as references. This makes the types simpler, but means you can't +-- really get an aggregate of them (if you ever wanted to for some +-- reason). +newtype STMLike t n r a = S { unS :: M t n r a } deriving (Functor, Applicative, Monad) + +-- | A convenience wrapper around 'STMLike' using 'STRef's. +type STMST t a = STMLike t (ST t) (STRef t) a + +-- | A convenience wrapper around 'STMLike' using 'IORef's. +type STMIO t a = STMLike t IO IORef a + +instance MonadThrow (STMLike t n r) where + throwM = throwSTM + +instance MonadCatch (STMLike t n r) where + catch = catchSTM + +instance Monad n => C.MonadSTM (STMLike t n r) where + type CTVar (STMLike t n r) = CTVar t r + + retry = retry + orElse = orElse + newCTVar = newCTVar + readCTVar = readCTVar + writeCTVar = writeCTVar + +-- | Abort the current transaction, restoring any 'CTVar's written to, +-- and returning the list of 'CTVar's read. +retry :: Monad n => STMLike t n r a +retry = S $ cont $ const ARetry + +-- | Run the first transaction and, if it 'retry's, +orElse :: Monad n => STMLike t n r a -> STMLike t n r a -> STMLike t n r a +orElse a b = S $ cont $ AOrElse (unS a) (unS b) + +-- | Check whether a condition is true and, if not, call 'retry'. +check :: Monad n => Bool -> STMLike t n r () +check = C.check + +-- | Throw an exception. This aborts the transaction and propagates +-- the exception. +throwSTM :: Exception e => e -> STMLike t n r a +throwSTM e = S $ cont $ const $ AThrow (SomeException e) + +-- | Handling exceptions from 'throwSTM'. +catchSTM :: Exception e => STMLike t n r a -> (e -> STMLike t n r a) -> STMLike t n r a +catchSTM stm handler = S $ cont $ ACatch (unS stm) (unS . handler) + +-- | Create a new 'CTVar' containing the given value. +newCTVar :: Monad n => a -> STMLike t n r (CTVar t r a) +newCTVar a = S $ cont lifted where + lifted c = ANew $ \ref ctvid -> c `liftM` newCTVar' ref ctvid + newCTVar' ref ctvid = (\r -> V (ctvid, r)) `liftM` newRef ref a + +-- | Return the current value stored in a 'CTVar'. +readCTVar :: Monad n => CTVar t r a -> STMLike t n r a +readCTVar ctvar = S $ cont $ ARead ctvar + +-- | Write the supplied value into the 'CTVar'. +writeCTVar :: Monad n => CTVar t r a -> a -> STMLike t n r () +writeCTVar ctvar a = S $ cont $ \c -> AWrite ctvar a $ c () + +-- | Run a transaction in the 'ST' monad, starting from a clean +-- environment, and discarding the environment afterwards. This is +-- suitable for testing individual transactions, but not for composing +-- multiple ones. +runTransaction :: (forall t. STMST t a) -> Result a +runTransaction ma = fst $ runST $ runTransactionST ma 0 + +-- | Run a transaction in the 'ST' monad, returning the result and new +-- initial 'CTVarId'. If the transaction ended by calling 'retry', any +-- 'CTVar' modifications are undone. +runTransactionST :: STMST t a -> CTVarId -> ST t (Result a, CTVarId) +runTransactionST = runTransactionM fixedST where + fixedST = refST $ \mb -> cont (\c -> ALift $ c `liftM` mb) + +-- | Run a transaction in the 'IO' monad, returning the result and new +-- initial 'CTVarId'. If the transaction ended by calling 'retry', any +-- 'CTVar' modifications are undone. +runTransactionIO :: STMIO t a -> CTVarId -> IO (Result a, CTVarId) +runTransactionIO = runTransactionM fixedIO where + fixedIO = refIO $ \mb -> cont (\c -> ALift $ c `liftM` mb) + +-- | Run a transaction in an arbitrary monad. +runTransactionM :: Monad n + => Fixed t n r -> STMLike t n r a -> CTVarId -> n (Result a, CTVarId) +runTransactionM ref ma ctvid = do + (res, undo, ctvid') <- doTransaction ref (unS ma) ctvid + + case res of + Success _ _ _ -> return (res, ctvid') + _ -> undo >> return (res, ctvid) diff --git a/Test/DejaFu/STM/Internal.hs b/Test/DejaFu/STM/Internal.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/STM/Internal.hs @@ -0,0 +1,180 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | 'MonadSTM' testing implementation, internal types and +-- definitions. +module Test.DejaFu.STM.Internal where + +import Control.Exception (Exception, SomeException(..), fromException) +import Control.Monad.Cont (Cont, runCont) +import Data.List (nub) +import Test.DejaFu.Internal + +#if __GLASGOW_HASKELL__ < 710 +import Data.Foldable (Foldable(..)) +import Data.Monoid (mempty) +#endif + +-------------------------------------------------------------------------------- +-- The @STMLike@ monad + +-- | The underlying monad is based on continuations over primitive +-- actions. +type M t n r a = Cont (STMAction t n r) a + +-- | Dict of methods for implementations to override. +type Fixed t n r = Ref n r (Cont (STMAction t n r)) + +-------------------------------------------------------------------------------- +-- * Primitive actions + +-- | STM transactions are represented as a sequence of primitive +-- actions. +data STMAction t n r + = forall a e. Exception e => ACatch (M t n r a) (e -> M t n r a) (a -> STMAction t n r) + | forall a. ARead (CTVar t r a) (a -> STMAction t n r) + | forall a. AWrite (CTVar t r a) a (STMAction t n r) + | forall a. AOrElse (M t n r a) (M t n r a) (a -> STMAction t n r) + | ANew (Fixed t n r -> CTVarId -> n (STMAction t n r)) + | ALift (n (STMAction t n r)) + | AThrow SomeException + | ARetry + | AStop + +-------------------------------------------------------------------------------- +-- * @CTVar@s + +-- | A 'CTVar' is a tuple of a unique ID and the value contained. The +-- ID is so that blocked transactions can be re-run when a 'CTVar' +-- they depend on has changed. +newtype CTVar t r a = V (CTVarId, r a) + +-- | The unique ID of a 'CTVar'. Only meaningful within a single +-- concurrent computation. +type CTVarId = Int + +-------------------------------------------------------------------------------- +-- * Output + +-- | The result of an STM transaction, along with which 'CTVar's it +-- touched whilst executing. +data Result a = + Success [CTVarId] [CTVarId] a + -- ^ The transaction completed successfully, reading the first list + -- 'CTVar's and writing to the second. + | Retry [CTVarId] + -- ^ The transaction aborted by calling 'retry', and read the + -- returned 'CTVar's. It should be retried when at least one of the + -- 'CTVar's has been mutated. + | Exception SomeException + -- ^ The transaction aborted by throwing an exception. + deriving Show + +instance Functor Result where + fmap f (Success rs ws a) = Success rs ws $ f a + fmap _ (Retry rs) = Retry rs + fmap _ (Exception e) = Exception e + +instance Foldable Result where + foldMap f (Success _ _ a) = f a + foldMap _ _ = mempty + +-------------------------------------------------------------------------------- +-- * Execution + +-- | Run a STM transaction, returning an action to undo its effects. +doTransaction :: Monad n => Fixed t n r -> M t n r a -> CTVarId -> n (Result a, n (), CTVarId) +doTransaction fixed ma newctvid = do + ref <- newRef fixed Nothing + + let c = runCont (ma >>= liftN fixed . writeRef fixed ref . Just . Right) $ const AStop + + (newctvid', undo, readen, written) <- go ref c (return ()) newctvid [] [] + + res <- readRef fixed ref + + case res of + Just (Right val) -> return (Success (nub readen) (nub written) val, undo, newctvid') + + Just (Left exc) -> undo >> return (Exception exc, return (), newctvid) + Nothing -> undo >> return (Retry $ nub readen, return (), newctvid) + + where + go ref act undo nctvid readen written = do + (act', undo', nctvid', readen', written') <- stepTrans fixed act nctvid + let ret = (nctvid', undo >> undo', readen' ++ readen, written' ++ written) + case act' of + AStop -> return ret + ARetry -> writeRef fixed ref Nothing >> return ret + AThrow exc -> writeRef fixed ref (Just $ Left exc) >> return ret + + _ -> go ref act' (undo >> undo') nctvid' (readen' ++ readen) (written' ++ written) + +-- | Run a transaction for one step. +stepTrans :: forall t n r. Monad n => Fixed t n r -> STMAction t n r -> CTVarId -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId]) +stepTrans fixed act newctvid = case act of + ACatch stm h c -> stepCatch stm h c + ARead ref c -> stepRead ref c + AWrite ref a c -> stepWrite ref a c + ANew na -> stepNew na + AOrElse a b c -> stepOrElse a b c + ALift na -> stepLift na + + AThrow exc -> return (AThrow exc, nothing, newctvid, [], []) + ARetry -> return (ARetry, nothing, newctvid, [], []) + AStop -> return (AStop, nothing, newctvid, [], []) + + where + nothing = return () + + stepCatch :: Exception e => M t n r a -> (e -> M t n r a) -> (a -> STMAction t n r) -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId]) + stepCatch stm h c = do + (res, undo, newctvid') <- doTransaction fixed stm newctvid + case res of + Success readen written val -> return (c val, undo, newctvid', readen, written) + Retry readen -> return (ARetry, nothing, newctvid, readen, []) + Exception exc -> case fromException exc of + Just exc' -> do + (rese, undoe, newctvide') <- doTransaction fixed (h exc') newctvid + case rese of + Success readen written val -> return (c val, undoe, newctvide', readen, written) + Exception exce -> return (AThrow exce, nothing, newctvid, [], []) + Retry readen -> return (ARetry, nothing, newctvid, readen, []) + Nothing -> return (AThrow exc, nothing, newctvid, [], []) + + stepRead :: CTVar t r a -> (a -> STMAction t n r) -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId]) + stepRead (V (ctvid, ref)) c = do + val <- readRef fixed ref + return (c val, nothing, newctvid, [ctvid], []) + + stepWrite :: CTVar t r a -> a -> STMAction t n r -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId]) + stepWrite (V (ctvid, ref)) a c = do + old <- readRef fixed ref + writeRef fixed ref a + return (c, writeRef fixed ref old, newctvid, [], [ctvid]) + + stepNew :: (Fixed t n r -> CTVarId -> n (STMAction t n r)) -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId]) + stepNew na = do + let newctvid' = newctvid + 1 + a <- na fixed newctvid + return (a, nothing, newctvid', [], [newctvid]) + + stepOrElse :: M t n r a -> M t n r a -> (a -> STMAction t n r) -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId]) + stepOrElse a b c = do + (resa, undoa, newctvida') <- doTransaction fixed a newctvid + case resa of + Success readen written val -> return (c val, undoa, newctvida', readen, written) + Exception exc -> return (AThrow exc, nothing, newctvid, [], []) + Retry _ -> do + (resb, undob, newctvidb') <- doTransaction fixed b newctvid + case resb of + Success readen written val -> return (c val, undob, newctvidb', readen, written) + Exception exc -> return (AThrow exc, nothing, newctvid, [], []) + Retry readen -> return (ARetry, nothing, newctvid, readen, []) + + stepLift :: n (STMAction t n r) -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId]) + stepLift na = do + a <- na + return (a, nothing, newctvid, [], []) diff --git a/dejafu.cabal b/dejafu.cabal new file mode 100644 --- /dev/null +++ b/dejafu.cabal @@ -0,0 +1,101 @@ +-- Initial monad-conc.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: dejafu +version: 0.1.0.0 +synopsis: Overloadable primitives for testable, potentially non-deterministic, concurrency. + +description: + /[Déjà Fu is] A martial art in which the user's limbs move in time as well as space, […] It is best described as "the feeling that you have been kicked in the head this way before"/ -- Terry Pratchett, Thief of Time + . + Concurrency is nice, deadlocks and race conditions not so much. The + @Par@ monad family, as defined in + + provides deterministic parallelism, but sometimes we can tolerate a + bit of nondeterminism. + . + This package provides a class of monads for potentially + nondeterministic concurrency, with an interface in the spirit of + GHC's normal concurrency abstraction. + . + == @MonadConc@ with 'IO': + . + The intention of the @MonadConc@ class is to provide concurrency + where any apparent nondeterminism arises purely from the scheduling + behaviour. To put it another way, a given computation, parametrised + with a fixed set of scheduling decisions, is deterministic. This + assumption is used by the testing functionality provided by + Test.DejaFu. + . + Whilst this assumption may not hold in general when 'IO' is + involved, you should strive to produce test cases where it does. + . + See the for more + details. + +homepage: https://github.com/barrucadu/dejafu +license: MIT +license-file: LICENSE +author: Michael Walker +maintainer: mike@barrucadu.co.uk +-- copyright: +category: Concurrency +build-type: Simple +-- extra-source-files: +cabal-version: >=1.10 + +source-repository head + type: git + location: https://github.com/barrucadu/dejafu.git + +source-repository this + type: git + location: https://github.com/barrucadu/dejafu.git + tag: 0.1.0.0 + +library + exposed-modules: Control.Monad.Conc.Class + , Control.Monad.STM.Class + + , Control.Concurrent.CVar + , Control.Concurrent.CVar.Strict + , Control.Concurrent.STM.CTVar + , Control.Concurrent.STM.CTMVar + + , Test.DejaFu + , Test.DejaFu.Deterministic + , Test.DejaFu.Deterministic.IO + , Test.DejaFu.Deterministic.Schedule + , Test.DejaFu.SCT + , Test.DejaFu.STM + + other-modules: Test.DejaFu.Deterministic.Internal + , Test.DejaFu.Deterministic.Internal.Common + , Test.DejaFu.Deterministic.Internal.CVar + , Test.DejaFu.Deterministic.Internal.Threading + , Test.DejaFu.Internal + , Test.DejaFu.SCT.Internal + , Test.DejaFu.STM.Internal + + , Data.List.Extra + + -- other-extensions: + build-depends: base >=4.5 && <5 + , containers + , deepseq + , exceptions >=0.7 + , monad-loops + , mtl + , random + , stm + , transformers + -- hs-source-dirs: + default-language: Haskell2010 + ghc-options: -Wall + +test-suite tests + hs-source-dirs: tests + type: exitcode-stdio-1.0 + main-is: Tests.hs + build-depends: dejafu, base + default-language: Haskell2010 diff --git a/tests/Tests.hs b/tests/Tests.hs new file mode 100644 --- /dev/null +++ b/tests/Tests.hs @@ -0,0 +1,37 @@ +module Main (main) where + +import Test.DejaFu +import System.Exit (exitFailure, exitSuccess) + +import qualified Tests.Cases as C +import qualified Tests.Logger as L + +andM :: (Functor m, Monad m) => [m Bool] -> m Bool +andM = fmap and . sequence + +runTests :: IO Bool +runTests = + andM [dejafu C.simple2Deadlock ("Simple 2-Deadlock", deadlocksSometimes) + ,dejafu (C.philosophers 2) ("2 Philosophers", deadlocksSometimes) + ,dejafu (C.philosophers 3) ("3 Philosophers", deadlocksSometimes) + ,dejafu (C.philosophers 4) ("4 Philosophers", deadlocksSometimes) + ,dejafu C.thresholdValue ("Threshold Value", notAlwaysSame) + ,dejafu C.forgottenUnlock ("Forgotten Unlock", deadlocksAlways) + ,dejafu C.simple2Race ("Simple 2-Race", notAlwaysSame) + ,dejafu C.raceyStack ("Racey Stack", notAlwaysSame) + ,dejafu C.threadKill ("killThread", deadlocksSometimes) + ,dejafu C.threadKillMask ("killThread+mask 1", deadlocksNever) + ,dejafu C.threadKillUmask ("killThread+mask 2", deadlocksSometimes) + ,dejafu C.stmAtomic ("STM Atomicity", alwaysTrue (\r -> fmap (`elem` [0,2]) r == Right True)) + ,dejafu C.stmRetry ("STM Retry", alwaysSame) + ,dejafu C.stmOrElse ("STM orElse", alwaysSame) + ,dejafu C.stmExc ("STM Exceptions", alwaysSame) + ,dejafu C.excNest ("Nested Excs", alwaysSame) + ,dejafus L.badLogger [("Logger (Valid)", L.validResult) + ,("Logger (Good)", L.isGood) + ,("Logger (Bad", L.isBad)]] + +main :: IO () +main = do + success <- runTests + if success then exitSuccess else exitFailure