dejafu 1.10.0.0 → 1.10.1.0

raw patch · 7 files changed

+91/−45 lines, 7 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.rst +14/−0
• Test/DejaFu/Internal.hs +1/−0
• Test/DejaFu/SCT.hs +3/−3
• Test/DejaFu/SCT/Internal.hs +22/−21
• Test/DejaFu/SCT/Internal/DPOR.hs +25/−19
• Test/DejaFu/Settings.hs +24/−0
• dejafu.cabal +2/−2

@@ -7,6 +7,20 @@ .. _PVP: https://pvp.haskell.org/  +1.10.1.0 (2018-06-17)+---------------------++* Git: :tag:`dejafu-1.10.1.0`+* Hackage: :hackage:`dejafu-1.10.1.0`++Added+~~~~~++* (:issue:`224`) The ``Test.DejaFu.Settings.lsafeIO`` option, for when+  all lifted IO is thread-safe (such as exclusively managing+  thread-local state).++ 1.10.0.0 (2018-06-17) --------------------- 

@@ -45,6 +45,7 @@   , _earlyExit :: Maybe (Either Failure a -> Bool)   , _equality :: Maybe (a -> a -> Bool)   , _simplify  :: Bool+  , _safeIO :: Bool   }  -- | How to explore the possible executions of a concurrent program.

@@ -200,11 +200,11 @@          step run dp (prefix, conservative, sleep) = do           (res, s, trace) <- run-            (dporSched (_memtype settings) (cBound cb0))+            (dporSched (_safeIO settings) (_memtype settings) (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 (_safeIO settings) (_memtype settings) (cBacktrack cb0) (schedBoundKill s) (schedBPoints s) trace+          let newDPOR = incorporateTrace (_safeIO settings) (_memtype settings) conservative trace dp            pure $ if schedIgnore s                  then (force newDPOR, Nothing)

@@ -176,7 +176,7 @@             pure (res, trace)   where     tidTrace = toTIdTrace trace-    simplifiedTrace = simplify (_memtype settings) tidTrace+    simplifiedTrace = simplify (_safeIO settings) (_memtype settings) tidTrace     fixup = renumber (_memtype settings) (fromId nTId) (fromId nCRId)      debugFatal = if _debugFatal settings then fatal else debugPrint@@ -207,10 +207,10 @@  -- | 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+simplify :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]+simplify safeIO memtype trc0 = loop (length trc0) (prepare trc0) where+  prepare = dropCommits safeIO memtype . lexicoNormalForm safeIO memtype+  step = pushForward safeIO memtype . pullBack safeIO memtype    loop 0 trc = trc   loop n trc =@@ -218,34 +218,35 @@     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+lexicoNormalForm :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]+lexicoNormalForm safeIO memtype = go where   go trc =-    let trc' = permuteBy memtype (repeat (>)) trc+    let trc' = permuteBy safeIO 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+  :: Bool+  -> MemType   -> [ThreadId -> ThreadId -> Bool]   -> [(ThreadId, ThreadAction)]   -> [(ThreadId, ThreadAction)]-permuteBy memtype = go initialDepState where+permuteBy safeIO 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)+    | independent safeIO 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+dropCommits :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]+dropCommits _ SequentialConsistency = id+dropCommits safeIO 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)+    | independent safeIO 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 _ [] = [] @@ -256,8 +257,8 @@ -- 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+pullBack :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]+pullBack safeIO memtype = go initialDepState where   go ds (t1@(tid1, ta1):trc@((tid2, _):_)) =     let ds' = updateDepState memtype ds tid1 ta1         trc' = if tid1 /= tid2@@ -271,7 +272,7 @@       | 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')+            | independent safeIO ds tid ta ftid fa -> Just (ft, t:trc')           _ -> Nothing     fgo _ _ = Nothing @@ -285,8 +286,8 @@ -- 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+pushForward :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]+pushForward safeIO memtype = go initialDepState where   go ds (t1@(tid1, ta1):trc@((tid2, _):_)) =     let ds' = updateDepState memtype ds tid1 ta1     in if tid1 /= tid2@@ -297,7 +298,7 @@   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+      | independent safeIO ds tid0 ta0 tid ta = (t:) <$> fgo (updateDepState memtype ds tid ta) trc       | otherwise = Nothing     fgo _ _ = Nothing 

@@ -154,7 +154,9 @@  -- | Add a new trace to the stack.  This won't work if to-dos aren't explored depth-first. incorporateTrace :: HasCallStack-  => MemType+  => Bool+  -- ^ True if all IO is thread-safe.+  -> MemType   -> Bool   -- ^ Whether the \"to-do\" point which was used to create this new   -- execution was conservative or not.@@ -163,7 +165,7 @@   -- and the action performed.   -> DPOR   -> DPOR-incorporateTrace memtype conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where+incorporateTrace safeIO memtype 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@@ -188,7 +190,7 @@   -- Construct a new subtree corresponding to a trace suffix.   subtree state tid sleep ((_, _, a):rest) = validateDPOR $     let state' = updateDepState memtype state tid a-        sleep' = M.filterWithKey (\t a' -> not $ dependent state' tid a t a') sleep+        sleep' = M.filterWithKey (\t a' -> not $ dependent safeIO state' tid a t a') sleep     in DPOR         { dporRunnable = S.fromList $ case rest of             ((d', runnable, _):_) -> tidOf tid d' : map fst runnable@@ -221,7 +223,9 @@ -- runnable, a dependency is imposed between this final action and -- everything else. findBacktrackSteps-  :: MemType+  :: Bool+  -- ^ True if all IO is thread-safe+  -> MemType   -> BacktrackFunc   -- ^ Backtracking function. Given a list of backtracking points, and   -- a thread to backtrack to at a specific point in that list, add@@ -239,7 +243,7 @@   -> Trace   -- ^ The execution trace.   -> [BacktrackStep]-findBacktrackSteps memtype backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where+findBacktrackSteps safeIO memtype 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) =@@ -296,7 +300,7 @@             -- 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' (bcktState b) (bcktThreadid b) (bcktAction b) u n+            | otherwise = dependent' safeIO (bcktState b) (bcktThreadid b) (bcktAction b) u n     in backtrack bs idxs  -- | Add new backtracking points, if they have not already been@@ -443,12 +447,14 @@ -- yielded. Furthermore, threads which /will/ yield are ignored in -- preference of those which will not. dporSched :: HasCallStack-  => MemType+  => Bool+  -- ^ True if all IO is thread safe.+  -> MemType   -> 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 safeIO memtype boundf = Scheduler $ \prior threads s ->   let     -- The next scheduler state     nextState rest = s@@ -523,7 +529,7 @@     [] ->       let choices  = restrictToBound id initialise           checkDep t a = case prior of-            Just (tid, act) -> dependent (schedDepState s) tid act t a+            Just (tid, act) -> dependent safeIO (schedDepState s) tid act t a             Nothing -> False           ssleep'  = M.filterWithKey (\t a -> not $ checkDep t a) $ schedSleep s           choices' = filter (`notElem` M.keys ssleep') choices@@ -546,12 +552,12 @@ -- -- This should not be used to re-order traces which contain -- subconcurrency.-independent :: DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool-independent ds t1 a1 t2 a2+independent :: Bool -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool+independent safeIO ds t1 a1 t2 a2     | t1 == t2 = False     | check t1 a1 t2 a2 = False     | check t2 a2 t1 a1 = False-    | otherwise = not (dependent ds t1 a1 t2 a2)+    | otherwise = not (dependent safeIO ds t1 a1 t2 a2)   where     -- @dontCheck@ must be the first thing in the computation.     check _ (DontCheck _) _ _ = True@@ -575,8 +581,8 @@ -- 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 :: DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool-dependent ds t1 a1 t2 a2 = case (a1, a2) of+dependent :: Bool -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool+dependent safeIO ds t1 a1 t2 a2 = case (a1, a2) of   -- 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@@ -594,8 +600,8 @@   (BlockedSTM _, STM _ _)      -> checkSTM   (BlockedSTM _, BlockedSTM _) -> checkSTM -  _ -> dependent' ds t1 a1 t2 (rewind a2)-    && dependent' ds t2 a2 t1 (rewind a1)+  _ -> dependent' safeIO ds t1 a1 t2 (rewind a2)+    && dependent' safeIO ds t2 a2 t1 (rewind a1)    where     -- STM actions A and B are dependent if A wrote to anything B@@ -607,10 +613,10 @@ -- -- Termination of the initial thread is handled specially in the DPOR -- implementation.-dependent' :: DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool-dependent' ds t1 a1 t2 l2 = case (a1, l2) of+dependent' :: Bool -> DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool+dependent' safeIO ds t1 a1 t2 l2 = case (a1, l2) of   -- Worst-case assumption: all IO is dependent.-  (LiftIO, WillLiftIO) -> True+  (LiftIO, WillLiftIO) -> not safeIO    -- Throwing an exception is only dependent with actions in that   -- thread and if the actions can be interrupted. We can also

@@ -188,6 +188,20 @@    , lsimplify +  -- ** Safe IO++  -- | Normally, dejafu has to assume any IO action can influence any+  -- other IO action, as there is no way to peek inside them.+  -- However, this adds considerable overhead to systematic testing.+  -- A perfectly legitimate use of IO is in managing thread-local+  -- state, such as a PRNG; in this case, there is no point in+  -- exploring interleavings of IO actions from other threads.+  --+  -- __Warning:__ Enabling this option is /unsound/ if your IO is not+  -- thread safe!++  , lsafeIO+   -- ** Debug output    -- | You can opt to receive debugging messages by setting debugging@@ -241,6 +255,7 @@   , _earlyExit = Nothing   , _equality = Nothing   , _simplify = False+  , _safeIO = False   }  -------------------------------------------------------------------------------@@ -408,6 +423,15 @@ -- @since 1.3.2.0 lsimplify :: Lens' (Settings n a) Bool lsimplify afb s = (\b -> s {_simplify = b}) <$> afb (_simplify s)++-------------------------------------------------------------------------------+-- Safe IO++-- | A lens into the safe IO flag.+--+-- @since 1.10.1.0+lsafeIO :: Lens' (Settings n a) Bool+lsafeIO afb s = (\b -> s {_safeIO = b}) <$> afb (_safeIO s)  ------------------------------------------------------------------------------- -- Debug output

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             1.10.0.0+version:             1.10.1.0 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.10.0.0+  tag:      dejafu-1.10.1.0  library   exposed-modules:     Test.DejaFu