dejafu 0.3.0.0 → 0.3.1.0

raw patch · 4 files changed

+95/−39 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Test/DejaFu/Deterministic/Internal.hs +1/−0
• Test/DejaFu/Deterministic/Internal/Common.hs +72/−26
• Test/DejaFu/SCT.hs +20/−11
• dejafu.cabal +2/−2

@@ -37,6 +37,7 @@  , Lookahead(..)  , isBlock  , lookahead+ , rewind  , willRelease  , preEmpCount  , showTrace

@@ -562,6 +562,50 @@   rnf (WillMessage m) = m `seq` ()   rnf l = l `seq` () +-- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has+-- happened. 'Killed' has no 'Lookahead' counterpart.+rewind :: ThreadAction -> Maybe Lookahead+rewind (Fork _) = Just WillFork+rewind MyThreadId = Just WillMyThreadId+rewind (GetNumCapabilities _) = Just WillGetNumCapabilities+rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i)+rewind Yield = Just WillYield+rewind (NewVar _) = Just WillNewVar+rewind (PutVar c _) = Just (WillPutVar c)+rewind (BlockedPutVar c) = Just (WillPutVar c)+rewind (TryPutVar c _ _) = Just (WillTryPutVar c)+rewind (ReadVar c) = Just (WillReadVar c)+rewind (BlockedReadVar c) = Just (WillReadVar c)+rewind (TakeVar c _) = Just (WillTakeVar c)+rewind (BlockedTakeVar c) = Just (WillTakeVar c)+rewind (TryTakeVar c _ _) = Just (WillTryTakeVar c)+rewind (NewRef _) = Just WillNewRef+rewind (ReadRef c) = Just (WillReadRef c)+rewind (ReadRefCas c) = Just (WillReadRefCas c)+rewind (PeekTicket c) = Just (WillPeekTicket c)+rewind (ModRef c) = Just (WillModRef c)+rewind (ModRefCas c) = Just (WillModRefCas c)+rewind (WriteRef c) = Just (WillWriteRef c)+rewind (CasRef c _) = Just (WillCasRef c)+rewind (CommitRef t c) = Just (WillCommitRef t c)+rewind (STM _ _) = Just WillSTM+rewind (BlockedSTM _) = Just WillSTM+rewind Catching = Just WillCatching+rewind PopCatching = Just WillPopCatching+rewind Throw = Just WillThrow+rewind (ThrowTo t) = Just (WillThrowTo t)+rewind (BlockedThrowTo t) = Just (WillThrowTo t)+rewind Killed = Nothing+rewind (SetMasking b m) = Just (WillSetMasking b m)+rewind (ResetMasking b m) = Just (WillResetMasking b m)+rewind Lift = Just WillLift+rewind Return = Just WillReturn+rewind KnowsAbout = Just WillKnowsAbout+rewind Forgets = Just WillForgets+rewind AllKnown = Just WillAllKnown+rewind (Message m) = Just (WillMessage m)+rewind Stop = Just WillStop+ -- | Look as far ahead in the given continuation as possible. lookahead :: Action n r s -> NonEmpty Lookahead lookahead = fromList . lookahead' where@@ -617,15 +661,36 @@ willRelease _ = False  -- Count the number of pre-emptions in a schedule prefix.+--+-- Commit threads complicate this a bit. Conceptually, commits are+-- happening truly in parallel, nondeterministically. The commit+-- thread implementation is just there to unify the two sources of+-- nondeterminism: commit timing and thread scheduling.+--+-- SO, we don't count a switch TO a commit thread as a+-- preemption. HOWEVER, the switch FROM a commit thread counts as a+-- preemption if it is not to the thread that the commit interrupted. preEmpCount :: [(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Int-preEmpCount ts (d, _) = go Nothing ts where-  go p ((d', a):rest) = preEmpC p d' + go (Just a) rest-  go p [] = preEmpC p d+preEmpCount ts (d, _) = go initialThread Nothing ts where+  go _ (Just Yield) ((SwitchTo t, a):rest) = go t (Just a) rest+  go tid prior ((SwitchTo t, a):rest)+    | isCommitThread t = go tid prior (skip rest)+    | otherwise = 1 + go t (Just a) rest+  go _   _ ((Start t,  a):rest) = go t   (Just a) rest+  go tid _ ((Continue, a):rest) = go tid (Just a) rest+  go _ prior [] = case (prior, d) of+    (Just Yield, SwitchTo _) -> 0+    (_, SwitchTo _) -> 1+    _ -> 0 -  preEmpC (Just Yield) (SwitchTo _) = 0-  preEmpC _ (SwitchTo t) = if t >= initialThread then 1 else 0-  preEmpC _ _ = 0+  -- Commit threads have negative thread IDs for easy identification.+  isCommitThread = (< initialThread) +  -- Skip until the next context switch.+  skip = dropWhile (not . isContextSwitch . fst)+  isContextSwitch Continue = False+  isContextSwitch _ = True+ -- | A simplified view of the possible actions a thread can perform. data ActionType =     UnsynchronisedRead  CRefId@@ -704,26 +769,7 @@ -- This is used in the SCT code to help determine interesting -- alternative scheduling decisions. simplify :: ThreadAction -> ActionType-simplify (PutVar c _)       = SynchronisedWrite c-simplify (BlockedPutVar c)  = SynchronisedWrite c-simplify (TryPutVar c _ _)  = SynchronisedWrite c-simplify (ReadVar c)        = SynchronisedRead c-simplify (BlockedReadVar c) = SynchronisedRead c-simplify (TakeVar c _)      = SynchronisedRead c-simplify (BlockedTakeVar c) = SynchronisedRead c-simplify (TryTakeVar c _ _) = SynchronisedRead c-simplify (ReadRef r)     = UnsynchronisedRead r-simplify (ReadRefCas r)  = UnsynchronisedRead r-simplify (ModRef r)      = SynchronisedModify r-simplify (ModRefCas r)   = PartiallySynchronisedModify r-simplify (WriteRef r)    = UnsynchronisedWrite r-simplify (CasRef r _)    = PartiallySynchronisedWrite r-simplify (CommitRef _ r) = PartiallySynchronisedCommit r-simplify (STM _ _)          = SynchronisedOther-simplify (BlockedSTM _)     = SynchronisedOther-simplify (ThrowTo _)        = SynchronisedOther-simplify (BlockedThrowTo _) = SynchronisedOther-simplify _ = UnsynchronisedOther+simplify = maybe UnsynchronisedOther simplify' . rewind  -- | Variant of 'simplify' that takes a 'Lookahead'. simplify' :: Lookahead -> ActionType

@@ -349,16 +349,25 @@  -- | Check if an action is dependent on another. dependent :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool-dependent _ _ (_, Lift) (_, Lift) = True-dependent _ _ (_, ThrowTo t) (t2, Stop) | t == t2 = False-dependent _ _ (t2, Stop) (_, ThrowTo t) | t == t2 = False-dependent _ _ (_, ThrowTo t) (t2, _) = t == t2-dependent _ _ (t2, _) (_, ThrowTo t) = t == t2-dependent _ _ (_, STM _ _) (_, STM _ _) = True-dependent _ _ (_, GetNumCapabilities a) (_, SetNumCapabilities b) = a /= b+-- 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:+--+--  - Firstly, @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.+--+--  - Secondly, 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. dependent _ _ (_, SetNumCapabilities a) (_, GetNumCapabilities b) = a /= b-dependent _ _ (_, SetNumCapabilities a) (_, SetNumCapabilities b) = a /= b-dependent memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify d2)+dependent memtype buf (t1, a1) (t2, a2) = case rewind a2 of+  Just l2 | not (isBlock a1 && isBarrier (simplify' l2)) ->+    dependent' memtype buf (t1, a1) (t2, l2)+  _ -> dependentActions memtype buf (simplify a1) (simplify a2)  -- | Variant of 'dependent' to handle 'ThreadAction''s dependent' :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, Lookahead) -> Bool@@ -376,8 +385,8 @@ -- -- UNLESS the pre-emption would possibly allow for a different relaxed -- memory stage.-dependent' _ _ (_, a1) (_, a2) | isBlock a1 && isBarrier (simplify' a2) = False-dependent' memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify' d2)+dependent' _ _ (_, a1) (_, l2) | isBlock a1 && isBarrier (simplify' l2) = False+dependent' memtype buf (_, a1) (_, l2) = dependentActions memtype buf (simplify a1) (simplify' l2)  -- | Check if two 'ActionType's are dependent. Note that this is not -- sufficient to know if two 'ThreadAction's are dependent, without

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             0.3.0.0+version:             0.3.1.0 synopsis:            Overloadable primitives for testable, potentially non-deterministic, concurrency.  description:@@ -75,7 +75,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-0.3.0.0+  tag:      dejafu-0.3.1.0  library   exposed-modules:     Control.Monad.Conc.Class