dejafu 1.3.0.1 → 1.3.0.2

raw patch · 9 files changed

+101/−523 lines, 9 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.rst +8/−16
• Test/DejaFu/Conc/Internal/Memory.hs +3/−6
• Test/DejaFu/Internal.hs +0/−2
• Test/DejaFu/SCT.hs +50/−9
• Test/DejaFu/SCT/Internal.hs +0/−359
• Test/DejaFu/SCT/Internal/DPOR.hs +36/−61
• Test/DejaFu/Settings.hs +0/−58
• Test/DejaFu/Utils.hs +2/−9
• dejafu.cabal +2/−3

@@ -6,25 +6,17 @@  .. _PVP: https://pvp.haskell.org/ -unreleased-------------Added-~~~~~--* (:issue:`183`) SCT settings for trace simplification:--    * ``Test.DejaFu.Settings.lequality``-    * ``Test.DejaFu.Settings.lsimplify``+1.3.0.2 (2018-03-11)+-------------------- -* (:issue:`183`) ``Test.DejaFu.Utils.toTIdTrace`` to extract thread-  IDs from a trace.+* Git: :tag:`dejafu-1.3.0.2`+* Hackage: :hackage:`dejafu-1.3.0.2` -Performance-~~~~~~~~~~~+Fixed+~~~~~ -* (:issue:`183`) Prune some unnecessary interleavings of ``CRef``-  actions in systematic testing when using sequential consistency.+* (:pull:`244`) Add missing dependency for ``setNumCapabilities``+  actions.   1.3.0.1 (2018-03-08)

@@ -131,18 +131,15 @@ -- | Add phantom threads to the thread list to commit pending writes. addCommitThreads :: WriteBuffer r -> Threads n r -> Threads n r addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where-  phantoms = [ (uncurry commitThreadId k, mkthread c)+  phantoms = [ (ThreadId (Id Nothing . negate $ commitTidOf k), mkthread c)              | (k, b) <- M.toList wb              , c <- maybeToList (go $ viewl b)              ]   go (BufferedWrite tid (CRef crid _) _ :< _) = Just $ ACommit tid crid   go EmptyL = Nothing --- | The ID of a commit thread.-commitThreadId :: ThreadId -> Maybe CRefId -> ThreadId-commitThreadId (ThreadId (Id _ t)) = ThreadId . Id Nothing . negate . go where-  go (Just (CRefId (Id _ c))) = t + 1 + c * 10000-  go Nothing = t + 1+  commitTidOf (ThreadId (Id _ t), Nothing) = t + 1+  commitTidOf (ThreadId (Id _ t), Just (CRefId (Id _ c))) = t + 1 + c * 10000  -- | Remove phantom threads. delCommitThreads :: Threads n r -> Threads n r

@@ -37,8 +37,6 @@   , _debugShow :: Maybe (a -> String)   , _debugPrint :: Maybe (String -> n ())   , _earlyExit :: Maybe (Either Failure a -> Bool)-  , _equality :: Maybe (a -> a -> Bool)-  , _simplify  :: Bool   }  -- | How to explore the possible executions of a concurrent program.

@@ -1,10 +1,13 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE LambdaCase #-}+ -- | -- Module      : Test.DejaFu.SCT -- Copyright   : (c) 2015--2018 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : portable+-- Portability : BangPatterns, LambdaCase -- -- Systematic testing for concurrent computations. module Test.DejaFu.SCT@@ -47,7 +50,6 @@  import           Test.DejaFu.Conc import           Test.DejaFu.Internal-import           Test.DejaFu.SCT.Internal import           Test.DejaFu.SCT.Internal.DPOR import           Test.DejaFu.SCT.Internal.Weighted import           Test.DejaFu.Settings@@ -197,13 +199,13 @@          check = findSchedulePrefix -        step run dp (prefix, conservative, sleep) = do+        step dp (prefix, conservative, sleep) run = do           (res, s, trace) <- run-            (dporSched (_memtype settings) (cBound cb0))+            (dporSched (cBound cb0))             (initialDPORSchedState sleep prefix) -          let bpoints = findBacktrackSteps (_memtype settings) (cBacktrack cb0) (schedBoundKill s) (schedBPoints s) trace-          let newDPOR = incorporateTrace (_memtype settings) conservative trace dp+          let bpoints = findBacktrackSteps (cBacktrack cb0) (schedBoundKill s) (schedBPoints s) trace+          let newDPOR = incorporateTrace conservative trace dp            pure $ if schedIgnore s                  then (force newDPOR, Nothing)@@ -216,7 +218,7 @@         check (_, 0) = Nothing         check s = Just s -        step run _ (g, n) = do+        step _ (g, n) run = do           (res, s, trace) <- run             (randSched $ \g' -> (1, g'))             (initialRandSchedState Nothing g)@@ -229,8 +231,8 @@         check (_, 0, _, _) = Nothing         check s = Just s -        step run s (g, n, 0, _) = step run s (g, n, max 1 use0, M.empty)-        step run _ (g, n, use, ws) = do+        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)@@ -504,6 +506,45 @@ sctWeightedRandomDiscard discard memtype g lim use = runSCTWithSettings $   set ldiscard (Just discard) (fromWayAndMemType (swarmy g lim use) memtype) {-# DEPRECATED sctWeightedRandomDiscard "Use runSCTWithSettings instead" #-}++-- | General-purpose SCT function.+sct :: (MonadConc n, MonadRef r n)+  => Settings n a+  -- ^ The SCT settings ('Way' is ignored)+  -> ([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+  -> ConcT r n a+  -> n [(Either Failure a, Trace)]+sct settings s0 sfun srun conc+    | canDCSnapshot conc = runForDCSnapshot conc >>= \case+        Just (Right snap, _) -> go (runSnap snap) (fst (threadsFromDCSnapshot snap))+        Just (Left f, trace) -> pure [(Left f, trace)]+        _ -> do+          debugPrint "Failed to construct snapshot, continuing without."+          go runFull [initialThread]+    | otherwise = go runFull [initialThread]+  where+    go run = go' Nothing . s0 where+      go' (Just res) _ | earlyExit res = pure []+      go' _ !s = case sfun s of+        Just t -> srun s t run >>= \case+          (s', Just (res, trace)) -> case discard res of+            Just DiscardResultAndTrace -> go' (Just res) s'+            Just DiscardTrace -> ((res, []):) <$> go' (Just res) s'+            Nothing -> ((res, trace):) <$> go' (Just res) s'+          (s', Nothing) -> go' Nothing s'+        Nothing -> pure []++    runFull sched s = runConcurrent sched (_memtype settings) s conc+    runSnap snap sched s = runWithDCSnapshot sched (_memtype settings) s snap++    debugPrint = fromMaybe (const (pure ())) (_debugPrint settings)+    earlyExit = fromMaybe (const False) (_earlyExit settings)+    discard = fromMaybe (const Nothing) (_discard settings)  ------------------------------------------------------------------------------- -- Utilities

@@ -1,359 +0,0 @@-{-# LANGUAGE BangPatterns #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE RankNTypes #-}---- |--- Module      : Test.DejaFu.SCT.Internal--- Copyright   : (c) 2018 Michael Walker--- License     : MIT--- Maintainer  : Michael Walker <mike@barrucadu.co.uk>--- Stability   : experimental--- Portability : BangPatterns, FlexibleContexts, LambdaCase, RankNTypes------ Internal types and functions for SCT.  This module is NOT--- considered to form part of the public interface of this library.-module Test.DejaFu.SCT.Internal where--import           Control.Monad.Conc.Class         (MonadConc)-import           Control.Monad.Ref                (MonadRef)-import           Data.Coerce                      (Coercible, coerce)-import qualified Data.IntMap.Strict               as I-import           Data.List                        (find, mapAccumL)-import           Data.Maybe                       (fromMaybe)--import           Test.DejaFu.Conc-import           Test.DejaFu.Conc.Internal.Memory (commitThreadId)-import           Test.DejaFu.Internal-import           Test.DejaFu.Schedule             (Scheduler(..))-import           Test.DejaFu.SCT.Internal.DPOR-import           Test.DejaFu.Types-import           Test.DejaFu.Utils------------------------------------------------------------------------------------ * Exploration---- | General-purpose SCT function.-sct :: (MonadConc n, MonadRef r n)-  => Settings n a-  -- ^ The SCT settings ('Way' is ignored)-  -> ([ThreadId] -> s)-  -- ^ Initial state-  -> (s -> Maybe t)-  -- ^ State predicate-  -> ((Scheduler g -> g -> n (Either Failure a, g, Trace)) -> s -> t -> n (s, Maybe (Either Failure a, Trace)))-  -- ^ Run the computation and update the state-  -> ConcT r n a-  -> n [(Either Failure a, Trace)]-sct settings s0 sfun srun conc-    | canDCSnapshot conc = runForDCSnapshot conc >>= \case-        Just (Right snap, _) -> sct' settings (s0 (fst (threadsFromDCSnapshot snap))) sfun (srun (runSnap snap)) (runSnap snap)-        Just (Left f, trace) -> pure [(Left f, trace)]-        _ -> do-          debugPrint "Failed to construct snapshot, continuing without."-          sct' settings (s0 [initialThread]) sfun (srun runFull) runFull-    | otherwise = sct' settings (s0 [initialThread]) sfun (srun runFull) runFull-  where-    runFull sched s = runConcurrent sched (_memtype settings) s conc-    runSnap snap sched s = runWithDCSnapshot sched (_memtype settings) s snap--    debugPrint = fromMaybe (const (pure ())) (_debugPrint settings)---- | Like 'sct' but given a function to run the computation.-sct' :: (MonadConc n, MonadRef r n)-  => Settings n a-  -- ^ The SCT settings ('Way' is ignored)-  -> s-  -- ^ Initial state-  -> (s -> Maybe t)-  -- ^ State predicate-  -> (s -> t -> n (s, Maybe (Either Failure a, Trace)))-  -- ^ Run the computation and update the state-  -> (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace))-  -- ^ Just run the computation-  -> n [(Either Failure a, Trace)]-sct' settings s0 sfun srun run = go Nothing [] s0 where-  go (Just res) _ _ | earlyExit res = pure []-  go _ seen !s = case sfun s of-    Just t -> srun s t >>= \case-      (s', Just (res, trace)) -> case discard res of-        Just DiscardResultAndTrace -> go (Just res) seen s'-        Just DiscardTrace -> result res [] seen s'-        Nothing -> result res trace seen s'-      (s', Nothing) -> go Nothing seen s'-    Nothing -> pure []--  -- Sadly, we have to use a list to store the set of unique results,-  -- as we don't have an @Ord a@ dict hanging around.  I suspect that-  -- most test cases will have a relatively small number of unique-  -- results, compared to the number of executions, however.-  -- Pathological cases (like IORef ones in dejafu-tests which produce-  -- a different result on every execution) are probably uncommon.-  result = case _equality settings of-    Just f -> \res trace seen s ->-      let eq cmp (Right a1) (Right a2) = cmp a1 a2-          eq _   (Left  e1) (Left  e2) = e1 == e2-          eq _ _ _ = False-      in if any (eq f res) seen-         then go (Just res) seen s-         else dosimplify res trace (res:seen) s-    Nothing -> dosimplify--  dosimplify res [] seen s = ((res, []) :) <$> go (Just res) seen s-  dosimplify res trace seen s-    | not (_simplify settings) = ((res, trace) :) <$> go (Just res) seen s-    | otherwise = do-        shrunk <- simplifyExecution settings run res trace-        (shrunk :) <$> go (Just res) seen s--  earlyExit = fromMaybe (const False) (_earlyExit settings)-  discard = fromMaybe (const Nothing) (_discard settings)---- | Given a result and a trace, produce a more minimal trace.------ In principle, simplification is semantics preserving and can be--- done without needing to execute the computation again.  However,--- there are two good reasons to do so:------  * It's a sanity check that there are no bugs.---  * It's easier to generate a reduced sequence of scheduling---    decisions and let dejafu generate the full trace, than to---    generate a reduced trace directly------ Unlike shrinking in randomised property-testing tools like--- QuickCheck or Hedgehog, we only run the test case /once/, at the--- end, rather than after every simplification step.-simplifyExecution :: (MonadConc n, MonadRef r n)-  => Settings n a-  -- ^ The SCT settings ('Way' is ignored)-  -> (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace))-  -- ^ Just run the computation-  -> Either Failure a-  -- ^ The expected result-  -> Trace-  -> n (Either Failure a, Trace)-simplifyExecution settings run res trace-    | tidTrace == simplifiedTrace = do-        debugPrint ("Simplifying new result '" ++ p res ++ "': no simplification possible!")-        pure (res, trace)-    | otherwise = do-        debugPrint ("Simplifying new result '" ++ p res ++ "': OK!")-        (res', _, trace') <- replay run simplifiedTrace-        case (_equality settings, res, res') of-          (Just f,  Right a1, Right a2) | f a1 a2  -> pure (res', trace')-          (_,       Left  e1, Left  e2) | e1 == e2 -> pure (res', trace')-          (Nothing, Right _,  Right _) -> pure (res', trace') -- this is a risky case!-          _ -> do-            debugPrint ("Got a different result after simplifying: '" ++ p res ++ "' /= '" ++ p res' ++ "'")-            pure (res, trace)-  where-    tidTrace = toTIdTrace trace-    simplifiedTrace = simplify (_memtype settings) tidTrace--    debugPrint = fromMaybe (const (pure ())) (_debugPrint settings)-    debugShow = fromMaybe (const "_") (_debugShow settings)-    p = either show debugShow---- | Replay an execution.-replay :: (MonadConc n, MonadRef r n)-  => (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace))-  -- ^ Run the computation-  -> [(ThreadId, ThreadAction)]-  -- ^ The reduced sequence of scheduling decisions-  -> n (Either Failure a, [(ThreadId, ThreadAction)], Trace)-replay run = run (Scheduler (const sched)) where-    sched runnable ((t, Stop):ts) = case findThread t runnable of-      Just t' -> (Just t', ts)-      Nothing -> sched runnable ts-    sched runnable ((t, _):ts) = (findThread t runnable, ts)-    sched _ _ = (Nothing, [])--    -- find a thread ignoring names-    findThread tid0 =-      fmap fst . find (\(tid,_) -> fromId tid == fromId tid0)------------------------------------------------------------------------------------ * Schedule simplification---- | Simplify a trace by permuting adjacent independent actions to--- reduce context switching.-simplify :: MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]-simplify memtype trc0 = loop (length trc0) (prepare trc0) where-  prepare = dropCommits memtype . lexicoNormalForm memtype-  step = pushForward memtype . pullBack memtype--  loop 0 trc = trc-  loop n trc =-    let trc' = step trc-    in if trc' /= trc then loop (n-1) trc' else trc---- | Put a trace into lexicographic (by thread ID) normal form.-lexicoNormalForm :: MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]-lexicoNormalForm memtype = go where-  go trc =-    let trc' = permuteBy memtype (repeat (>)) trc-    in if trc == trc' then trc else go trc'---- | Swap adjacent independent actions in the trace if a predicate--- holds.-permuteBy-  :: MemType-  -> [ThreadId -> ThreadId -> Bool]-  -> [(ThreadId, ThreadAction)]-  -> [(ThreadId, ThreadAction)]-permuteBy memtype = go initialDepState where-  go ds (p:ps) (t1@(tid1, ta1):t2@(tid2, ta2):trc)-    | independent ds tid1 ta1 tid2 ta2 && p tid1 tid2 = go' ds ps t2 (t1 : trc)-    | otherwise = go' ds ps t1 (t2 : trc)-  go _ _ trc = trc--  go' ds ps t@(tid, ta) trc = t : go (updateDepState memtype ds tid ta) ps trc---- | Throw away commit actions which are followed by a memory barrier.-dropCommits :: MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]-dropCommits SequentialConsistency = id-dropCommits memtype = go initialDepState where-  go ds (t1@(tid1, ta1@(CommitCRef _ _)):t2@(tid2, ta2):trc)-    | isBarrier (simplifyAction ta2) = go ds (t2:trc)-    | independent ds tid1 ta1 tid2 ta2 = t2 : go (updateDepState memtype ds tid2 ta2) (t1:trc)-  go ds (t@(tid,ta):trc) = t : go (updateDepState memtype ds tid ta) trc-  go _ [] = []---- | Attempt to reduce context switches by \"pulling\" thread actions--- back to a prior execution of that thread.------ Simple example, say we have @[(tidA, act1), (tidB, act2), (tidA,--- act3)]@, where @act2@ and @act3@ are independent.  In this case--- 'pullBack' will swap them, giving the sequence @[(tidA, act1),--- (tidA, act3), (tidB, act2)]@.  It works for arbitrary separations.-pullBack :: MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]-pullBack memtype = go initialDepState where-  go ds (t1@(tid1, ta1):trc@((tid2, _):_)) =-    let ds' = updateDepState memtype ds tid1 ta1-        trc' = if tid1 /= tid2-               then maybe trc (uncurry (:)) (findAction tid1 ds' trc)-               else trc-    in t1 : go ds' trc'-  go _ trc = trc--  findAction tid0 = fgo where-    fgo ds (t@(tid, ta):trc)-      | tid == tid0 = Just (t, trc)-      | otherwise = case fgo (updateDepState memtype ds tid ta) trc of-          Just (ft@(ftid, fa), trc')-            | independent ds tid ta ftid fa -> Just (ft, t:trc')-          _ -> Nothing-    fgo _ _ = Nothing---- | Attempt to reduce context switches by \"pushing\" thread actions--- forward to a future execution of that thread.------ This is kind of the opposite of 'pullBack', but there are cases--- where one applies but not the other.------ Simple example, say we have @[(tidA, act1), (tidB, act2), (tidA,--- act3)]@, where @act1@ and @act2@ are independent.  In this case--- 'pushForward' will swap them, giving the sequence @[(tidB, act2),--- (tidA, act1), (tidA, act3)]@.  It works for arbitrary separations.-pushForward :: MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]-pushForward memtype = go initialDepState where-  go ds (t1@(tid1, ta1):trc@((tid2, _):_)) =-    let ds' = updateDepState memtype ds tid1 ta1-    in if tid1 /= tid2-       then maybe (t1 : go ds' trc) (go ds) (findAction tid1 ta1 ds trc)-       else t1 : go ds' trc-  go _ trc = trc--  findAction tid0 ta0 = fgo where-    fgo ds (t@(tid, ta):trc)-      | tid == tid0 = Just ((tid0, ta0) : t : trc)-      | independent ds tid0 ta0 tid ta = (t:) <$> fgo (updateDepState memtype ds tid ta) trc-      | otherwise = Nothing-    fgo _ _ = Nothing---- | Re-number threads and CRefs.------ Permuting forks or newCRefs makes the existing numbering invalid,--- which then causes problems for scheduling.  Just re-numbering--- threads isn't enough, as CRef IDs are used to determine commit--- thread IDs.------ Renumbered things will not fix their names, so don't rely on those--- at all.-renumber-  :: MemType-  -- ^ The memory model determines how commit threads are numbered.-  -> Int-  -- ^ First free thread ID.-  -> Int-  -- ^ First free @CRef@ ID.-  -> [(ThreadId, ThreadAction)]-  -> [(ThreadId, ThreadAction)]-renumber memtype tid0 crid0 = snd . mapAccumL go (I.empty, tid0, I.empty, crid0) where-  go s@(tidmap, _, cridmap, _) (_, CommitCRef tid crid) =-    let tid'  = renumbered tidmap  tid-        crid' = renumbered cridmap crid-        act' = CommitCRef tid' crid'-    in case memtype of-         PartialStoreOrder -> (s, (commitThreadId tid' (Just crid'), act'))-         _ -> (s, (commitThreadId tid' Nothing, act'))-  go s@(tidmap, _, _, _) (tid, act) =-    let (s', act') = updateAction s act-    in (s', (renumbered tidmap tid, act'))--  -- I can't help but feel there should be some generic programming-  -- solution to this sort of thing (and to the many other functions-  -- operating over @ThreadAction@s / @Lookahead@s)-  updateAction (tidmap, nexttid, cridmap, nextcrid) (Fork old) =-    let tidmap' = I.insert (fromId old) nexttid tidmap-        nexttid' = nexttid + 1-    in ((tidmap', nexttid', cridmap, nextcrid), Fork (toId nexttid))-  updateAction (tidmap, nexttid, cridmap, nextcrid) (ForkOS old) =-    let tidmap' = I.insert (fromId old) nexttid tidmap-        nexttid' = nexttid + 1-    in ((tidmap', nexttid', cridmap, nextcrid), ForkOS (toId nexttid))-  updateAction s@(tidmap, _, _, _) (PutMVar mvid olds) =-    (s, PutMVar mvid (map (renumbered tidmap) olds))-  updateAction s@(tidmap, _, _, _) (TryPutMVar mvid b olds) =-    (s, TryPutMVar mvid b (map (renumbered tidmap) olds))-  updateAction s@(tidmap, _, _, _) (TakeMVar mvid olds) =-    (s, TakeMVar mvid (map (renumbered tidmap) olds))-  updateAction s@(tidmap, _, _, _) (TryTakeMVar mvid b olds) =-    (s, TryTakeMVar mvid b (map (renumbered tidmap) olds))-  updateAction (tidmap, nexttid, cridmap, nextcrid) (NewCRef old) =-    let cridmap' = I.insert (fromId old) nextcrid cridmap-        nextcrid' = nextcrid + 1-    in ((tidmap, nexttid, cridmap', nextcrid'), NewCRef (toId nextcrid))-  updateAction s@(_, _, cridmap, _) (ReadCRef old) =-    (s, ReadCRef (renumbered cridmap old))-  updateAction s@(_, _, cridmap, _) (ReadCRefCas old) =-    (s, ReadCRefCas (renumbered cridmap old))-  updateAction s@(_, _, cridmap, _) (ModCRef old) =-    (s, ModCRef (renumbered cridmap old))-  updateAction s@(_, _, cridmap, _) (ModCRefCas old) =-    (s, ModCRefCas (renumbered cridmap old))-  updateAction s@(_, _, cridmap, _) (WriteCRef old) =-    (s, WriteCRef (renumbered cridmap old))-  updateAction s@(_, _, cridmap, _) (CasCRef old b) =-    (s, CasCRef (renumbered cridmap old) b)-  updateAction s@(tidmap, _, _, _) (STM tas olds) =-    (s, STM tas (map (renumbered tidmap) olds))-  updateAction s@(tidmap, _, _, _) (ThrowTo old) =-    (s, ThrowTo (renumbered tidmap old))-  updateAction s@(tidmap, _, _, _) (BlockedThrowTo old) =-    (s, BlockedThrowTo (renumbered tidmap old))-  updateAction s act = (s, act)--  renumbered :: (Coercible a Id, Coercible Id a) => I.IntMap Int -> a -> a-  renumbered idmap id_ = toId $ I.findWithDefault (fromId id_) (fromId id_) idmap------------------------------------------------------------------------------------ * Utilities---- | Helper function for constructing IDs of any sort.-toId :: Coercible Id a => Int -> a-toId = coerce . Id Nothing---- | Helper function for deconstructing IDs of any sort.-fromId :: Coercible a Id => a -> Int-fromId a = let (Id _ id_) = coerce a in id_

@@ -167,8 +167,7 @@  -- | Add a new trace to the stack.  This won't work if to-dos aren't explored depth-first. incorporateTrace-  :: MemType-  -> Bool+  :: Bool   -- ^ Whether the \"to-do\" point which was used to create this new   -- execution was conservative or not.   -> Trace@@ -176,10 +175,10 @@   -- and the action performed.   -> DPOR   -> DPOR-incorporateTrace memtype conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where+incorporateTrace conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where   grow state tid trc@((d, _, a):rest) dpor =     let tid'   = tidOf tid d-        state' = updateDepState memtype state tid' a+        state' = updateDepState state tid' a     in case dporNext dpor of          Just (t, child)            | t == tid' ->@@ -200,7 +199,7 @@    -- Construct a new subtree corresponding to a trace suffix.   subtree state tid sleep ((_, _, a):rest) = validateDPOR "incorporateTrace (subtree)" $-    let state' = updateDepState memtype state tid a+    let state' = updateDepState state tid a         sleep' = M.filterWithKey (\t a' -> not $ dependent state' tid a t a') sleep     in DPOR         { dporRunnable = S.fromList $ case rest of@@ -234,8 +233,7 @@ -- runnable, a dependency is imposed between this final action and -- everything else. findBacktrackSteps-  :: MemType-  -> BacktrackFunc+  :: BacktrackFunc   -- ^ Backtracking function. Given a list of backtracking points, and   -- a thread to backtrack to at a specific point in that list, add   -- the new backtracking points. There will be at least one: this@@ -252,12 +250,12 @@   -> Trace   -- ^ The execution trace.   -> [BacktrackStep]-findBacktrackSteps memtype backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where+findBacktrackSteps backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where   -- Walk through the traces one step at a time, building up a list of   -- new backtracking points.   go state allThreads tid bs ((e,i):is) ((d,_,a):ts) =     let tid' = tidOf tid d-        state' = updateDepState memtype state tid' a+        state' = updateDepState state tid' a         this = BacktrackStep           { bcktThreadid   = tid'           , bcktDecision   = d@@ -465,19 +463,18 @@ -- yielded. Furthermore, threads which /will/ yield are ignored in -- preference of those which will not. dporSched-  :: MemType-  -> IncrementalBoundFunc k+  :: IncrementalBoundFunc k   -- ^ Bound function: returns true if that schedule prefix terminated   -- with the lookahead decision fits within the bound.   -> Scheduler (DPORSchedState k)-dporSched memtype boundf = Scheduler $ \prior threads s ->+dporSched boundf = Scheduler $ \prior threads s ->   let     -- The next scheduler state     nextState rest = s       { schedBPoints  = schedBPoints s |> (restrictToBound fst threads', rest)       , schedDepState = nextDepState       }-    nextDepState = let ds = schedDepState s in maybe ds (uncurry $ updateDepState memtype ds) prior+    nextDepState = let ds = schedDepState s in maybe ds (uncurry $ updateDepState ds) prior      -- Pick a new thread to run, not considering bounds. Choose the     -- current thread if available and it hasn't just yielded,@@ -637,20 +634,18 @@   -- thread and if the actions can be interrupted. We can also   -- slightly improve on that by not considering interrupting the   -- normal termination of a thread: it doesn't make a difference.-  (ThrowTo t, WillStop) | t == t2 -> False-  (Stop, WillThrowTo t) | t == t1 -> False-  (ThrowTo t, _)     | t == t2 -> canInterruptL ds t2 l2-  (_, WillThrowTo t) | t == t1 -> canInterrupt  ds t1 a1+  (ThrowTo t, _)     | t == t2 -> canInterruptL ds t2 l2 && l2 /= WillStop+  (_, WillThrowTo t) | t == t1 -> canInterrupt  ds t1 a1 && a1 /= Stop    -- Another worst-case: assume all STM is dependent.   (STM _ _, WillSTM) -> True   (BlockedSTM _, WillSTM) -> True -  -- This is a bit pessimistic: Set/Get are only dependent if the-  -- value set is not the same as the value that will be got, but we-  -- can't know that here. 'dependent' optimises this case.+  -- the number of capabilities is essentially a global shared+  -- variable   (GetNumCapabilities _, WillSetNumCapabilities _) -> True   (SetNumCapabilities _, WillGetNumCapabilities)   -> True+  (SetNumCapabilities _, WillSetNumCapabilities _) -> True    _ -> dependentActions ds (simplifyAction a1) (simplifyLookahead l2) @@ -659,56 +654,37 @@ -- being so great an over-approximation as to be useless! dependentActions :: DepState -> ActionType -> ActionType -> Bool dependentActions ds 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, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> a2 /= UnsynchronisedRead r1-  (UnsynchronisedWrite         r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True-  (PartiallySynchronisedWrite  r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True-  (PartiallySynchronisedModify r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True-  (SynchronisedModify          r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True+  (UnsynchronisedRead _, UnsynchronisedRead _) -> False    -- Unsynchronised writes and synchronisation where the buffer is not   -- empty.   --   -- See [RMMVerification], lemma 5.25.-  (UnsynchronisedWrite r1, PartiallySynchronisedCommit _) | same crefOf && isBuffered ds r1 -> False-  (PartiallySynchronisedCommit _, UnsynchronisedWrite r2) | same crefOf && isBuffered ds r2 -> False+  (UnsynchronisedWrite r1, PartiallySynchronisedCommit r2) | r1 == r2 && isBuffered ds r1 -> False+  (PartiallySynchronisedCommit r1, UnsynchronisedWrite r2) | r1 == r2 && isBuffered ds r1 -> False    -- Unsynchronised reads where a memory barrier would flush a   -- buffered write-  (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered ds r1-  (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered ds r2+  (UnsynchronisedRead r1, _) | isBarrier a2 && isBuffered ds r1 -> True+  (_, UnsynchronisedRead r2) | isBarrier a1 && isBuffered ds r2 -> True    -- Commits and memory barriers must be dependent, as memory barriers   -- (currently) flush in a consistent order.  Alternative orders need   -- to be explored as well.  Perhaps a better implementation of   -- memory barriers would just block every non-commit thread while   -- any buffer is nonempty.-  (PartiallySynchronisedCommit _, _) | isBarrier a2 -> True-  (_, PartiallySynchronisedCommit _) | isBarrier a1 -> True+  (PartiallySynchronisedCommit r1, _) | synchronises a2 r1 -> True+  (_, PartiallySynchronisedCommit r2) | synchronises a1 r2 -> True    -- Two @MVar@ puts are dependent if they're to the same empty   -- @MVar@, and two takes are dependent if they're to the same full   -- @MVar@.-  (SynchronisedWrite v1, SynchronisedWrite v2) -> v1 == v2 && not (isFull ds v1)-  (SynchronisedRead  v1, SynchronisedRead  v2) -> v1 == v2 && isFull ds v1--  (_, _) -> case getSame crefOf of-    -- Two actions on the same CRef where at least one is synchronised-    Just r -> synchronises a1 r || synchronises a2 r-    -- Two actions on the same MVar-    _ -> same mvarOf--  where-    same :: Eq a => (ActionType -> Maybe a) -> Bool-    same = isJust . getSame+  (SynchronisedWrite v1, SynchronisedWrite v2) | v1 == v2 -> not (isFull ds v1)+  (SynchronisedRead  v1, SynchronisedRead  v2) | v1 == v2 -> isFull ds v1+  (SynchronisedWrite v1, SynchronisedRead  v2) | v1 == v2 -> True+  (SynchronisedRead  v1, SynchronisedWrite v2) | v1 == v2 -> True -    getSame :: Eq a => (ActionType -> Maybe a) -> Maybe a-    getSame f =-      let f1 = f a1-          f2 = f a2-      in if f1 == f2 then f1 else Nothing+  (_, _) -> maybe False (\r -> Just r == crefOf a2) (crefOf a1)  ------------------------------------------------------------------------------- -- ** Dependency function state@@ -737,20 +713,19 @@  -- | Update the dependency state with the action that has just -- happened.-updateDepState :: MemType -> DepState -> ThreadId -> ThreadAction -> DepState-updateDepState memtype depstate tid act = DepState-  { depCRState   = updateCRState memtype act $ depCRState   depstate-  , depMVState   = updateMVState         act $ depMVState   depstate-  , depMaskState = updateMaskState tid   act $ depMaskState depstate+updateDepState :: DepState -> ThreadId -> ThreadAction -> DepState+updateDepState depstate tid act = DepState+  { depCRState   = updateCRState       act $ depCRState   depstate+  , depMVState   = updateMVState       act $ depMVState   depstate+  , depMaskState = updateMaskState tid act $ depMaskState depstate   }  -- | Update the @CRef@ buffer state with the action that has just -- happened.-updateCRState :: MemType -> ThreadAction -> Map CRefId Bool -> Map CRefId Bool-updateCRState SequentialConsistency _ = const M.empty-updateCRState _ (CommitCRef _ r) = M.delete r-updateCRState _ (WriteCRef    r) = M.insert r True-updateCRState _ ta+updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool+updateCRState (CommitCRef _ r) = M.delete r+updateCRState (WriteCRef    r) = M.insert r True+updateCRState ta   | isBarrier $ simplifyAction ta = const M.empty   | otherwise = id 

@@ -150,44 +150,6 @@    , learlyExit -  -- ** Representative traces--  -- | There may be many different execution traces which give rise to-  -- the same result, but some traces can be more complex than others.-  ---  -- By supplying an equality predicate on results, all but the-  -- simplest trace for each distinct result can be thrown away.-  ---  -- __Slippage:__ Just comparing results can lead to different errors-  -- which happen to have the same result comparing as equal.  For-  -- example, all deadlocks have the same result (@Left Deadlock@),-  -- but may have different causes.  See issue @#241@.--  , lequality--  -- ** Trace simplification--  -- | There may be many ways to reveal the same bug, and dejafu is-  -- not guaranteed to find the simplest way first.  This is-  -- particularly problematic with random testing, where the schedules-  -- generated tend to involve a lot of context switching.-  -- Simplification produces smaller traces, which still have the same-  -- essential behaviour.-  ---  -- __Performance:__ Simplification in dejafu, unlike shrinking in-  -- most random testing tools, is quite cheap.  Simplification is-  -- guaranteed to preserve semantics, so the test case does not need-  -- to be re-run repeatedly during the simplification process.  The-  -- test case is re-run only /once/, after the process completes, for-  -- implementation reasons.-  ---  -- Concurrency tests can be rather large, however.  So-  -- simplification is disabled by default, and it is /highly/-  -- recommended to also use 'lequality', to reduce the number of-  -- traces to simplify.--  , lsimplify-   -- ** Debug output    -- | You can opt to receive debugging messages by setting debugging@@ -235,8 +197,6 @@   , _debugShow = Nothing   , _debugPrint = Nothing   , _earlyExit = Nothing-  , _equality = Nothing-  , _simplify = False   }  -------------------------------------------------------------------------------@@ -406,24 +366,6 @@ -- @since 1.2.0.0 learlyExit :: Lens' (Settings n a) (Maybe (Either Failure a -> Bool)) learlyExit afb s = (\b -> s {_earlyExit = b}) <$> afb (_earlyExit s)------------------------------------------------------------------------------------ Representative traces---- | A lens into the equality predicate.------ @since unreleased-lequality :: Lens' (Settings n a) (Maybe (a -> a -> Bool))-lequality afb s = (\b -> s {_equality = b}) <$> afb (_equality s)------------------------------------------------------------------------------------ Simplification---- | A lens into the simplify flag.------ @since unreleased-lsimplify :: Lens' (Settings n a) Bool-lsimplify afb s = (\b -> s {_simplify = b}) <$> afb (_simplify s)  ------------------------------------------------------------------------------- -- Debug output

@@ -1,6 +1,6 @@ -- |--- Module      : Test.DejaFu.Utils--- Copyright   : (c) 2017--2018 Michael Walker+-- Module      : Test.DejaFu.utils+-- Copyright   : (c) 2017 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental@@ -18,13 +18,6 @@  ------------------------------------------------------------------------------- -- * Traces---- | Turn a 'Trace' into an abbreviated form.------ @since unreleased-toTIdTrace :: Trace -> [(ThreadId, ThreadAction)]-toTIdTrace =-  tail . scanl (\(t, _) (d, _, a) -> (tidOf t d, a)) (initialThread, undefined)  -- | Pretty-print a trace, including a key of the thread IDs (not -- including thread 0). Each line of the key is indented by two

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             1.3.0.1+version:             1.3.0.2 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.3.0.1+  tag:      dejafu-1.3.0.2  library   exposed-modules:     Test.DejaFu@@ -52,7 +52,6 @@                      , Test.DejaFu.Conc.Internal.STM                      , Test.DejaFu.Conc.Internal.Threading                      , Test.DejaFu.Internal-                     , Test.DejaFu.SCT.Internal                      , Test.DejaFu.SCT.Internal.DPOR                      , Test.DejaFu.SCT.Internal.Weighted