dejafu 1.0.0.2 → 1.1.0.0

raw patch · 12 files changed

+628/−204 lines, 12 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.rst +35/−1
• Test/DejaFu.hs +5/−1
• Test/DejaFu/Conc.hs +206/−15
• Test/DejaFu/Conc/Internal.hs +248/−101
• Test/DejaFu/Conc/Internal/Common.hs +2/−0
• Test/DejaFu/Conc/Internal/Memory.hs +29/−25
• Test/DejaFu/Internal.hs +2/−0
• Test/DejaFu/SCT.hs +63/−47
• Test/DejaFu/SCT/Internal/DPOR.hs +15/−9
• Test/DejaFu/Types.hs +20/−3
• Test/DejaFu/Utils.hs +1/−0
• dejafu.cabal +2/−2

@@ -7,7 +7,41 @@ .. _PVP: https://pvp.haskell.org/  -1.0.0.2 (2017-02-18)+1.1.0.0 (2018-02-22)+--------------------++* Git: :tag:`dejafu-1.1.0.0`+* Hackage: :hackage:`dejafu-1.1.0.0`++**Contributors:** :u:`qrilka` (:pull:`228`).++Added+~~~~~++* (:pull:`219`) The testing-only ``Test.DejaFu.Conc.dontCheck``+  function, and associated definitions:++    * ``Test.DejaFu.Types.DontCheck``+    * ``Test.DejaFu.Types.WillDontCheck``+    * ``Test.DejaFu.Types.IllegalDontCheck``+    * ``Test.DejaFu.Types.isIllegalDontCheck``++* (:pull:`219`) A snapshotting approach based on+  ``Test.DejaFu.Conc.dontCheck``:++    * ``Test.DejaFu.Conc.runForDCSnapshot``+    * ``Test.DejaFu.Conc.runWithDCSnapshot``+    * ``Test.DejaFu.Conc.canDCSnapshot``+    * ``Test.DejaFu.Conc.threadsFromDCSnapshot``++Changed+~~~~~~~++* (:pull:`219`) SCT functions automatically use the snapshotting+  mechanism when possible.+++1.0.0.2 (2018-02-18) --------------------  * Git: :tag:`dejafu-1.0.0.2`

@@ -72,9 +72,12 @@    aren't using a scheduler you wrote yourself, please [file a    bug](https://github.com/barrucadu/dejafu/issues). -Finally, there is one failure which can arise through improper use of+Finally, there are two failures which can arise through improper use of dejafu: + * 'IllegalDontCheck', the "Test.DejaFu.Conc.dontCheck" function is+   used as anything other than the fist action in the main thread.+  * 'IllegalSubconcurrency', the "Test.DejaFu.Conc.subconcurrency"    function is used when multiple threads exist, or is used inside    another @subconcurrency@ call.@@ -323,6 +326,7 @@   , isDeadlock   , isUncaughtException   , isIllegalSubconcurrency+  , isIllegalDontCheck    -- * Property testing 

@@ -28,7 +28,18 @@   , MemType(..)   , runConcurrent   , subconcurrency+  , dontCheck +  -- ** Snapshotting++  -- $snapshotting_io++  , DCSnapshot+  , runForDCSnapshot+  , runWithDCSnapshot+  , canDCSnapshot+  , threadsFromDCSnapshot+   -- * Execution traces   , Trace   , Decision(..)@@ -45,26 +56,31 @@   , module Test.DejaFu.Schedule   ) where -import           Control.Exception                (MaskingState(..))-import qualified Control.Monad.Catch              as Ca-import qualified Control.Monad.IO.Class           as IO-import           Control.Monad.Ref                (MonadRef)-import qualified Control.Monad.Ref                as Re-import           Control.Monad.Trans.Class        (MonadTrans(..))-import qualified Data.Foldable                    as F-import           Data.IORef                       (IORef)+import           Control.Exception                   (MaskingState(..))+import qualified Control.Monad.Catch                 as Ca+import qualified Control.Monad.IO.Class              as IO+import           Control.Monad.Ref                   (MonadRef)+import qualified Control.Monad.Ref                   as Re+import           Control.Monad.Trans.Class           (MonadTrans(..))+import qualified Data.Foldable                       as F+import           Data.IORef                          (IORef)+import           Data.List                           (partition)+import qualified Data.Map.Strict                     as M+import           Data.Maybe                          (isNothing) import           Test.DejaFu.Schedule -import qualified Control.Monad.Conc.Class         as C+import qualified Control.Monad.Conc.Class            as C import           Test.DejaFu.Conc.Internal import           Test.DejaFu.Conc.Internal.Common import           Test.DejaFu.Conc.Internal.STM+import           Test.DejaFu.Conc.Internal.Threading (Thread(_blocking),+                                                      Threads) import           Test.DejaFu.Internal import           Test.DejaFu.Types import           Test.DejaFu.Utils  #if MIN_VERSION_base(4,9,0)-import qualified Control.Monad.Fail               as Fail+import qualified Control.Monad.Fail                  as Fail #endif  -- | @since 0.6.0.0@@ -214,16 +230,191 @@   -> ConcT r n a   -> n (Either Failure a, s, Trace) runConcurrent sched memtype s ma = do-  (res, ctx, trace, _) <- runConcurrency sched memtype s initialIdSource 2 (unC ma)-  pure (res, cSchedState ctx, F.toList trace)+  res <- runConcurrency False sched memtype s initialIdSource 2 (unC ma)+  out <- efromJust "runConcurrent" <$> Re.readRef (finalRef res)+  pure ( out+       , cSchedState (finalContext res)+       , F.toList (finalTrace res)+       )  -- | Run a concurrent computation and return its result. -- -- This can only be called in the main thread, when no other threads--- exist. Calls to 'subconcurrency' cannot be nested. Violating either--- of these conditions will result in the computation failing with--- @IllegalSubconcurrency@.+-- exist. Calls to 'subconcurrency' cannot be nested, or placed inside+-- a call to 'dontCheck'. Violating either of these conditions will+-- result in the computation failing with @IllegalSubconcurrency@. -- -- @since 0.6.0.0 subconcurrency :: ConcT r n a -> ConcT r n (Either Failure a) subconcurrency ma = toConc (ASub (unC ma))++-- | Run an arbitrary action which gets some special treatment:+--+--  * For systematic testing, 'dontCheck' is not dependent with+--    anything, even if the action has dependencies.+--+--  * For pre-emption bounding, 'dontCheck' counts for zero+--    pre-emptions, even if the action performs pre-emptive context+--    switches.+--+--  * For fair bounding, 'dontCheck' counts for zero yields/delays,+--    even if the action performs yields or delays.+--+--  * For length bounding, 'dontCheck' counts for one step, even if+--    the action has many.+--+--   * All SCT functions use 'runForDCSnapshot' / 'runWithDCSnapshot'+--     to ensure that the action is only executed once, although you+--     should be careful with @IO@ (see note on snapshotting @IO@).+--+-- The action is executed atomically with a deterministic scheduler+-- under sequential consistency.  Any threads created inside the+-- action continue to exist in the main computation.+--+-- This must be the first thing done in the main thread.  Violating+-- this condition will result in the computation failing with+-- @IllegalDontCheck@.+--+-- If the action fails (deadlock, length bound exceeded, etc), the+-- whole computation fails.+--+-- @since 1.1.0.0+dontCheck+  :: Maybe Int+  -- ^ An optional length bound.+  -> ConcT r n a+  -- ^ The action to execute.+  -> ConcT r n a+dontCheck lb ma = toConc (ADontCheck lb (unC ma))++-------------------------------------------------------------------------------+-- Snapshotting++-- $snapshotting_io+--+-- __Snapshotting @IO@:__ A snapshot captures entire state of your+-- concurrent program: the state of every thread, the number of+-- capabilities, the values of any @CRef@s, @MVar@s, and @TVar@s, and+-- records any @IO@ that you performed.+--+-- When restoring a snapshot this @IO@ is replayed, in order.  But the+-- whole snapshotted computation is not.  So the effects of the @IO@+-- take place again, but any return values are ignored.  For example,+-- this program will not do what you want:+--+-- @+-- bad_snapshot = do+--   r <- dontCheck Nothing $ do+--     r <- liftIO (newIORef 0)+--     liftIO (modifyIORef r (+1))+--     pure r+--   liftIO (readIORef r)+-- @+--+-- When the snapshot is taken, the value in the @IORef@ will be 1.+-- When the snapshot is restored for the first time, those @IO@+-- actions will be run again, /but their return values will be discarded/.+-- The value in the @IORef@ will be 2.  When the snapshot+-- is restored for the second time, the value in the @IORef@ will be+-- 3.  And so on.+--+-- To safely use @IO@ in a snapshotted computation, __the combined effect must be idempotent__.+-- You should either use actions which set the state to the final+-- value directly, rather than modifying it (eg, using a combination+-- of @liftIO . readIORef@ and @liftIO . writeIORef@ here), or reset+-- the state to a known value.  Both of these approaches will work:+--+-- @+-- good_snapshot1 = do+--   r <- dontCheck Nothing $ do+--     let modify r f = liftIO (readIORef r) >>= liftIO . writeIORef r . f+--     r <- liftIO (newIORef 0)+--     modify r (+1)+--     pure r+--   liftIO (readIORef r)+--+-- good_snapshot2 = do+--   r <- dontCheck Nothing $ do+--     r <- liftIO (newIORef 0)+--     liftIO (writeIORef r 0)+--     liftIO (modifyIORef r (+1))+--     pure r+--   liftIO (readIORef r)+-- @++-- | A snapshot of the concurrency state immediately after 'dontCheck'+-- finishes.+--+-- @since 1.1.0.0+data DCSnapshot r n a = DCSnapshot+  { dcsContext :: Context n r ()+  -- ^ The execution context.  The scheduler state is ignored when+  -- restoring.+  , dcsRestore :: Threads n r -> n ()+  -- ^ Action to restore CRef, MVar, and TVar values.+  , dcsRef :: r (Maybe (Either Failure a))+  -- ^ Reference where the result will be written.+  }++-- | Like 'runConcurrent', but terminates immediately after running+-- the 'dontCheck' action with a 'DCSnapshot' which can be used in+-- 'runWithDCSnapshot' to avoid doing that work again.+--+-- If this program does not contain a legal use of 'dontCheck', then+-- the result will be @Nothing@.+--+-- If you are using the SCT functions on an action which contains a+-- 'dontCheck', snapshotting will be handled for you, without you+-- needing to call this function yourself.+--+-- @since 1.1.0.0+runForDCSnapshot :: (C.MonadConc n, MonadRef r n)+  => ConcT r n a+  -> n (Maybe (Either Failure (DCSnapshot r n a), Trace))+runForDCSnapshot ma = do+  res <- runConcurrency True roundRobinSchedNP SequentialConsistency () initialIdSource 2 (unC ma)+  out <- Re.readRef (finalRef res)+  pure $ case (finalRestore res, out) of+    (Just _, Just (Left f)) -> Just (Left f, F.toList (finalTrace res))+    (Just restore, _) -> Just (Right (DCSnapshot (finalContext res) restore (finalRef res)), F.toList (finalTrace res))+    (_, _) -> Nothing++-- | Like 'runConcurrent', but uses a 'DCSnapshot' produced by+-- 'runForDCSnapshot' to skip the 'dontCheck' work.+--+-- If you are using the SCT functions on an action which contains a+-- 'dontCheck', snapshotting will be handled for you, without you+-- needing to call this function yourself.+--+-- @since 1.1.0.0+runWithDCSnapshot :: (C.MonadConc n, MonadRef r n)+  => Scheduler s+  -> MemType+  -> s+  -> DCSnapshot r n a+  -> n (Either Failure a, s, Trace)+runWithDCSnapshot sched memtype s snapshot = do+  let context = (dcsContext snapshot) { cSchedState = s }+  let restore = dcsRestore snapshot+  let ref = dcsRef snapshot+  res <- runConcurrencyWithSnapshot sched memtype context restore ref+  out <- efromJust "runWithDCSnapshot" <$> Re.readRef (finalRef res)+  pure ( out+       , cSchedState (finalContext res)+       , F.toList (finalTrace res)+       )++-- | Check if a 'DCSnapshot' can be taken from this computation.+--+-- @since 1.1.0.0+canDCSnapshot :: ConcT r n a -> Bool+canDCSnapshot (C (M k)) = lookahead (k undefined) == WillDontCheck++-- | Get the threads which exist in a snapshot, partitioned into+-- runnable and not runnable.+--+-- @since 1.1.0.0+threadsFromDCSnapshot :: DCSnapshot r n a -> ([ThreadId], [ThreadId])+threadsFromDCSnapshot snapshot = partition isRunnable (M.keys threads) where+  threads = cThreads (dcsContext snapshot)+  isRunnable tid = isNothing (_blocking =<< M.lookup tid threads)

@@ -21,10 +21,12 @@                                                       rtsSupportsBoundThreads) import           Control.Monad.Ref                   (MonadRef, newRef, readRef,                                                       writeRef)+import           Data.Foldable                       (foldrM, toList) import           Data.Functor                        (void) import           Data.List                           (sortOn) import qualified Data.Map.Strict                     as M-import           Data.Maybe                          (isJust)+import           Data.Maybe                          (fromMaybe, isJust,+                                                      isNothing) import           Data.Monoid                         ((<>)) import           Data.Sequence                       (Seq, (<|)) import qualified Data.Sequence                       as Seq@@ -44,33 +46,97 @@ type SeqTrace   = Seq (Decision, [(ThreadId, Lookahead)], ThreadAction) +-- | The result of running a concurrent program.+data CResult n r g a = CResult+  { finalContext :: Context n r g+  , finalRef :: r (Maybe (Either Failure a))+  , finalRestore :: Maybe (Threads n r -> n ())+  -- ^ Meaningless if this result doesn't come from a snapshotting+  -- execution.+  , finalTrace :: SeqTrace+  , finalDecision :: Maybe (ThreadId, ThreadAction)+  }+ -- | Run a concurrent computation with a given 'Scheduler' and initial -- state, returning a failure reason on error. Also returned is the -- final state of the scheduler, and an execution trace. runConcurrency :: (MonadConc n, MonadRef r n)-  => Scheduler g+  => Bool+  -> Scheduler g   -> MemType   -> g   -> IdSource   -> Int   -> M n r a-  -> n (Either Failure a, Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction))-runConcurrency sched memtype g idsrc caps ma = do-  (c, ref) <- runRefCont AStop (Just . Right) (runM ma)-  let threads0 = launch' Unmasked initialThread (const c) M.empty-  threads <- (if rtsSupportsBoundThreads then makeBound initialThread else pure) threads0+  -> n (CResult n r g a)+runConcurrency forSnapshot sched memtype g idsrc caps ma = do   let ctx = Context { cSchedState = g                     , cIdSource   = idsrc-                    , cThreads    = threads+                    , cThreads    = M.empty                     , cWriteBuf   = emptyBuffer                     , cCaps       = caps                     }-  (finalCtx, trace, finalAction) <- runThreads sched memtype ref ctx-  let finalThreads = cThreads finalCtx-  mapM_ (`kill` finalThreads) (M.keys finalThreads)-  out <- readRef ref-  pure (efromJust "runConcurrency" out, finalCtx, trace, finalAction)+  res <- runConcurrency' forSnapshot sched memtype ctx ma+  killAllThreads (finalContext res)+  pure res +-- | Like 'runConcurrency' but starts from a snapshot.+runConcurrencyWithSnapshot :: (MonadConc n, MonadRef r n)+  => Scheduler g+  -> MemType+  -> Context n r g+  -> (Threads n r -> n ())+  -> r (Maybe (Either Failure a))+  -> n (CResult n r g a)+runConcurrencyWithSnapshot sched memtype ctx restore ref = do+  let boundThreads = M.filter (isJust . _bound) (cThreads ctx)+  threads <- foldrM makeBound (cThreads ctx) (M.keys boundThreads)+  let ctx' = ctx { cThreads = threads }+  restore (cThreads ctx')+  res <- runConcurrency'' False sched memtype ref ctx { cThreads = threads}+  killAllThreads (finalContext res)+  pure res++-- | Kill the remaining threads+killAllThreads :: MonadConc n => Context n r g -> n ()+killAllThreads ctx =+  let finalThreads = cThreads ctx+  in mapM_ (`kill` finalThreads) (M.keys finalThreads)++-- | Run a concurrent program using the given context, and without+-- killing threads which remain at the end.  The context must have no+-- main thread.+runConcurrency' :: (MonadConc n, MonadRef r n)+  => Bool+  -> Scheduler g+  -> MemType+  -> Context n r g+  -> M n r a+  -> n (CResult n r g a)+runConcurrency' forSnapshot sched memtype ctx ma = do+  (c, ref) <- runRefCont AStop (Just . Right) (runM ma)+  let threads0 = launch' Unmasked initialThread (const c) (cThreads ctx)+  threads <- (if rtsSupportsBoundThreads then makeBound initialThread else pure) threads0+  runConcurrency'' forSnapshot sched memtype ref ctx { cThreads = threads}++-- | Like 'runConcurrency'' but doesn't do *ANY* set up at all.+runConcurrency'' :: (MonadConc n, MonadRef r n)+  => Bool+  -> Scheduler g+  -> MemType+  -> r (Maybe (Either Failure a))+  -> Context n r g+  -> n (CResult n r g a)+runConcurrency'' forSnapshot sched memtype ref ctx = do+  (finalCtx, trace, finalD, restore) <- runThreads forSnapshot sched memtype ref ctx+  pure CResult+    { finalContext = finalCtx+    , finalRef = ref+    , finalRestore = restore+    , finalTrace = trace+    , finalDecision = finalD+    }+ -- | The context a collection of threads are running in. data Context n r g = Context   { cSchedState :: g@@ -82,25 +148,26 @@  -- | Run a collection of threads, until there are no threads left. runThreads :: (MonadConc n, MonadRef r n)-  => Scheduler g+  => Bool+  -> Scheduler g   -> MemType   -> r (Maybe (Either Failure a))   -> Context n r g-  -> n (Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction))-runThreads sched memtype ref = go Seq.empty Nothing where-  go sofar prior ctx-    | isTerminated  = pure (ctx, sofar, prior)-    | isDeadlocked  = die sofar prior Deadlock ctx-    | isSTMLocked   = die sofar prior STMDeadlock ctx+  -> n (Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction), Maybe (Threads n r -> n ()))+runThreads forSnapshot sched memtype ref = go (const $ pure ()) Seq.empty Nothing where+  go restore sofar prior ctx+    | isTerminated  = stop restore sofar prior ctx+    | isDeadlocked  = die restore sofar prior Deadlock ctx+    | isSTMLocked   = die restore sofar prior STMDeadlock ctx     | otherwise =       let ctx' = ctx { cSchedState = g' }       in case choice of            Just chosen -> case M.lookup chosen threadsc of              Just thread-               | isBlocked thread -> die sofar prior InternalError ctx'+               | isBlocked thread -> die restore sofar prior InternalError ctx'                | otherwise -> step chosen thread ctx'-             Nothing -> die sofar prior InternalError ctx'-           Nothing -> die sofar prior Abort ctx'+             Nothing -> die restore sofar prior InternalError ctx'+           Nothing -> die restore sofar prior Abort ctx'     where       (choice, g')  = scheduleThread sched prior (efromList "runThreads" runnable') (cSchedState ctx)       runnable'     = [(t, lookahead (_continuation a)) | (t, a) <- sortOn fst $ M.assocs runnable]@@ -121,54 +188,86 @@           Just (OnMask t) | t == tid -> thrd { _blocking = Nothing }           _ -> thrd -      die sofar' finalDecision reason finalCtx = do+      die restore' sofar' finalD reason finalCtx = do         writeRef ref (Just $ Left reason)-        pure (finalCtx, sofar', finalDecision)+        stop restore' sofar' finalD finalCtx +      stop restore' sofar' finalD finalCtx =+        pure (finalCtx, sofar', finalD, if forSnapshot then Just restore' else Nothing)+       step chosen thread ctx' = do-          (res, actOrTrc) <- stepThread sched memtype chosen (_continuation thread) $ ctx { cSchedState = g' }+          (res, actOrTrc, actionSnap) <- stepThread+              forSnapshot+              (isNothing prior)+              sched+              memtype+              chosen+              (_continuation thread)+              ctx { cSchedState = g' }           let trc    = getTrc actOrTrc           let sofar' = sofar <> trc           let prior' = getPrior actOrTrc+          let restore' threads' =+                if forSnapshot+                then restore threads' >> actionSnap threads'+                else restore threads'           case res of-            Right ctx'' ->+            Succeeded ctx'' ->               let threads' = if (interruptible <$> M.lookup chosen (cThreads ctx'')) /= Just False                              then unblockWaitingOn chosen (cThreads ctx'')                              else cThreads ctx''                   ctx''' = ctx'' { cThreads = delCommitThreads threads' }-              in go sofar' prior' ctx'''-            Left failure ->+              in go restore' sofar' prior' ctx'''+            Failed failure ->               let ctx'' = ctx' { cThreads = delCommitThreads threads }-              in die sofar' prior' failure ctx''+              in die restore' sofar' prior' failure ctx''+            Snap ctx'' ->+              stop actionSnap sofar' prior' ctx''         where           decision             | Just chosen == (fst <$> prior) = Continue             | (fst <$> prior) `notElem` map (Just . fst) runnable' = Start chosen             | otherwise = SwitchTo chosen -          getTrc (Single a)    = Seq.singleton (decision, alternatives, a)-          getTrc (SubC   as _) = (decision, alternatives, Subconcurrency) <| as+          getTrc (Single a) = Seq.singleton (decision, alternatives, a)+          getTrc (SubC as _) = (decision, alternatives, Subconcurrency) <| as            alternatives = filter (\(t, _) -> t /= chosen) runnable' -          getPrior (Single a)      = Just (chosen, a)+          getPrior (Single a) = Just (chosen, a)           getPrior (SubC _ finalD) = finalD  -------------------------------------------------------------------------------- -- * Single-step execution --- | What a thread did.+-- | What a thread did, for trace purposes. data Act   = Single ThreadAction   -- ^ Just one action.   | SubC SeqTrace (Maybe (ThreadId, ThreadAction))-  -- ^ Subconcurrency, with the given trace and final action.+  -- ^ @subconcurrency@, with the given trace and final action.   deriving (Eq, Show) +-- | What a thread did, for execution purposes.+data What n r g+  = Succeeded (Context n r g)+  -- ^ Action succeeded: continue execution.+  | Failed Failure+  -- ^ Action caused computation to fail: stop.+  | Snap (Context n r g)+  -- ^ Action was a snapshot point and we're in snapshot mode: stop.+ -- | Run a single thread one step, by dispatching on the type of -- 'Action'.+--+-- Note: the returned snapshot action will definitely not do the right+-- thing with relaxed memory. stepThread :: forall n r g. (MonadConc n, MonadRef r n)-  => Scheduler g+  => Bool+  -- ^ Should we record a snapshot?+  -> Bool+  -- ^ Is this the first action?+  -> Scheduler g   -- ^ The scheduler.   -> MemType   -- ^ The memory model to use.@@ -178,131 +277,138 @@   -- ^ Action to step   -> Context n r g   -- ^ The execution context.-  -> n (Either Failure (Context n r g), Act)-stepThread sched memtype tid action ctx = case action of+  -> n (What n r g, Act, Threads n r -> n ())+stepThread forSnapshot isFirst sched memtype tid action ctx = case action of     -- start a new thread, assigning it the next 'ThreadId'     AFork n a b -> pure $       let threads' = launch tid newtid a (cThreads ctx)           (idSource', newtid) = nextTId n (cIdSource ctx)-      in (Right ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }, Single (Fork newtid))+      in (Succeeded ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }, Single (Fork newtid), noSnap)      -- start a new bound thread, assigning it the next 'ThreadId'     AForkOS n a b -> do       let (idSource', newtid) = nextTId n (cIdSource ctx)       let threads' = launch tid newtid a (cThreads ctx)       threads'' <- makeBound newtid threads'-      pure (Right ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }, Single (ForkOS newtid))+      pure (Succeeded ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }, Single (ForkOS newtid), noSnap)      -- check if the current thread is bound     AIsBound c ->       let isBound = isJust . _bound $ elookup "stepThread.AIsBound" tid (cThreads ctx)-      in simple (goto (c isBound) tid (cThreads ctx)) (IsCurrentThreadBound isBound)+      in simple (goto (c isBound) tid (cThreads ctx)) (IsCurrentThreadBound isBound) noSnap      -- get the 'ThreadId' of the current thread-    AMyTId c -> simple (goto (c tid) tid (cThreads ctx)) MyThreadId+    AMyTId c -> simple (goto (c tid) tid (cThreads ctx)) MyThreadId noSnap      -- get the number of capabilities-    AGetNumCapabilities c -> simple (goto (c (cCaps ctx)) tid (cThreads ctx)) $ GetNumCapabilities (cCaps ctx)+    AGetNumCapabilities c -> simple (goto (c (cCaps ctx)) tid (cThreads ctx)) (GetNumCapabilities $ cCaps ctx) noSnap      -- set the number of capabilities     ASetNumCapabilities i c -> pure-      (Right ctx { cThreads = goto c tid (cThreads ctx), cCaps = i }, Single (SetNumCapabilities i))+      (Succeeded ctx { cThreads = goto c tid (cThreads ctx), cCaps = i }, Single (SetNumCapabilities i), noSnap)      -- yield the current thread-    AYield c -> simple (goto c tid (cThreads ctx)) Yield+    AYield c -> simple (goto c tid (cThreads ctx)) Yield noSnap      -- yield the current thread (delay is ignored)-    ADelay n c -> simple (goto c tid (cThreads ctx)) (ThreadDelay n)+    ADelay n c -> simple (goto c tid (cThreads ctx)) (ThreadDelay n) noSnap      -- create a new @MVar@, using the next 'MVarId'.     ANewMVar n c -> do       let (idSource', newmvid) = nextMVId n (cIdSource ctx)       ref <- newRef Nothing       let mvar = MVar newmvid ref-      pure (Right ctx { cThreads = goto (c mvar) tid (cThreads ctx), cIdSource = idSource' }, Single (NewMVar newmvid))+      pure ( Succeeded ctx { cThreads = goto (c mvar) tid (cThreads ctx), cIdSource = idSource' }+           , Single (NewMVar newmvid)+           , const (writeRef ref Nothing)+           )      -- put a value into a @MVar@, blocking the thread until it's empty.     APutMVar cvar@(MVar cvid _) a c -> synchronised $ do-      (success, threads', woken) <- putIntoMVar cvar a c tid (cThreads ctx)-      simple threads' $ if success then PutMVar cvid woken else BlockedPutMVar cvid+      (success, threads', woken, effect) <- putIntoMVar cvar a c tid (cThreads ctx)+      simple threads' (if success then PutMVar cvid woken else BlockedPutMVar cvid) (const effect)      -- try to put a value into a @MVar@, without blocking.     ATryPutMVar cvar@(MVar cvid _) a c -> synchronised $ do-      (success, threads', woken) <- tryPutIntoMVar cvar a c tid (cThreads ctx)-      simple threads' $ TryPutMVar cvid success woken+      (success, threads', woken, effect) <- tryPutIntoMVar cvar a c tid (cThreads ctx)+      simple threads' (TryPutMVar cvid success woken) (const effect)      -- get the value from a @MVar@, without emptying, blocking the     -- thread until it's full.     AReadMVar cvar@(MVar cvid _) c -> synchronised $ do-      (success, threads', _) <- readFromMVar cvar c tid (cThreads ctx)-      simple threads' $ if success then ReadMVar cvid else BlockedReadMVar cvid+      (success, threads', _, _) <- readFromMVar cvar c tid (cThreads ctx)+      simple threads' (if success then ReadMVar cvid else BlockedReadMVar cvid) noSnap      -- try to get the value from a @MVar@, without emptying, without     -- blocking.     ATryReadMVar cvar@(MVar cvid _) c -> synchronised $ do-      (success, threads', _) <- tryReadFromMVar cvar c tid (cThreads ctx)-      simple threads' $ TryReadMVar cvid success+      (success, threads', _, _) <- tryReadFromMVar cvar c tid (cThreads ctx)+      simple threads' (TryReadMVar cvid success) noSnap      -- take the value from a @MVar@, blocking the thread until it's     -- full.     ATakeMVar cvar@(MVar cvid _) c -> synchronised $ do-      (success, threads', woken) <- takeFromMVar cvar c tid (cThreads ctx)-      simple threads' $ if success then TakeMVar cvid woken else BlockedTakeMVar cvid+      (success, threads', woken, effect) <- takeFromMVar cvar c tid (cThreads ctx)+      simple threads' (if success then TakeMVar cvid woken else BlockedTakeMVar cvid) (const effect)      -- try to take the value from a @MVar@, without blocking.     ATryTakeMVar cvar@(MVar cvid _) c -> synchronised $ do-      (success, threads', woken) <- tryTakeFromMVar cvar c tid (cThreads ctx)-      simple threads' $ TryTakeMVar cvid success woken+      (success, threads', woken, effect) <- tryTakeFromMVar cvar c tid (cThreads ctx)+      simple threads' (TryTakeMVar cvid success woken) (const effect)      -- create a new @CRef@, using the next 'CRefId'.     ANewCRef n a c -> do       let (idSource', newcrid) = nextCRId n (cIdSource ctx)-      ref <- newRef (M.empty, 0, a)+      let val = (M.empty, 0, a)+      ref <- newRef val       let cref = CRef newcrid ref-      pure (Right ctx { cThreads = goto (c cref) tid (cThreads ctx), cIdSource = idSource' }, Single (NewCRef newcrid))+      pure ( Succeeded ctx { cThreads = goto (c cref) tid (cThreads ctx), cIdSource = idSource' }+           , Single (NewCRef newcrid)+           , const (writeRef ref val)+           )      -- read from a @CRef@.     AReadCRef cref@(CRef crid _) c -> do       val <- readCRef cref tid-      simple (goto (c val) tid (cThreads ctx)) $ ReadCRef crid+      simple (goto (c val) tid (cThreads ctx)) (ReadCRef crid) noSnap      -- read from a @CRef@ for future compare-and-swap operations.     AReadCRefCas cref@(CRef crid _) c -> do       tick <- readForTicket cref tid-      simple (goto (c tick) tid (cThreads ctx)) $ ReadCRefCas crid+      simple (goto (c tick) tid (cThreads ctx)) (ReadCRefCas crid) noSnap      -- modify a @CRef@.     AModCRef cref@(CRef crid _) f c -> synchronised $ do       (new, val) <- f <$> readCRef cref tid-      writeImmediate cref new-      simple (goto (c val) tid (cThreads ctx)) $ ModCRef crid+      effect <- writeImmediate cref new+      simple (goto (c val) tid (cThreads ctx)) (ModCRef crid) (const effect)      -- modify a @CRef@ using a compare-and-swap.     AModCRefCas cref@(CRef crid _) f c -> synchronised $ do       tick@(Ticket _ _ old) <- readForTicket cref tid       let (new, val) = f old-      void $ casCRef cref tid tick new-      simple (goto (c val) tid (cThreads ctx)) $ ModCRefCas crid+      (_, _, effect) <- casCRef cref tid tick new+      simple (goto (c val) tid (cThreads ctx)) (ModCRefCas crid) (const effect)      -- write to a @CRef@ without synchronising.     AWriteCRef cref@(CRef crid _) a c -> case memtype of       -- write immediately.       SequentialConsistency -> do-        writeImmediate cref a-        simple (goto c tid (cThreads ctx)) $ WriteCRef crid+        effect <- writeImmediate cref a+        simple (goto c tid (cThreads ctx)) (WriteCRef crid) (const effect)       -- add to buffer using thread id.       TotalStoreOrder -> do         wb' <- bufferWrite (cWriteBuf ctx) (tid, Nothing) cref a-        pure (Right ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Single (WriteCRef crid))+        pure (Succeeded ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Single (WriteCRef crid), noSnap)       -- add to buffer using both thread id and cref id       PartialStoreOrder -> do         wb' <- bufferWrite (cWriteBuf ctx) (tid, Just crid) cref a-        pure (Right ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Single (WriteCRef crid))+        pure (Succeeded ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Single (WriteCRef crid), noSnap)      -- perform a compare-and-swap on a @CRef@.     ACasCRef cref@(CRef crid _) tick a c -> synchronised $ do-      (suc, tick') <- casCRef cref tid tick a-      simple (goto (c (suc, tick')) tid (cThreads ctx)) $ CasCRef crid suc+      (suc, tick', effect) <- casCRef cref tid tick a+      simple (goto (c (suc, tick')) tid (cThreads ctx)) (CasCRef crid suc) (const effect)      -- commit a @CRef@ write     ACommit t c -> do@@ -314,30 +420,34 @@         TotalStoreOrder -> commitWrite (cWriteBuf ctx) (t, Nothing)         -- commit using the cref id.         PartialStoreOrder -> commitWrite (cWriteBuf ctx) (t, Just c)-      pure (Right ctx { cWriteBuf = wb' }, Single (CommitCRef t c))+      pure (Succeeded ctx { cWriteBuf = wb' }, Single (CommitCRef t c), noSnap)      -- run a STM transaction atomically.     AAtom stm c -> synchronised $ do-      (res, idSource', trace) <- runTransaction stm (cIdSource ctx)+      let transaction = runTransaction stm (cIdSource ctx)+      let effect = const (void transaction)+      (res, idSource', trace) <- transaction       case res of         Success _ written val ->           let (threads', woken) = wake (OnTVar written) (cThreads ctx)-          in pure (Right ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' }, Single (STM trace woken))+          in pure (Succeeded ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' }, Single (STM trace woken), effect)         Retry touched ->           let threads' = block (OnTVar touched) tid (cThreads ctx)-          in pure (Right ctx { cThreads = threads', cIdSource = idSource'}, Single (BlockedSTM trace))+          in pure (Succeeded ctx { cThreads = threads', cIdSource = idSource'}, Single (BlockedSTM trace), effect)         Exception e -> do           let act = STM trace []           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)+            (Succeeded ctx', _, effect') -> (Succeeded ctx' { cIdSource = idSource' }, Single act, effect')+            (Failed err, _, effect') -> (Failed err, Single act, effect')+            (Snap _, _, _) -> fatal "stepThread.AAtom" "Unexpected snapshot while propagating STM exception"      -- lift an action from the underlying monad into the @Conc@     -- computation.     ALift na -> do-      a <- runLiftedAct tid (cThreads ctx) na-      simple (goto a tid (cThreads ctx)) LiftIO+      let effect threads = runLiftedAct tid threads na+      a <- effect (cThreads ctx)+      simple (goto a tid (cThreads ctx)) LiftIO (void <$> effect)      -- throw an exception, and propagate it to the appropriate     -- handler.@@ -351,20 +461,20 @@       in case M.lookup t (cThreads ctx) of            Just thread              | interruptible thread -> stepThrow t threads' (ThrowTo t) e-             | otherwise -> simple blocked $ BlockedThrowTo t-           Nothing -> simple threads' $ ThrowTo t+             | otherwise -> simple blocked (BlockedThrowTo t) noSnap+           Nothing -> simple threads' (ThrowTo t) noSnap      -- run a subcomputation in an exception-catching context.     ACatching h ma c ->       let a        = runCont ma (APopCatching . c)           e exc    = runCont (h exc) c           threads' = goto a tid (catching e tid (cThreads ctx))-      in simple threads' Catching+      in simple threads' Catching noSnap      -- pop the top exception handler from the thread's stack.     APopCatching a ->       let threads' = goto a tid (uncatching tid (cThreads ctx))-      in simple threads' PopCatching+      in simple threads' PopCatching noSnap      -- execute a subcomputation with a new masking state, and give it     -- a function to run a computation with the current masking state.@@ -374,39 +484,66 @@           umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> pure b           resetMask typ ms = cont $ \k -> AResetMask typ True ms $ k ()           threads' = goto a tid (mask m tid (cThreads ctx))-      in simple threads' $ SetMasking False m+      in simple threads' (SetMasking False m) noSnap       -- reset the masking thread of the state.     AResetMask b1 b2 m c ->       let act      = (if b1 then SetMasking else ResetMasking) b2 m           threads' = goto c tid (mask m tid (cThreads ctx))-      in simple threads' act+      in simple threads' act noSnap      -- execute a 'return' or 'pure'.-    AReturn c -> simple (goto c tid (cThreads ctx)) Return+    AReturn c -> simple (goto c tid (cThreads ctx)) Return noSnap      -- kill the current thread.     AStop na -> do       na       threads' <- kill tid (cThreads ctx)-      simple threads' Stop+      simple threads' Stop noSnap      -- run a subconcurrent computation.     ASub ma c-      | M.size (cThreads ctx) > 1 -> pure (Left IllegalSubconcurrency, Single Subconcurrency)+      | forSnapshot -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, noSnap)+      | M.size (cThreads ctx) > 1 -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, noSnap)       | otherwise -> do-          (res, ctx', trace, finalDecision) <--            runConcurrency sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma-          pure (Right ctx { cThreads    = goto (AStopSub (c res)) tid (cThreads ctx)-                          , cIdSource   = cIdSource ctx'-                          , cSchedState = cSchedState ctx' }, SubC trace finalDecision)+          res <- runConcurrency False sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma+          out <- efromJust "stepThread.ASub" <$> readRef (finalRef res)+          pure (Succeeded ctx+                { cThreads    = goto (AStopSub (c out)) tid (cThreads ctx)+                , cIdSource   = cIdSource (finalContext res)+                , cSchedState = cSchedState (finalContext res)+                }+               , SubC (finalTrace res) (finalDecision res)+               , noSnap+               )      -- after the end of a subconcurrent computation. does nothing,     -- only exists so that: there is an entry in the trace for     -- returning to normal computation; and every item in the trace     -- corresponds to a scheduling point.-    AStopSub c -> simple (goto c tid (cThreads ctx)) StopSubconcurrency+    AStopSub c -> simple (goto c tid (cThreads ctx)) StopSubconcurrency noSnap++    -- run an action atomically, with a non-preemptive length bounded+    -- round robin scheduler, under sequential consistency.+    ADontCheck lb ma c+      | isFirst -> do+          -- create a restricted context+          threads' <- kill tid (cThreads ctx)+          let dcCtx = ctx { cThreads = threads', cSchedState = lb }+          res <- runConcurrency' forSnapshot dcSched SequentialConsistency dcCtx ma+          out <- efromJust "stepThread.ADontCheck" <$> readRef (finalRef res)+          case out of+            Right a -> do+              let threads'' = launch' Unmasked tid (const (c a)) (cThreads (finalContext res))+              threads''' <- (if rtsSupportsBoundThreads then makeBound tid else pure) threads''+              pure ( (if forSnapshot then Snap else Succeeded) (finalContext res) { cThreads = threads''', cSchedState = cSchedState ctx }+                   , Single (DontCheck (toList (finalTrace res)))+                   , fromMaybe noSnap (finalRestore res)+                   )+            Left f ->+              pure (Failed f, Single (DontCheck (toList (finalTrace res))), noSnap)+      | otherwise -> pure (Failed IllegalDontCheck, Single (DontCheck []), noSnap)   where      -- this is not inline in the long @case@ above as it's needed by@@ -414,15 +551,15 @@     stepThrow t ts act e =       let some = toException e       in case propagate some t ts of-           Just ts' -> simple ts' act+           Just ts' -> simple ts' act noSnap            Nothing-             | t == initialThread -> pure (Left (UncaughtException some), Single act)+             | t == initialThread -> pure (Failed (UncaughtException some), Single act, noSnap)              | otherwise -> do                  ts' <- kill t ts-                 simple ts' act+                 simple ts' act noSnap      -- helper for actions which only change the threads.-    simple threads' act = pure (Right ctx { cThreads = threads' }, Single act)+    simple threads' act effect = pure (Succeeded ctx { cThreads = threads' }, Single act, effect)      -- helper for actions impose a write barrier.     synchronised ma = do@@ -430,5 +567,15 @@       res <- ma        pure $ case res of-        (Right ctx', act) -> (Right ctx' { cWriteBuf = emptyBuffer }, act)+        (Succeeded ctx', act, effect) -> (Succeeded ctx' { cWriteBuf = emptyBuffer }, act, effect)         _ -> res++    -- scheduler for @ADontCheck@+    dcSched = Scheduler go where+      go _ _ (Just 0) = (Nothing, Just 0)+      go prior threads s =+        let (t, _) = scheduleThread roundRobinSchedNP prior threads ()+        in (t, fmap (\lb -> lb - 1) s)++    -- no snapshot+    noSnap _ = pure ()

@@ -151,6 +151,7 @@    | forall a. ASub (M n r a) (Either Failure a -> Action n r)   | AStopSub (Action n r)+  | forall a. ADontCheck (Maybe Int) (M n r a) (a -> Action n r)  -------------------------------------------------------------------------------- -- * Scheduling & Traces@@ -192,3 +193,4 @@ lookahead (AStop _) = WillStop lookahead (ASub _ _) = WillSubconcurrency lookahead (AStopSub _) = WillStopSubconcurrency+lookahead (ADontCheck _ _ _) = WillDontCheck

@@ -75,7 +75,7 @@ commitWrite :: MonadRef r n => WriteBuffer r -> (ThreadId, Maybe CRefId) -> n (WriteBuffer r) commitWrite w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of   BufferedWrite _ cref a :< rest -> do-    writeImmediate cref a+    _ <- writeImmediate cref a     pure . WriteBuffer $ M.insert k rest wb    EmptyL -> pure w@@ -96,16 +96,16 @@  -- | Perform a compare-and-swap on a @CRef@ if the ticket is still -- valid. This is strict in the \"new\" value argument.-casCRef :: MonadRef r n => CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a)+casCRef :: MonadRef r n => CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a, n ()) casCRef cref tid (Ticket _ cc _) !new = do   tick'@(Ticket _ cc' _) <- readForTicket cref tid    if cc == cc'   then do-    writeImmediate cref new+    effect <- writeImmediate cref new     tick'' <- readForTicket cref tid-    pure (True, tick'')-  else pure (False, tick')+    pure (True, tick'', effect)+  else pure (False, tick', pure ())  -- | Read the local state of a @CRef@. readCRefPrim :: MonadRef r n => CRef r a -> ThreadId -> n (a, Integer)@@ -116,10 +116,12 @@  -- | Write and commit to a @CRef@ immediately, clearing the update map -- and incrementing the write count.-writeImmediate :: MonadRef r n => CRef r a -> a -> n ()+writeImmediate :: MonadRef r n => CRef r a -> a -> n (n ()) writeImmediate (CRef _ ref) a = do   (_, count, _) <- readRef ref-  writeRef ref (M.empty, count + 1, a)+  let effect = writeRef ref (M.empty, count + 1, a)+  effect+  pure effect  -- | Flush all writes in the buffer. writeBarrier :: MonadRef r n => WriteBuffer r -> n ()@@ -152,38 +154,38 @@  -- | Put into a @MVar@, blocking if full. putIntoMVar :: MonadRef r n => MVar r a -> a -> Action n r-            -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])+            -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) putIntoMVar cvar a c = mutMVar Blocking cvar a (const c)  -- | Try to put into a @MVar@, not blocking if full. tryPutIntoMVar :: MonadRef r n => MVar r a -> a -> (Bool -> Action n r)-               -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])+               -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) tryPutIntoMVar = mutMVar NonBlocking  -- | Read from a @MVar@, blocking if empty. readFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r)-            -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])+            -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) readFromMVar cvar c = seeMVar NonEmptying Blocking cvar (c . efromJust "readFromMVar")  -- | Try to read from a @MVar@, not blocking if empty. tryReadFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r)-                -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])+                -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) tryReadFromMVar = seeMVar NonEmptying NonBlocking  -- | Take from a @MVar@, blocking if empty. takeFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r)-             -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])+             -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) takeFromMVar cvar c = seeMVar Emptying Blocking cvar (c . efromJust "takeFromMVar")  -- | Try to take from a @MVar@, not blocking if empty. tryTakeFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r)-                -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])+                -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) tryTakeFromMVar = seeMVar Emptying NonBlocking  -- | Mutate a @MVar@, in either a blocking or nonblocking way. mutMVar :: MonadRef r n         => Blocking -> MVar r a -> a -> (Bool -> Action n r)-        -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])+        -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) mutMVar blocking (MVar cvid ref) a c threadid threads = do   val <- readRef ref @@ -191,34 +193,36 @@     Just _ -> case blocking of       Blocking ->         let threads' = block (OnMVarEmpty cvid) threadid threads-        in pure (False, threads', [])+        in pure (False, threads', [], pure ())       NonBlocking ->-        pure (False, goto (c False) threadid threads, [])+        pure (False, goto (c False) threadid threads, [], pure ())      Nothing -> do-      writeRef ref $ Just a+      let effect = writeRef ref $ Just a       let (threads', woken) = wake (OnMVarFull cvid) threads-      pure (True, goto (c True) threadid threads', woken)+      effect+      pure (True, goto (c True) threadid threads', woken, effect)  -- | Read a @MVar@, in either a blocking or nonblocking -- way. seeMVar :: MonadRef r n         => Emptying -> Blocking -> MVar r a -> (Maybe a -> Action n r)-        -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])+        -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId], n ()) seeMVar emptying blocking (MVar cvid ref) c threadid threads = do   val <- readRef ref    case val of     Just _ -> do-      case emptying of-        Emptying    -> writeRef ref Nothing-        NonEmptying -> pure ()+      let effect = case emptying of+            Emptying -> writeRef ref Nothing+            NonEmptying -> pure ()       let (threads', woken) = wake (OnMVarEmpty cvid) threads-      pure (True, goto (c val) threadid threads', woken)+      effect+      pure (True, goto (c val) threadid threads', woken, effect)      Nothing -> case blocking of       Blocking ->         let threads' = block (OnMVarFull cvid) threadid threads-        in pure (False, threads', [])+        in pure (False, threads', [], pure ())       NonBlocking ->-        pure (False, goto (c Nothing) threadid threads, [])+        pure (False, goto (c Nothing) threadid threads, [], pure ())

@@ -167,6 +167,7 @@ rewind Stop = Just WillStop rewind Subconcurrency = Just WillSubconcurrency rewind StopSubconcurrency = Just WillStopSubconcurrency+rewind (DontCheck _) = Just WillDontCheck  -- | Check if an operation could enable another thread. willRelease :: Lookahead -> Bool@@ -184,6 +185,7 @@ willRelease (WillSetMasking _ _) = True willRelease (WillResetMasking _ _) = True willRelease WillStop = True+willRelease WillDontCheck = True willRelease _ = False  -------------------------------------------------------------------------------

@@ -1,6 +1,7 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}  -- | -- Module      : Test.DejaFu.SCT@@ -8,7 +9,7 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : BangPatterns, GADTs, GeneralizedNewtypeDeriving+-- Portability : BangPatterns, GADTs, GeneralizedNewtypeDeriving, LambdaCase -- -- Systematic testing for concurrent computations. module Test.DejaFu.SCT@@ -498,30 +499,18 @@   -> ConcT r n a   -- ^ The computation to run many times   -> n [(Either Failure a, Trace)]-sctBoundDiscard discard memtype cb conc = go initialState where-  -- Repeatedly run the computation gathering all the results and-  -- traces into a list until there are no schedules remaining to try.-  go !dp = case findSchedulePrefix dp of-    Just (prefix, conservative, sleep) -> do-      (res, s, trace) <- runConcurrent scheduler-                                       memtype-                                       (initialDPORSchedState sleep prefix)-                                       conc--      let bpoints = findBacktracks (schedBoundKill s) (schedBPoints s) trace-      let newDPOR = incorporateTrace conservative trace dp--      if schedIgnore s-        then go (force newDPOR)-        else checkDiscard discard res trace $ go (force (incorporateBacktrackSteps bpoints newDPOR))--    Nothing -> pure []+sctBoundDiscard discard0 memtype0 cb0 = sct initialState findSchedulePrefix step discard0 memtype0 where+  step dp (prefix, conservative, sleep) run = do+    (res, s, trace) <- run+      (dporSched (cBound cb0))+      (initialDPORSchedState sleep prefix) -  -- The DPOR scheduler.-  scheduler = dporSched (cBound cb)+    let bpoints = findBacktrackSteps (cBacktrack cb0) (schedBoundKill s) (schedBPoints s) trace+    let newDPOR = incorporateTrace conservative trace dp -  -- Find the new backtracking steps.-  findBacktracks = findBacktrackSteps (cBacktrack cb)+    pure $ if schedIgnore s+           then (force newDPOR, Nothing)+           else (force (incorporateBacktrackSteps bpoints newDPOR), Just (res, trace))  -- | SCT via uniform random scheduling. --@@ -561,15 +550,16 @@   -> ConcT r n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)]-sctUniformRandomDiscard discard memtype g0 lim0 conc = go g0 (max 0 lim0) where-  go _ 0 = pure []-  go g n = do-    (res, s, trace) <- runConcurrent (randSched $ \g' -> (1, g'))-                                     memtype-                                     (initialRandSchedState Nothing g)-                                     conc-    checkDiscard discard res trace $ go (schedGen s) (n-1)+sctUniformRandomDiscard discard0 memtype0 g0 lim0 = sct (const (g0, max 0 lim0)) check step discard0 memtype0 where+  check (_, 0) = Nothing+  check s = Just s +  step _ (g, n) run = do+    (res, s, trace) <- run+      (randSched $ \g' -> (1, g'))+      (initialRandSchedState Nothing g)+    pure ((schedGen s, n-1), Just (res, trace))+ -- | SCT via weighted random scheduling. -- -- Schedules are generated by assigning to each new thread a random@@ -612,16 +602,49 @@   -> ConcT r n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)]-sctWeightedRandomDiscard discard memtype g0 lim0 use0 conc = go g0 (max 0 lim0) (max 1 use0) M.empty where-  go _ 0 _ _ = pure []-  go g n 0 _ = go g n (max 1 use0) M.empty-  go g n use ws = do-    (res, s, trace) <- runConcurrent (randSched $ randomR (1, 50))-                                     memtype-                                     (initialRandSchedState (Just ws) g)-                                     conc-    checkDiscard discard res trace $ go (schedGen s) (n-1) (use-1) (schedWeights s)+sctWeightedRandomDiscard discard0 memtype0 g0 lim0 use0 = sct (const (g0, max 0 lim0, max 1 use0, M.empty)) check step discard0 memtype0 where+  check (_, 0, _, _) = Nothing+  check s = Just s +  step s (g, n, 0, _) run = step s (g, n, max 1 use0, M.empty) run+  step _ (g, n, use, ws) run = do+    (res, s, trace) <- run+      (randSched $ randomR (1, 50))+      (initialRandSchedState (Just ws) g)+    pure ((schedGen s, n-1, use-1, schedWeights s), Just (res, trace))++-- | General-purpose SCT function.+sct :: (MonadConc n, MonadRef r n)+  => ([ThreadId] -> s)+  -- ^ Initial state+  -> (s -> Maybe t)+  -- ^ State predicate+  -> (s -> t -> (Scheduler g -> g -> n (Either Failure a, g, Trace)) -> n (s, Maybe (Either Failure a, Trace)))+  -- ^ Run the computation and update the state+  -> (Either Failure a -> Maybe Discard)+  -> MemType+  -> ConcT r n a+  -> n [(Either Failure a, Trace)]+sct s0 sfun srun discard memtype conc+    | canDCSnapshot conc = runForDCSnapshot conc >>= \case+        Just (Right snap, _) -> go (runSnap snap) (fst (threadsFromDCSnapshot snap))+        Just (Left f, trace) -> pure [(Left f, trace)]+        _ -> fatal "sct" "Failed to construct snapshot"+    | otherwise = go runFull [initialThread]+  where+    go run = go' . s0 where+      go' !s = case sfun s of+        Just t -> srun s t run >>= \case+          (s', Just (res, trace)) -> case discard res of+            Just DiscardResultAndTrace -> go' s'+            Just DiscardTrace -> ((res, []):) <$> go' s'+            Nothing -> ((res, trace):) <$> go' s'+          (s', Nothing) -> go' s'+        Nothing -> pure []++    runFull sched s = runConcurrent sched memtype s conc+    runSnap snap sched s = runWithDCSnapshot sched memtype s snap+ ------------------------------------------------------------------------------- -- Utilities @@ -678,10 +701,3 @@     in go m' xs   go m [] = m   go' x0 m x = m `max` abs (x0 - x)---- | Apply the discard function.-checkDiscard :: Functor f => (a -> Maybe Discard) -> a -> [b] -> f [(a, [b])] -> f [(a, [b])]-checkDiscard discard res trace rest = case discard res of-  Just DiscardResultAndTrace -> rest-  Just DiscardTrace -> ((res, []):) <$> rest-  Nothing -> ((res, trace):) <$> rest

@@ -122,15 +122,19 @@  -- | Initial DPOR state, given an initial thread ID. This initial -- thread should exist and be runnable at the start of execution.-initialState :: DPOR-initialState = DPOR-  { dporRunnable = S.singleton initialThread-  , dporTodo     = M.singleton initialThread False-  , dporNext     = Nothing-  , dporDone     = S.empty-  , dporSleep    = M.empty-  , dporTaken    = M.empty-  }+--+-- The main thread must be in the list of initially runnable threads.+initialState :: [ThreadId] -> DPOR+initialState threads+  | initialThread `elem` threads = DPOR+    { dporRunnable = S.fromList threads+    , dporTodo     = M.singleton initialThread False+    , dporNext     = Nothing+    , dporDone     = S.empty+    , dporSleep    = M.empty+    , dporTaken    = M.empty+    }+  | otherwise = fatal "initialState" "Initial thread is not in initially runnable set"  -- | Produce a new schedule prefix from a @DPOR@ tree. If there are no new -- prefixes remaining, return 'Nothing'. Also returns whether the@@ -568,6 +572,8 @@     | check t2 a2 t1 a1 = False     | otherwise = not (dependent ds t1 a1 t2 a2)   where+    -- @dontCheck@ must be the first thing in the computation.+    check _ (DontCheck _) _ _ = True     -- can't re-order any action of a thread with the fork which     -- created it.     check _ (Fork t) tid _ | t == tid = True

@@ -85,7 +85,7 @@  -- | All the actions that a thread can perform. ----- @since 1.0.0.0+-- @since 1.1.0.0 data ThreadAction =     Fork ThreadId   -- ^ Start a new thread.@@ -177,6 +177,8 @@   -- ^ Start executing an action with @subconcurrency@.   | StopSubconcurrency   -- ^ Stop executing an action with @subconcurrency@.+  | DontCheck Trace+  -- ^ Execute an action with @dontCheck@.   deriving (Eq, Show)  instance NFData ThreadAction where@@ -209,11 +211,12 @@   rnf (BlockedThrowTo t) = rnf t   rnf (SetMasking b m) = b `seq` m `seq` ()   rnf (ResetMasking b m) = b `seq` m `seq` ()+  rnf (DontCheck t) = rnf t   rnf a = a `seq` ()  -- | A one-step look-ahead at what a thread will do next. ----- @since 1.0.0.0+-- @since 1.1.0.0 data Lookahead =     WillFork   -- ^ Will start a new thread.@@ -294,6 +297,8 @@   -- ^ Will execute an action with @subconcurrency@.   | WillStopSubconcurrency   -- ^ Will stop executing an extion with @subconcurrency@.+  | WillDontCheck+  -- ^ Will execute an action with @dontCheck@.   deriving (Eq, Show)  instance NFData Lookahead where@@ -390,7 +395,7 @@ -- The @Eq@, @Ord@, and @NFData@ instances compare/evaluate the -- exception with @show@ in the @UncaughtException@ case. ----- @since 0.9.0.0+-- @since 1.1.0.0 data Failure   = InternalError   -- ^ Will be raised if the scheduler does something bad. This should@@ -412,6 +417,9 @@   | IllegalSubconcurrency   -- ^ Calls to @subconcurrency@ were nested, or attempted when   -- multiple threads existed.+  | IllegalDontCheck+  -- ^ A call to @dontCheck@ was attempted after the first action of+  -- the initial thread.   deriving Show  instance Eq Failure where@@ -421,6 +429,7 @@   STMDeadlock            == STMDeadlock            = True   (UncaughtException e1) == (UncaughtException e2) = show e1 == show e2   IllegalSubconcurrency  == IllegalSubconcurrency  = True+  IllegalDontCheck       == IllegalDontCheck       = True   _ == _ = False  instance Ord Failure where@@ -432,6 +441,7 @@     transform STMDeadlock = (3, Nothing)     transform (UncaughtException e) = (4, Just (show e))     transform IllegalSubconcurrency = (5, Nothing)+    transform IllegalDontCheck = (6, Nothing)  instance NFData Failure where   rnf (UncaughtException e) = rnf (show e)@@ -472,6 +482,13 @@ isIllegalSubconcurrency :: Failure -> Bool isIllegalSubconcurrency IllegalSubconcurrency = True isIllegalSubconcurrency _ = False++-- | Check if a failure is an @IllegalDontCheck@+--+-- @since 1.1.0.0+isIllegalDontCheck :: Failure -> Bool+isIllegalDontCheck IllegalDontCheck = True+isIllegalDontCheck _ = False  ------------------------------------------------------------------------------- -- * Discarding results and traces

@@ -81,6 +81,7 @@ showFail InternalError = "[internal-error]" showFail (UncaughtException exc) = "[" ++ displayException exc ++ "]" showFail IllegalSubconcurrency = "[illegal-subconcurrency]"+showFail IllegalDontCheck = "[illegal-dontcheck]"  ------------------------------------------------------------------------------- -- * Scheduling

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             1.0.0.2+version:             1.1.0.0 synopsis:            A library for unit-testing concurrent programs.  description:@@ -33,7 +33,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-1.0.0.2+  tag:      dejafu-1.1.0.0  library   exposed-modules:     Test.DejaFu