diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown --- a/CHANGELOG.markdown +++ b/CHANGELOG.markdown @@ -7,6 +7,24 @@ *de facto* standard Haskell versioning scheme. +0.9.0.2 +------- + +- **Date** 2017-11-02 +- **Git tag** [dejafu-0.9.0.2][] +- **Hackage** https://hackage.haskell.org/package/dejafu-0.9.0.2 + +### Miscellaneous + +- Small improvement to dependency detection of STM transactions. +- A fair bound of 0 will now prevent all yields. + +[dejafu-0.9.0.2]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.9.0.2 + + +--------------------------------------------------------------------------------------------------- + + 0.9.0.1 ------- diff --git a/Test/DejaFu/Common.hs b/Test/DejaFu/Common.hs --- a/Test/DejaFu/Common.hs +++ b/Test/DejaFu/Common.hs @@ -27,6 +27,8 @@ , ThreadAction(..) , isBlock , tvarsOf + , tvarsWritten + , tvarsRead -- ** Lookahead , Lookahead(..) , rewind @@ -410,14 +412,35 @@ -- -- @since 0.4.0.0 tvarsOf :: ThreadAction -> Set TVarId -tvarsOf act = S.fromList $ case act of +tvarsOf act = tvarsRead act `S.union` tvarsWritten act + +-- | Get the @TVar@s a transaction wrote to (or would have, if it +-- didn't @retry@). +-- +-- @since 0.9.0.2 +tvarsWritten :: ThreadAction -> Set TVarId +tvarsWritten act = S.fromList $ case act of STM trc _ -> concatMap tvarsOf' trc BlockedSTM trc -> concatMap tvarsOf' trc _ -> [] where - tvarsOf' (TRead tv) = [tv] tvarsOf' (TWrite tv) = [tv] + tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' _ = [] + +-- | Get the @TVar@s a transaction read from. +-- +-- @since 0.9.0.2 +tvarsRead :: ThreadAction -> Set TVarId +tvarsRead act = S.fromList $ case act of + STM trc _ -> concatMap tvarsOf' trc + BlockedSTM trc -> concatMap tvarsOf' trc + _ -> [] + + where + tvarsOf' (TRead tv) = [tv] tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) tvarsOf' _ = [] diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -428,7 +428,9 @@ 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 + in if not (willYield (snd lhead)) || 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. @@ -663,7 +665,7 @@ where ycount tnext | willYield lnext = M.alter (Just . maybe 1 (+1)) tnext sofar - | otherwise = M.alter (Just . fromMaybe 0) tnext sofar + | otherwise = M.alter (Just . fromMaybe 0) tnext sofar -- | Determine if an action is a commit or not. isCommitRef :: ThreadAction -> Bool 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 @@ -277,7 +277,14 @@ _ -> False {-# INLINE isDependent #-} - isDependent b = dependent' memtype (bcktState b) (bcktThreadid b) (bcktAction b) u n + isDependent b + -- Don't impose a dependency if the other thread will + -- immediately block already. This is safe because a + -- context switch will occur anyway so there's no point + -- pre-empting the action UNLESS the pre-emption would + -- possibly allow for a different relaxed memory stage. + | isBlock (bcktAction b) && isBarrier (simplifyLookahead n) = False + | otherwise = dependent' memtype (bcktState b) (bcktThreadid b) (bcktAction b) u n in backtrack bs idxs -- | Add new backtracking points, if they have not already been @@ -453,7 +460,7 @@ -- otherwise add all runnable threads. initialise = tryDaemons . yieldsToEnd $ case prior of Just (tid, act) - | not (didYield act) && tid `elem` tids -> [tid] + | not (didYield act) && tid `elem` tids && isInBound tid -> [tid] _ -> tids -- If one of the chosen actions will kill the computation, and @@ -484,8 +491,8 @@ doesKill t = killsDaemons t (action t) -- Restrict the possible decisions to those in the bound. - restrictToBound f = - filter (\x -> let t = f x in isJust $ boundf (schedBState s) prior (decision t, action t)) + restrictToBound f = filter (isInBound . f) + isInBound t = 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 @@ -575,44 +582,43 @@ -- Dependency function -- | Check if an action is dependent on another. -dependent :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool --- This is basically the same as 'dependent'', but can make use of the --- additional information in a 'ThreadAction' to make different --- decisions in a few cases: -- --- - @SetNumCapabilities@ and @GetNumCapabilities@ are NOT dependent --- IF the value read is the same as the value written. 'dependent'' --- can not see the value read (as it hasn't happened yet!), and so --- is more pessimistic here. --- --- - When masked interruptible, a thread can only be interrupted when --- actually blocked. 'dependent'' has to assume that all --- potentially-blocking operations can block, and so is more --- pessimistic in this case. --- --- - The @isBlock@ / @isBarrier@ case in 'dependent'' is NOT a sound --- optimisation when dealing with a 'ThreadAction' that has been --- converted to a 'Lookahead'. I'm not entirely sure why, which --- makes me question whether the \"optimisation\" is sound as it --- is. --- --- - Dependency of STM transactions can be /greatly/ improved here, --- as the 'Lookahead' does not know which @TVar@s will be touched, --- and so has to assume all transactions are dependent. -dependent _ _ _ (SetNumCapabilities a) _ (GetNumCapabilities b) = a /= b -dependent _ ds _ (ThrowTo t) t2 a = t == t2 && canInterrupt ds t2 a -dependent memtype ds t1 a1 t2 a2 = case rewind a2 of - Just l2 - | isSTM a1 && isSTM a2 - -> not . S.null $ tvarsOf a1 `S.intersection` tvarsOf a2 - | not (isBlock a1 && isBarrier (simplifyLookahead l2)) -> - dependent' memtype ds t1 a1 t2 l2 - _ -> dependentActions memtype ds (simplifyAction a1) (simplifyAction a2) +-- This is basically the same as 'dependent'', but can make use of the +-- additional information in a 'ThreadAction' to make better decisions +-- in a few cases. +dependent :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool +dependent memtype ds t1 a1 t2 a2 = case (a1, a2) of + -- @SetNumCapabilities@ and @GetNumCapabilities@ are NOT dependent + -- IF the value read is the same as the value written. 'dependent'' + -- can not see the value read (as it hasn't happened yet!), and so + -- is more pessimistic here. + (SetNumCapabilities a, GetNumCapabilities b) | a == b -> False + (GetNumCapabilities a, SetNumCapabilities b) | a == b -> False + -- When masked interruptible, a thread can only be interrupted when + -- actually blocked. 'dependent'' has to assume that all + -- potentially-blocking operations can block, and so is more + -- pessimistic in this case. + (ThrowTo t, _) | t == t2 -> canInterrupt ds t2 a2 && a2 /= Stop + (_, ThrowTo t) | t == t1 -> canInterrupt ds t1 a1 && a1 /= Stop + + -- Dependency of STM transactions can be /greatly/ improved here, as + -- the 'Lookahead' does not know which @TVar@s will be touched, and + -- so has to assume all transactions are dependent. + (STM _ _, STM _ _) -> checkSTM + (STM _ _, BlockedSTM _) -> checkSTM + (BlockedSTM _, STM _ _) -> checkSTM + (BlockedSTM _, BlockedSTM _) -> checkSTM + + _ -> case (,) <$> rewind a1 <*> rewind a2 of + Just (l1, l2) -> dependent' memtype ds t1 a1 t2 l2 && dependent' memtype ds t2 a2 t1 l1 + _ -> dependentActions memtype ds (simplifyAction a1) (simplifyAction a2) + where - isSTM (STM _ _) = True - isSTM (BlockedSTM _) = True - isSTM _ = False + -- STM actions A and B are dependent if A wrote to anything B + -- touched, or vice versa. + checkSTM = checkSTM' a1 a2 || checkSTM' a2 a1 + checkSTM' a b = not . S.null $ tvarsWritten a `S.intersection` tvarsOf b -- | Variant of 'dependent' to handle 'Lookahead'. -- @@ -629,8 +635,8 @@ -- 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 + (_, WillThrowTo t) | t == t1 -> canInterrupt ds t1 a1 -- Another worst-case: assume all STM is dependent. (STM _ _, WillSTM) -> True @@ -642,13 +648,7 @@ (SetNumCapabilities _, WillGetNumCapabilities) -> True (SetNumCapabilities a, WillSetNumCapabilities b) -> a /= b - -- Don't impose a dependency if the other thread will immediately - -- block already. This is safe because a context switch will occur - -- anyway so there's no point pre-empting the action UNLESS the - -- pre-emption would possibly allow for a different relaxed memory - -- stage. - _ | isBlock a1 && isBarrier (simplifyLookahead l2) -> False - | otherwise -> dependentActions memtype ds (simplifyAction a1) (simplifyLookahead l2) + _ -> dependentActions memtype ds (simplifyAction a1) (simplifyLookahead l2) -- | Check if two 'ActionType's are dependent. Note that this is not -- sufficient to know if two 'ThreadAction's are dependent, without 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.9.0.1 +version: 0.9.0.2 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.9.0.1 + tag: dejafu-0.9.0.2 library exposed-modules: Test.DejaFu