dejafu 0.1.0.0 → 0.2.0.0
raw patch · 16 files changed
+2253/−1497 lines, 16 filesdep +atomic-primopsdep −dejafudep ~base
Dependencies added: atomic-primops
Dependencies removed: dejafu
Dependency ranges changed: base
Files
- Control/Monad/Conc/Class.hs +178/−49
- Test/DejaFu.hs +307/−85
- Test/DejaFu/Deterministic.hs +111/−255
- Test/DejaFu/Deterministic/IO.hs +0/−337
- Test/DejaFu/Deterministic/Internal.hs +250/−177
- Test/DejaFu/Deterministic/Internal/CVar.hs +0/−54
- Test/DejaFu/Deterministic/Internal/Common.hs +429/−87
- Test/DejaFu/Deterministic/Internal/Memory.hs +192/−0
- Test/DejaFu/Deterministic/Internal/Threading.hs +33/−10
- Test/DejaFu/Deterministic/Schedule.hs +9/−9
- Test/DejaFu/SCT.hs +362/−87
- Test/DejaFu/SCT/Internal.hs +256/−153
- Test/DejaFu/STM.hs +38/−82
- Test/DejaFu/STM/Internal.hs +59/−63
- dejafu.cabal +29/−12
- tests/Tests.hs +0/−37
Control/Monad/Conc/Class.hs view
@@ -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
Test/DejaFu.hs view
@@ -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]"
Test/DejaFu/Deterministic.hs view
@@ -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 -- <https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html>-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)
− Test/DejaFu/Deterministic/IO.hs
@@ -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
Test/DejaFu/Deterministic/Internal.hs view
@@ -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 (<oldctvid) readen || any (<oldctvid) written -> let (threads', woken) = wake (OnCTVar written) threads- in return $ Right (knows (map Right written) tid $ goto (c val) tid threads', idSource { _nextCTVId = newctvid }, STM woken)+ 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
− Test/DejaFu/Deterministic/Internal/CVar.hs
@@ -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, [])
Test/DejaFu/Deterministic/Internal/Common.hs view
@@ -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
+ Test/DejaFu/Deterministic/Internal/Memory.hs view
@@ -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, [])
Test/DejaFu/Deterministic/Internal/Threading.hs view
@@ -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
Test/DejaFu/Deterministic/Schedule.hs view
@@ -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
Test/DejaFu/SCT.hs view
@@ -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
Test/DejaFu/SCT/Internal.hs view
@@ -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):<is) ((d,_,a):ts) =+findBacktrack :: MemType+ -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])+ -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])+ -> Trace'+ -> [BacktrackStep]+findBacktrack memtype backtrack = go initialCRState S.empty 0 [] . Sq.viewl where+ go crstate allThreads tid bs ((e,i):<is) ((d,_,a):ts) = let tid' = tidOf tid d- this = BacktrackStep { _threadid = tid'- , _decision = (d, a)- , _runnable = S.fromList . map fst . toList $ e- , _backtrack = I.fromList $ map (\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
Test/DejaFu/STM.hs view
@@ -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')
Test/DejaFu/STM/Internal.hs view
@@ -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, [], []))
dejafu.cabal view
@@ -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 <https://github.com/barrucadu/dejafu README> 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
− tests/Tests.hs
@@ -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