diff --git a/CHANGELOG.rst b/CHANGELOG.rst --- a/CHANGELOG.rst +++ b/CHANGELOG.rst @@ -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) --------------------- diff --git a/Test/DejaFu/Internal.hs b/Test/DejaFu/Internal.hs --- a/Test/DejaFu/Internal.hs +++ b/Test/DejaFu/Internal.hs @@ -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. diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -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) 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 @@ -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 diff --git a/Test/DejaFu/SCT/Internal/DPOR.hs b/Test/DejaFu/SCT/Internal/DPOR.hs --- a/Test/DejaFu/SCT/Internal/DPOR.hs +++ b/Test/DejaFu/SCT/Internal/DPOR.hs @@ -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 diff --git a/Test/DejaFu/Settings.hs b/Test/DejaFu/Settings.hs --- a/Test/DejaFu/Settings.hs +++ b/Test/DejaFu/Settings.hs @@ -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 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: 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