diff --git a/Test/DejaFu/Conc.hs b/Test/DejaFu/Conc.hs --- a/Test/DejaFu/Conc.hs +++ b/Test/DejaFu/Conc.hs @@ -50,7 +50,8 @@ import qualified Control.Monad.Base as Ba import qualified Control.Monad.Catch as Ca import qualified Control.Monad.IO.Class as IO -import Control.Monad.Ref (MonadRef,) +import Control.Monad.Ref (MonadRef) +import qualified Control.Monad.Ref as Re import Control.Monad.ST (ST) import qualified Data.Foldable as F import Data.IORef (IORef) @@ -86,6 +87,18 @@ instance Ba.MonadBase IO ConcIO where liftBase = IO.liftIO + +instance Re.MonadRef (CRef r) (Conc n r) where + newRef a = toConc (\c -> ANewCRef "" a c) + + readRef ref = toConc (AReadCRef ref) + + writeRef ref a = toConc (\c -> AWriteCRef ref a (c ())) + + modifyRef ref f = toConc (AModCRef ref (\a -> (f a, ()))) + +instance Re.MonadAtomicRef (CRef r) (Conc n r) where + atomicModifyRef ref f = toConc (AModCRef ref f) instance Ca.MonadCatch (Conc n r) where catch ma h = toConc (ACatching (unC . h) (unC ma)) diff --git a/Test/DejaFu/Conc/Internal.hs b/Test/DejaFu/Conc/Internal.hs --- a/Test/DejaFu/Conc/Internal.hs +++ b/Test/DejaFu/Conc/Internal.hs @@ -81,31 +81,27 @@ -- sofar is the 'SeqTrace', sofarSched is the @[(Decision, -- ThreadAction)]@ trace the scheduler needs. go sofar sofarSched prior ctx - | isTerminated = stop prior ctx - | isDeadlocked = die prior Deadlock ctx - | isSTMLocked = die prior STMDeadlock ctx - | isAborted = die prior Abort $ ctx { cSchedState = g' } - | isNonexistant = die prior InternalError $ ctx { cSchedState = g' } - | isBlocked = die prior InternalError $ ctx { cSchedState = g' } + | isTerminated = pure (ctx, sofar, prior) + | isDeadlocked = die sofar prior Deadlock ctx + | isSTMLocked = die sofar prior STMDeadlock ctx + | isAborted = die sofar prior Abort $ ctx { cSchedState = g' } + | isNonexistant = die sofar prior InternalError $ ctx { cSchedState = g' } + | isBlocked = die sofar prior InternalError $ ctx { cSchedState = g' } | otherwise = do stepped <- stepThread sched memtype chosen (_continuation $ fromJust thread) $ ctx { cSchedState = g' } case stepped of (Right ctx', actOrTrc) -> - let (sofar', sofarSched', prior', ctx'') = setupNext actOrTrc ctx' - in go sofar' sofarSched' prior' ctx'' - (Left UncaughtException, actOrTrc) - | chosen == initialThread -> - let ctx' = ctx { cSchedState = g' } - (_, _, prior', ctx'') = setupNext actOrTrc ctx' - in die prior' UncaughtException ctx'' - | otherwise -> - let ctx' = ctx { cThreads = kill chosen threadsc, cSchedState = g' } - (sofar', sofarSched', prior', ctx'') = setupNext actOrTrc ctx' - in go sofar' sofarSched' prior' ctx'' + let (act, trc) = getActAndTrc actOrTrc + threads' = if (interruptible <$> M.lookup chosen (cThreads ctx')) /= Just False + then unblockWaitingOn chosen (cThreads ctx') + else cThreads ctx' + sofarSched' = sofarSched <> map (\(d,_,a) -> (d,a)) (F.toList trc) + ctx'' = ctx' { cThreads = delCommitThreads threads' } + in go (sofar <> trc) sofarSched' (getPrior actOrTrc) ctx'' (Left failure, actOrTrc) -> - let ctx' = ctx { cSchedState = g' } - (_, _, prior', ctx'') = setupNext actOrTrc ctx' - in die prior' failure ctx'' + let (_, trc) = getActAndTrc actOrTrc + ctx' = ctx { cSchedState = g', cThreads = delCommitThreads threads } + in die (sofar <> trc) (getPrior actOrTrc) failure ctx' where (choice, g') = sched sofarSched prior (fromList $ map (\(t,l:|_) -> (t,l)) runnable') (cSchedState ctx) @@ -138,23 +134,16 @@ nextActions t = lookahead . _continuation . fromJust $ M.lookup t threadsc - stop finalDecision finalCtx = pure (finalCtx, sofar, finalDecision) - die finalDecision reason finalCtx = writeRef ref (Just $ Left reason) >> stop finalDecision finalCtx + die sofar' finalDecision reason finalCtx = do + writeRef ref (Just $ Left reason) + pure (finalCtx, sofar', finalDecision) - setupNext trcOrAct ctx' = - let (act, trc) = case trcOrAct of - Single a -> (a, Seq.singleton (decision, runnable', a)) - SubC as _ -> (Subconcurrency, (decision, runnable', Subconcurrency) <| as) - threads' = if (interruptible <$> M.lookup chosen (cThreads ctx')) /= Just False - then unblockWaitingOn chosen (cThreads ctx') - else cThreads ctx' - sofar' = sofar <> trc - sofarSched' = sofarSched <> map (\(d,_,a) -> (d,a)) (F.toList trc) - prior' = case trcOrAct of - Single _ -> Just (chosen, act) - SubC _ finalD -> finalD - in (sofar', sofarSched', prior', ctx' { cThreads = delCommitThreads threads' }) + getActAndTrc (Single a) = (a, Seq.singleton (decision, runnable', a)) + getActAndTrc (SubC as _) = (Subconcurrency, (decision, runnable', Subconcurrency) <| as) + getPrior (Single a) = Just (chosen, a) + getPrior (SubC _ finalD) = finalD + -------------------------------------------------------------------------------- -- * Single-step execution @@ -314,7 +303,7 @@ in pure (Right ctx { cThreads = threads', cIdSource = idSource'}, Single (BlockedSTM trace)) Exception e -> do let act = STM trace [] - res' <- stepThrow act e + res' <- stepThrow tid (cThreads ctx) act e pure $ case res' of (Right ctx', _) -> (Right ctx' { cIdSource = idSource' }, Single act) (Left err, _) -> (Left err, Single act) @@ -327,7 +316,7 @@ -- throw an exception, and propagate it to the appropriate -- handler. - AThrow e -> stepThrow Throw e + AThrow e -> stepThrow tid (cThreads ctx) Throw e -- throw an exception to the target thread, and propagate it to -- the appropriate handler. @@ -336,11 +325,7 @@ blocked = block (OnMask t) tid (cThreads ctx) in case M.lookup t (cThreads ctx) of Just thread - | interruptible thread -> case propagate (toException e) t threads' of - Just threads'' -> simple threads'' $ ThrowTo t - Nothing - | t == initialThread -> pure (Left UncaughtException, Single (ThrowTo t)) - | otherwise -> simple (kill t threads') $ ThrowTo t + | interruptible thread -> stepThrow t threads' (ThrowTo t) e | otherwise -> simple blocked $ BlockedThrowTo t Nothing -> simple threads' $ ThrowTo t @@ -395,10 +380,12 @@ -- this is not inline in the long @case@ above as it's needed by -- @AAtom@, @AThrow@, and @AThrowTo@. - stepThrow act e = - case propagate (toException e) tid (cThreads ctx) of - Just threads' -> simple threads' act - Nothing -> pure (Left UncaughtException, Single act) + stepThrow t ts act e = + case propagate (toException e) t ts of + Just ts' -> simple ts' act + Nothing + | t == initialThread -> pure (Left UncaughtException, Single act) + | otherwise -> simple (kill t ts) act -- helper for actions which only change the threads. simple threads' act = pure (Right ctx { cThreads = threads' }, Single act) diff --git a/dejafu.cabal b/dejafu.cabal --- a/dejafu.cabal +++ b/dejafu.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu -version: 0.5.1.1 +version: 0.5.1.2 synopsis: Systematic testing for Haskell concurrency. description: @@ -74,7 +74,7 @@ source-repository this type: git location: https://github.com/barrucadu/dejafu.git - tag: dejafu-0.5.1.1 + tag: dejafu-0.5.1.2 library exposed-modules: Test.DejaFu @@ -94,7 +94,7 @@ -- other-modules: -- other-extensions: build-depends: base >=4.8 && <5 - , concurrency ==1.1.0.* + , concurrency ==1.1.1.* , containers >=0.5 && <0.6 , deepseq >=1.1 && <2 , exceptions >=0.7 && <0.9