diff --git a/CHANGELOG.rst b/CHANGELOG.rst --- a/CHANGELOG.rst +++ b/CHANGELOG.rst @@ -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) 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,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 diff --git a/Test/DejaFu/Internal.hs b/Test/DejaFu/Internal.hs --- a/Test/DejaFu/Internal.hs +++ b/Test/DejaFu/Internal.hs @@ -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. diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -1,10 +1,13 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE LambdaCase #-} + -- | -- Module : Test.DejaFu.SCT -- Copyright : (c) 2015--2018 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- 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 diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs deleted file mode 100644 --- a/Test/DejaFu/SCT/Internal.hs +++ /dev/null @@ -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 --- 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,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 diff --git a/Test/DejaFu/Settings.hs b/Test/DejaFu/Settings.hs --- a/Test/DejaFu/Settings.hs +++ b/Test/DejaFu/Settings.hs @@ -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 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--2018 Michael Walker +-- Module : Test.DejaFu.utils +-- Copyright : (c) 2017 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- 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 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.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