diff --git a/Control/Monad/Conc/Class.hs b/Control/Monad/Conc/Class.hs --- a/Control/Monad/Conc/Class.hs +++ b/Control/Monad/Conc/Class.hs @@ -7,10 +7,20 @@ -- monads. module Control.Monad.Conc.Class ( MonadConc(..) + -- * Utilities , spawn , forkFinally , killThread + , cas + + -- * Bound Threads + + -- | @MonadConc@ does not support bound threads, if you need that + -- sort of thing you will have to use regular @IO@. + + , rtsSupportsBoundThreads + , isCurrentThreadBound ) where import Control.Concurrent (forkIO) @@ -22,7 +32,7 @@ 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 Data.IORef (IORef, atomicModifyIORef, newIORef, readIORef, writeIORef, atomicWriteIORef) import qualified Control.Concurrent as C import qualified Control.Monad.Catch as Ca @@ -33,6 +43,7 @@ import qualified Control.Monad.State.Strict as SS import qualified Control.Monad.Writer.Lazy as WL import qualified Control.Monad.Writer.Strict as WS +import qualified Data.Atomics as A #if __GLASGOW_HASKELL__ < 710 import Control.Applicative (Applicative) @@ -44,18 +55,6 @@ -- 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 @@ -71,17 +70,25 @@ -- \"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. + -- | The mutable non-blocking reference type. These may suffer from + -- relaxed memory effects if functions outside the set @newCRef@, + -- @readCRef@, @modifyCRef@, and @atomicWriteCRef@ are used. type CRef m :: * -> * + -- | When performing compare-and-swap operations on @CRef@s, a + -- @Ticket@ is a proof that a thread observed a specific previous + -- value. + type Ticket m :: * -> * + -- | An abstract handle to a thread. type ThreadId m :: * -- | Fork a computation to happen concurrently. Communication may -- happen over @CVar@s. + -- + -- > fork ma = forkWithUnmask (\_ -> ma) fork :: m () -> m (ThreadId m) + fork ma = forkWithUnmask (\_ -> ma) -- | Like 'fork', but the child thread is passed a function that can -- be used to unmask asynchronous exceptions. This function should @@ -93,14 +100,28 @@ -- correspond to physical processors or cores but this is -- implementation dependent. The int is interpreted modulo to the -- total number of capabilities as returned by 'getNumCapabilities'. + -- + -- > forkOn c ma = forkOnWithUnmask c (\_ -> ma) forkOn :: Int -> m () -> m (ThreadId m) + forkOn c ma = forkOnWithUnmask c (\_ -> ma) + -- | Like 'forkWithUnmask' but the child thread is pinned to the + -- given CPU, as with 'forkOn'. + forkOnWithUnmask :: Int -> ((forall a. m a -> m a) -> m ()) -> m (ThreadId m) + -- | Get the number of Haskell threads that can run simultaneously. getNumCapabilities :: m Int + -- | Set the number of Haskell threads that can run simultaneously. + setNumCapabilities :: Int -> m () + -- | Get the @ThreadId@ of the current thread. myThreadId :: m (ThreadId m) + -- | Allows a context-switch to any other currently runnable thread + -- (if any). + yield :: m () + -- | Create a new empty @CVar@. newEmptyCVar :: m (CVar m a) @@ -133,17 +154,55 @@ newCRef :: a -> m (CRef m a) -- | Read the current value stored in a reference. + -- + -- > readCRef cref = readForCAS cref >>= peekTicket readCRef :: CRef m a -> m a + readCRef cref = readForCAS cref >>= peekTicket - -- | Atomically modify the value stored in a reference. + -- | Atomically modify the value stored in a reference. This imposes + -- a full memory barrier. modifyCRef :: CRef m a -> (a -> (a, b)) -> m b - -- | Replace the value stored in a reference. - -- - -- > writeCRef r a = modifyCRef r $ const (a, ()) + -- | Write a new value into an @CRef@, without imposing a memory + -- barrier. This means that relaxed memory effects can be observed. writeCRef :: CRef m a -> a -> m () - writeCRef r a = modifyCRef r $ const (a, ()) + -- | Replace the value stored in a reference, with the + -- barrier-to-reordering property that 'modifyCRef' has. + -- + -- > atomicWriteCRef r a = modifyCRef r $ const (a, ()) + atomicWriteCRef :: CRef m a -> a -> m () + atomicWriteCRef r a = modifyCRef r $ const (a, ()) + + -- | Read the current value stored in a reference, returning a + -- @Ticket@, for use in future compare-and-swap operations. + readForCAS :: CRef m a -> m (Ticket m a) + + -- | Extract the actual Haskell value from a @Ticket@. + -- + -- This shouldn't need to do any monadic computation, the @m@ + -- appears in the result type because of the need for injectivity in + -- the @Ticket@ type family, which can't be expressed currently. + peekTicket :: Ticket m a -> m a + + -- | Perform a machine-level compare-and-swap (CAS) operation on a + -- @CRef@. Returns an indication of success and a @Ticket@ for the + -- most current value in the @CRef@. + -- + -- This is strict in the \"new\" value argument. + casCRef :: CRef m a -> Ticket m a -> a -> m (Bool, Ticket m a) + + -- | A replacement for 'modifyCRef' using a compare-and-swap. + -- + -- This is strict in the \"new\" value argument. + modifyCRefCAS :: CRef m a -> (a -> (a, b)) -> m b + + -- | A variant of 'modifyCRefCAS' which doesn't return a result. + -- + -- > modifyCRefCAS_ cref f = modifyCRefCAS cref (\a -> (f a, ())) + modifyCRefCAS_ :: CRef m a -> (a -> a) -> m () + modifyCRefCAS_ cref f = modifyCRefCAS cref (\a -> (f a, ())) + -- | Perform an STM transaction atomically. atomically :: STMLike m a -> m a @@ -199,27 +258,6 @@ 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 @@ -271,14 +309,18 @@ type STMLike IO = STM type CVar IO = MVar type CRef IO = IORef + type Ticket IO = A.Ticket type ThreadId IO = C.ThreadId readCVar = readMVar fork = forkIO forkWithUnmask = C.forkIOWithUnmask forkOn = C.forkOn + forkOnWithUnmask = C.forkOnWithUnmask getNumCapabilities = C.getNumCapabilities + setNumCapabilities = C.setNumCapabilities myThreadId = C.myThreadId + yield = C.yield throwTo = C.throwTo newEmptyCVar = newEmptyMVar putCVar = putMVar @@ -288,6 +330,12 @@ newCRef = newIORef readCRef = readIORef modifyCRef = atomicModifyIORef + writeCRef = writeIORef + atomicWriteCRef = atomicWriteIORef + readForCAS = A.readForCAS + peekTicket = return . A.peekTicket + casCRef = A.casIORef + modifyCRefCAS = A.atomicModifyIORefCAS atomically = S.atomically -- | Create a concurrent computation for the provided action, and @@ -315,6 +363,24 @@ killThread :: MonadConc m => ThreadId m -> m () killThread tid = throwTo tid ThreadKilled +-- | Provided for compatibility, always returns 'False'. +rtsSupportsBoundThreads :: Bool +rtsSupportsBoundThreads = False + +-- | Provided for compatibility, always returns 'False'. +isCurrentThreadBound :: MonadConc m => m Bool +isCurrentThreadBound = return False + +-- | Compare-and-swap a value in a @CRef@, returning an indication of +-- success and the new value. +cas :: MonadConc m => CRef m a -> a -> m (Bool, a) +cas cref a = do + tick <- readForCAS cref + (suc, tick') <- casCRef cref tick a + a' <- peekTicket tick' + + return (suc, a') + ------------------------------------------------------------------------------- -- Transformer instances @@ -322,15 +388,18 @@ type STMLike (ReaderT r m) = STMLike m type CVar (ReaderT r m) = CVar m type CRef (ReaderT r m) = CRef m + type Ticket (ReaderT r m) = Ticket m type ThreadId (ReaderT r m) = ThreadId m fork = reader fork forkOn i = reader (forkOn i) forkWithUnmask ma = ReaderT $ \r -> forkWithUnmask (\f -> runReaderT (ma $ reader f) r) - _concNoTest = reader _concNoTest + forkOnWithUnmask i ma = ReaderT $ \r -> forkOnWithUnmask i (\f -> runReaderT (ma $ reader f) r) getNumCapabilities = lift getNumCapabilities + setNumCapabilities = lift . setNumCapabilities myThreadId = lift myThreadId + yield = lift yield throwTo t = lift . throwTo t newEmptyCVar = lift newEmptyCVar readCVar = lift . readCVar @@ -341,6 +410,12 @@ newCRef = lift . newCRef readCRef = lift . readCRef modifyCRef r = lift . modifyCRef r + writeCRef r = lift . writeCRef r + atomicWriteCRef r = lift . atomicWriteCRef r + readForCAS = lift . readForCAS + peekTicket = lift . peekTicket + casCRef r t = lift . casCRef r t + modifyCRefCAS r = lift . modifyCRefCAS r atomically = lift . atomically _concKnowsAbout = lift . _concKnowsAbout _concForgets = lift . _concForgets @@ -353,15 +428,18 @@ type STMLike (WL.WriterT w m) = STMLike m type CVar (WL.WriterT w m) = CVar m type CRef (WL.WriterT w m) = CRef m + type Ticket (WL.WriterT w m) = Ticket m type ThreadId (WL.WriterT w m) = ThreadId m fork = writerlazy fork forkOn i = writerlazy (forkOn i) forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WL.runWriterT (ma $ writerlazy f)) - _concNoTest = writerlazy _concNoTest + forkOnWithUnmask i ma = lift $ forkOnWithUnmask i (\f -> fst `liftM` WL.runWriterT (ma $ writerlazy f)) getNumCapabilities = lift getNumCapabilities + setNumCapabilities = lift . setNumCapabilities myThreadId = lift myThreadId + yield = lift yield throwTo t = lift . throwTo t newEmptyCVar = lift newEmptyCVar readCVar = lift . readCVar @@ -372,6 +450,12 @@ newCRef = lift . newCRef readCRef = lift . readCRef modifyCRef r = lift . modifyCRef r + writeCRef r = lift . writeCRef r + atomicWriteCRef r = lift . atomicWriteCRef r + readForCAS = lift . readForCAS + peekTicket = lift . peekTicket + casCRef r t = lift . casCRef r t + modifyCRefCAS r = lift . modifyCRefCAS r atomically = lift . atomically _concKnowsAbout = lift . _concKnowsAbout _concForgets = lift . _concForgets @@ -384,15 +468,18 @@ type STMLike (WS.WriterT w m) = STMLike m type CVar (WS.WriterT w m) = CVar m type CRef (WS.WriterT w m) = CRef m + type Ticket (WS.WriterT w m) = Ticket m type ThreadId (WS.WriterT w m) = ThreadId m fork = writerstrict fork forkOn i = writerstrict (forkOn i) forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WS.runWriterT (ma $ writerstrict f)) - _concNoTest = writerstrict _concNoTest + forkOnWithUnmask i ma = lift $ forkOnWithUnmask i (\f -> fst `liftM` WS.runWriterT (ma $ writerstrict f)) getNumCapabilities = lift getNumCapabilities + setNumCapabilities = lift . setNumCapabilities myThreadId = lift myThreadId + yield = lift yield throwTo t = lift . throwTo t newEmptyCVar = lift newEmptyCVar readCVar = lift . readCVar @@ -403,6 +490,12 @@ newCRef = lift . newCRef readCRef = lift . readCRef modifyCRef r = lift . modifyCRef r + writeCRef r = lift . writeCRef r + atomicWriteCRef r = lift . atomicWriteCRef r + readForCAS = lift . readForCAS + peekTicket = lift . peekTicket + casCRef r t = lift . casCRef r t + modifyCRefCAS r = lift . modifyCRefCAS r atomically = lift . atomically _concKnowsAbout = lift . _concKnowsAbout _concForgets = lift . _concForgets @@ -415,15 +508,18 @@ type STMLike (SL.StateT s m) = STMLike m type CVar (SL.StateT s m) = CVar m type CRef (SL.StateT s m) = CRef m + type Ticket (SL.StateT s m) = Ticket m type ThreadId (SL.StateT s m) = ThreadId m 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 + forkOnWithUnmask i ma = SL.StateT $ \s -> (\a -> (a,s)) `liftM` forkOnWithUnmask i (\f -> SL.evalStateT (ma $ statelazy f) s) getNumCapabilities = lift getNumCapabilities + setNumCapabilities = lift . setNumCapabilities myThreadId = lift myThreadId + yield = lift yield throwTo t = lift . throwTo t newEmptyCVar = lift newEmptyCVar readCVar = lift . readCVar @@ -434,6 +530,12 @@ newCRef = lift . newCRef readCRef = lift . readCRef modifyCRef r = lift . modifyCRef r + writeCRef r = lift . writeCRef r + atomicWriteCRef r = lift . atomicWriteCRef r + readForCAS = lift . readForCAS + peekTicket = lift . peekTicket + casCRef r t = lift . casCRef r t + modifyCRefCAS r = lift . modifyCRefCAS r atomically = lift . atomically _concKnowsAbout = lift . _concKnowsAbout _concForgets = lift . _concForgets @@ -446,15 +548,18 @@ type STMLike (SS.StateT s m) = STMLike m type CVar (SS.StateT s m) = CVar m type CRef (SS.StateT s m) = CRef m + type Ticket (SS.StateT s m) = Ticket m type ThreadId (SS.StateT s m) = ThreadId m 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 + forkOnWithUnmask i ma = SS.StateT $ \s -> (\a -> (a,s)) `liftM` forkOnWithUnmask i (\f -> SS.evalStateT (ma $ statestrict f) s) getNumCapabilities = lift getNumCapabilities + setNumCapabilities = lift . setNumCapabilities myThreadId = lift myThreadId + yield = lift yield throwTo t = lift . throwTo t newEmptyCVar = lift newEmptyCVar readCVar = lift . readCVar @@ -465,6 +570,12 @@ newCRef = lift . newCRef readCRef = lift . readCRef modifyCRef r = lift . modifyCRef r + writeCRef r = lift . writeCRef r + atomicWriteCRef r = lift . atomicWriteCRef r + readForCAS = lift . readForCAS + peekTicket = lift . peekTicket + casCRef r t = lift . casCRef r t + modifyCRefCAS r = lift . modifyCRefCAS r atomically = lift . atomically _concKnowsAbout = lift . _concKnowsAbout _concForgets = lift . _concForgets @@ -477,15 +588,18 @@ type STMLike (RL.RWST r w s m) = STMLike m type CVar (RL.RWST r w s m) = CVar m type CRef (RL.RWST r w s m) = CRef m + type Ticket (RL.RWST r w s m) = Ticket m type ThreadId (RL.RWST r w s m) = ThreadId m fork = rwslazy fork forkOn i = rwslazy (forkOn i) forkWithUnmask ma = RL.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkWithUnmask (\f -> fst `liftM` RL.evalRWST (ma $ rwslazy f) r s) - _concNoTest = rwslazy _concNoTest + forkOnWithUnmask i ma = RL.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkOnWithUnmask i (\f -> fst `liftM` RL.evalRWST (ma $ rwslazy f) r s) getNumCapabilities = lift getNumCapabilities + setNumCapabilities = lift . setNumCapabilities myThreadId = lift myThreadId + yield = lift yield throwTo t = lift . throwTo t newEmptyCVar = lift newEmptyCVar readCVar = lift . readCVar @@ -496,6 +610,12 @@ newCRef = lift . newCRef readCRef = lift . readCRef modifyCRef r = lift . modifyCRef r + writeCRef r = lift . writeCRef r + atomicWriteCRef r = lift . atomicWriteCRef r + readForCAS = lift . readForCAS + peekTicket = lift . peekTicket + casCRef r t = lift . casCRef r t + modifyCRefCAS r = lift . modifyCRefCAS r atomically = lift . atomically _concKnowsAbout = lift . _concKnowsAbout _concForgets = lift . _concForgets @@ -508,15 +628,18 @@ type STMLike (RS.RWST r w s m) = STMLike m type CVar (RS.RWST r w s m) = CVar m type CRef (RS.RWST r w s m) = CRef m + type Ticket (RS.RWST r w s m) = Ticket m type ThreadId (RS.RWST r w s m) = ThreadId m 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 + forkOnWithUnmask i ma = RS.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkOnWithUnmask i (\f -> fst `liftM` RS.evalRWST (ma $ rwsstrict f) r s) getNumCapabilities = lift getNumCapabilities + setNumCapabilities = lift . setNumCapabilities myThreadId = lift myThreadId + yield = lift yield throwTo t = lift . throwTo t newEmptyCVar = lift newEmptyCVar readCVar = lift . readCVar @@ -527,6 +650,12 @@ newCRef = lift . newCRef readCRef = lift . readCRef modifyCRef r = lift . modifyCRef r + writeCRef r = lift . writeCRef r + atomicWriteCRef r = lift . atomicWriteCRef r + readForCAS = lift . readForCAS + peekTicket = lift . peekTicket + casCRef r t = lift . casCRef r t + modifyCRefCAS r = lift . modifyCRefCAS r atomically = lift . atomically _concKnowsAbout = lift . _concKnowsAbout _concForgets = lift . _concForgets diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs --- a/Test/DejaFu.hs +++ b/Test/DejaFu.hs @@ -8,8 +8,8 @@ -- 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 +-- > example1 :: MonadConc m => m Int +-- > example1 = do -- > a <- newEmptyCVar -- > b <- newEmptyCVar -- > @@ -33,7 +33,7 @@ -- -- Here is what Deja Fu has to say about it: -- --- > > autocheck bad +-- > > autocheck example1 -- > [fail] Never Deadlocks (checked: 2) -- > [deadlock] S0---------S1--P2---S1- -- > [pass] No Exceptions (checked: 11) @@ -65,16 +65,117 @@ -- -- If you simply wish to check that something is deterministic, see -- the 'autocheck' and 'autocheckIO' functions. + -- + -- These functions use a Total Store Order (TSO) memory model for + -- unsynchronised actions, see \"Testing under Alternative Memory + -- Models\" for some explanation of this. autocheck , dejafu , dejafus - , dejafus' , autocheckIO , dejafuIO , dejafusIO + + -- * Testing with different settings + + , autocheck' + , autocheckIO' + , dejafu' + , dejafus' + , dejafuIO' , dejafusIO' + -- ** Memory Models + + -- | Threads running under modern multicore processors do not behave + -- as a simple interleaving of the individual thread + -- actions. Processors do all sorts of complex things to increase + -- speed, such as buffering writes. For concurrent programs which + -- make use of non-synchronised functions (such as 'readCRef' + -- coupled with 'writeCRef') different memory models may yield + -- different results. + -- + -- As an example, consider this program (modified from the + -- Data.IORef documentation). Two @CRef@s are created, and two + -- threads spawned to write to and read from both. Each thread + -- returns the value it observes. + -- + -- > example2 :: MonadConc m => m (Bool, Bool) + -- > example2 = do + -- > r1 <- newCRef False + -- > r2 <- newCRef False + -- > + -- > x <- spawn $ writeCRef r1 True >> readCRef r2 + -- > y <- spawn $ writeCRef r2 True >> readCRef r1 + -- > + -- > (,) <$> readCVar x <*> readCVar y + -- + -- Under a sequentially consistent memory model the possible results + -- are @(True, True)@, @(True, False)@, and @(False, True)@. Under + -- total or partial store order, @(False, False)@ is also a possible + -- result, even though there is no interleaving of the threads which + -- can lead to this. + -- + -- We can see this by testing with different memory models: + -- + -- > > autocheck' SequentialConsistency example2 + -- > [pass] Never Deadlocks (checked: 6) + -- > [pass] No Exceptions (checked: 6) + -- > [fail] Consistent Result (checked: 5) + -- > (False,True) S0-------S1-----S0--S2-----S0--- + -- > (True,False) S0-------S1-P2-----S1----S0---- + -- > (True,True) S0-------S1--P2-----S1---S0---- + -- > (False,True) S0-------S1---P2-----S1--S0---- + -- > (True,False) S0-------S2-----S1-----S0---- + -- > ... + -- > False + -- + -- > > autocheck' TotalStoreOrder example2 + -- > [pass] Never Deadlocks (checked: 303) + -- > [pass] No Exceptions (checked: 303) + -- > [fail] Consistent Result (checked: 302) + -- > (False,True) S0-------S1-----C-S0--S2-----C-S0--- + -- > (True,False) S0-------S1-P2-----C-S1----S0---- + -- > (True,True) S0-------S1-P2--C-S1----C-S0--S2---S0--- + -- > (False,True) S0-------S1-P2--P1--C-C-S1--S0--S2---S0--- + -- > (False,False) S0-------S1-P2--P1----S2---C-C-S0---- + -- > ... + -- > False + -- + -- Traces for non-sequentially-consistent memory models show where + -- writes to @CRef@s are /committed/, which makes a write visible to + -- all threads rather than just the one which performed the + -- write. Only 'writeCRef' is broken up into separate write and + -- commit steps, 'modifyCRef' is still atomic and imposes a memory + -- barrier. + + , MemType(..) + , defaultMemType + + -- ** Schedule Bounding + + -- | Schedule bounding is an optimisation which only considers + -- schedules within some /bound/. This sacrifices completeness + -- outside of the bound, but can drastically reduce the number of + -- schedules to test, and is in fact necessary for non-terminating + -- programs. + -- + -- The standard testing mechanism uses a combination of pre-emption + -- bounding, fair bounding, and length bounding. Pre-emption + fair + -- bounding is useful for programs which use loop/yield control + -- flows but are otherwise terminating. Length bounding makes it + -- possible to test potentially non-terminating programs. + + , Bounds(..) + , defaultBounds + , PreemptionBound(..) + , defaultPreemptionBound + , FairBound(..) + , defaultFairBound + , LengthBound(..) + , defaultLengthBound + -- * Results -- | The results of a test can be pretty-printed to the console, as @@ -104,6 +205,10 @@ -- results. , Predicate + , representative + , abortsNever + , abortsAlways + , abortsSometimes , deadlocksNever , deadlocksAlways , deadlocksSometimes @@ -115,14 +220,19 @@ , alwaysTrue , alwaysTrue2 , somewhereTrue + , gives + , gives' ) where import Control.Arrow (first) import Control.DeepSeq (NFData(..)) -import Control.Monad (when) +import Control.Monad (when, unless) +import Data.Function (on) +import Data.List (minimumBy) import Data.List.Extra +import Data.Monoid ((<>)) +import Data.Ord (comparing) import Test.DejaFu.Deterministic -import Test.DejaFu.Deterministic.IO (ConcIO) import Test.DejaFu.SCT #if __GLASGOW_HASKELL__ < 710 @@ -130,6 +240,10 @@ import Data.Foldable (Foldable(..)) #endif +-- | The default memory model: @TotalStoreOrder@ +defaultMemType :: MemType +defaultMemType = TotalStoreOrder + -- | Automatically test a computation. In particular, look for -- deadlocks, uncaught exceptions, and multiple return values. -- @@ -137,80 +251,115 @@ -- 'MonadConc'. If you need to test something which also uses -- 'MonadIO', use 'autocheckIO'. autocheck :: (Eq a, Show a) - => (forall t. Conc t a) + => (forall t. ConcST t a) -- ^ The computation to test -> IO Bool -autocheck conc = dejafus conc cases where - cases = [ ("Never Deadlocks", deadlocksNever) - , ("No Exceptions", exceptionsNever) - , ("Consistent Result", alwaysSame) - ] +autocheck = autocheck' defaultMemType +-- | Variant of 'autocheck' which tests a computation under a given +-- memory model. +autocheck' :: (Eq a, Show a) + => MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> (forall t. ConcST t a) + -- ^ The computation to test + -> IO Bool +autocheck' memtype conc = dejafus' memtype defaultBounds conc autocheckCases + -- | 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) - ] +autocheckIO :: (Eq a, Show a) => ConcIO a -> IO Bool +autocheckIO = autocheckIO' defaultMemType +-- | Variant of 'autocheck'' for computations which do 'IO'. +autocheckIO' :: (Eq a, Show a) => MemType -> ConcIO a -> IO Bool +autocheckIO' memtype concio = dejafusIO' memtype defaultBounds concio autocheckCases + +-- | Predicates for the various autocheck functions. +autocheckCases :: (Eq a, Show a) => [(String, Predicate a)] +autocheckCases = + [ ("Never Deadlocks", representative deadlocksNever) + , ("No Exceptions", representative exceptionsNever) + , ("Consistent Result", alwaysSame) -- already representative + ] + -- | Check a predicate and print the result to stdout, return 'True' -- if it passes. -dejafu :: (Eq a, Show a) - => (forall t. Conc t a) +dejafu :: Show a + => (forall t. ConcST t a) -- ^ The computation to test -> (String, Predicate a) -- ^ The predicate (with a name) to check -> IO Bool -dejafu conc test = dejafus conc [test] +dejafu = dejafu' defaultMemType defaultBounds +-- | Variant of 'dejafu'' which takes a memory model and schedule +-- bounds. +-- +-- Schedule bounding is used to filter the large number of possible +-- schedules, and can be iteratively increased for further coverage +-- guarantees. Empirical studies (/Concurrency Testing Using Schedule +-- Bounding: an Empirical Study/, P. Thompson, A. Donaldson, and +-- A. Betts) have found that many concurrency bugs can be exhibited +-- with as few as two threads and two pre-emptions, which is part of +-- what 'dejafus' uses. +-- +-- __Warning:__ Using largers bounds will almost certainly +-- significantly increase the time taken to test! +dejafu' :: Show a + => MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> Bounds + -- ^ The schedule bounds + -> (forall t. ConcST t a) + -- ^ The computation to test + -> (String, Predicate a) + -- ^ The predicate (with a name) to check + -> IO Bool +dejafu' memtype cb conc test = dejafus' memtype cb 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) +dejafus :: Show a + => (forall t. ConcST t a) -- ^ The computation to test -> [(String, Predicate a)] -- ^ The list of predicates (with names) to check -> IO Bool -dejafus = dejafus' 2 +dejafus = dejafus' defaultMemType defaultBounds --- | 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) +-- | Variant of 'dejafus' which takes a memory model and schedule +-- bounds. +dejafus' :: Show a + => MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> Bounds + -- ^ The schedule bounds. + -> (forall t. ConcST t a) -- ^ The computation to test -> [(String, Predicate a)] -- ^ The list of predicates (with names) to check -> IO Bool -dejafus' pb conc tests = do - let traces = sctPreBound pb conc +dejafus' memtype cb conc tests = do + let traces = sctBound memtype cb 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] +dejafuIO :: Show a => ConcIO a -> (String, Predicate a) -> IO Bool +dejafuIO = dejafuIO' defaultMemType defaultBounds +-- | Variant of 'dejafu'' for computations which do 'IO'. +dejafuIO' :: Show a => MemType -> Bounds -> ConcIO a -> (String, Predicate a) -> IO Bool +dejafuIO' memtype cb concio test = dejafusIO' memtype cb 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 +dejafusIO :: Show a => ConcIO a -> [(String, Predicate a)] -> IO Bool +dejafusIO = dejafusIO' defaultMemType defaultBounds -- | 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 +dejafusIO' :: Show a => MemType -> Bounds -> ConcIO a -> [(String, Predicate a)] -> IO Bool +dejafusIO' memtype cb concio tests = do + traces <- sctBoundIO memtype cb concio results <- mapM (\(name, test) -> doTest name $ test traces) tests return $ and results @@ -225,10 +374,20 @@ -- ^ The number of cases checked. , _failures :: [(Either Failure a, Trace)] -- ^ The failing cases, if any. + , _failureMsg :: String + -- ^ A message to display on failure, if nonempty } deriving (Show, Eq) +-- | A failed result, taking the given list of failures. +defaultFail :: [(Either Failure a, Trace)] -> Result a +defaultFail failures = Result False 0 failures "" + +-- | A passed result. +defaultPass :: Result a +defaultPass = Result True 0 [] "" + instance NFData a => NFData (Result a) where - rnf r = rnf (_pass r, _casesChecked r, _failures r) + rnf r = rnf (_pass r, _casesChecked r, _failures r, _failureMsg r) instance Functor Result where fmap f r = r { _failures = map (first $ fmap f) $ _failures r } @@ -236,35 +395,37 @@ 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. +-- | Run a predicate over all executions within the default schedule +-- bounds. runTest :: Predicate a -- ^ The predicate to check - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> Result a -runTest = runTest' 2 +runTest = runTest' defaultMemType defaultBounds --- | Variant of 'runTest' which takes a pre-emption bound. +-- | Variant of 'runTest' which takes a memory model and schedule +-- bounds. runTest' :: - Int - -- ^ The maximum number of pre-emptions to allow in a single - -- execution + MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> Bounds + -- ^ The schedule bounds. -> Predicate a -- ^ The predicate to check - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to test -> Result a -runTest' pb predicate conc = predicate $ sctPreBound pb conc +runTest' memtype cb predicate conc = predicate $ sctBound memtype cb conc -- | Variant of 'runTest' for computations which do 'IO'. -runTestIO :: Predicate a -> (forall t. ConcIO t a) -> IO (Result a) -runTestIO = runTestIO' 2 +runTestIO :: Predicate a -> ConcIO a -> IO (Result a) +runTestIO = runTestIO' defaultMemType defaultBounds -- | 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 +runTestIO' :: MemType -> Bounds -> Predicate a -> ConcIO a -> IO (Result a) +runTestIO' memtype cb predicate conc = predicate <$> sctBoundIO memtype cb conc -- * Predicates @@ -272,6 +433,38 @@ -- into a 'Result'. type Predicate a = [(Either Failure a, Trace)] -> Result a +-- | Reduce the list of failures in a @Predicate@ to one +-- representative trace for each unique result. +-- +-- This may throw away \"duplicate\" failures which have a unique +-- cause but happen to manifest in the same way. However, it is +-- convenient for filtering out true duplicates. +representative :: Eq a => Predicate a -> Predicate a +representative p xs = result { _failures = choose . collect $ _failures result } where + result = p xs + collect = groupBy' [] ((==) `on` fst) + choose = map $ minimumBy (comparing $ \(_, trc) -> (preEmpCount' trc, length trc)) + + groupBy' res _ [] = res + groupBy' res eq (x:xs) = groupBy' (insert' eq x res) eq xs + + insert' eq x [] = [[x]] + insert' eq x (ys@(y:_):yss) + | x `eq` y = (x:ys) : yss + | otherwise = ys : insert' eq x yss + +-- | Check that a computation never aborts. +abortsNever :: Predicate a +abortsNever = alwaysTrue (not . either (==Abort) (const False)) + +-- | Check that a computation always aborts. +abortsAlways :: Predicate a +abortsAlways = alwaysTrue $ either (==Abort) (const False) + +-- | Check that a computation aborts at least once. +abortsSometimes :: Predicate a +abortsSometimes = somewhereTrue $ either (==Abort) (const False) + -- | Check that a computation never deadlocks. deadlocksNever :: Predicate a deadlocksNever = alwaysTrue (not . either (`elem` [Deadlock, STMDeadlock]) (const False)) @@ -300,12 +493,12 @@ -- 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 (==) +alwaysSame = representative $ 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 +notAlwaysSame [x] = (defaultFail [x]) { _casesChecked = 1 } +notAlwaysSame xs = go xs $ defaultFail [] where go [y1,y2] res | fst y1 /= fst y2 = incCC res { _pass = True } | otherwise = incCC res { _failures = y1 : y2 : _failures res } @@ -317,12 +510,14 @@ -- | 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 +alwaysTrue p xs = go xs $ (defaultFail failures) { _pass = True } where go (y:ys) res | p (fst y) = go ys . incCC $ res | otherwise = incCC $ res { _pass = False } go [] res = res + failures = filter (not . p . fst) xs + -- | 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. @@ -330,8 +525,8 @@ -- 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 +alwaysTrue2 _ [_] = defaultPass { _casesChecked = 1 } +alwaysTrue2 p xs = go xs $ defaultPass { _failures = failures } where go [y1,y2] res | p (fst y1) (fst y2) = incCC res | otherwise = incCC res { _pass = False } @@ -340,24 +535,56 @@ | 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 _ = [] + failures = fgo xs where + fgo (y1:y2:ys) + | p (fst y1) (fst y2) = fgo (y2:ys) + | otherwise = y1 : y2 : fgo2 y2 ys + fgo _ = [] + fgo2 y1 (y2:ys) + | p (fst y1) (fst y2) = fgo (y2:ys) + | otherwise = y2 : fgo2 y2 ys + fgo2 _ _ = [] + -- | 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 +somewhereTrue p xs = go xs $ defaultFail failures where go (y:ys) res | p (fst y) = incCC $ res { _pass = True } | otherwise = go ys . incCC $ res { _failures = y : _failures res } go [] res = res + failures = filter (not . p . fst) xs + +-- | Predicate for when there is a known set of results where every +-- result must be exhibited at least once. +gives :: (Eq a, Show a) => [Either Failure a] -> Predicate a +gives expected results = go expected [] results $ defaultFail failures where + go waitingFor alreadySeen ((x, _):xs) res + -- If it's a result we're waiting for, move it to the + -- @alreadySeen@ list and continue. + | x `elem` waitingFor = go (filter (/=x) waitingFor) (x:alreadySeen) xs res { _casesChecked = _casesChecked res + 1 } + + -- If it's a result we've already seen, continue. + | x `elem` alreadySeen = go waitingFor alreadySeen xs res { _casesChecked = _casesChecked res + 1 } + + -- If it's not a result we expected, fail. + | otherwise = res { _casesChecked = _casesChecked res + 1 } + + go [] _ [] res = res { _pass = True } + go es _ [] res = res { _failureMsg = unlines $ map (\e -> "Expected: " ++ show e) es } + + failures = filter (\(r, _) -> r `notElem` expected) results + +-- | Variant of 'gives' that doesn't allow for expected failures. +gives' :: (Eq a, Show a) => [a] -> Predicate a +gives' = gives . map Right + -- * Internal -- | Run a test and print to stdout -doTest :: (Eq a, Show a) => String -> Result a -> IO Bool +doTest :: Show a => String -> Result a -> IO Bool doTest name result = do if _pass result then @@ -367,8 +594,11 @@ -- Display a failure message, and the first 5 (simplified) failed traces putStrLn ("\27[31m[fail]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")") + unless (null $ _failureMsg result) $ + putStrLn $ _failureMsg result + let failures = _failures result - mapM_ (\(r, t) -> putStrLn $ "\t" ++ either showfail show r ++ " " ++ showTrace t) $ take 5 failures + mapM_ (\(r, t) -> putStrLn $ "\t" ++ either showFail show r ++ " " ++ showTrace t) $ take 5 failures when (moreThan failures 5) $ putStrLn "\t..." @@ -377,11 +607,3 @@ -- | 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 --- a/Test/DejaFu/Deterministic.hs +++ b/Test/DejaFu/Deterministic.hs @@ -1,10 +1,11 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeSynonymInstances #-} --- | Deterministic traced execution of concurrent computations which --- don't do @IO@. +-- | Deterministic traced execution of concurrent computations. -- -- This works by executing the computation on a single thread, calling -- out to the supplied scheduler after each step to determine which @@ -12,47 +13,16 @@ 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 + , ConcST + , ConcIO - -- * Testing - , _concNoTest - , _concKnowsAbout - , _concForgets - , _concAllKnown + -- * Executing computations + , Failure(..) + , MemType(..) + , runConcST + , runConcIO + , runConcST' + , runConcIO' -- * Execution traces , Trace @@ -63,264 +33,128 @@ , CVarId , CRefId , MaskingState(..) - , showTrace , toTrace + , showTrace + , showFail -- * Scheduling , module Test.DejaFu.Deterministic.Schedule ) where -import Control.Exception (Exception, MaskingState(..), SomeException(..)) -import Control.Monad.Cont (cont, runCont) +import Control.Exception (MaskingState(..)) import Control.Monad.ST (ST, runST) -import Data.STRef (STRef, newSTRef) +import Data.IORef (IORef) +import Data.STRef (STRef) import Test.DejaFu.Deterministic.Internal import Test.DejaFu.Deterministic.Schedule -import Test.DejaFu.Internal (refST) -import Test.DejaFu.STM (STMLike, runTransactionST) +import Test.DejaFu.Internal (refST, refIO) +import Test.DejaFu.STM (STMLike, STMIO, STMST, runTransactionIO, runTransactionST) 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 @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 +{-# ANN module ("HLint: ignore Use const" :: String) #-} -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 +newtype Conc n r s a = C { unC :: M n r s a } deriving (Functor, Applicative, Monad) - 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 +-- | A 'MonadConc' implementation using @ST@, this should be preferred +-- if you do not need 'liftIO'. +type ConcST t = Conc (ST t) (STRef t) (STMST t) -fixed :: Fixed (ST t) (STRef t) (STMLike t) -fixed = refST $ \ma -> cont (\c -> ALift $ c <$> ma) +-- | A 'MonadConc' implementation using @IO@. +type ConcIO = Conc IO IORef STMIO --- | 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 +toConc :: ((a -> Action n r s) -> Action n r s) -> Conc n r s a +toConc = C . cont --- | 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 +wrap :: (M n r s a -> M n r s a) -> Conc n r s a -> Conc n r s a +wrap f = C . f . unC --- | Run the provided computation concurrently, returning the result. -spawn :: Conc t a -> Conc t (CVar t a) -spawn = C.spawn +instance IO.MonadIO ConcIO where + liftIO ma = toConc (\c -> ALift (fmap c ma)) --- | 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 +instance Ca.MonadCatch (Conc n r s) where + catch ma h = toConc (ACatching (unC . h) (unC ma)) --- | Run the provided computation concurrently. -fork :: Conc t () -> Conc t ThreadId -fork (C ma) = C $ cont $ AFork (const' $ runCont ma $ const AStop) +instance Ca.MonadThrow (Conc n r s) where + throwM e = toConc (\_ -> AThrow e) --- | Get the 'ThreadId' of the current thread. -myThreadId :: Conc t ThreadId -myThreadId = C $ cont AMyTId +instance Ca.MonadMask (Conc n r s) where + mask mb = toConc (AMasking MaskedInterruptible (\f -> unC $ mb $ wrap f)) + uninterruptibleMask mb = toConc (AMasking MaskedUninterruptible (\f -> unC $ mb $ wrap f)) --- | 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 +instance Monad n => C.MonadConc (Conc n r (STMLike n r)) where + type CVar (Conc n r (STMLike n r)) = CVar r + type CRef (Conc n r (STMLike n r)) = CRef r + type Ticket (Conc n r (STMLike n r)) = Ticket + type STMLike (Conc n r (STMLike n r)) = STMLike n r + type ThreadId (Conc n r (STMLike n r)) = ThreadId --- | 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 () + forkWithUnmask ma = toConc (AFork (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop))) + forkOnWithUnmask _ = C.forkWithUnmask --- | 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 + -- This implementation lies and returns 2 until a value is set. This + -- will potentially avoid special-case behaviour for 1 capability, + -- so it seems a sane choice. + getNumCapabilities = toConc AGetNumCapabilities + setNumCapabilities caps = toConc (\c -> ASetNumCapabilities caps (c ())) --- | 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 + myThreadId = toConc AMyTId --- | 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 + yield = toConc (\c -> AYield (c ())) --- | 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 + newCRef a = toConc (\c -> ANewRef a c) --- | 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 + readCRef ref = toConc (AReadRef ref) + readForCAS ref = toConc (AReadRefCas ref) --- | Replace the value stored inside a 'CRef'. -writeCRef :: CRef t a -> a -> Conc t () -writeCRef ref a = modifyCRef ref $ const (a, ()) + peekTicket tick = toConc (APeekTicket tick) --- | 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) + writeCRef ref a = toConc (\c -> AWriteRef ref a (c ())) + casCRef ref tick a = toConc (ACasRef ref tick a) --- | 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 () + modifyCRef ref f = toConc (AModRef ref f) + modifyCRefCAS ref f = toConc (AModRefCas ref f) --- | 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) + newEmptyCVar = toConc (\c -> ANewVar c) --- | 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 + putCVar var a = toConc (\c -> APutVar var a (c ())) + readCVar var = toConc (AReadVar var) + takeCVar var = toConc (ATakeVar var) --- | 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) + tryPutCVar var a = toConc (ATryPutVar var a) + tryTakeCVar var = toConc (ATryTakeVar var) --- | 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) + throwTo tid e = toConc (\c -> AThrowTo tid e (c ())) --- | 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 + atomically = toConc . AAtom --- | 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 ()) + _concKnowsAbout (Left (CVar (cvarid, _))) = toConc (\c -> AKnowsAbout (Left cvarid) (c ())) + _concKnowsAbout (Right (CTVar (ctvarid, _))) = toConc (\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 ()) + _concForgets (Left (CVar (cvarid, _))) = toConc (\c -> AForgets (Left cvarid) (c ())) + _concForgets (Right (CTVar (ctvarid, _))) = toConc (\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 ()) + _concAllKnown = toConc (\c -> AAllKnown (c ())) -- | Run a concurrent computation with a given 'Scheduler' and initial -- state, returning a failure reason on error. Also returned is the @@ -329,17 +163,39 @@ -- 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 +-- > runConc roundRobinSched SequentialConsistency () 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 +runConcST :: Scheduler s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace) +runConcST sched memtype s ma = + let (r, s', t') = runConcST' sched memtype s ma in (r, s', toTrace t') --- | Variant of '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 +-- | Variant of 'runConcST' which produces a 'Trace''. +runConcST' :: Scheduler s -> MemType -> s -> (forall t. ConcST t a) -> (Either Failure a, s, Trace') +runConcST' sched memtype s ma = runST $ runFixed fixed runTransactionST sched memtype s $ unC ma where + fixed = refST $ \mb -> cont (\c -> ALift $ c <$> mb) + +-- | Run a concurrent computation in the @IO@ monad with a given +-- 'Scheduler' and initial state, returning a failure reason on +-- error. Also returned is the final state of the scheduler, and an +-- execution trace. +-- +-- __Warning:__ Blocking on the action of another thread in 'liftIO' +-- cannot be detected! So if you perform some potentially blocking +-- action in a 'liftIO' the entire collection of threads may deadlock! +-- You should therefore keep @IO@ blocks small, and only perform +-- blocking operations with the supplied primitives, insofar as +-- possible. +runConcIO :: Scheduler s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace) +runConcIO sched memtype s ma = do + (r, s', t') <- runConcIO' sched memtype s ma + return (r, s', toTrace t') + +-- | Variant of 'runConcIO' which produces a 'Trace''. +runConcIO' :: Scheduler s -> MemType -> s -> ConcIO a -> IO (Either Failure a, s, Trace') +runConcIO' sched memtype s ma = runFixed fixed runTransactionIO sched memtype s $ unC ma where + fixed = refIO $ \mb -> cont (\c -> ALift $ c <$> mb) diff --git a/Test/DejaFu/Deterministic/IO.hs b/Test/DejaFu/Deterministic/IO.hs deleted file mode 100644 --- a/Test/DejaFu/Deterministic/IO.hs +++ /dev/null @@ -1,337 +0,0 @@ -{-# 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 --- a/Test/DejaFu/Deterministic/Internal.hs +++ b/Test/DejaFu/Deterministic/Internal.hs @@ -2,13 +2,6 @@ {-# 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 @@ -17,19 +10,25 @@ , runFixed' -- * The @Conc@ Monad - , M - , V - , R + , M(..) + , CVar(..) + , CRef(..) + , Ticket(..) , Fixed + , cont + , runCont -- * Primitive Actions , Action(..) -- * Identifiers - , ThreadId - , CVarId - , CRefId + , ThreadId(..) + , CVarId(..) + , CRefId(..) + -- * Memory Models + , MemType(..) + -- * Scheduling & Traces , Scheduler , Trace @@ -37,37 +36,44 @@ , ThreadAction(..) , Lookahead(..) , Trace' - , showTrace + , lookahead + , willRelease , toTrace + , showTrace + , showFail + -- * Synchronised and Unsynchronised Actions + , ActionType(..) + , isBarrier + , synchronises + , crefOf + , cvarOf + , simplify + , simplify' + -- * Failures , Failure(..) - - -- * Utils - , const' ) where -import Control.Exception (MaskingState(..)) -import Control.Monad.Cont (cont, runCont) +import Control.Exception (MaskingState(..), SomeException(..)) import Data.List (sort) import Data.List.Extra -import Data.Maybe (fromJust, isJust, isNothing, listToMaybe) +import Data.Maybe (fromJust, isJust, fromMaybe, isNothing, listToMaybe) +import Data.Typeable (cast) 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.Memory import Test.DejaFu.Deterministic.Internal.Threading -import qualified Data.Map as M +import qualified Data.Map.Strict 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 +{-# ANN module ("HLint: ignore Use const" :: String) #-} -------------------------------------------------------------------------------- -- * Execution @@ -76,21 +82,21 @@ -- 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 +runFixed :: (Functor n, Monad n) => Fixed n r s -> (forall x. s x -> CTVarId -> n (Result x, CTVarId)) + -> Scheduler g -> MemType -> g -> M n r s a -> n (Either Failure a, g, Trace') +runFixed fixed runstm sched memtype s ma = (\(e,g,_,t) -> (e,g,t)) <$> runFixed' fixed runstm sched memtype s initialIdSource ma -- | Same as 'runFixed', be parametrised by an 'IdSource'. runFixed' :: forall n r s g a. (Functor n, Monad n) - => Fixed n r s -> (forall x. s 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 + => Fixed n r s -> (forall x. s x -> CTVarId -> n (Result x, CTVarId)) + -> Scheduler g -> MemType -> g -> IdSource -> M n r s a -> n (Either Failure a, g, IdSource, Trace') +runFixed' fixed runstm sched memtype s idSource ma = do ref <- newRef fixed Nothing let c = ma >>= liftN fixed . writeRef fixed ref . Just . Right - let threads = launch' Unmasked 0 (const' $ runCont c $ const AStop) M.empty + let threads = launch' Unmasked 0 ((\a _ -> a) $ runCont c $ const AStop) M.empty - (s', idSource', trace) <- runThreads fixed runstm sched s threads idSource ref + (s', idSource', trace) <- runThreads fixed runstm sched memtype s threads idSource ref out <- readRef fixed ref return (fromJust out, s', idSource', reverse trace) @@ -101,37 +107,35 @@ -- 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) +runThreads :: (Functor n, Monad n) => Fixed n r s -> (forall x. s x -> CTVarId -> n (Result x, CTVarId)) + -> Scheduler g -> MemType -> g -> Threads n r s -> IdSource -> r (Maybe (Either Failure a)) -> n (g, IdSource, Trace') +runThreads fixed runstm sched memtype origg origthreads idsrc ref = go idsrc [] Nothing origg origthreads emptyBuffer 2 where + go idSource sofar prior g threads wb caps + | isTerminated = stop g + | isDeadlocked = die g Deadlock + | isSTMLocked = die g STMDeadlock + | isAborted = die g' Abort + | isNonexistant = die g' InternalError + | isBlocked = die g' InternalError | otherwise = do - stepped <- stepThread fixed runconc runstm (_continuation $ fromJust thread) idSource chosen threads + stepped <- stepThread fixed runstm memtype (_continuation $ fromJust thread) idSource chosen threads wb caps 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'' + Right (threads', idSource', act, wb', caps') -> loop threads' idSource' act wb' caps' 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' + | chosen == 0 -> die g' UncaughtException + | otherwise -> loop (kill chosen threads) idSource Killed wb caps - Left failure -> writeRef fixed ref (Just $ Left failure) >> return (g, idSource, sofar) + Left failure -> die g' failure where - (chosen, g') = sched g ((\p (_,_,a) -> (p,a)) <$> prior <*> listToMaybe sofar) $ unsafeToNonEmpty runnable' + (choice, g') = sched g (map (\(d,_,a) -> (d,a)) $ reverse sofar) ((\p (_,_,a) -> (p,a)) <$> prior <*> listToMaybe sofar) $ unsafeToNonEmpty runnable' + chosen = fromJust choice runnable' = [(t, nextActions t) | t <- sort $ M.keys runnable] - runnable = M.filter (isNothing . _blocking) threads - thread = M.lookup chosen threads + runnable = M.filter (isNothing . _blocking) threadsc + thread = M.lookup chosen threadsc + threadsc = addCommitThreads wb threads + isAborted = isNothing choice isBlocked = isJust . _blocking $ fromJust thread isNonexistant = isNothing thread isTerminated = 0 `notElem` M.keys threads @@ -140,9 +144,7 @@ ((~= 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 + unblockWaitingOn tid = fmap unblock where unblock thrd = case _blocking thrd of Just (OnMask t) | t == tid -> thrd { _blocking = Nothing } _ -> thrd @@ -157,64 +159,61 @@ | 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] + nextActions t = lookahead . _continuation . fromJust $ M.lookup t threadsc + stop outg = return (outg, idSource, sofar) + die outg reason = writeRef fixed ref (Just $ Left reason) >> stop outg + + loop threads' idSource' act wb' = + let sofar' = ((decision, alternatives, act) : sofar) + threads'' = if (interruptible <$> M.lookup chosen threads') /= Just False then unblockWaitingOn chosen threads' else threads' + in go idSource' sofar' (Just chosen) g' (delCommitThreads threads'') wb' + -------------------------------------------------------------------------------- -- * Single-step execution -- | Run a single thread one step, by dispatching on the type of -- 'Action'. stepThread :: forall n r s. (Functor n, Monad n) => Fixed n r s - -> (forall x. 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 + -> (forall x. s x -> CTVarId -> n (Result x, CTVarId)) + -- ^ Run a 'MonadSTM' transaction atomically. + -> MemType + -- ^ The memory model + -> Action n r s + -- ^ Action to step + -> IdSource + -- ^ Source of fresh IDs + -> ThreadId + -- ^ ID of the current thread + -> Threads n r s + -- ^ Current state of threads + -> WriteBuffer r + -- ^ @CRef@ write buffer + -> Int + -- ^ The number of capabilities + -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int)) +stepThread fixed runstm memtype action idSource tid threads wb caps = case action of AFork 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 + AGetNumCapabilities c -> stepGetNumCapabilities c + ASetNumCapabilities i c -> stepSetNumCapabilities i c + AYield c -> stepYield c + ANewVar c -> stepNewVar c + APutVar var a c -> stepPutVar var a c + ATryPutVar var a c -> stepTryPutVar var a c + AReadVar var c -> stepReadVar var c + ATakeVar var c -> stepTakeVar var c + ATryTakeVar var c -> stepTryTakeVar var c + ANewRef a c -> stepNewRef a c AReadRef ref c -> stepReadRef ref c + AReadRefCas ref c -> stepReadRefCas ref c + APeekTicket tick c -> stepPeekTicket tick c AModRef ref f c -> stepModRef ref f c + AModRefCas ref f c -> stepModRefCas ref f c + AWriteRef ref a c -> stepWriteRef ref a c + ACasRef ref tick a c -> stepCasRef ref tick a c + ACommit t c -> stepCommit t c AAtom stm c -> stepAtom stm c - ANew na -> stepNew na - ANewRef na -> stepNewRef na ALift na -> stepLift na AThrow e -> stepThrow e AThrowTo t e c -> stepThrowTo t e c @@ -222,7 +221,7 @@ 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 + AReturn c -> stepReturn c AKnowsAbout v c -> stepKnowsAbout v c AForgets v c -> stepForgets v c AAllKnown c -> stepAllKnown c @@ -230,103 +229,163 @@ where -- | Start a new thread, assigning it the next 'ThreadId' - stepFork a b = return $ Right (goto (b newtid) tid threads', idSource', Fork newtid) where + stepFork a b = return $ Right (goto (b newtid) tid threads', idSource', Fork newtid, wb, caps) where threads' = launch tid newtid a threads (idSource', newtid) = nextTId idSource -- | Get the 'ThreadId' of the current thread - stepMyTId c = return $ Right (goto (c tid) tid threads, idSource, MyThreadId) + stepMyTId c = simple (goto (c tid) tid threads) MyThreadId + -- | Get the number of capabilities + stepGetNumCapabilities c = simple (goto (c caps) tid threads) $ GetNumCapabilities caps + + -- | Set the number of capabilities + stepSetNumCapabilities i c = return $ Right (goto c tid threads, idSource, SetNumCapabilities i, wb, i) + + -- | Yield the current thread + stepYield c = simple (goto c tid threads) Yield + -- | Put a value into a @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) + stepPutVar cvar@(CVar (cvid, _)) a c = synchronised $ do + (success, threads', woken) <- putIntoCVar cvar a c fixed tid threads + simple threads' $ if success then PutVar cvid woken else BlockedPutVar cvid -- | Try to put a value into a @CVar@, without blocking. - 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) + stepTryPutVar cvar@(CVar (cvid, _)) a c = synchronised $ do + (success, threads', woken) <- tryPutIntoCVar cvar a c fixed tid threads + simple threads' $ TryPutVar 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) + stepReadVar cvar@(CVar (cvid, _)) c = synchronised $ do + (success, threads', _) <- readFromCVar cvar c fixed tid threads + simple threads' $ if success then ReadVar cvid else BlockedReadVar cvid -- | Take the value from a @CVar@, blocking the thread until it's -- 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) + stepTakeVar cvar@(CVar (cvid, _)) c = synchronised $ do + (success, threads', woken) <- takeFromCVar cvar c fixed tid threads + simple threads' $ if success then TakeVar cvid woken else BlockedTakeVar cvid -- | Try to take the value from a @CVar@, without blocking. - stepTryTake cvar@(cvid, _) c = do - (success, threads', woken) <- readFromCVar True False cvar c fixed tid threads - return $ Right (threads', idSource, TryTake cvid success woken) + stepTryTakeVar cvar@(CVar (cvid, _)) c = synchronised $ do + (success, threads', woken) <- tryTakeFromCVar cvar c fixed tid threads + simple threads' $ TryTakeVar 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) + stepReadRef cref@(CRef (crid, _)) c = do + val <- readCRef fixed cref tid + simple (goto (c val) tid threads) $ ReadRef crid + -- | Read from a @CRef@ for future compare-and-swap operations. + stepReadRefCas cref@(CRef (crid, _)) c = do + tick <- readForTicket fixed cref tid + simple (goto (c tick) tid threads) $ ReadRefCas crid + + -- | Extract the value from a @Ticket@. + stepPeekTicket (Ticket (crid, _, a)) c = simple (goto (c a) tid threads) $ PeekTicket crid + -- | Modify a @CRef@. - stepModRef (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) + stepModRef cref@(CRef (crid, _)) f c = synchronised $ do + (new, val) <- f <$> readCRef fixed cref tid + writeImmediate fixed cref new + simple (goto (c val) tid threads) $ ModRef crid + -- | Modify a @CRef@ using a compare-and-swap. + stepModRefCas cref@(CRef (crid, _)) f c = synchronised $ do + tick@(Ticket (_, _, old)) <- readForTicket fixed cref tid + let (new, val) = f old + casCRef fixed cref tid tick new + simple (goto (c val) tid threads) $ ModRefCas crid + + -- | Write to a @CRef@ without synchronising + stepWriteRef cref@(CRef (crid, _)) a c = case memtype of + -- Write immediately. + SequentialConsistency -> do + writeImmediate fixed cref a + simple (goto c tid threads) $ WriteRef crid + + -- Add to buffer using thread id. + TotalStoreOrder -> do + let (ThreadId tid') = tid + wb' <- bufferWrite fixed wb tid' cref a tid + return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps) + + -- Add to buffer using cref id + PartialStoreOrder -> do + let (CRefId crid') = crid + wb' <- bufferWrite fixed wb crid' cref a tid + return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps) + + -- | Perform a compare-and-swap on a @CRef@. + stepCasRef cref@(CRef (crid, _)) tick a c = synchronised $ do + (suc, tick') <- casCRef fixed cref tid tick a + simple (goto (c (suc, tick')) tid threads) $ CasRef crid suc + + -- | Commit a @CRef@ write + stepCommit t@(ThreadId t') c@(CRefId c') = do + wb' <- case memtype of + -- Shouldn't ever get here + SequentialConsistency -> + error "Attempting to commit under SequentialConsistency" + + -- Commit using the thread id. + TotalStoreOrder -> commitWrite fixed wb t' + + -- Commit using the cref id. + PartialStoreOrder -> commitWrite fixed wb c' + + return $ Right (threads, idSource, CommitRef t c, wb', caps) + -- | Run a STM transaction atomically. - stepAtom stm c = do + stepAtom stm c = synchronised $ 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) + in return $ Right (knows (map Right written) tid $ goto (c val) tid threads', idSource { _nextCTVId = newctvid }, STM woken, wb, caps) | otherwise -> - return $ Right (knows (map Right written) tid $ goto (c val) tid threads, idSource { _nextCTVId = newctvid }, FreshSTM) + return $ Right (knows (map Right written) tid $ goto (c val) tid threads, idSource { _nextCTVId = newctvid }, FreshSTM, wb, caps) Retry touched -> let threads' = block (OnCTVar touched) tid threads - in return $ Right (threads', idSource { _nextCTVId = newctvid }, BlockedSTM) + in return $ Right (threads', idSource { _nextCTVId = newctvid }, BlockedSTM, wb, caps) Exception e -> stepThrow e -- | Run a subcomputation in an exception-catching context. - stepCatching h ma c = return $ Right (threads', idSource, Catching) where + stepCatching h ma c = simple threads' 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 + threads' = goto a tid (catching e 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 + stepPopCatching a = simple threads' PopCatching where + threads' = goto a tid (uncatching tid threads) -- | Throw an exception, and propagate it to the appropriate -- handler. - stepThrow e = 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 + stepThrow e = + case propagate (wrap e) tid threads of + Just threads' -> simple threads' Throw + Nothing -> return $ Left UncaughtException -- | Throw an exception to the target thread, and propagate it to -- the appropriate handler. - stepThrowTo t e c = return $ + stepThrowTo t e c = synchronised $ 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 + blocked = block (OnMask t) tid threads 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) + | interruptible thread -> case propagate (wrap e) t threads' of + Just threads'' -> simple threads'' $ 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) + | t == 0 -> return $ Left UncaughtException + | otherwise -> simple (kill t threads') $ ThrowTo t + | otherwise -> simple blocked $ BlockedThrowTo t + Nothing -> simple threads' $ ThrowTo t -- | Execute a subcomputation with a new masking state, and give -- it a function to run a computation with the current masking @@ -337,54 +396,68 @@ 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 + -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int)) + stepMasking m ma c = simple threads' $ SetMasking False m where a = runCont (ma umask) (AResetMask False False m' . c) m' = _masking . fromJust $ M.lookup tid threads umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> return b - resetMask typ mask = cont $ \k -> AResetMask typ True mask $ k () + resetMask typ ms = cont $ \k -> AResetMask typ True ms $ k () - threads' = M.alter (\(Just thread) -> Just $ thread { _continuation = a, _masking = m }) tid threads + threads' = goto a tid (mask 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 + stepResetMask b1 b2 m c = simple threads' action where + action = (if b1 then SetMasking else ResetMasking) b2 m + threads' = goto c tid (mask m tid threads) -- | Create a new @CVar@, using the next 'CVarId'. - stepNew na = do + stepNewVar c = do let (idSource', newcvid) = nextCVId idSource - a <- na newcvid - return $ Right (knows [Left newcvid] tid $ goto a tid threads, idSource', New newcvid) + ref <- newRef fixed Nothing + let cvar = CVar (newcvid, ref) + return $ Right (knows [Left newcvid] tid $ goto (c cvar) tid threads, idSource', NewVar newcvid, wb, caps) -- | Create a new @CRef@, using the next 'CRefId'. - stepNewRef na = do + stepNewRef a c = do let (idSource', newcrid) = nextCRId idSource - a <- na newcrid - return $ Right (goto a tid threads, idSource', NewRef newcrid) + ref <- newRef fixed (M.empty, 0, a) + let cref = CRef (newcrid, ref) + return $ Right (goto (c cref) tid threads, idSource', NewRef newcrid, wb, caps) -- | Lift an action from the underlying monad into the @Conc@ -- computation. stepLift na = do a <- na - return $ Right (goto a tid threads, idSource, Lift) + simple (goto a tid threads) 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 + -- | Execute a 'return' or 'pure'. + stepReturn c = simple (goto c tid threads) Return -- | Record that a variable is known about. - stepKnowsAbout v c = return $ Right (knows [v] tid $ goto c tid threads, idSource, KnowsAbout) + stepKnowsAbout v c = simple (knows [v] tid $ goto c tid threads) KnowsAbout -- | Record that a variable will never be touched again. - stepForgets v c = return $ Right (forgets [v] tid $ goto c tid threads, idSource, Forgets) + stepForgets v c = simple (forgets [v] tid $ goto c tid threads) Forgets -- | Record that all shared variables are known. - stepAllKnown c = return $ Right (fullknown tid $ goto c tid threads, idSource, AllKnown) + stepAllKnown c = simple (fullknown tid $ goto c tid threads) AllKnown -- | Kill the current thread. - stepStop = return $ Right (kill tid threads, idSource, Stop) + stepStop = simple (kill tid threads) Stop + + -- | Helper for actions which don't touch the 'IdSource' or + -- 'WriteBuffer' + simple threads' act = return $ Right (threads', idSource, act, wb, caps) + + -- | Helper for actions impose a write barrier. + synchronised ma = do + writeBarrier fixed wb + res <- ma + + return $ case res of + Right (threads', idSource', act', _, caps') -> Right (threads', idSource', act', emptyBuffer, caps') + _ -> res + + -- | Helper function for wrapping up exceptions. + wrap e = fromMaybe (SomeException e) $ cast e diff --git a/Test/DejaFu/Deterministic/Internal/CVar.hs b/Test/DejaFu/Deterministic/Internal/CVar.hs deleted file mode 100644 --- a/Test/DejaFu/Deterministic/Internal/CVar.hs +++ /dev/null @@ -1,54 +0,0 @@ --- | 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 --- a/Test/DejaFu/Deterministic/Internal/Common.hs +++ b/Test/DejaFu/Deterministic/Internal/Common.hs @@ -1,34 +1,80 @@ -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# 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 Control.Exception (Exception, MaskingState(..)) +import Data.Map.Strict (Map) import Data.List.Extra import Test.DejaFu.Internal import Test.DejaFu.STM (CTVarId) +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative (Applicative(..)) +#endif + -------------------------------------------------------------------------------- -- * The @Conc@ Monad -- | The underlying monad is based on continuations over Actions. -type M n r s a = Cont (Action n r s) a +newtype M n r s a = M { runM :: (a -> Action n r s) -> Action n r s } --- | CVars are represented as a unique numeric identifier, and a +instance Functor (M n r s) where + fmap f m = M $ \ c -> runM m (c . f) + +instance Applicative (M n r s) where + pure x = M $ \c -> AReturn $ c x + f <*> v = M $ \c -> runM f (\g -> runM v (c . g)) + +instance Monad (M n r s) where + return = pure + m >>= k = M $ \c -> runM m (\x -> runM (k x) c) + +-- | The concurrent variable type used with the 'Conc' monad. One +-- notable difference between these and 'MVar's is that 'MVar's are +-- single-wakeup, and wake up in a FIFO order. Writing to a @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. +-- +-- @CVar@s are represented as a unique numeric identifier, and a -- reference containing a Maybe value. -type V r a = (CVarId, r (Maybe a)) +newtype CVar r a = CVar (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) +-- | The mutable non-blocking reference type. These are like 'IORef's. +-- +-- @CRef@s are represented as a unique numeric identifier and a +-- reference containing (a) any thread-local non-synchronised writes +-- (so each thread sees its latest write), (b) a commit count (used in +-- compare-and-swaps), and (c) the current value visible to all +-- threads. +newtype CRef r a = CRef (CRefId, r (Map ThreadId a, Integer, a)) +-- | The compare-and-swap proof type. +-- +-- @Ticket@s are represented as just a wrapper around the identifier +-- of the 'CRef' it came from, the commit count at the time it was +-- produced, and an @a@ value. This doesn't work in the source package +-- (atomic-primops) because of the need to use pointer equality. Here +-- we can just pack extra information into 'CRef' to avoid that need. +newtype Ticket a = Ticket (CRefId, Integer, a) + -- | Dict of methods for implementations to override. -type Fixed n r s = Ref n r (Cont (Action n r s)) +type Fixed n r s = Ref n r (M n r s) +-- | Construct a continuation-passing operation from a function. +cont :: ((a -> Action n r s) -> Action n r s) -> M n r s a +cont = M + +-- | Run a CPS computation with the given final computation. +runCont :: M n r s a -> (a -> Action n r s) -> Action n r s +runCont = runM + -------------------------------------------------------------------------------- -- * Primitive Actions @@ -37,43 +83,70 @@ -- 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) + 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) + + | AGetNumCapabilities (Int -> Action n r s) + | ASetNumCapabilities Int (Action n r s) + + | forall a. ANewVar (CVar r a -> Action n r s) + | forall a. APutVar (CVar r a) a (Action n r s) + | forall a. ATryPutVar (CVar r a) a (Bool -> Action n r s) + | forall a. AReadVar (CVar r a) (a -> Action n r s) + | forall a. ATakeVar (CVar r a) (a -> Action n r s) + | forall a. ATryTakeVar (CVar r a) (Maybe a -> Action n r s) + + | forall a. ANewRef a (CRef r a -> Action n r s) + | forall a. AReadRef (CRef r a) (a -> Action n r s) + | forall a. AReadRefCas (CRef r a) (Ticket a -> Action n r s) + | forall a. APeekTicket (Ticket a) (a -> Action n r s) + | forall a b. AModRef (CRef r a) (a -> (a, b)) (b -> Action n r s) + | forall a b. AModRefCas (CRef r a) (a -> (a, b)) (b -> Action n r s) + | forall a. AWriteRef (CRef r a) a (Action n r s) + | forall a. ACasRef (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r s) + + | forall e. Exception e => AThrow e + | forall e. Exception e => AThrowTo ThreadId e (Action n r s) | forall a e. Exception e => ACatching (e -> M n r s a) (M n r s a) (a -> Action n r s) | APopCatching (Action n r s) | forall a. AMasking MaskingState ((forall b. M n r s b -> M n r s b) -> M n r s a) (a -> Action n r s) | AResetMask Bool Bool MaskingState (Action n r s) + | AKnowsAbout (Either CVarId CTVarId) (Action n r s) - | AForgets (Either CVarId CTVarId) (Action n r s) - | AAllKnown (Action n r s) + | AForgets (Either CVarId CTVarId) (Action n r s) + | AAllKnown (Action n r s) + + | forall a. AAtom (s a) (a -> Action n r s) + | ALift (n (Action n r s)) + | AYield (Action n r s) + | AReturn (Action n r s) + | ACommit ThreadId CRefId | AStop -------------------------------------------------------------------------------- -- * Identifiers -- | Every live thread has a unique identitifer. -type ThreadId = Int +newtype ThreadId = ThreadId Int + deriving (NFData, Enum, Eq, Ord, Num, Real, Integral) +instance Show ThreadId where + show (ThreadId i) = show i + -- | Every 'CVar' has a unique identifier. -type CVarId = Int +newtype CVarId = CVarId Int + deriving (NFData, Enum, Eq, Ord, Num, Real, Integral) +instance Show CVarId where + show (CVarId i) = show i + -- | Every 'CRef' has a unique identifier. -type CRefId = Int +newtype CRefId = CRefId Int + deriving (NFData, Enum, Eq, Ord, Num, Real, Integral) +instance Show CRefId where + show (CRefId i) = show i + -- | The number of ID parameters was getting a bit unwieldy, so this -- hides them all away. data IdSource = Id { _nextCRId :: CRefId, _nextCVId :: CVarId, _nextCTVId :: CTVarId, _nextTId :: ThreadId } @@ -101,10 +174,10 @@ -------------------------------------------------------------------------------- -- * 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 +-- | A @Scheduler@ maintains some internal state; @s@, takes the trace +-- so far; the 'ThreadId' and 'ThreadAction' of the last thread +-- scheduled (or 'Nothing' if this is the first decision); and the +-- list of runnable threads including a lookahead (as far as can be -- determined). It produces a 'ThreadId' to schedule, and a new state. -- -- __Note:__ In order to prevent computation from hanging, the runtime @@ -112,7 +185,7 @@ -- 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) +type Scheduler s = s -> [(Decision, ThreadAction)] -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, NonEmpty Lookahead) -> (Maybe ThreadId, s) -- | One of the outputs of the runner is a @Trace@, which is a log of -- decisions made, alternative decisions (including what action would @@ -127,14 +200,20 @@ -- | 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) + go (_, alters, CommitRef t c) = (Commit, goA alters, CommitRef t c) + go (dec, alters, act) = (dec, goA alters, act) + goA = map $ \x -> case x of + (_, WillCommitRef t c:|_) -> (Commit, WillCommitRef t c) + (d, a:|_) -> (d, a) + -- | Pretty-print a trace. showTrace :: Trace -> String showTrace = trace "" 0 where trace prefix num ((Start tid,_,_):ds) = thread prefix num ++ trace ("S" ++ show tid) 1 ds trace prefix num ((SwitchTo tid,_,_):ds) = thread prefix num ++ trace ("P" ++ show tid) 1 ds trace prefix num ((Continue,_,_):ds) = trace prefix (num + 1) ds + trace prefix num ((Commit,_,_):ds) = thread prefix num ++ trace "C" 1 ds trace prefix num [] = thread prefix num thread prefix num = prefix ++ replicate num '-' @@ -150,12 +229,15 @@ -- ^ Continue running the last thread for another step. | SwitchTo ThreadId -- ^ Pre-empt the running thread, and switch to another. + | Commit + -- ^ Commit a 'CRef' write action so that every thread can see the + -- result. deriving (Eq, Show) instance NFData Decision where rnf (Start tid) = rnf tid rnf (SwitchTo tid) = rnf tid - rnf Continue = () + rnf d = d `seq` () -- | All the actions that a thread can perform. data ThreadAction = @@ -163,30 +245,50 @@ -- ^ Start a new thread. | MyThreadId -- ^ Get the 'ThreadId' of the current thread. - | New CVarId + | GetNumCapabilities Int + -- ^ Get the number of Haskell threads that can run simultaneously. + | SetNumCapabilities Int + -- ^ Set the number of Haskell threads that can run simultaneously. + | Yield + -- ^ Yield the current thread. + | NewVar CVarId -- ^ Create a new 'CVar'. - | Put CVarId [ThreadId] + | PutVar CVarId [ThreadId] -- ^ Put into a 'CVar', possibly waking up some threads. - | BlockedPut CVarId + | BlockedPutVar CVarId -- ^ Get blocked on a put. - | TryPut CVarId Bool [ThreadId] + | TryPutVar CVarId Bool [ThreadId] -- ^ Try to put into a 'CVar', possibly waking up some threads. - | Read CVarId + | ReadVar CVarId -- ^ Read from a 'CVar'. - | BlockedRead CVarId + | BlockedReadVar CVarId -- ^ Get blocked on a read. - | Take CVarId [ThreadId] + | TakeVar CVarId [ThreadId] -- ^ Take from a 'CVar', possibly waking up some threads. - | BlockedTake CVarId + | BlockedTakeVar CVarId -- ^ Get blocked on a take. - | TryTake CVarId Bool [ThreadId] + | TryTakeVar 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'. + | ReadRefCas CRefId + -- ^ Read from a 'CRef' for a future compare-and-swap. + | PeekTicket CRefId + -- ^ Extract the value from a 'Ticket'. | ModRef CRefId -- ^ Modify a 'CRef'. + | ModRefCas CRefId + -- ^ Modify a 'CRef' using a compare-and-swap. + | WriteRef CRefId + -- ^ Write to a 'CRef' without synchronising. + | CasRef CRefId Bool + -- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising + -- it. + | CommitRef ThreadId CRefId + -- ^ Commit the last write to the given 'CRef' by the given thread, + -- so that all threads can see the updated value. | STM [ThreadId] -- ^ An STM transaction was executed, possibly waking up some -- threads. @@ -219,9 +321,8 @@ -- ^ 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. + | Return + -- ^ A 'return' or 'pure' action was executed. | KnowsAbout -- ^ A '_concKnowsAbout' annotation was processed. | Forgets @@ -233,21 +334,33 @@ 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` () + rnf (Fork t) = rnf t + rnf (GetNumCapabilities i) = rnf i + rnf (SetNumCapabilities i) = rnf i + rnf (NewVar c) = rnf c + rnf (PutVar c ts) = rnf (c, ts) + rnf (BlockedPutVar c) = rnf c + rnf (TryPutVar c b ts) = rnf (c, b, ts) + rnf (ReadVar c) = rnf c + rnf (BlockedReadVar c) = rnf c + rnf (TakeVar c ts) = rnf (c, ts) + rnf (BlockedTakeVar c) = rnf c + rnf (TryTakeVar c b ts) = rnf (c, b, ts) + rnf (NewRef c) = rnf c + rnf (ReadRef c) = rnf c + rnf (ReadRefCas c) = rnf c + rnf (PeekTicket c) = rnf c + rnf (ModRef c) = rnf c + rnf (ModRefCas c) = rnf c + rnf (WriteRef c) = rnf c + rnf (CasRef c b) = rnf (c, b) + rnf (CommitRef t c) = rnf (t, c) + rnf (STM ts) = rnf ts + rnf (ThrowTo t) = rnf t + rnf (BlockedThrowTo t) = rnf t + rnf (SetMasking b m) = b `seq` m `seq` () + rnf (ResetMasking b m) = b `seq` m `seq` () + rnf a = a `seq` () -- | A one-step look-ahead at what a thread will do next. data Lookahead = @@ -255,24 +368,45 @@ -- ^ Will start a new thread. | WillMyThreadId -- ^ Will get the 'ThreadId'. - | WillNew + | WillGetNumCapabilities + -- ^ Will get the number of Haskell threads that can run + -- simultaneously. + | WillSetNumCapabilities Int + -- ^ Will set the number of Haskell threads that can run + -- simultaneously. + | WillYield + -- ^ Will yield the current thread. + | WillNewVar -- ^ Will create a new 'CVar'. - | WillPut CVarId + | WillPutVar CVarId -- ^ Will put into a 'CVar', possibly waking up some threads. - | WillTryPut CVarId + | WillTryPutVar CVarId -- ^ Will try to put into a 'CVar', possibly waking up some threads. - | WillRead CVarId + | WillReadVar CVarId -- ^ Will read from a 'CVar'. - | WillTake CVarId + | WillTakeVar CVarId -- ^ Will take from a 'CVar', possibly waking up some threads. - | WillTryTake CVarId + | WillTryTakeVar 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'. + | WillPeekTicket CRefId + -- ^ Will extract the value from a 'Ticket'. + | WillReadRefCas CRefId + -- ^ Will read from a 'CRef' for a future compare-and-swap. | WillModRef CRefId -- ^ Will modify a 'CRef'. + | WillModRefCas CRefId + -- ^ Will nodify a 'CRef' using a compare-and-swap. + | WillWriteRef CRefId + -- ^ Will write to a 'CRef' without synchronising. + | WillCasRef CRefId + -- ^ Will attempt to to a 'CRef' using a compare-and-swap, + -- synchronising it. + | WillCommitRef ThreadId CRefId + -- ^ Will commit the last write by the given thread to the 'CRef'. | WillSTM -- ^ Will execute an STM transaction, possibly waking up some -- threads. @@ -296,9 +430,8 @@ -- ^ 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. + | WillReturn + -- ^ Will execute a 'return' or 'pure' action. | WillKnowsAbout -- ^ Will process a '_concKnowsAbout' annotation. | WillForgets @@ -310,17 +443,191 @@ 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 (WillSetNumCapabilities i) = rnf i + rnf (WillPutVar c) = rnf c + rnf (WillTryPutVar c) = rnf c + rnf (WillReadVar c) = rnf c + rnf (WillTakeVar c) = rnf c + rnf (WillTryTakeVar c) = rnf c rnf (WillReadRef c) = rnf c - rnf (WillModRef c) = rnf c - rnf ta = ta `seq` () + rnf (WillReadRefCas c) = rnf c + rnf (WillPeekTicket c) = rnf c + rnf (WillModRef c) = rnf c + rnf (WillModRefCas c) = rnf c + rnf (WillWriteRef c) = rnf c + rnf (WillCasRef c) = rnf c + rnf (WillCommitRef t c) = rnf (t, c) + rnf (WillThrowTo t) = rnf t + rnf (WillSetMasking b m) = b `seq` m `seq` () + rnf (WillResetMasking b m) = b `seq` m `seq` () + rnf l = l `seq` () +-- | Look as far ahead in the given continuation as possible. +lookahead :: Action n r s -> NonEmpty Lookahead +lookahead = unsafeToNonEmpty . lookahead' where + lookahead' (AFork _ _) = [WillFork] + lookahead' (AMyTId _) = [WillMyThreadId] + lookahead' (AGetNumCapabilities _) = [WillGetNumCapabilities] + lookahead' (ASetNumCapabilities i k) = WillSetNumCapabilities i : lookahead' k + lookahead' (ANewVar _) = [WillNewVar] + lookahead' (APutVar (CVar (c, _)) _ k) = WillPutVar c : lookahead' k + lookahead' (ATryPutVar (CVar (c, _)) _ _) = [WillTryPutVar c] + lookahead' (AReadVar (CVar (c, _)) _) = [WillReadVar c] + lookahead' (ATakeVar (CVar (c, _)) _) = [WillTakeVar c] + lookahead' (ATryTakeVar (CVar (c, _)) _) = [WillTryTakeVar c] + lookahead' (ANewRef _ _) = [WillNewRef] + lookahead' (AReadRef (CRef (r, _)) _) = [WillReadRef r] + lookahead' (AReadRefCas (CRef (r, _)) _) = [WillReadRefCas r] + lookahead' (APeekTicket (Ticket (r, _, _)) _) = [WillPeekTicket r] + lookahead' (AModRef (CRef (r, _)) _ _) = [WillModRef r] + lookahead' (AModRefCas (CRef (r, _)) _ _) = [WillModRefCas r] + lookahead' (AWriteRef (CRef (r, _)) _ k) = WillWriteRef r : lookahead' k + lookahead' (ACasRef (CRef (r, _)) _ _ _) = [WillCasRef r] + lookahead' (ACommit t c) = [WillCommitRef t c] + lookahead' (AAtom _ _) = [WillSTM] + lookahead' (AThrow _) = [WillThrow] + lookahead' (AThrowTo tid _ k) = WillThrowTo tid : lookahead' k + lookahead' (ACatching _ _ _) = [WillCatching] + lookahead' (APopCatching k) = WillPopCatching : lookahead' k + lookahead' (AMasking ms _ _) = [WillSetMasking False ms] + lookahead' (AResetMask b1 b2 ms k) = (if b1 then WillSetMasking else WillResetMasking) b2 ms : lookahead' k + lookahead' (ALift _) = [WillLift] + lookahead' (AKnowsAbout _ k) = WillKnowsAbout : lookahead' k + lookahead' (AForgets _ k) = WillForgets : lookahead' k + lookahead' (AAllKnown k) = WillAllKnown : lookahead' k + lookahead' (AYield k) = WillYield : lookahead' k + lookahead' (AReturn k) = WillReturn : lookahead' k + lookahead' AStop = [WillStop] + +-- | Check if an operation could enable another thread. +willRelease :: Lookahead -> Bool +willRelease WillFork = True +willRelease WillYield = True +willRelease (WillPutVar _) = True +willRelease (WillTryPutVar _) = True +willRelease (WillReadVar _) = True +willRelease (WillTakeVar _) = True +willRelease (WillTryTakeVar _) = True +willRelease WillSTM = True +willRelease WillThrow = True +willRelease (WillSetMasking _ _) = True +willRelease (WillResetMasking _ _) = True +willRelease WillStop = True +willRelease _ = False + +-- | A simplified view of the possible actions a thread can perform. +data ActionType = + UnsynchronisedRead CRefId + -- ^ A 'readCRef' or a 'readForCAS'. + | UnsynchronisedWrite CRefId + -- ^ A 'writeCRef'. + | UnsynchronisedOther + -- ^ Some other action which doesn't require cross-thread + -- communication. + | PartiallySynchronisedCommit CRefId + -- ^ A commit. + | PartiallySynchronisedWrite CRefId + -- ^ A 'casCRef' + | PartiallySynchronisedModify CRefId + -- ^ A 'modifyCRefCAS' + | SynchronisedModify CRefId + -- ^ An 'atomicModifyCRef'. + | SynchronisedRead CVarId + -- ^ A 'readCVar' or 'takeCVar' (or @try@/@blocked@ variants). + | SynchronisedWrite CVarId + -- ^ A 'putCVar' (or @try@/@blocked@ variant). + | SynchronisedOther + -- ^ Some other action which does require cross-thread + -- communication. + deriving (Eq, Show) + +instance NFData ActionType where + rnf (UnsynchronisedRead r) = rnf r + rnf (UnsynchronisedWrite r) = rnf r + rnf (PartiallySynchronisedCommit r) = rnf r + rnf (PartiallySynchronisedWrite r) = rnf r + rnf (PartiallySynchronisedModify r) = rnf r + rnf (SynchronisedModify r) = rnf r + rnf (SynchronisedRead c) = rnf c + rnf (SynchronisedWrite c) = rnf c + rnf a = a `seq` () + +-- | Check if an action imposes a write barrier. +isBarrier :: ActionType -> Bool +isBarrier (SynchronisedModify _) = True +isBarrier (SynchronisedRead _) = True +isBarrier (SynchronisedWrite _) = True +isBarrier SynchronisedOther = True +isBarrier _ = False + +-- | Check if an action is synchronises a given 'CRef'. +synchronises :: ActionType -> CRefId -> Bool +synchronises (PartiallySynchronisedCommit c) r = c == r +synchronises (PartiallySynchronisedWrite c) r = c == r +synchronises (PartiallySynchronisedModify c) r = c == r +synchronises a _ = isBarrier a + +-- | Get the 'CRef' affected. +crefOf :: ActionType -> Maybe CRefId +crefOf (UnsynchronisedRead r) = Just r +crefOf (UnsynchronisedWrite r) = Just r +crefOf (SynchronisedModify r) = Just r +crefOf (PartiallySynchronisedCommit r) = Just r +crefOf (PartiallySynchronisedWrite r) = Just r +crefOf (PartiallySynchronisedModify r) = Just r +crefOf _ = Nothing + +-- | Get the 'CVar' affected. +cvarOf :: ActionType -> Maybe CVarId +cvarOf (SynchronisedRead c) = Just c +cvarOf (SynchronisedWrite c) = Just c +cvarOf _ = Nothing + +-- | Throw away information from a 'ThreadAction' and give a +-- simplified view of what is happening. +-- +-- This is used in the SCT code to help determine interesting +-- alternative scheduling decisions. +simplify :: ThreadAction -> ActionType +simplify (PutVar c _) = SynchronisedWrite c +simplify (BlockedPutVar c) = SynchronisedWrite c +simplify (TryPutVar c _ _) = SynchronisedWrite c +simplify (ReadVar c) = SynchronisedRead c +simplify (BlockedReadVar c) = SynchronisedRead c +simplify (TakeVar c _) = SynchronisedRead c +simplify (BlockedTakeVar c) = SynchronisedRead c +simplify (TryTakeVar c _ _) = SynchronisedRead c +simplify (ReadRef r) = UnsynchronisedRead r +simplify (ReadRefCas r) = UnsynchronisedRead r +simplify (ModRef r) = SynchronisedModify r +simplify (ModRefCas r) = PartiallySynchronisedModify r +simplify (WriteRef r) = UnsynchronisedWrite r +simplify (CasRef r _) = PartiallySynchronisedWrite r +simplify (CommitRef _ r) = PartiallySynchronisedCommit r +simplify (STM _) = SynchronisedOther +simplify BlockedSTM = SynchronisedOther +simplify (ThrowTo _) = SynchronisedOther +simplify (BlockedThrowTo _) = SynchronisedOther +simplify _ = UnsynchronisedOther + +-- | Variant of 'simplify' that takes a 'Lookahead'. +simplify' :: Lookahead -> ActionType +simplify' (WillPutVar c) = SynchronisedWrite c +simplify' (WillTryPutVar c) = SynchronisedWrite c +simplify' (WillReadVar c) = SynchronisedRead c +simplify' (WillTakeVar c) = SynchronisedRead c +simplify' (WillTryTakeVar c) = SynchronisedRead c +simplify' (WillReadRef r) = UnsynchronisedRead r +simplify' (WillReadRefCas r) = UnsynchronisedRead r +simplify' (WillModRef r) = SynchronisedModify r +simplify' (WillModRefCas r) = PartiallySynchronisedModify r +simplify' (WillWriteRef r) = UnsynchronisedWrite r +simplify' (WillCasRef r) = PartiallySynchronisedWrite r +simplify' (WillCommitRef _ r) = PartiallySynchronisedCommit r +simplify' WillSTM = SynchronisedOther +simplify' (WillThrowTo _) = SynchronisedOther +simplify' _ = UnsynchronisedOther + -------------------------------------------------------------------------------- -- * Failures @@ -330,16 +637,51 @@ -- ^ Will be raised if the scheduler does something bad. This should -- never arise unless you write your own, faulty, scheduler! If it -- does, please file a bug report. + | Abort + -- ^ The scheduler chose to abort execution. This will be produced + -- if, for example, all possible decisions exceed the specified + -- bounds (there have been too many pre-emptions, the computation + -- has executed for too long, or there have been too many yields). | Deadlock -- ^ The computation became blocked indefinitely on @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) + deriving (Eq, Show, Read, Ord, Enum, Bounded) instance NFData Failure where rnf f = f `seq` () -- WHNF == NF + +-- | Pretty-print a failure +showFail :: Failure -> String +showFail Abort = "[abort]" +showFail Deadlock = "[deadlock]" +showFail STMDeadlock = "[stm-deadlock]" +showFail InternalError = "[internal-error]" +showFail UncaughtException = "[exception]" + +-------------------------------------------------------------------------------- +-- * Memory Models + +-- | The memory model to use for non-synchronised 'CRef' operations. +data MemType = + SequentialConsistency + -- ^ The most intuitive model: a program behaves as a simple + -- interleaving of the actions in different threads. When a 'CRef' + -- is written to, that write is immediately visible to all threads. + | TotalStoreOrder + -- ^ Each thread has a write buffer. A thread sees its writes + -- immediately, but other threads will only see writes when they are + -- committed, which may happen later. Writes are committed in the + -- same order that they are created. + | PartialStoreOrder + -- ^ Each 'CRef' has a write buffer. A thread sees its writes + -- immediately, but other threads will only see writes when they are + -- committed, which may happen later. Writes to different 'CRef's + -- are not necessarily committed in the same order that they are + -- created. + deriving (Eq, Show, Read, Ord, Enum, Bounded) + +instance NFData MemType where + rnf m = m `seq` () -- WHNF == NF diff --git a/Test/DejaFu/Deterministic/Internal/Memory.hs b/Test/DejaFu/Deterministic/Internal/Memory.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/Deterministic/Internal/Memory.hs @@ -0,0 +1,192 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE GADTs #-} + +-- | Operations over @CRef@s and @CVar@s +module Test.DejaFu.Deterministic.Internal.Memory where + +import Control.Monad (when) +import Data.IntMap.Strict (IntMap) +import Data.Maybe (isJust, fromJust) +import Data.Monoid ((<>)) +import Data.Sequence (Seq, ViewL(..), (><), singleton, viewl) +import Test.DejaFu.Deterministic.Internal.Common +import Test.DejaFu.Deterministic.Internal.Threading +import Test.DejaFu.Internal + +import qualified Data.IntMap.Strict as I +import qualified Data.Map.Strict as M + +#if __GLASGOW_HASKELL__ < 710 +import Data.Foldable (mapM_) +import Prelude hiding (mapM_) +#endif + +-------------------------------------------------------------------------------- +-- * Manipulating @CRef@s + +-- | In non-sequentially-consistent memory models, non-synchronised +-- writes get buffered. +-- +-- In TSO, the keys are @ThreadId@s. In PSO, the keys are @CRefId@s. +newtype WriteBuffer r = WriteBuffer { buffer :: IntMap (Seq (BufferedWrite r)) } + +-- | A buffered write is a reference to the variable, and the value to +-- write. Universally quantified over the value type so that the only +-- thing which can be done with it is to write it to the reference. +data BufferedWrite r where + BufferedWrite :: ThreadId -> CRef r a -> a -> BufferedWrite r + +-- | An empty write buffer. +emptyBuffer :: WriteBuffer r +emptyBuffer = WriteBuffer I.empty + +-- | Add a new write to the end of a buffer. +bufferWrite :: Monad n => Fixed n r s -> WriteBuffer r -> Int -> CRef r a -> a -> ThreadId -> n (WriteBuffer r) +bufferWrite fixed (WriteBuffer wb) i cref@(CRef (_, ref)) new tid = do + -- Construct the new write buffer + let write = singleton $ BufferedWrite tid cref new + let buffer' = I.insertWith (><) i write wb + + -- Write the thread-local value to the @CRef@'s update map. + (map, count, def) <- readRef fixed ref + writeRef fixed ref (M.insert tid new map, count, def) + + return $ WriteBuffer buffer' + +-- | Commit the write at the head of a buffer. +commitWrite :: Monad n => Fixed n r s -> WriteBuffer r -> Int -> n (WriteBuffer r) +commitWrite fixed w@(WriteBuffer wb) i = case maybe EmptyL viewl $ I.lookup i wb of + BufferedWrite _ cref a :< rest -> do + writeImmediate fixed cref a + return . WriteBuffer $ I.insert i rest wb + + EmptyL -> return w + +-- | Read from a @CRef@, returning a newer thread-local non-committed +-- write if there is one. +readCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n a +readCRef fixed cref tid = do + (val, _) <- readCRefPrim fixed cref tid + return val + +-- | Read from a @CRef@, returning a @Ticket@ representing the current +-- view of the thread. +readForTicket :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (Ticket a) +readForTicket fixed cref@(CRef (crid, _)) tid = do + (val, count) <- readCRefPrim fixed cref tid + return $ Ticket (crid, count, val) + +-- | Perform a compare-and-swap on a @CRef@ if the ticket is still +-- valid. This is strict in the \"new\" value argument. +casCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a) +casCRef fixed cref tid (Ticket (_, cc, _)) !new = do + tick'@(Ticket (_, cc', _)) <- readForTicket fixed cref tid + + if cc == cc' + then do + writeImmediate fixed cref new + tick'' <- readForTicket fixed cref tid + return (True, tick'') + else return (False, tick') + +-- | Read the local state of a @CRef@. +readCRefPrim :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (a, Integer) +readCRefPrim fixed (CRef (_, ref)) tid = do + (vals, count, def) <- readRef fixed ref + + return (M.findWithDefault def tid vals, count) + +-- | Write and commit to a @CRef@ immediately, clearing the update map +-- and incrementing the write count. +writeImmediate :: Monad n => Fixed n r s -> CRef r a -> a -> n () +writeImmediate fixed (CRef (_, ref)) a = do + (_, count, _) <- readRef fixed ref + writeRef fixed ref (M.empty, count + 1, a) + +-- | Flush all writes in the buffer. +writeBarrier :: Monad n => Fixed n r s -> WriteBuffer r -> n () +writeBarrier fixed (WriteBuffer wb) = mapM_ flush $ I.elems wb where + flush = mapM_ $ \(BufferedWrite _ cref a) -> writeImmediate fixed cref a + +-- | Add phantom threads to the thread list to commit pending writes. +addCommitThreads :: WriteBuffer r -> Threads n r s -> Threads n r s +addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where + phantoms = [(ThreadId $ negate k - 1, mkthread $ fromJust c) | (k, b) <- I.toList wb, let c = go $ viewl b, isJust c] + go (BufferedWrite tid (CRef (crid, _)) _ :< _) = Just $ ACommit tid crid + go EmptyL = Nothing + +-- | Remove phantom threads. +delCommitThreads :: Threads n r s -> Threads n r s +delCommitThreads = M.filterWithKey $ \k _ -> k >= 0 + +-------------------------------------------------------------------------------- +-- * Manipulating @CVar@s + +-- | Put into a @CVar@, blocking if full. +putIntoCVar :: Monad n => CVar r a -> a -> Action n r s + -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId]) +putIntoCVar cvar a c = mutCVar True cvar a (const c) + +-- | Try to put into a @CVar@, not blocking if full. +tryPutIntoCVar :: Monad n => CVar r a -> a -> (Bool -> Action n r s) + -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId]) +tryPutIntoCVar = mutCVar False + +-- | Read from a @CVar@, blocking if empty. +readFromCVar :: Monad n => CVar r a -> (a -> Action n r s) + -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId]) +readFromCVar cvar c = seeCVar False True cvar (c . fromJust) + +-- | Take from a @CVar@, blocking if empty. +takeFromCVar :: Monad n => CVar r a -> (a -> Action n r s) + -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId]) +takeFromCVar cvar c = seeCVar True True cvar (c . fromJust) + +-- | Try to take from a @CVar@, not blocking if empty. +tryTakeFromCVar :: Monad n => CVar r a -> (Maybe a -> Action n r s) + -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId]) +tryTakeFromCVar = seeCVar True False + +-- | Mutate a @CVar@, in either a blocking or nonblocking way. +mutCVar :: Monad n + => Bool -> CVar r a -> a -> (Bool -> Action n r s) + -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId]) +mutCVar blocking (CVar (cvid, ref)) a c fixed threadid threads = do + 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) + +-- | Read a @CVar@, in either a blocking or nonblocking +-- way. +seeCVar :: Monad n + => Bool -> Bool -> CVar r a -> (Maybe a -> Action n r s) + -> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId]) +seeCVar emptying blocking (CVar (cvid, ref)) c fixed threadid threads = do + 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/Threading.hs b/Test/DejaFu/Deterministic/Internal/Threading.hs --- a/Test/DejaFu/Deterministic/Internal/Threading.hs +++ b/Test/DejaFu/Deterministic/Internal/Threading.hs @@ -5,15 +5,14 @@ -- | 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 Control.Exception (Exception, MaskingState(..), SomeException, fromException) import Data.List (intersect, nub) -import Data.Map (Map) +import Data.Map.Strict (Map) import Data.Maybe (fromMaybe, isJust, isNothing) import Test.DejaFu.STM (CTVarId) import Test.DejaFu.Deterministic.Internal.Common -import qualified Data.Map as M +import qualified Data.Map.Strict as M #if __GLASGOW_HASKELL__ < 710 import Control.Applicative ((<$>)) @@ -43,6 +42,10 @@ -- detection of nonglobal deadlock. } +-- | Construct a thread with just one action +mkthread :: Action n r s -> Thread n r s +mkthread c = Thread c Nothing [] Unmasked [] False + -------------------------------------------------------------------------------- -- * Blocking @@ -92,7 +95,7 @@ -- thread under consideration. check lookingfor thetid thethread | thetid == tid = False - | otherwise = (not . null $ lookingfor `intersect` _known thethread) && isNothing (_blocking thethread) + | otherwise = (not . null $ lookingfor `intersect` _known thethread) && isNothing (_blocking thethread) -------------------------------------------------------------------------------- -- * Exceptions @@ -102,15 +105,35 @@ -- | 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 +propagate :: SomeException -> ThreadId -> Threads n r s -> Maybe (Threads n r s) +propagate e tid threads = case M.lookup tid threads >>= go . _handlers of + Just (act, hs) -> Just $ except act hs tid threads + Nothing -> Nothing + where + go [] = Nothing + go (Handler h:hs) = maybe (go hs) (\act -> Just (act, hs)) $ h <$> fromException e + -- | Check if a thread can be interrupted by an exception. interruptible :: Thread n r s -> Bool interruptible thread = _masking thread == Unmasked || (_masking thread == MaskedInterruptible && isJust (_blocking thread)) +-- | Register a new exception handler. +catching :: Exception e => (e -> Action n r s) -> ThreadId -> Threads n r s -> Threads n r s +catching h = M.alter $ \(Just thread) -> Just $ thread { _handlers = Handler h : _handlers thread } + +-- | Remove the most recent exception handler. +uncatching :: ThreadId -> Threads n r s -> Threads n r s +uncatching = M.alter $ \(Just thread) -> Just $ thread { _handlers = tail $ _handlers thread } + +-- | Raise an exception in a thread. +except :: Action n r s -> [Handler n r s] -> ThreadId -> Threads n r s -> Threads n r s +except act hs = M.alter $ \(Just thread) -> Just $ thread { _continuation = act, _handlers = hs, _blocking = Nothing } + +-- | Set the masking state of a thread. +mask :: MaskingState -> ThreadId -> Threads n r s -> Threads n r s +mask ms = M.alter $ \(Just thread) -> Just $ thread { _masking = ms } + -------------------------------------------------------------------------------- -- * Manipulating threads @@ -146,7 +169,7 @@ -- 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 +wake blockedOn threads = (unblock <$> threads, M.keys $ M.filter isBlocked threads) where unblock thread | isBlocked thread = thread { _blocking = Nothing } | otherwise = thread diff --git a/Test/DejaFu/Deterministic/Schedule.hs b/Test/DejaFu/Deterministic/Schedule.hs --- a/Test/DejaFu/Deterministic/Schedule.hs +++ b/Test/DejaFu/Deterministic/Schedule.hs @@ -21,7 +21,7 @@ -- | 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 +randomSched g _ _ threads = (Just $ threads' !! choice, g') where (choice, g') = randomR (0, length threads' - 1) g threads' = map fst $ toList threads @@ -34,10 +34,10 @@ -- | 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', ()) +roundRobinSched _ _ Nothing _ = (Just 0, ()) +roundRobinSched _ _ (Just (prior, _)) threads + | prior >= maximum threads' = (Just $ minimum threads', ()) + | otherwise = (Just . minimum $ filter (>prior) threads', ()) where threads' = map fst $ toList threads @@ -51,7 +51,7 @@ -- 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 + newsched s trc p@(Just (prior, _)) threads + | prior `elem` map fst (toList threads) = (Just prior, s) + | otherwise = sched s trc p threads + newsched s trc Nothing threads = sched s trc Nothing threads diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -1,5 +1,6 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE RankNTypes #-} -- | Systematic testing for concurrent computations. module Test.DejaFu.SCT @@ -24,11 +25,33 @@ -- K. McKinley for more details. BacktrackStep(..) + , BoundFunc + , sctBounded , sctBoundedIO - -- * Pre-emption Bounding + -- * Combination Bounds + -- | Combination schedule bounding, where individual bounds are + -- enabled if they are set. + -- + -- * Pre-emption + fair bounding is useful for programs which use + -- loop/yield control flows but are otherwise terminating. + -- + -- * Pre-emption, fair + length bounding is useful for + -- non-terminating programs, and used by the testing functionality + -- in @Test.DejaFu@. + + , Bounds(..) + , defaultBounds + + , sctBound + , sctBoundIO + + -- * Individual Bounds + + -- ** 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 @@ -36,58 +59,168 @@ -- -- See the BPOR paper for more details. + , PreemptionBound(..) + , defaultPreemptionBound , sctPreBound , sctPreBoundIO + -- ** Fair Bounding + + -- | BPOR using fair bounding. This bounds the maximum difference + -- between the number of yield operations different threads have + -- performed. + -- + -- See the BPOR paper for more details. + + , FairBound(..) + , defaultFairBound + , sctFairBound + , sctFairBoundIO + + -- ** Length Bounding + + -- | BPOR using length bounding. This bounds the maximum length (in + -- terms of primitive actions) of an execution. + + , LengthBound(..) + , defaultLengthBound + , sctLengthBound + , sctLengthBoundIO + -- * Utilities + , (&+&) + , trueBound , tidOf , decisionOf , activeTid , preEmpCount + , preEmpCount' + , yieldCount + , maxYieldCountDiff + , initialise , initialCVState , updateCVState , willBlock , willBlockSafely ) where -import Control.DeepSeq (force) +import Control.DeepSeq (NFData, force) import Data.Functor.Identity (Identity(..), runIdentity) -import Data.IntMap.Strict (IntMap) +import Data.List (nub, partition) import Data.Sequence (Seq, (|>)) -import Data.Maybe (maybeToList, isNothing) +import Data.Map (Map) +import Data.Maybe (isNothing, isJust, fromJust) import Test.DejaFu.Deterministic -import Test.DejaFu.Deterministic.IO (ConcIO, runConcIO') +import Test.DejaFu.Deterministic.Internal (willRelease) import Test.DejaFu.SCT.Internal -import qualified Data.IntMap.Strict as I -import qualified Data.Set as S +import qualified Data.Map.Strict as M import qualified Data.Sequence as Sq +import qualified Data.Set as S #if __GLASGOW_HASKELL__ < 710 import Control.Applicative ((<$>), (<*>)) #endif +-- | A bounding function takes the scheduling decisions so far and a +-- decision chosen to come next, and returns if that decision is +-- within the bound. +type BoundFunc = [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool + +-- | Combine two bounds into a larger bound, where both must be +-- satisfied. +(&+&) :: BoundFunc -> BoundFunc -> BoundFunc +(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl + +-- | The \"true\" bound, which allows everything. +trueBound :: BoundFunc +trueBound _ _ = True + +-- * Combined Bounds + +data Bounds = Bounds + { preemptionBound :: Maybe PreemptionBound + , fairBound :: Maybe FairBound + , lengthBound :: Maybe LengthBound + } + +-- | All bounds enabled, using their default values. +defaultBounds :: Bounds +defaultBounds = Bounds + { preemptionBound = Just defaultPreemptionBound + , fairBound = Just defaultFairBound + , lengthBound = Just defaultLengthBound + } + +-- | An SCT runner using a bounded scheduler +sctBound :: MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> Bounds + -- ^ The combined bounds. + -> (forall t. ConcST t a) + -- ^ The computation to run many times + -> [(Either Failure a, Trace)] +sctBound memtype cb = sctBounded memtype (cBound cb) (cBacktrack cb) + +-- | Variant of 'sctBound' for computations which do 'IO'. +sctBoundIO :: MemType -> Bounds -> ConcIO a -> IO [(Either Failure a, Trace)] +sctBoundIO memtype cb = sctBoundedIO memtype (cBound cb) (cBacktrack cb) + +-- | Combination bound function +cBound :: Bounds -> BoundFunc +cBound (Bounds pb fb lb) = maybe trueBound pbBound pb &+& maybe trueBound fBound fb &+& maybe trueBound lBound lb + +-- | Combination backtracking function. Add all backtracking points +-- corresponding to enabled bound functions. +cBacktrack :: Bounds -> [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep] +cBacktrack (Bounds pb fb lb) bs i t = lBack . fBack $ pBack bs where + pBack backs = if isJust pb then pbBacktrack backs i t else backs + fBack backs = if isJust fb then fBacktrack backs i t else backs + lBack backs = if isJust lb then lBacktrack backs i t else backs + -- * Pre-emption bounding +newtype PreemptionBound = PreemptionBound Int + deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show) + +-- | A sensible default pre-emption bound: 2 +defaultPreemptionBound :: PreemptionBound +defaultPreemptionBound = 2 + -- | An SCT runner using a pre-emption bounding scheduler. -sctPreBound :: - Int +sctPreBound :: MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> PreemptionBound -- ^ The maximum number of pre-emptions to allow in a single -- execution - -> (forall t. Conc t a) + -> (forall t. ConcST t a) -- ^ The computation to run many times -> [(Either Failure a, Trace)] -sctPreBound pb = sctBounded (pbBv pb) pbBacktrack pbInitialise +sctPreBound memtype pb = sctBounded memtype (pbBound pb) pbBacktrack -- | 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 +sctPreBoundIO :: MemType -> PreemptionBound -> ConcIO a -> IO [(Either Failure a, Trace)] +sctPreBoundIO memtype pb = sctBoundedIO memtype (pbBound pb) pbBacktrack --- | Check if a schedule is in the bound. -pbBv :: Int -> [Decision] -> Bool -pbBv pb ds = preEmpCount ds <= pb +-- | Pre-emption bound function +pbBound :: PreemptionBound -> BoundFunc +pbBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb +-- | Count the number of pre-emptions in a schedule prefix. +preEmpCount :: [(Decision, ThreadAction)] -> (Decision, a) -> Int +preEmpCount ts (d, _) = go Nothing ts where + go p ((d, a):rest) = preEmpC p d + go (Just a) rest + go p [] = preEmpC p d + + preEmpC (Just Yield) (SwitchTo _) = 0 + preEmpC _ (SwitchTo t) = if t >= 0 then 1 else 0 + preEmpC _ _ = 0 + +-- | Count the number of pre-emptions in an entire trace +preEmpCount' :: Trace -> Int +preEmpCount' trc = preEmpCount (map (\(d,_,a) -> (d, a)) trc) (Continue, WillStop) + -- | 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 @@ -97,39 +230,146 @@ -- 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' + | _threadid b1 /= _threadid b2 && not (commit b1) && not (commit b2) = Just j' | otherwise = goJ rest goJ [] = Nothing {-# INLINE pairs #-} pairs = zip <*> tail + commit b = case _decision b of + (_, CommitRef _ _) -> True + _ -> False + -- Add a backtracking point. If the thread isn't runnable, add all -- runnable threads. backtrack c bx@(b:rest) 0 t -- If the backtracking point is already present, don't re-add it, -- UNLESS this would force it to backtrack (it's conservative) -- where before it might not. - | t `S.member` _runnable b = - let val = I.lookup t $ _backtrack b + | t `M.member` _runnable b = + let val = M.lookup t $ _backtrack b in if isNothing val || (val == Just False && c) - then b { _backtrack = I.insert t c $ _backtrack b } : rest + then b { _backtrack = M.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 + | otherwise = b { _backtrack = M.fromList [ (t',c) | t' <- M.keys $ _runnable b ] } : rest backtrack c (b:rest) n t = b : backtrack c rest (n-1) t backtrack _ [] _ _ = error "Ran out of schedule whilst backtracking!" --- | 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 +-- * Fair bounding +newtype FairBound = FairBound Int + deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show) + +-- | A sensible default fair bound: 5 +defaultFairBound :: FairBound +defaultFairBound = 5 + +-- | An SCT runner using a fair bounding scheduler. +sctFairBound :: MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> FairBound + -- ^ The maximum difference between the number of yield operations + -- performed by different threads. + -> (forall t. ConcST t a) + -- ^ The computation to run many times + -> [(Either Failure a, Trace)] +sctFairBound memtype fb = sctBounded memtype (fBound fb) fBacktrack + +-- | Variant of 'sctFairBound' for computations which do 'IO'. +sctFairBoundIO :: MemType -> FairBound -> ConcIO a -> IO [(Either Failure a, Trace)] +sctFairBoundIO memtype fb = sctBoundedIO memtype (fBound fb) fBacktrack + +-- | Fair bound function +fBound :: FairBound -> BoundFunc +fBound (FairBound fb) ts dl = maxYieldCountDiff ts dl <= fb + +-- | Count the number of yields by a thread in a schedule prefix. +yieldCount :: ThreadId -> [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Int +yieldCount tid ts (_, l) = go 0 ts where + go t ((Start t', Yield):rest) = (if t == tid then 1 else 0) + go t' rest + go t ((SwitchTo t', Yield):rest) = (if t == tid then 1 else 0) + go t' rest + go t ((Continue, Yield):rest) = (if t == tid then 1 else 0) + go t rest + go _ ((Start t', _):rest) = go t' rest + go _ ((SwitchTo t', _):rest) = go t' rest + go t ((Continue, _):rest) = go t rest + go t (_:rest) = go t rest + go t [] = if l == WillYield && t == tid then 1 else 0 + +-- | Get the maximum difference between the yield counts of all +-- threads in this schedule prefix. +maxYieldCountDiff :: [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Int +maxYieldCountDiff ts dl = maximum yieldCountDiffs where + yieldCounts = [yieldCount tid ts dl | tid <- nub $ allTids ts] + yieldCountDiffs = [y1 - y2 | y1 <- yieldCounts, y2 <- yieldCounts] + + allTids ((_, Fork tid):rest) = tid : allTids rest + allTids (_:rest) = allTids rest + allTids [] = [0] + +-- | Add a backtrack point. If the thread isn't runnable, or performs +-- a release operation, add all runnable threads. +fBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep] +fBacktrack bx@(b:rest) 0 t + -- If the backtracking point is already present, don't re-add it, + -- UNLESS this would force it to backtrack (it's conservative) where + -- before it might not. + | Just False == (willRelease <$> M.lookup t (_runnable b)) = + let val = M.lookup t $ _backtrack b + in if isNothing val + then b { _backtrack = M.insert t False $ _backtrack b } : rest + else bx + + -- Otherwise just backtrack to everything runnable. + | otherwise = b { _backtrack = M.fromList [ (t',False) | t' <- M.keys $ _runnable b ] } : rest + +fBacktrack (b:rest) n t = b : fBacktrack rest (n-1) t +fBacktrack [] _ _ = error "Ran out of schedule whilst backtracking!" + +-- * Length Bounding + +newtype LengthBound = LengthBound Int + deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show) + +-- | A sensible default length bound: 250 +defaultLengthBound :: LengthBound +defaultLengthBound = 250 + +-- | An SCT runner using a length bounding scheduler. +sctLengthBound :: MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> LengthBound + -- ^ The maximum length of a schedule, in terms of primitive + -- actions. + -> (forall t. ConcST t a) + -- ^ The computation to run many times + -> [(Either Failure a, Trace)] +sctLengthBound memtype lb = sctBounded memtype (lBound lb) lBacktrack + +-- | Variant of 'sctFairBound' for computations which do 'IO'. +sctLengthBoundIO :: MemType -> LengthBound -> ConcIO a -> IO [(Either Failure a, Trace)] +sctLengthBoundIO memtype lb = sctBoundedIO memtype (lBound lb) lBacktrack + +-- | Length bound function +lBound :: LengthBound -> BoundFunc +lBound (LengthBound lb) ts _ = length ts < lb + +-- | Add a backtrack point. If the thread isn't runnable, add all +-- runnable threads. +lBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep] +lBacktrack bx@(b:rest) 0 t + | t `M.member` _runnable b = + let val = M.lookup t $ _backtrack b + in if isNothing val + then b { _backtrack = M.insert t False $ _backtrack b } : rest + else bx + | otherwise = b { _backtrack = M.fromList [ (t',False) | t' <- M.keys $ _runnable b ] } : rest +lBacktrack (b:rest) n t = b : lBacktrack rest (n-1) t +lBacktrack [] _ _ = error "Ran out of schedule whilst backtracking!" + -- * BPOR -- | SCT via BPOR. @@ -144,46 +384,45 @@ -- 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 +sctBounded :: MemType + -- ^ The memory model to use for non-synchronised @CRef@ operations. + -> BoundFunc + -- ^ 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. + -> (forall t. ConcST t a) -> [(Either Failure a, Trace)] +sctBounded memtype bf backtrack c = runIdentity $ sctBoundedM memtype bf backtrack run where + run memty sched s = Identity $ runConcST' sched memty s c -- | Variant of 'sctBounded' for computations which do 'IO'. -sctBoundedIO :: ([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 +sctBoundedIO :: MemType -> BoundFunc + -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) + -> ConcIO a -> IO [(Either Failure a, Trace)] +sctBoundedIO memtype bf backtrack c = sctBoundedM memtype bf backtrack run where + run memty sched s = runConcIO' sched memty 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 + => MemType + -> ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool) + -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) + -> (MemType -> Scheduler SchedState -> SchedState -> m (Either Failure a, SchedState, Trace')) + -- ^ Monadic runner, with computation fixed. + -> m [(Either Failure a, Trace)] +sctBoundedM memtype bf backtrack run = go initialState where go bpor = case next bpor of - Just (sched, conservative, bpor') -> do - (res, s, trace) <- run (bporSched initialise) (initialSchedState sched) + Just (sched, conservative, sleep) -> do + (res, s, trace) <- run memtype (bporSched memtype $ initialise bf) (initialSchedState sleep sched) - let bpoints = findBacktrack backtrack (_sbpoints s) trace - let bpor'' = grow conservative trace bpor' - let bpor''' = todo bv bpoints bpor'' + let bpoints = findBacktrack memtype backtrack (_sbpoints s) trace + let newBPOR = grow memtype conservative trace bpor - ((res, toTrace trace):) <$> go bpor''' + if _signore s + then go newBPOR + else ((res, toTrace trace):) <$> go (pruneCommits $ todo bf bpoints newBPOR) Nothing -> return [] @@ -191,49 +430,85 @@ -- | The scheduler state data SchedState = SchedState - { _sprefix :: [ThreadId] + { _ssleep :: Map ThreadId ThreadAction + -- ^ The sleep set: decisions not to make until something dependent + -- with them happens. + , _sprefix :: [ThreadId] -- ^ Decisions still to make , _sbpoints :: Seq (NonEmpty (ThreadId, Lookahead), [ThreadId]) -- ^ Which threads are runnable at each step, and the alternative -- decisions still to make. - , _scvstate :: IntMap Bool - -- ^ The 'CVar' block state. - } + , _signore :: Bool + -- ^ Whether to ignore this execution or not: @True@ if the + -- execution is aborted due to all possible decisions being in the + -- sleep set, as then everything in this execution is covered by + -- another. + } deriving Show -- | Initial scheduler state for a given prefix -initialSchedState :: [ThreadId] -> SchedState -initialSchedState prefix = SchedState - { _sprefix = prefix +initialSchedState :: Map ThreadId ThreadAction -> [ThreadId] -> SchedState +initialSchedState sleep prefix = SchedState + { _ssleep = sleep + , _sprefix = prefix , _sbpoints = Sq.empty - , _scvstate = initialCVState + , _signore = False } -- | 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 +bporSched :: MemType + -> ([(Decision, ThreadAction)] -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> [ThreadId]) + -> Scheduler SchedState +bporSched memtype init = force $ \s trc prior threads -> case _sprefix s of -- If there is a decision available, make it (d:ds) -> let threads' = fmap (\(t,a:|_) -> (t,a)) threads - cvstate' = maybe (_scvstate s) (updateCVState (_scvstate s) . snd) prior - in (d, s { _sprefix = ds, _sbpoints = _sbpoints s |> (threads', []), _scvstate = cvstate' }) + in (Just d, s { _sprefix = ds, _sbpoints = _sbpoints s |> (threads', []) }) -- Otherwise query the initialise function for a list of possible - -- choices, and make one of them arbitrarily (recording the others). + -- choices, filter out anything in the sleep set, and make one of + -- them arbitrarily (recording the others). [] -> let threads' = fmap (\(t,a:|_) -> (t,a)) threads - choices = 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 - ] + choices = init trc prior threads' + checkDep t a = case prior of + Just (tid, act) -> dependent memtype unknownCRState (tid, act) (t, a) + Nothing -> False + ssleep' = M.filterWithKey (\t a -> not $ checkDep t a) $ _ssleep s + choices' = filter (`notElem` M.keys ssleep') choices + signore' = not (null choices) && all (`elem` M.keys ssleep') choices in case choices' of - (nextTid:rest) -> (nextTid, s { _sbpoints = _sbpoints s |> (threads', rest), _scvstate = cvstate' }) + (nextTid:rest) -> (Just nextTid, s { _sbpoints = _sbpoints s |> (threads', rest), _ssleep = ssleep' }) + [] -> (Nothing, s { _sbpoints = _sbpoints s |> (threads', []), _signore = signore' }) - -- TODO: abort the execution here. - [] -> case choices of - (nextTid:|_) -> (nextTid, s { _sbpoints = _sbpoints s |> (threads', []), _scvstate = cvstate' }) +-- | Pick a new thread to run, which does not exceed the bound. Choose +-- the current thread if available and it hasn't just yielded, +-- otherwise add all runnable threads. +initialise :: BoundFunc + -> [(Decision, ThreadAction)] + -> Maybe (ThreadId, ThreadAction) + -> NonEmpty (ThreadId, Lookahead) + -> [ThreadId] +initialise bf trc prior threads = restrictToBound . yieldsToEnd $ case prior of + Just (_, Yield) -> map fst threads' + Just (tid, _) + | any (\(t, _) -> t == tid) threads' -> [tid] + _ -> map fst threads' + + where + -- Restrict the possible decisions to those in the bound. + restrictToBound = fst . partition (\t -> bf trc (decision t, action t)) + + -- Move the threads which will immediately yield to the end of the list + yieldsToEnd ts = case partition ((== WillYield) . action) ts of + (willYield, noYield) -> noYield ++ willYield + + -- Get the decision that will lead to a thread being scheduled. + decision = decisionOf (fst <$> prior) (S.fromList $ map fst threads') + + -- Get the action of a thread + action t = fromJust $ lookup t threads' + + -- The list of threads + threads' = toList threads diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs --- a/Test/DejaFu/SCT/Internal.hs +++ b/Test/DejaFu/SCT/Internal.hs @@ -4,15 +4,16 @@ 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.List (foldl', partition, sortBy, intercalate) +import Data.Map.Strict (Map) +import Data.Maybe (mapMaybe, isJust, fromJust, listToMaybe) +import Data.Ord (Down(..), comparing) import Data.Sequence (Seq, ViewL(..)) import Data.Set (Set) -import Test.DejaFu.Deterministic +import Test.DejaFu.Deterministic.Internal +import Test.DejaFu.Deterministic.Schedule -import qualified Data.IntMap.Strict as I +import qualified Data.Map.Strict as M import qualified Data.Sequence as Sq import qualified Data.Set as S @@ -30,9 +31,9 @@ -- ^ The thread running at this step , _decision :: (Decision, ThreadAction) -- ^ What happened at this step. - , _runnable :: Set ThreadId + , _runnable :: Map ThreadId Lookahead -- ^ The threads runnable at this step - , _backtrack :: IntMap Bool + , _backtrack :: Map ThreadId Bool -- ^ The list of alternative threads to run, and whether those -- alternatives were added conservatively due to the bound. } deriving (Eq, Show) @@ -45,7 +46,7 @@ data BPOR = BPOR { _brunnable :: Set ThreadId -- ^ What threads are runnable at this step. - , _btodo :: IntMap Bool + , _btodo :: Map ThreadId Bool -- ^ Follow-on decisions still to make, and whether that decision -- was added conservatively due to the bound. , _bignore :: Set ThreadId @@ -53,82 +54,139 @@ -- the chosen thread immediately blocking without achieving -- anything, which can't have any effect on the result of the -- program. - , _bdone :: IntMap BPOR + , _bdone :: Map ThreadId BPOR -- ^ Follow-on decisions that have been made. - , _bsleep :: IntMap ThreadAction + , _bsleep :: Map ThreadId ThreadAction -- ^ Transitions to ignore (in this node and children) until a -- dependent transition happens. - , _btaken :: IntMap ThreadAction + , _btaken :: Map ThreadId 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. + -- conservatively-added ones. This is used in implementing sleep + -- sets. + , _baction :: Maybe ThreadAction + -- ^ What happened at this step. This will be 'Nothing' at the root, + -- 'Just' everywhere else. } +-- | Render a 'BPOR' value as a graph in GraphViz \"dot\" format. +toDot :: BPOR -> String +toDot bpor = "digraph {\n" ++ go "L" bpor ++ "\n}" where + go l b = unlines $ node l b : [edge l l' i ++ go l' b' | (i, b') <- M.toList (_bdone b), let l' = l ++ show' i] + + -- Display a labelled node. + node n b = n ++ " [label=\"" ++ label b ++ "\"]" + + -- A node label, summary of the BPOR state at that node. + label b = intercalate "," + [ show $ _baction b + , "Run:" ++ show (S.toList $ _brunnable b) + , "Tod:" ++ show (M.keys $ _btodo b) + , "Ign:" ++ show (S.toList $ _bignore b) + , "Slp:" ++ show (M.toList $ _bsleep b) + ] + + -- Display a labelled edge + edge n1 n2 l = n1 ++ "-> " ++ n2 ++ " [label=\"" ++ show l ++ "\"]\n" + + -- Show a number, replacing a minus sign for \"N\". + show' i = if i < 0 then "N" ++ show (negate i) else show i + +-- | Variant of 'toDot' which doesn't include aborted subtrees. +toDotSmall :: BPOR -> String +toDotSmall bpor = "digraph {\n" ++ go "L" bpor ++ "\n}" where + go l b = unlines $ node l b : [edge l l' i ++ go l' b' | (i, b') <- M.toList (_bdone b), check b', let l' = l ++ show' i] + + -- Check that a subtree has at least one non-aborted branch. + check b = S.null (_brunnable b) || any check (M.elems $ _bdone b) + + -- Display a labelled node. + node n b = n ++ " [label=\"" ++ label b ++ "\"]" + + -- A node label, summary of the BPOR state at that node. + label b = intercalate "," + [ show $ _baction b + , "Run:" ++ show (S.toList $ _brunnable b) + , "Tod:" ++ show (M.keys $ _btodo b) + , "Ign:" ++ show (S.toList $ _bignore b) + , "Slp:" ++ show (M.toList $ _bsleep b) + ] + + -- Display a labelled edge + edge n1 n2 l = n1 ++ "-> " ++ n2 ++ " [label=\"" ++ show l ++ "\"]\n" + + -- Show a number, replacing a minus sign for \"N\". + show' i = if i < 0 then "N" ++ show (negate i) else show i + -- | Initial BPOR state. initialState :: BPOR initialState = BPOR - { _brunnable = S.singleton 0 - , _btodo = I.singleton 0 False + { _brunnable = S.singleton (ThreadId 0) + , _btodo = M.singleton (ThreadId 0) False , _bignore = S.empty - , _bdone = I.empty - , _bsleep = I.empty - , _btaken = I.empty + , _bdone = M.empty + , _bsleep = M.empty + , _btaken = M.empty + , _baction = Nothing } -- | Produce a new schedule from a BPOR tree. If there are no new -- schedules remaining, return 'Nothing'. Also returns whether the --- decision made was added conservatively. +-- decision was added conservatively, and the sleep set at the point +-- where divergence happens. -- -- This returns the longest prefix, on the assumption that this will -- lead to lots of backtracking points being identified before -- higher-up decisions are reconsidered, so enlarging the sleep sets. -next :: BPOR -> Maybe ([ThreadId], Bool, BPOR) +next :: BPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction) next = go 0 where go tid bpor = -- All the possible prefix traces from this point, with -- updated BPOR subtrees if taken from the done list. - let prefixes = mapMaybe go' (I.toList $ _bdone bpor) ++ [Left t | t <- I.toList $ _btodo bpor] + let prefixes = mapMaybe go' (M.toList $ _bdone bpor) ++ [([t], c, sleeps bpor) | (t, c) <- M.toList $ _btodo bpor] -- Sort by number of preemptions, in descending order. - cmp = comparing $ preEmps tid bpor . either (\(a,_) -> [a]) (\(a,_,_) -> a) + cmp = preEmps tid bpor . (\(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!" + else case partition (\(t:_,_,_) -> t < 0) $ sortBy (comparing $ Down . cmp) prefixes of + (commits, others) + | not $ null others -> listToMaybe others + | not $ null commits -> listToMaybe commits + | otherwise -> error "Invariant failure in 'next': empty prefix list!" - -- 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,slp) -> (tid:ts,c,slp)) <$> go tid bpor - go' (tid, bpor) = (\(ts,c,b) -> Right (tid:ts, c, b)) <$> go tid bpor + sleeps bpor = _bsleep bpor `M.union` _btaken 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 + let rest = preEmps t (fromJust . M.lookup t $ _bdone bpor) ts + in if t > 0 && tid /= t && tid `S.member` _brunnable bpor then 1 + rest else rest preEmps _ _ [] = 0::Int -- | Produce a list of new backtracking points from an execution -- trace. -findBacktrack :: ([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): ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) + -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId]) + -> Trace' + -> [BacktrackStep] +findBacktrack memtype backtrack = go initialCRState S.empty 0 [] . Sq.viewl where + go crstate allThreads tid bs ((e,i): (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 + crstate' = updateCRState crstate a + this = BacktrackStep + { _threadid = tid' + , _decision = (d, a) + , _runnable = M.fromList . toList $ e + , _backtrack = M.fromList $ map (\i' -> (i', False)) i + } + allThreads' = allThreads `S.union` S.fromList (M.keys $ _runnable this) + killsEarly = null ts && any (/=0) (M.keys $ _runnable this) + bs' = doBacktrack killsEarly crstate' allThreads' (toList e) (bs++[this]) + in go crstate' allThreads' tid' bs' (Sq.viewl is) ts + go _ _ _ bs _ _ = bs - doBacktrack allThreads enabledThreads bs = + doBacktrack killsEarly crstate allThreads enabledThreads bs = let tagged = reverse $ zip [0..] bs idxs = [ (head is, u) | (u, n) <- enabledThreads @@ -137,46 +195,50 @@ , let is = [ i | (i, b) <- tagged , _threadid b == v - , dependent' (snd $ _decision b) (u, n) + , killsEarly || dependent' memtype crstate (_threadid b, snd $ _decision b) (u, n) ] , not $ null is] :: [(Int, ThreadId)] in foldl' (\b (i, u) -> backtrack b i u) bs idxs -- | Add a new trace to the tree, creating a new subtree. -grow :: Bool -> Trace' -> BPOR -> BPOR -grow conservative = grow' initialCVState 0 where - grow' cvstate tid trc@((d, _, a):rest) bpor = +grow :: MemType -> Bool -> Trace' -> BPOR -> BPOR +grow memtype conservative = grow' initialCVState initialCRState 0 where + grow' cvstate crstate tid trc@((d, _, a):rest) bpor = let tid' = tidOf tid d cvstate' = updateCVState cvstate a - 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 + crstate' = updateCRState crstate a + in case M.lookup tid' $ _bdone bpor of + Just bpor' -> bpor { _bdone = M.insert tid' (grow' cvstate' crstate' tid' rest bpor') $ _bdone bpor } + Nothing -> bpor { _btaken = if conservative then _btaken bpor else M.insert tid' a $ _btaken bpor + , _btodo = M.delete tid' $ _btodo bpor + , _bdone = M.insert tid' (subtree cvstate' crstate' tid' (_bsleep bpor `M.union` _btaken bpor) trc) $ _bdone bpor } + grow' _ _ _ [] bpor = bpor - subtree cvstate tid sleep ((d, ts, a):rest) = + subtree cvstate crstate tid sleep ((d, ts, a):rest) = let cvstate' = updateCVState cvstate a - sleep' = I.filterWithKey (\t a' -> not $ dependent a (t,a')) sleep + crstate' = updateCRState crstate a + sleep' = M.filterWithKey (\t a' -> not $ dependent memtype crstate' (tid, a) (t,a')) sleep in BPOR { _brunnable = S.fromList $ tids tid d a ts - , _btodo = I.empty + , _btodo = M.empty , _bignore = S.fromList [tidOf tid d' | (d',as) <- ts, willBlockSafely cvstate' $ toList as] - , _bdone = I.fromList $ case rest of + , _bdone = M.fromList $ case rest of ((d', _, _):_) -> let tid' = tidOf tid d' - in [(tid', subtree cvstate' tid' sleep' rest)] + in [(tid', subtree cvstate' crstate' tid' sleep' rest)] [] -> [] , _bsleep = sleep' , _btaken = case rest of - ((d', _, a'):_) -> I.singleton (tidOf tid d') a' - [] -> I.empty + ((d', _, a'):_) -> M.singleton (tidOf tid d') a' + [] -> M.empty + , _baction = Just a } - subtree _ _ _ [] = error "Invariant failure in 'subtree': suffix 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 _ (BlockedPutVar _) ts = map (tidOf tid . fst) ts + tids tid _ (BlockedReadVar _) ts = map (tidOf tid . fst) ts + tids tid _ (BlockedTakeVar _) ts = map (tidOf tid . fst) ts tids tid _ BlockedSTM ts = map (tidOf tid . fst) ts tids tid _ (BlockedThrowTo _) ts = map (tidOf tid . fst) ts tids tid _ Stop ts = map (tidOf tid . fst) ts @@ -184,36 +246,57 @@ -- | 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 :: ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool) -> [BacktrackStep] -> BPOR -> BPOR todo bv = step where step bs bpor = let (bpor', bs') = go 0 [] Nothing bs bpor - in if all (I.null . _backtrack) bs' + in if all (M.null . _backtrack) bs' then bpor' else step bs' bpor' go tid pref lastb (b:bs) bpor = let (bpor', blocked) = backtrack pref b bpor tid' = tidOf tid . fst $ _decision b - (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' } + pref' = pref ++ [_decision b] + (child, blocked') = go tid' pref' (Just b) bs . fromJust $ M.lookup tid' (_bdone bpor) + bpor'' = bpor' { _bdone = M.insert tid' child $ _bdone bpor' } in case lastb of Just b' -> (bpor'', b' { _backtrack = blocked } : blocked') Nothing -> (bpor'', blocked') - go _ _ (Just b') _ bpor = (bpor, [b' { _backtrack = I.empty }]) + go _ _ (Just b') _ bpor = (bpor, [b' { _backtrack = M.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) + | x@(t,c) <- M.toList $ _backtrack b + , let decision = decisionOf (Just . activeTid $ map fst pref) (_brunnable bpor) t + , let lookahead = fromJust . M.lookup t $ _runnable b + , bv pref (decision, lookahead) + , t `notElem` M.keys (_bdone bpor) + , c || M.notMember t (_bsleep bpor) ] (blocked, nxt) = partition (\(t,_) -> t `S.member` _bignore bpor) todo' - in (bpor { _btodo = _btodo bpor `I.union` I.fromList nxt }, I.fromList blocked) + in (bpor { _btodo = _btodo bpor `M.union` M.fromList nxt }, M.fromList blocked) +-- | Remove commits from the todo sets where every other action will +-- result in a write barrier (and so a commit) occurring. +-- +-- To get the benefit from this, do not execute commit actions from +-- the todo set until there are no other choises. +pruneCommits :: BPOR -> BPOR +pruneCommits bpor + | not onlycommits || not alldonesync = go bpor + | otherwise = go bpor { _btodo = M.empty, _bdone = pruneCommits <$> _bdone bpor } + + where + go b = b { _bdone = pruneCommits <$> _bdone bpor } + + onlycommits = all (<0) . M.keys $ _btodo bpor + alldonesync = all barrier . M.elems $ _bdone bpor + + barrier = isBarrier . simplify . fromJust . _baction + -- * Utilities -- | Get the resultant 'ThreadId' of a 'Decision', with a default case @@ -221,7 +304,7 @@ tidOf :: ThreadId -> Decision -> ThreadId tidOf _ (Start t) = t tidOf _ (SwitchTo t) = t -tidOf tid Continue = tid +tidOf tid _ = tid -- | Get the 'Decision' that would have resulted in this 'ThreadId', -- given a prior 'ThreadId' (if any) and list of runnable threads. @@ -234,101 +317,121 @@ -- | 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 +activeTid = foldl' tidOf 0 --- | 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. +dependent :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool +dependent _ _ (_, Lift) (_, Lift) = True +dependent _ _ (_, ThrowTo t) (t2, a) = t == t2 && a /= Stop +dependent _ _ (t2, a) (_, ThrowTo t) = t == t2 && a /= Stop +dependent _ _ (_, STM _) (_, STM _) = True +dependent _ _ (_, GetNumCapabilities a) (_, SetNumCapabilities b) = a /= b +dependent _ _ (_, SetNumCapabilities a) (_, GetNumCapabilities b) = a /= b +dependent _ _ (_, SetNumCapabilities a) (_, SetNumCapabilities b) = a /= b +dependent memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify d2) --- | 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 +-- | Variant of 'dependent' to handle 'ThreadAction''s +dependent' :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, Lookahead) -> Bool +dependent' _ _ (_, Lift) (_, WillLift) = True +dependent' _ _ (_, ThrowTo t) (t2, a) = t == t2 && a /= WillStop +dependent' _ _ (t2, a) (_, WillThrowTo t) = t == t2 && a /= Stop +dependent' _ _ (_, STM _) (_, WillSTM) = True +dependent' _ _ (_, GetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b +dependent' _ _ (_, SetNumCapabilities a) (_, WillGetNumCapabilities) = True +dependent' _ _ (_, SetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b +dependent' memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify' d2) - 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 +-- | Check if two 'ActionType's are dependent. Note that this is not +-- sufficient to know if two 'ThreadAction's are dependent, without +-- being so great an over-approximation as to be useless! +dependentActions :: MemType -> CRState -> ActionType -> ActionType -> Bool +dependentActions memtype buf a1 a2 = case (a1, a2) of + -- Unsynchronised reads and writes are always dependent, even under + -- a relaxed memory model, as an unsynchronised write gives rise to + -- a commit, which synchronises. + (UnsynchronisedRead r1, UnsynchronisedWrite r2) -> r1 == r2 + (UnsynchronisedWrite r1, UnsynchronisedRead r2) -> r1 == r2 + (UnsynchronisedWrite r1, UnsynchronisedWrite r2) -> r1 == r2 - ctvar = ctvar' d1 && ctvar' d2 - ctvar' (STM _) = True - ctvar' _ = False + -- Unsynchronised reads where a memory barrier would flush a + -- buffered write + (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered buf r1 && memtype /= SequentialConsistency + (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered buf r2 && memtype /= SequentialConsistency --- | 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 + (_, _) + -- Two actions on the same CRef where at least one is synchronised + | same crefOf && (synchronises a1 (fromJust $ crefOf a1) || synchronises a2 (fromJust $ crefOf a2)) -> True + -- Two actions on the same CVar + | same cvarOf -> True - 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 + _ -> False - ctvar = ctvar' d1 && ctvar'' d2 - ctvar' (STM _) = True - ctvar' _ = False - ctvar'' WillSTM = True - ctvar'' _ = False + where + same f = isJust (f a1) && f a1 == f a2 -- * Keeping track of 'CVar' full/empty states +type CVState = Map CVarId Bool + -- | Initial global 'CVar' state -initialCVState :: IntMap Bool -initialCVState = I.empty +initialCVState :: CVState +initialCVState = M.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 -> ThreadAction -> CVState +updateCVState cvstate (PutVar c _) = M.insert c True cvstate +updateCVState cvstate (TakeVar c _) = M.insert c False cvstate +updateCVState cvstate (TryPutVar c True _) = M.insert c True cvstate +updateCVState cvstate (TryTakeVar c True _) = M.insert c False cvstate updateCVState cvstate _ = cvstate -- | Check if an action will block. -willBlock :: 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 :: CVState -> Lookahead -> Bool +willBlock cvstate (WillPutVar c) = M.lookup c cvstate == Just True +willBlock cvstate (WillTakeVar c) = M.lookup c cvstate == Just False +willBlock cvstate (WillReadVar c) = M.lookup c cvstate == Just False willBlock _ _ = False -- | Check if a list of actions will block safely (without modifying -- any global state). This allows further lookahead at, say, the -- 'spawn' of a thread (which always starts with 'KnowsAbout'). -willBlockSafely :: IntMap Bool -> [Lookahead] -> Bool +willBlockSafely :: CVState -> [Lookahead] -> Bool +willBlockSafely cvstate (WillMyThreadId:as) = willBlockSafely cvstate as +willBlockSafely cvstate (WillNewVar:as) = willBlockSafely cvstate as +willBlockSafely cvstate (WillNewRef:as) = willBlockSafely cvstate as +willBlockSafely cvstate (WillReturn:as) = willBlockSafely cvstate as willBlockSafely cvstate (WillKnowsAbout:as) = willBlockSafely cvstate as willBlockSafely cvstate (WillForgets:as) = willBlockSafely cvstate as willBlockSafely cvstate (WillAllKnown:as) = willBlockSafely cvstate as -willBlockSafely cvstate (WillPut c:_) = willBlock cvstate (WillPut c) -willBlockSafely cvstate (WillTake c:_) = willBlock cvstate (WillTake c) +willBlockSafely cvstate (WillPutVar c:_) = willBlock cvstate (WillPutVar c) +willBlockSafely cvstate (WillTakeVar c:_) = willBlock cvstate (WillTakeVar c) willBlockSafely _ _ = False + +-- * Keeping track of 'CRef' buffer state + +data CRState = Known (Map CRefId Bool) | Unknown + +-- | Initial global 'CRef buffer state. +initialCRState :: CRState +initialCRState = Known M.empty + +-- | 'CRef' buffer state with nothing known. +unknownCRState :: CRState +unknownCRState = Unknown + +-- | Update the 'CRef' buffer state with the action that has just +-- happened. +updateCRState :: CRState -> ThreadAction -> CRState +updateCRState Unknown _ = Unknown +updateCRState (Known crstate) (CommitRef _ r) = Known $ M.delete r crstate +updateCRState (Known crstate) (WriteRef r) = Known $ M.insert r True crstate +updateCRState crstate ta + | isBarrier $ simplify ta = initialCRState + | otherwise = crstate + +-- | Check if a 'CRef' has a buffered write pending. +-- +-- If the state is @Unknown@, this assumes @True@. +isBuffered :: CRState -> CRefId -> Bool +isBuffered Unknown _ = True +isBuffered (Known crstate) r = M.findWithDefault False r crstate diff --git a/Test/DejaFu/STM.hs b/Test/DejaFu/STM.hs --- a/Test/DejaFu/STM.hs +++ b/Test/DejaFu/STM.hs @@ -10,31 +10,18 @@ STMLike , STMST , STMIO + + -- * Executing Transactions , Result(..) - , runTransaction + , CTVarId , 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 Control.Monad.ST (ST) import Data.IORef (IORef) import Data.STRef (STRef) import Test.DejaFu.Internal @@ -48,97 +35,66 @@ {-# 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 +newtype STMLike n r a = S { runSTM :: M n r a } deriving (Functor, Applicative, Monad) -instance Monad n => C.MonadSTM (STMLike t n r) where - type CTVar (STMLike t n r) = CTVar t r +-- | Create a new STM continuation. +toSTM :: ((a -> STMAction n r) -> STMAction n r) -> STMLike n r a +toSTM = S . cont - retry = retry - orElse = orElse - newCTVar = newCTVar - readCTVar = readCTVar - writeCTVar = writeCTVar +-- | A 'MonadSTM' implementation using @ST@, it encapsulates a single +-- atomic transaction. The environment, that is, the collection of +-- defined 'CTVar's is implicit, there is no list of them, they exist +-- purely as references. This makes the types simpler, but means you +-- can't really get an aggregate of them (if you ever wanted to for +-- some reason). +type STMST t = STMLike (ST t) (STRef t) --- | 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 +-- | A 'MonadSTM' implementation using @ST@, it encapsulates a single +-- atomic transaction. The environment, that is, the collection of +-- defined 'CTVar's is implicit, there is no list of them, they exist +-- purely as references. This makes the types simpler, but means you +-- can't really get an aggregate of them (if you ever wanted to for +-- some reason). +type STMIO = STMLike IO IORef --- | 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) +instance MonadThrow (STMLike n r) where + throwM e = toSTM (\_ -> SThrow e) --- | Check whether a condition is true and, if not, call 'retry'. -check :: Monad n => Bool -> STMLike t n r () -check = C.check +instance MonadCatch (STMLike n r) where + catch stm handler = toSTM (SCatch (runSTM . handler) (runSTM stm)) --- | 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) +instance Monad n => C.MonadSTM (STMLike n r) where + type CTVar (STMLike n r) = CTVar r --- | 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) + retry = toSTM (\_ -> SRetry) --- | 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 + orElse a b = toSTM (SOrElse (runSTM a) (runSTM b)) --- | 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 + newCTVar a = toSTM (SNew a) --- | 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 () + readCTVar ctvar = toSTM (SRead ctvar) --- | 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 + writeCTVar ctvar a = toSTM (\c -> SWrite ctvar a (c ())) -- | Run a transaction in the 'ST' monad, returning the result and new -- initial 'CTVarId'. If the transaction ended by calling 'retry', any -- 'CTVar' modifications are undone. runTransactionST :: STMST t a -> CTVarId -> ST t (Result a, CTVarId) runTransactionST = runTransactionM fixedST where - fixedST = refST $ \mb -> cont (\c -> ALift $ c `liftM` mb) + fixedST = refST $ \mb -> cont (\c -> SLift $ c `liftM` mb) -- | Run a transaction in the 'IO' monad, returning the result and new -- initial 'CTVarId'. If the transaction ended by calling 'retry', any -- 'CTVar' modifications are undone. -runTransactionIO :: STMIO t a -> CTVarId -> IO (Result a, CTVarId) +runTransactionIO :: STMIO a -> CTVarId -> IO (Result a, CTVarId) runTransactionIO = runTransactionM fixedIO where - fixedIO = refIO $ \mb -> cont (\c -> ALift $ c `liftM` mb) + fixedIO = refIO $ \mb -> cont (\c -> SLift $ 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) + => Fixed n r -> STMLike n r a -> CTVarId -> n (Result a, CTVarId) runTransactionM ref ma ctvid = do - (res, undo, ctvid') <- doTransaction ref (unS ma) ctvid + (res, undo, ctvid') <- doTransaction ref (runSTM ma) ctvid case res of Success _ _ _ -> return (res, ctvid') diff --git a/Test/DejaFu/STM/Internal.hs b/Test/DejaFu/STM/Internal.hs --- a/Test/DejaFu/STM/Internal.hs +++ b/Test/DejaFu/STM/Internal.hs @@ -10,6 +10,8 @@ import Control.Exception (Exception, SomeException(..), fromException) import Control.Monad.Cont (Cont, runCont) import Data.List (nub) +import Data.Maybe (fromMaybe) +import Data.Typeable (cast) import Test.DejaFu.Internal #if __GLASGOW_HASKELL__ < 710 @@ -22,26 +24,26 @@ -- | The underlying monad is based on continuations over primitive -- actions. -type M t n r a = Cont (STMAction t n r) a +type M n r a = Cont (STMAction n r) a -- | Dict of methods for implementations to override. -type Fixed t n r = Ref n r (Cont (STMAction t n r)) +type Fixed n r = Ref n r (Cont (STMAction 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 +data STMAction n r + = forall a e. Exception e => SCatch (e -> M n r a) (M n r a) (a -> STMAction n r) + | forall a. SRead (CTVar r a) (a -> STMAction n r) + | forall a. SWrite (CTVar r a) a (STMAction n r) + | forall a. SOrElse (M n r a) (M n r a) (a -> STMAction n r) + | forall a. SNew a (CTVar r a -> STMAction n r) + | SLift (n (STMAction n r)) + | forall e. Exception e => SThrow e + | SRetry + | SStop -------------------------------------------------------------------------------- -- * @CTVar@s @@ -49,7 +51,7 @@ -- | 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) +newtype CTVar r a = CTVar (CTVarId, r a) -- | The unique ID of a 'CTVar'. Only meaningful within a single -- concurrent computation. @@ -85,11 +87,11 @@ -- * 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 :: Monad n => Fixed n r -> M 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 + let c = runCont (ma >>= liftN fixed . writeRef fixed ref . Just . Right) $ const SStop (newctvid', undo, readen, written) <- go ref c (return ()) newctvid [] [] @@ -106,75 +108,69 @@ (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 + SStop -> return ret + SRetry -> writeRef fixed ref Nothing >> return ret + SThrow exc -> writeRef fixed ref (Just . Left $ wrap exc) >> return ret _ -> go ref act' (undo >> undo') nctvid' (readen' ++ readen) (written' ++ written) + -- | This wraps up an uncaught exception inside a @SomeException@, + -- unless it already is a @SomeException@. This is because + -- multiple levels of @SomeException@ do not play nicely with + -- @fromException@. + wrap e = fromMaybe (SomeException e) $ cast e + -- | 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 :: Monad n => Fixed n r -> STMAction n r -> CTVarId -> n (STMAction 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 + SCatch h stm c -> stepCatch h stm c + SRead ref c -> stepRead ref c + SWrite ref a c -> stepWrite ref a c + SNew a c -> stepNew a c + SOrElse a b c -> stepOrElse a b c + SLift na -> stepLift na - AThrow exc -> return (AThrow exc, nothing, newctvid, [], []) - ARetry -> return (ARetry, nothing, newctvid, [], []) - AStop -> return (AStop, nothing, newctvid, [], []) + halt -> return (halt, 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, [], []) + stepCatch h stm c = onFailure stm c + (\readen -> return (SRetry, nothing, newctvid, readen, [])) + (\exc -> case fromException exc of + Just exc' -> transaction (h exc') c + Nothing -> return (SThrow exc, nothing, newctvid, [], [])) - 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 + stepRead (CTVar (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 + stepWrite (CTVar (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 + stepNew a c = do let newctvid' = newctvid + 1 - a <- na fixed newctvid - return (a, nothing, newctvid', [], [newctvid]) + ref <- newRef fixed a + let ctvar = CTVar (newctvid, ref) + return (c ctvar, 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, []) + stepOrElse a b c = onFailure a c + (\_ -> transaction b c) + (\exc -> return (SThrow exc, nothing, newctvid, [], [])) - stepLift :: n (STMAction t n r) -> n (STMAction t n r, n (), CTVarId, [CTVarId], [CTVarId]) stepLift na = do a <- na return (a, nothing, newctvid, [], []) + + onFailure stm onSuccess onRetry onException = do + (res, undo, newctvid') <- doTransaction fixed stm newctvid + case res of + Success readen written val -> return (onSuccess val, undo, newctvid', readen, written) + Retry readen -> onRetry readen + Exception exc -> onException exc + + transaction stm onSuccess = onFailure stm onSuccess + (\readen -> return (SRetry, nothing, newctvid, readen, [])) + (\exc -> return (SThrow exc, nothing, newctvid, [], [])) diff --git a/dejafu.cabal b/dejafu.cabal --- a/dejafu.cabal +++ b/dejafu.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu -version: 0.1.0.0 +version: 0.2.0.0 synopsis: Overloadable primitives for testable, potentially non-deterministic, concurrency. description: @@ -30,6 +30,30 @@ Whilst this assumption may not hold in general when 'IO' is involved, you should strive to produce test cases where it does. . + == Memory Model + . + The testing functionality supports a few different memory models, + for computations which use non-synchronised `CRef` operations. The + supported models are: + . + * __Sequential Consistency:__ A program behaves as a simple + interleaving of the actions in different threads. When a CRef is + written to, that write is immediately visible to all threads. + . + * __Total Store Order (TSO):__ Each thread has a write buffer. A + thread sees its writes immediately, but other threads will only + see writes when they are committed, which may happen later. Writes + are committed in the same order that they are created. + . + * __Partial Store Order (PSO):__ Each CRef has a write buffer. A + thread sees its writes immediately, but other threads will only + see writes when they are committed, which may happen later. Writes + to different CRefs are not necessarily committed in the same order + that they are created. + . + If a testing function does not take the memory model as a parameter, + it uses TSO. + . See the for more details. @@ -64,23 +88,23 @@ , 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 , Test.DejaFu.Deterministic.Internal.Common - , Test.DejaFu.Deterministic.Internal.CVar + , Test.DejaFu.Deterministic.Internal.Memory , Test.DejaFu.Deterministic.Internal.Threading , Test.DejaFu.Internal , Test.DejaFu.SCT.Internal , Test.DejaFu.STM.Internal - , Data.List.Extra + -- other-modules: -- other-extensions: build-depends: base >=4.5 && <5 + , atomic-primops , containers , deepseq , exceptions >=0.7 @@ -92,10 +116,3 @@ -- 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 deleted file mode 100644 --- a/tests/Tests.hs +++ /dev/null @@ -1,37 +0,0 @@ -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