dejafu 0.7.1.2 → 0.7.1.3

raw patch · 5 files changed

+159/−128 lines, 5 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +19/−1
• Test/DejaFu/SCT.hs +72/−60
• Test/DejaFu/SCT/Internal.hs +65/−64
• Test/DejaFu/STM/Internal.hs +1/−1
• dejafu.cabal +2/−2

@@ -7,8 +7,26 @@ *de facto* standard Haskell versioning scheme.  +0.7.1.3+-------++- **Date**    2017-09-08+- **Git tag** [dejafu-0.7.1.3][]+- **Hackage** https://hackage.haskell.org/package/dejafu-0.7.1.3++### Miscellaneous++- Aborted STM transactions are now rolled back correctly (issue #111).+- Slightly improved run-time of systematic testing.++[dejafu-0.7.1.3]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.1.3+++---------------------------------------------------------------------------------------------------++ 0.7.1.2-----------+-------  - **Date**    2017-08-21 - **Git tag** [dejafu-0.7.1.2][]

@@ -111,6 +111,7 @@ import           Control.Monad.Ref        (MonadRef) import           Data.List                (foldl') import qualified Data.Map.Strict          as M+import           Data.Maybe               (fromMaybe) import           Data.Set                 (Set) import qualified Data.Set                 as S import           System.Random            (RandomGen, randomR)@@ -354,11 +355,11 @@   }  -- | Combination bound function-cBound :: Bounds -> BoundFunc+cBound :: Bounds -> IncrementalBoundFunc (((Int, Maybe ThreadId), M.Map ThreadId Int), Int) cBound (Bounds pb fb lb) =-  maybe trueBound pBound pb &+&-  maybe trueBound fBound fb &+&-  maybe trueBound lBound lb+  maybe (trueBound (0, Nothing)) pBound pb &+&+  maybe (trueBound M.empty)      fBound fb &+&+  maybe (trueBound 0)            lBound lb  -- | Combination backtracking function. Add all backtracking points -- corresponding to enabled bound functions.@@ -384,8 +385,10 @@  -- | Pre-emption bound function. This does not count pre-emptive -- context switches to a commit thread.-pBound :: PreemptionBound -> BoundFunc-pBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb+pBound :: PreemptionBound -> IncrementalBoundFunc (Int, Maybe ThreadId)+pBound (PreemptionBound pb) k prior lhead =+  let k'@(pcount, _) = preEmpCountInc (fromMaybe (0, Nothing) k) prior lhead+  in if pcount <= pb then Just k' else Nothing  -- | Add a backtrack point, and also conservatively add one prior to -- the most recent transition before that point. This may result in@@ -420,8 +423,10 @@   rnf (FairBound i) = rnf i  -- | Fair bound function-fBound :: FairBound -> BoundFunc-fBound (FairBound fb) ts (_, l) = maxYieldCountDiff ts l <= fb+fBound :: FairBound -> IncrementalBoundFunc (M.Map ThreadId Int)+fBound (FairBound fb) k prior lhead =+  let k' = yieldCountInc (fromMaybe M.empty k) prior lhead+  in if maxDiff (M.elems k') <= fb then Just k' else Nothing  -- | Add a backtrack point. If the thread isn't runnable, or performs -- a release operation, add all runnable threads.@@ -443,8 +448,10 @@   rnf (LengthBound i) = rnf i  -- | Length bound function-lBound :: LengthBound -> BoundFunc-lBound (LengthBound lb) ts _ = length ts < lb+lBound :: LengthBound -> IncrementalBoundFunc Int+lBound (LengthBound lb) len _ _ =+  let len' = maybe 1 (+1) len+  in if len' < lb then Just len' else Nothing  -- | Add a backtrack point. If the thread isn't runnable, add all -- runnable threads.@@ -505,7 +512,7 @@        if schedIgnore s         then go (force newDPOR)-        else checkDiscard discard res trace $ go (force (addBacktracks bpoints newDPOR))+        else checkDiscard discard res trace $ go (force (incorporateBacktrackSteps bpoints newDPOR))      Nothing -> pure [] @@ -518,9 +525,6 @@   -- Incorporate a trace into the DPOR tree.   addTrace = incorporateTrace memtype -  -- Incorporate the new backtracking steps into the DPOR tree.-  addBacktracks = incorporateBacktrackSteps (cBound cb)- -- | SCT via uniform random scheduling. -- -- Schedules are generated by assigning to each new thread a random@@ -619,63 +623,71 @@ ------------------------------------------------------------------------------- -- Utilities +-- | An incremental version of 'preEmpCount', going one step at a time.+preEmpCountInc+  :: (Int, Maybe ThreadId)+  -- ^ The number of preemptions so far and, if currently executing a+  -- commit thread, what the prior thread was.+  -> Maybe (ThreadId, ThreadAction)+  -- ^ What just happened.+  -> (Decision, a)+  -- ^ What's coming up.+  -> (Int, Maybe ThreadId)+preEmpCountInc (sofar, lastnoncommit) prior (d, _) = case (prior, d) of+    (Just (tid, _),   Start    tnext) -> cswitch tid tnext False+    (Just (tid, act), SwitchTo tnext) -> cswitch tid tnext (not (didYield act))+    (_, Continue) -> (sofar, lastnoncommit)+    (Nothing, _)  -> (sofar, lastnoncommit)+  where+    cswitch tid tnext isPreemptive+      | isCommitThread tnext = (sofar, if isCommitThread tid then lastnoncommit else Just tid)+      | isCommitThread tid   = (if lastnoncommit == Just tnext then sofar else sofar + 1, Nothing)+      | otherwise = (if isPreemptive then sofar + 1 else sofar, Nothing)++    isCommitThread = (< initialThread)++-- | An incremental count of yields, going one step at a time.+yieldCountInc+  :: M.Map ThreadId Int+  -- ^ The number of yields of each thread so far+  -> Maybe (ThreadId, a)+  -- ^ What just happened.+  -> (Decision, Lookahead)+  -- ^ What's coming up.+  -> M.Map ThreadId Int+yieldCountInc sofar prior (d, lnext) = case prior of+    Just (tid, _) -> ycount (tidOf tid d)+    Nothing       -> ycount initialThread+  where+    ycount tnext = case lnext of+      WillYield -> M.alter (Just . maybe 1 (+1)) tnext sofar+      _ -> M.alter (Just . maybe 0 id) tnext sofar+ -- | Determine if an action is a commit or not. isCommitRef :: ThreadAction -> Bool isCommitRef (CommitCRef _ _) = True isCommitRef _ = False --- | Extra threads created in a fork.-forkTids :: ThreadAction -> [ThreadId]-forkTids (Fork t) = [t]-forkTids _ = []---- | Count the number of yields by a thread in a schedule prefix.-yieldCount :: ThreadId-  -- ^ The thread to count yields for.-  -> [(Decision, ThreadAction)]-  -> Lookahead-  -> Int-yieldCount tid ts l = go initialThread ts where-  go t ((Start    t', act):rest) = go' t t' act rest-  go t ((SwitchTo t', act):rest) = go' t t' act rest-  go t ((Continue,    act):rest) = go' t t  act rest-  go t []-    | t == tid && willYield l = 1-    | otherwise = 0--  {-# INLINE go' #-}-  go' t t' act rest-    | t == tid && didYield act = 1 + go t' rest-    | otherwise = go t' rest---- | Get the maximum difference between the yield counts of all--- threads in this schedule prefix.-maxYieldCountDiff :: [(Decision, ThreadAction)]-  -> Lookahead-  -> Int-maxYieldCountDiff ts l = go 0 yieldCounts where-  go m (yc:ycs) =-    let m' = m `max` foldl' (go' yc) 0 ycs-    in go m' ycs+-- | Get the maximum difference between two ints in a list.+maxDiff :: [Int] -> Int+maxDiff = go 0 where+  go m (x:xs) =+    let m' = m `max` foldl' (go' x) 0 xs+    in go m' xs   go m [] = m-  go' yc0 m yc = m `max` abs (yc0 - yc)--  yieldCounts = [yieldCount t ts l | t <- allTids ts]--  -- All the threads created during the lifetime of the system.-  allTids ((_, act):rest) =-    let tids' = forkTids act-    in if null tids' then allTids rest else tids' ++ allTids rest-  allTids [] = [initialThread]+  go' x0 m x = m `max` abs (x0 - x)  -- | The \"true\" bound, which allows everything.-trueBound :: BoundFunc-trueBound _ _ = True+trueBound :: k -> IncrementalBoundFunc k+trueBound k _ _ _ = Just k  -- | Combine two bounds into a larger bound, where both must be -- satisfied.-(&+&) :: BoundFunc -> BoundFunc -> BoundFunc-(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl+(&+&) :: IncrementalBoundFunc k1 -> IncrementalBoundFunc k2 -> IncrementalBoundFunc (k1, k2)+(&+&) f1 f2 ks prior lhead =+  let k1' = f1 (fst <$> ks) prior lhead+      k2' = f2 (snd <$> ks) prior lhead+  in (,) <$> k1' <*> k2'  -- | Apply the discard function. checkDiscard :: Functor f => (a -> Maybe Discard) -> a -> [b] -> f [(a, [b])] -> f [(a, [b])]

@@ -1,10 +1,12 @@+{-# LANGUAGE TupleSections #-}+ -- | -- Module      : Test.DejaFu.SCT.Internal -- Copyright   : (c) 2016 Michael Walker -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : portable+-- Portability : TupleSections -- -- Internal types and functions for dynamic partial-order -- reduction. This module is NOT considered to form part of the public@@ -17,7 +19,7 @@ import qualified Data.Foldable        as F import           Data.Function        (on) import           Data.List            (nubBy, partition, sortOn)-import           Data.List.NonEmpty   (NonEmpty(..), toList)+import           Data.List.NonEmpty   (toList) import           Data.Map.Strict      (Map) import qualified Data.Map.Strict      as M import           Data.Maybe           (catMaybes, fromJust, fromMaybe, isJust,@@ -216,9 +218,9 @@   -> Bool   -- ^ Whether the computation was aborted due to no decisions being   -- in-bounds.-  -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])-  -- ^ A sequence of threads at each step: the nonempty list of-  -- runnable threads (with lookahead values), and the list of threads+  -> Seq ([(ThreadId, Lookahead)], [ThreadId])+  -- ^ A sequence of threads at each step: the list of runnable+  -- in-bound threads (with lookahead values), and the list of threads   -- still to try. The reason for the two separate lists is because   -- the threads chosen to try will be dependent on the specific   -- domain.@@ -235,11 +237,11 @@           { bcktThreadid   = tid'           , bcktDecision   = d           , bcktAction     = a-          , bcktRunnable   = M.fromList . toList $ e+          , bcktRunnable   = M.fromList e           , bcktBacktracks = M.fromList $ map (\i' -> (i', False)) i           , bcktState      = state'           }-        bs' = doBacktrack killsEarly allThreads' (toList e) (bs++[this])+        bs' = doBacktrack killsEarly allThreads' e (bs++[this])         runnable = S.fromList (M.keys $ bcktRunnable this)         allThreads' = allThreads `S.union` runnable         killsEarly = null ts && boundKill@@ -280,53 +282,44 @@     in backtrack bs idxs  -- | Add new backtracking points, if they have not already been--- visited, fit into the bound, and aren't in the sleep set.-incorporateBacktrackSteps-  :: ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool)-  -- ^ Bound function: returns true if that schedule prefix terminated-  -- with the lookahead decision fits within the bound.-  -> [BacktrackStep]-  -- ^ Backtracking steps identified by 'findBacktrackSteps'.-  -> DPOR-  -> DPOR-incorporateBacktrackSteps bv = go Nothing [] where-  go priorTid pref (b:bs) dpor =-    let dpor' = doBacktrack priorTid pref b dpor-        tid   = bcktThreadid b-        pref' = pref ++ [(bcktDecision b, bcktAction b)]-        child = case dporNext dpor of-                  Just (t, d)-                    | t /= tid -> err "incorporateBacktrackSteps" "incorporating wrong trace!"-                    | otherwise -> go (Just t) pref' bs d-                  Nothing -> err "incorporateBacktrackSteps" "child is missing!"-    in dpor' { dporNext = Just (tid, child) }-  go _ _ [] dpor = dpor+-- visited and aren't in the sleep set.+incorporateBacktrackSteps :: [BacktrackStep] -> DPOR -> DPOR+incorporateBacktrackSteps (b:bs) dpor = dpor' where+  tid = bcktThreadid b -  doBacktrack priorTid pref b dpor =-    let todo' = [ x-                | x@(t,c) <- M.toList $ bcktBacktracks b-                , let decision  = decisionOf priorTid (dporRunnable dpor) t-                , let lahead = fromJust . M.lookup t $ bcktRunnable b-                , bv pref (decision, lahead)-                , Just t /= (fst <$> dporNext dpor)-                , S.notMember t (dporDone dpor)-                , c || M.notMember t (dporSleep dpor)-                ]-    in dpor { dporTodo = dporTodo dpor `M.union` M.fromList todo' }+  dpor' = dpor+    { dporTodo = dporTodo dpor `M.union` M.fromList todo+    , dporNext = Just (tid, child)+    } +  todo =+    [ x+    | x@(t,c) <- M.toList $ bcktBacktracks b+    , Just t /= (fst <$> dporNext dpor)+    , S.notMember t (dporDone dpor)+    , c || M.notMember t (dporSleep dpor)+    ]++  child = case dporNext dpor of+    Just (t, d)+      | t /= tid -> err "incorporateBacktrackSteps" "incorporating wrong trace!"+      | otherwise -> incorporateBacktrackSteps bs d+    Nothing -> err "incorporateBacktrackSteps" "child is missing!"+incorporateBacktrackSteps [] dpor = dpor+ ------------------------------------------------------------------------------- -- * DPOR scheduler  -- | The scheduler state-data DPORSchedState = DPORSchedState+data DPORSchedState k = DPORSchedState   { schedSleep     :: Map ThreadId ThreadAction   -- ^ The sleep set: decisions not to make until something dependent   -- with them happens.   , schedPrefix    :: [ThreadId]   -- ^ Decisions still to make-  , schedBPoints   :: Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])-  -- ^ Which threads are runnable at each step, and the alternative-  -- decisions still to make.+  , schedBPoints   :: Seq ([(ThreadId, Lookahead)], [ThreadId])+  -- ^ Which threads are runnable and in-bound at each step, and the+  -- alternative decisions still to make.   , schedIgnore    :: Bool   -- ^ Whether to ignore this execution or not: @True@ if the   -- execution is aborted due to all possible decisions being in the@@ -338,15 +331,18 @@   , schedDepState  :: DepState   -- ^ State used by the dependency function to determine when to   -- remove decisions from the sleep set.+  , schedBState    :: Maybe k+  -- ^ State used by the incremental bounding function.   } deriving (Eq, Show) -instance NFData DPORSchedState where+instance NFData k => NFData (DPORSchedState k) where   rnf s = rnf ( schedSleep     s               , schedPrefix    s               , schedBPoints   s               , schedIgnore    s               , schedBoundKill s               , schedDepState  s+              , schedBState    s               )  -- | Initial DPOR scheduler state for a given prefix@@ -354,7 +350,7 @@   -- ^ The initial sleep set.   -> [ThreadId]   -- ^ The schedule prefix.-  -> DPORSchedState+  -> DPORSchedState k initialDPORSchedState sleep prefix = DPORSchedState   { schedSleep     = sleep   , schedPrefix    = prefix@@ -362,13 +358,14 @@   , schedIgnore    = False   , schedBoundKill = False   , schedDepState  = initialDepState+  , schedBState    = Nothing   } --- | A bounding function takes the scheduling decisions so far and a--- decision chosen to come next, and returns if that decision is--- within the bound.-type BoundFunc-  = [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool+-- | An incremental bounding function is a stateful function that+-- takes the last and next decisions, and returns a new state only if+-- the next decision is within the bound.+type IncrementalBoundFunc k+  = Maybe k -> Maybe (ThreadId, ThreadAction) -> (Decision, Lookahead) -> Maybe k  -- | A backtracking step is a point in the execution where another -- decision needs to be made, in order to explore interesting new@@ -439,21 +436,23 @@ dporSched   :: MemType   -- ^ Memory model.-  -> BoundFunc+  -> IncrementalBoundFunc k   -- ^ Bound function: returns true if that schedule prefix terminated   -- with the lookahead decision fits within the bound.-  -> Scheduler DPORSchedState-dporSched memtype inBound trc prior threads s = schedule where+  -> Scheduler (DPORSchedState k)+dporSched memtype boundf _ prior threads s = schedule where   -- Pick a thread to run.   schedule = case schedPrefix s of     -- If there is a decision available, make it-    (d:ds) -> (Just d, (nextState []) { schedPrefix = ds })+    (t:ts) ->+      let bstate' = boundf (schedBState s) prior (decision t, action t)+      in (Just t, (nextState []) { schedPrefix = ts, schedBState = bstate' })      -- Otherwise query the initialise function for a list of possible     -- choices, filter out anything in the sleep set, and make one of     -- them arbitrarily (recording the others).     [] ->-      let choices  = restrictToBound initialise+      let choices  = restrictToBound id initialise           checkDep t a = case prior of             Just (tid, act) -> dependent memtype (schedDepState s) tid act t a             Nothing -> False@@ -462,12 +461,15 @@           signore' = not (null choices) && all (`elem` M.keys ssleep') choices           sbkill'  = not (null initialise) && null choices       in case choices' of-            (nextTid:rest) -> (Just nextTid, (nextState rest) { schedSleep = ssleep' })-            [] -> (Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill' })+            (nextTid:rest) ->+              let bstate' = boundf (schedBState s) prior (decision nextTid, action nextTid)+              in (Just nextTid, (nextState rest) { schedSleep = ssleep', schedBState = bstate' })+            [] ->+              (Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill', schedBState = Nothing })    -- The next scheduler state   nextState rest = s-    { schedBPoints  = schedBPoints s |> (threads, rest)+    { schedBPoints  = schedBPoints s |> (restrictToBound fst threads', rest)     , schedDepState = nextDepState     }   nextDepState = let ds = schedDepState s in maybe ds (uncurry $ updateDepState ds) prior@@ -478,7 +480,7 @@   initialise = tryDaemons . yieldsToEnd $ case prior of     Just (tid, act)       | not (didYield act) && tid `elem` tids -> [tid]-    _ -> tids'+    _ -> tids    -- If one of the chosen actions will kill the computation, and there   -- are daemon threads, try them instead.@@ -501,30 +503,29 @@   -- See commits a056f54 and 8554ce9, and my 4th June comment in issue   -- #52.   tryDaemons ts-    | any doesKill ts = case partition doesKill tids' of+    | any doesKill ts = case partition doesKill tids of         (kills, nokills) -> nokills ++ kills     | otherwise = ts   doesKill t = killsDaemons t (action t)    -- Restrict the possible decisions to those in the bound.-  restrictToBound = filter (\t -> inBound trc (decision t, action t))+  restrictToBound f = filter (\x -> let t = f x in isJust $ boundf (schedBState s) prior (decision t, action t))    -- Move the threads which will immediately yield to the end of the list   yieldsToEnd ts = case partition (willYield . action) ts of     (yields, noyields) -> noyields ++ yields    -- Get the decision that will lead to a thread being scheduled.-  decision = decisionOf (fst <$> prior) (S.fromList tids')+  decision = decisionOf (fst <$> prior) (S.fromList tids)    -- Get the action of a thread   action t = fromJust $ lookup t threads'    -- The runnable thread IDs-  tids = fst <$> threads+  tids = map fst threads'    -- The runnable threads as a normal list.   threads' = toList threads-  tids'    = toList tids  ------------------------------------------------------------------------------- -- Weighted random scheduler

@@ -151,7 +151,7 @@        let newIDSource = nidsrc'           newAct = act'-          newUndo = undo >> undo'+          newUndo = undo' >> undo           newReaden = readen' ++ readen           newWritten = written' ++ written           newSofar = tact : sofar

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             0.7.1.2+version:             0.7.1.3 synopsis:            Systematic testing for Haskell concurrency.  description:@@ -37,7 +37,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-0.7.1.2+  tag:      dejafu-0.7.1.3  library   exposed-modules:     Test.DejaFu