diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown --- a/CHANGELOG.markdown +++ b/CHANGELOG.markdown @@ -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][] diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -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])] diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs --- a/Test/DejaFu/SCT/Internal.hs +++ b/Test/DejaFu/SCT/Internal.hs @@ -1,10 +1,12 @@ +{-# LANGUAGE TupleSections #-} + -- | -- Module : Test.DejaFu.SCT.Internal -- Copyright : (c) 2016 Michael Walker -- License : MIT -- Maintainer : Michael Walker -- 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 diff --git a/Test/DejaFu/STM/Internal.hs b/Test/DejaFu/STM/Internal.hs --- a/Test/DejaFu/STM/Internal.hs +++ b/Test/DejaFu/STM/Internal.hs @@ -151,7 +151,7 @@ let newIDSource = nidsrc' newAct = act' - newUndo = undo >> undo' + newUndo = undo' >> undo newReaden = readen' ++ readen newWritten = written' ++ written newSofar = tact : sofar 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: 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