dejafu 1.3.1.0 → 1.3.2.0

raw patch · 17 files changed

+564/−100 lines, 17 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.rst +27/−0
• LICENSE +1/−1
• Test/DejaFu/Conc.hs +1/−15
• Test/DejaFu/Conc/Internal.hs +15/−1
• Test/DejaFu/Conc/Internal/Common.hs +1/−1
• Test/DejaFu/Conc/Internal/Memory.hs +7/−4
• Test/DejaFu/Conc/Internal/STM.hs +1/−1
• Test/DejaFu/Conc/Internal/Threading.hs +1/−1
• Test/DejaFu/Internal.hs +3/−0
• Test/DejaFu/Refinement.hs +1/−1
• Test/DejaFu/SCT.hs +9/−50
• Test/DejaFu/SCT/Internal.hs +389/−0
• Test/DejaFu/SCT/Internal/DPOR.hs +23/−19
• Test/DejaFu/Schedule.hs +1/−1
• Test/DejaFu/Settings.hs +71/−0
• Test/DejaFu/Utils.hs +9/−2
• dejafu.cabal +4/−3

@@ -7,6 +7,33 @@ .. _PVP: https://pvp.haskell.org/  +1.3.2.0 (2018-03-12)+--------------------++* Git: :tag:`dejafu-1.3.2.0`+* Hackage: :hackage:`dejafu-1.3.2.0`++Added+~~~~~++* (:issue:`183`) SCT settings for trace simplification:++    * ``Test.DejaFu.Settings.lequality``+    * ``Test.DejaFu.Settings.lsimplify``++* (:pull:`248`) ``Test.DejaFu.Utils.toTIdTrace`` to extract thread IDs+  from a trace.++* (:pull:`248`) SCT setting to make some recoverable errors fatal:+  ``Test.DejaFu.Settings.ldebugFatal``++Performance+~~~~~~~~~~~++* (:pull:`248`) Prune some unnecessary interleavings of ``CRef``+  actions in systematic testing when using sequential consistency.++ 1.3.1.0 (2018-03-11) -------------------- 

@@ -1,4 +1,4 @@-Copyright (c) 2015--2017, Michael Walker <mike@barrucadu.co.uk>+Copyright (c) 2015--2018, Michael Walker <mike@barrucadu.co.uk>  Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the

@@ -7,7 +7,7 @@  -- | -- Module      : Test.DejaFu.Conc--- Copyright   : (c) 2016--2017 Michael Walker+-- Copyright   : (c) 2016--2018 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental@@ -359,20 +359,6 @@ --     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

@@ -4,7 +4,7 @@  -- | -- Module      : Test.DejaFu.Conc.Internal--- Copyright   : (c) 2016--2017 Michael Walker+-- Copyright   : (c) 2016--2018 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental@@ -55,6 +55,20 @@   -- execution.   , finalTrace :: SeqTrace   , finalDecision :: Maybe (ThreadId, ThreadAction)+  }++-- | 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.   }  -- | Run a concurrent computation with a given 'Scheduler' and initial

@@ -4,7 +4,7 @@  -- | -- Module      : Test.DejaFu.Conc.Internal.Common--- Copyright   : (c) 2016--2017 Michael Walker+-- Copyright   : (c) 2016--2018 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental

@@ -4,7 +4,7 @@  -- | -- Module      : Test.DejaFu.Conc.Internal.Memory--- Copyright   : (c) 2016--2017 Michael Walker+-- Copyright   : (c) 2016--2018 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental@@ -131,15 +131,18 @@ -- | 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 = [ (ThreadId (Id Nothing . negate $ commitTidOf k), mkthread c)+  phantoms = [ (uncurry commitThreadId 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 -  commitTidOf (ThreadId (Id _ t), Nothing) = t + 1-  commitTidOf (ThreadId (Id _ t), Just (CRefId (Id _ c))) = t + 1 + c * 10000+-- | 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  -- | Remove phantom threads. delCommitThreads :: Threads n r -> Threads n r

@@ -8,7 +8,7 @@  -- | -- Module      : Test.DejaFu.Conc.Internal.STM--- Copyright   : (c) 2017 Michael Walker+-- Copyright   : (c) 2017--2018 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental

@@ -3,7 +3,7 @@  -- | -- Module      : Test.DejaFu.Conc.Internal.Threading--- Copyright   : (c) 2016--2017 Michael Walker+-- Copyright   : (c) 2016--2018 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental

@@ -39,7 +39,10 @@   , _discard :: Maybe (Either Failure a -> Maybe Discard)   , _debugShow :: Maybe (a -> String)   , _debugPrint :: Maybe (String -> n ())+  , _debugFatal :: Bool   , _earlyExit :: Maybe (Either Failure a -> Bool)+  , _equality :: Maybe (a -> a -> Bool)+  , _simplify  :: Bool   }  -- | How to explore the possible executions of a concurrent program.

@@ -7,7 +7,7 @@  -- | -- Module      : Test.DejaFu.Refinement--- Copyright   : (c) 2017 Michael Walker+-- Copyright   : (c) 2017--2018 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental

@@ -1,13 +1,10 @@-{-# 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 : BangPatterns, LambdaCase+-- Portability : portable -- -- Systematic testing for concurrent computations. module Test.DejaFu.SCT@@ -50,6 +47,7 @@  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@@ -199,13 +197,13 @@          check = findSchedulePrefix -        step dp (prefix, conservative, sleep) run = do+        step run dp (prefix, conservative, sleep) = do           (res, s, trace) <- run-            (dporSched (cBound cb0))+            (dporSched (_memtype settings) (cBound cb0))             (initialDPORSchedState sleep prefix) -          let bpoints = findBacktrackSteps (cBacktrack cb0) (schedBoundKill s) (schedBPoints s) trace-          let newDPOR = incorporateTrace conservative trace dp+          let bpoints = findBacktrackSteps (_memtype settings) (cBacktrack cb0) (schedBoundKill s) (schedBPoints s) trace+          let newDPOR = incorporateTrace (_memtype settings) conservative trace dp            pure $ if schedIgnore s                  then (force newDPOR, Nothing)@@ -218,7 +216,7 @@         check (_, 0) = Nothing         check s = Just s -        step _ (g, n) run = do+        step run _ (g, n) = do           (res, s, trace) <- run             (randSched $ \g' -> (1, g'))             (initialRandSchedState Nothing g)@@ -231,8 +229,8 @@         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+        step run s (g, n, 0, _) = step run s (g, n, max 1 use0, M.empty)+        step run _ (g, n, use, ws) = do           (res, s, trace) <- run             (randSched $ randomR (1, 50))             (initialRandSchedState (Just ws) g)@@ -506,45 +504,6 @@ 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

@@ -0,0 +1,389 @@+{-# 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        (Context(..), DCSnapshot(..))+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'Snap snap+        Just (Left f, trace) -> pure [(Left f, trace)]+        _ -> do+          debugFatal "Failed to construct snapshot, continuing without."+          sct'Full+    | otherwise = sct'Full+  where+    sct'Full = sct'+      settings+      (s0 [initialThread])+      sfun+      (srun runFull)+      runFull+      (toId 1)+      (toId 1)++    sct'Snap snap = let idsrc = cIdSource (dcsContext snap) in sct'+      settings+      (s0 (fst (threadsFromDCSnapshot snap)))+      sfun+      (srun (runSnap snap))+      (runSnap snap)+      (toId $ 1 + fst (_tids  idsrc))+      (toId $ 1 + fst (_crids idsrc))++    runFull sched s = runConcurrent sched (_memtype settings) s conc+    runSnap snap sched s = runWithDCSnapshot sched (_memtype settings) s snap++    debugFatal = if _debugFatal settings then fatal "sct" else debugPrint+    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+  -> ThreadId+  -- ^ The first available @ThreadId@+  -> CRefId+  -- ^ The first available @CRefId@+  -> n [(Either Failure a, Trace)]+sct' settings s0 sfun srun run nextTId nextCRId = 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 nextTId nextCRId 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+  -> ThreadId+  -- ^ The first available @ThreadId@+  -> CRefId+  -- ^ The first available @CRefId@+  -> Either Failure a+  -- ^ The expected result+  -> Trace+  -> n (Either Failure a, Trace)+simplifyExecution settings run nextTId nextCRId 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 (fixup 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+            debugFatal ("Got a different result after simplifying: '" ++ p res ++ "' /= '" ++ p res' ++ "'")+            pure (res, trace)+  where+    tidTrace = toTIdTrace trace+    simplifiedTrace = simplify (_memtype settings) tidTrace+    fixup = renumber (_memtype settings) (fromId nextTId) (fromId nextCRId)++    debugFatal = if _debugFatal settings then fatal "sct" else debugPrint+    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_

@@ -152,7 +152,8 @@  -- | Add a new trace to the stack.  This won't work if to-dos aren't explored depth-first. incorporateTrace-  :: Bool+  :: MemType+  -> Bool   -- ^ Whether the \"to-do\" point which was used to create this new   -- execution was conservative or not.   -> Trace@@ -160,10 +161,10 @@   -- and the action performed.   -> DPOR   -> DPOR-incorporateTrace conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where+incorporateTrace memtype 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 state tid' a+        state' = updateDepState memtype state tid' a     in case dporNext dpor of          Just (t, child)            | t == tid' ->@@ -184,7 +185,7 @@    -- Construct a new subtree corresponding to a trace suffix.   subtree state tid sleep ((_, _, a):rest) = validateDPOR "incorporateTrace (subtree)" $-    let state' = updateDepState state tid a+    let state' = updateDepState memtype state tid a         sleep' = M.filterWithKey (\t a' -> not $ dependent state' tid a t a') sleep     in DPOR         { dporRunnable = S.fromList $ case rest of@@ -218,7 +219,8 @@ -- runnable, a dependency is imposed between this final action and -- everything else. findBacktrackSteps-  :: BacktrackFunc+  :: MemType+  -> 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@@ -235,12 +237,12 @@   -> Trace   -- ^ The execution trace.   -> [BacktrackStep]-findBacktrackSteps backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where+findBacktrackSteps memtype 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 state tid' a+        state' = updateDepState memtype state tid' a         this = BacktrackStep           { bcktThreadid   = tid'           , bcktDecision   = d@@ -438,18 +440,19 @@ -- yielded. Furthermore, threads which /will/ yield are ignored in -- preference of those which will not. dporSched-  :: IncrementalBoundFunc k+  :: MemType+  -> IncrementalBoundFunc k   -- ^ Bound function: returns true if that schedule prefix terminated   -- with the lookahead decision fits within the bound.   -> Scheduler (DPORSchedState k)-dporSched boundf = Scheduler $ \prior threads s ->+dporSched memtype 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 ds) prior+    nextDepState = let ds = schedDepState s in maybe ds (uncurry $ updateDepState memtype ds) prior      -- Pick a new thread to run, not considering bounds. Choose the     -- current thread if available and it hasn't just yielded,@@ -688,19 +691,20 @@  -- | Update the dependency state with the action that has just -- happened.-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+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   }  -- | Update the @CRef@ buffer state with the action that has just -- happened.-updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool-updateCRState (CommitCRef _ r) = M.delete r-updateCRState (WriteCRef    r) = M.insert r True-updateCRState ta+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   | isBarrier $ simplifyAction ta = const M.empty   | otherwise = id 

@@ -1,6 +1,6 @@ -- | -- Module      : Test.DejaFu.Schedule--- Copyright   : (c) 2016--2017 Michael Walker+-- Copyright   : (c) 2016--2018 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental

@@ -150,6 +150,44 @@    , 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@@ -160,6 +198,12 @@   , ldebugShow   , ldebugPrint +  -- | The debugging output includes both recoverable errors and+  -- informative messages.  Those recoverable errors can be made fatal+  -- instead.++  , ldebugFatal+   -- * Lens helpers   , get   , set@@ -196,7 +240,10 @@   , _discard = Nothing   , _debugShow = Nothing   , _debugPrint = Nothing+  , _debugFatal = False   , _earlyExit = Nothing+  , _equality = Nothing+  , _simplify = False   }  -------------------------------------------------------------------------------@@ -368,6 +415,24 @@ learlyExit afb s = (\b -> s {_earlyExit = b}) <$> afb (_earlyExit s)  -------------------------------------------------------------------------------+-- Representative traces++-- | A lens into the equality predicate.+--+-- @since 1.3.2.0+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 1.3.2.0+lsimplify :: Lens' (Settings n a) Bool+lsimplify afb s = (\b -> s {_simplify = b}) <$> afb (_simplify s)++------------------------------------------------------------------------------- -- Debug output  -- | A lens into the debug 'show' function.@@ -381,6 +446,12 @@ -- @since 1.2.0.0 ldebugPrint :: Lens' (Settings n a) (Maybe (String -> n ())) ldebugPrint afb s = (\b -> s {_debugPrint = b}) <$> afb (_debugPrint s)++-- | A lens into the make-recoverable-errors-fatal flag.+--+-- @since 1.3.2.0+ldebugFatal :: Lens' (Settings n a) Bool+ldebugFatal afb s = (\b -> s {_debugFatal = b}) <$> afb (_debugFatal s)  ------------------------------------------------------------------------------- -- Lens helpers

@@ -1,6 +1,6 @@ -- |--- Module      : Test.DejaFu.utils--- Copyright   : (c) 2017 Michael Walker+-- Module      : Test.DejaFu.Utils+-- Copyright   : (c) 2017--2018 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental@@ -18,6 +18,13 @@  ------------------------------------------------------------------------------- -- * Traces++-- | Turn a 'Trace' into an abbreviated form.+--+-- @since 1.3.2.0+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.1.0+version:             1.3.2.0 synopsis:            A library for unit-testing concurrent programs.  description:@@ -20,7 +20,7 @@ license-file:        LICENSE author:              Michael Walker maintainer:          mike@barrucadu.co.uk-copyright:           (c) 2015--2017 Michael Walker+copyright:           (c) 2015--2018 Michael Walker category:            Concurrency build-type:          Simple extra-source-files:  README.markdown CHANGELOG.rst@@ -33,7 +33,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-1.3.1.0+  tag:      dejafu-1.3.2.0  library   exposed-modules:     Test.DejaFu@@ -52,6 +52,7 @@                      , 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