diff --git a/CHANGELOG.rst b/CHANGELOG.rst --- a/CHANGELOG.rst +++ b/CHANGELOG.rst @@ -6,6 +6,40 @@ .. _PVP: https://pvp.haskell.org/ +unreleased +---------- + +Added +~~~~~ + +* (:issue:`183`) SCT settings for trace simplification: + + * ``Test.DejaFu.Settings.lequality`` + * ``Test.DejaFu.Settings.lsimplify`` + +* (:issue:`183`) ``Test.DejaFu.Utils.toTIdTrace`` to extract thread + IDs from a trace. + +Performance +~~~~~~~~~~~ + +* (:issue:`183`) Prune some unnecessary interleavings of ``CRef`` + actions in systematic testing when using sequential consistency. + + +1.3.0.1 (2018-03-08) +-------------------- + +* Git: :tag:`dejafu-1.3.0.1` +* Hackage: :hackage:`dejafu-1.3.0.1` + +Fixed +~~~~~ + +* (:pull:`242`) A compilation error when building with + :hackage:`exceptions-0.9.0`. + + 1.3.0.0 (2018-03-06) -------------------- diff --git a/Test/DejaFu/Conc.hs b/Test/DejaFu/Conc.hs --- a/Test/DejaFu/Conc.hs +++ b/Test/DejaFu/Conc.hs @@ -134,9 +134,9 @@ #if MIN_VERSION_exceptions(0,9,0) -- from https://github.com/fpco/stackage/issues/3315#issuecomment-368583481 - generalBracket acquire release cleanup use = mask $ \unmasked -> do + generalBracket acquire release cleanup use = Ca.mask $ \unmasked -> do resource <- acquire - result <- unmasked (use resource) `catch` (\e -> cleanup resource e >> throwM e) + result <- unmasked (use resource) `Ca.catch` (\e -> cleanup resource e >> Ca.throwM e) _ <- release resource pure result #endif diff --git a/Test/DejaFu/Conc/Internal/Memory.hs b/Test/DejaFu/Conc/Internal/Memory.hs --- a/Test/DejaFu/Conc/Internal/Memory.hs +++ b/Test/DejaFu/Conc/Internal/Memory.hs @@ -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 diff --git a/Test/DejaFu/Internal.hs b/Test/DejaFu/Internal.hs --- a/Test/DejaFu/Internal.hs +++ b/Test/DejaFu/Internal.hs @@ -37,6 +37,8 @@ , _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. diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -1,13 +1,10 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE LambdaCase #-} - -- | -- Module : Test.DejaFu.SCT -- Copyright : (c) 2015--2018 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- 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 diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs new file mode 100644 --- /dev/null +++ b/Test/DejaFu/SCT/Internal.hs @@ -0,0 +1,359 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} + +-- | +-- Module : Test.DejaFu.SCT.Internal +-- Copyright : (c) 2018 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- 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_ diff --git a/Test/DejaFu/SCT/Internal/DPOR.hs b/Test/DejaFu/SCT/Internal/DPOR.hs --- a/Test/DejaFu/SCT/Internal/DPOR.hs +++ b/Test/DejaFu/SCT/Internal/DPOR.hs @@ -167,7 +167,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 @@ -175,10 +176,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' -> @@ -199,7 +200,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 @@ -233,7 +234,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 @@ -250,12 +252,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 @@ -463,18 +465,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, @@ -734,19 +737,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 diff --git a/Test/DejaFu/Settings.hs b/Test/DejaFu/Settings.hs --- a/Test/DejaFu/Settings.hs +++ b/Test/DejaFu/Settings.hs @@ -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 @@ -197,6 +235,8 @@ , _debugShow = Nothing , _debugPrint = Nothing , _earlyExit = Nothing + , _equality = Nothing + , _simplify = False } ------------------------------------------------------------------------------- @@ -366,6 +406,24 @@ -- @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 diff --git a/Test/DejaFu/Utils.hs b/Test/DejaFu/Utils.hs --- a/Test/DejaFu/Utils.hs +++ b/Test/DejaFu/Utils.hs @@ -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 -- Stability : experimental @@ -18,6 +18,13 @@ ------------------------------------------------------------------------------- -- * 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 diff --git a/dejafu.cabal b/dejafu.cabal --- a/dejafu.cabal +++ b/dejafu.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu -version: 1.3.0.0 +version: 1.3.0.1 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.0 + tag: dejafu-1.3.0.1 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