Merge pull request #271 from barrucadu/224-safe-io

Add a "safe IO" flag
This commit is contained in:
Michael Walker 2018-06-17 14:20:35 +01:00 committed by GitHub
commit cbbebdaf5e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
14 changed files with 111 additions and 58 deletions

View File

@ -46,7 +46,7 @@ There are a few different packages under the Déjà Fu umbrella:
| | Version | Summary |
| - | ------- | ------- |
| [concurrency][h:conc] | 1.5.0.0 | Typeclasses, functions, and data types for concurrency and STM. |
| [dejafu][h:dejafu] | 1.10.0.0 | Systematic testing for Haskell concurrency. |
| [dejafu][h:dejafu] | 1.10.1.0 | Systematic testing for Haskell concurrency. |
| [hunit-dejafu][h:hunit] | 1.2.0.5 | Deja Fu support for the HUnit test framework. |
| [tasty-dejafu][h:tasty] | 1.2.0.6 | Deja Fu support for the Tasty test framework. |

View File

@ -43,9 +43,10 @@ instance IsTest T where
toTestList (T n c p) = toTestList (TEST n c p (map (second toSettings) defaultWays) True)
toTestList (W n c p w) = toTestList (TEST n c p [second toSettings w] True)
toTestList (B n c p b) = toTestList (TEST n c p (map (second toSettings) (defaultWaysFor b)) True)
toTestList (TEST n c p ss subc) = toTestList . testGroup n $
let mk (name, settings) = testDejafuWithSettings settings name p c
in map mk ss ++ [H.testProperty "dependency func." (prop_dep_fun c) | subc]
toTestList (TEST n c p ss subc) = toTestList (TEST' False n c p ss subc)
toTestList (TEST' b n c p ss subc) = toTestList . testGroup n $
let mk (name, settings) = testDejafuWithSettings (set lsafeIO b settings) name p c
in map mk ss ++ [H.testProperty "dependency func." (prop_dep_fun b c) | subc]
instance IsTest t => IsTest [t] where
toTestList = concatMap toTestList
@ -55,6 +56,7 @@ data T where
W :: (Eq a, Show a) => String -> ConcIO a -> Predicate a -> (String, Way) -> T
B :: (Eq a, Show a) => String -> ConcIO a -> Predicate a -> Bounds -> T
TEST :: (Eq a, Show a) => String -> ConcIO a -> Predicate a -> [(String, Settings IO a)] -> Bool -> T
TEST' :: (Eq a, Show a) => Bool -> String -> ConcIO a -> Predicate a -> [(String, Settings IO a)] -> Bool -> T
toSettings :: (Applicative f, Eq a, Show a) => Way -> Settings f a
toSettings w
@ -105,15 +107,15 @@ testProperty name = H.testProperty name . H.property
-- | Check that the independence function correctly decides
-- commutativity for this program.
prop_dep_fun :: (Eq a, Show a) => ConcIO a -> H.Property
prop_dep_fun conc = H.property $ do
prop_dep_fun :: (Eq a, Show a) => Bool -> ConcIO a -> H.Property
prop_dep_fun safeIO conc = H.property $ do
mem <- H.forAll HGen.enumBounded
seed <- H.forAll genInt
fs <- H.forAll $ genList HGen.bool
(efa1, tids1, efa2, tids2) <- liftIO $ runNorm
seed
(renumber mem 1 1 . permuteBy mem (map (\f _ _ -> f) fs))
(renumber mem 1 1 . permuteBy safeIO mem (map (\f _ _ -> f) fs))
mem
H.footnote (" to: " ++ show tids2)
H.footnote ("rewritten from: " ++ show tids1)

View File

@ -11,7 +11,7 @@ import Common
tests :: [TestTree]
tests = toTestList
[ W "random testing exposes a deadlock" parFilter deadlocksSometimes ("randomly", randomly (mkStdGen 0) 150)
[ TEST' True "testing exposes a deadlock" parFilter deadlocksSometimes [("randomly", toSettings (randomly (mkStdGen 0) 150)), ("systematically", defaultSettings)] True
]
parFilter :: (MonadConc m, MonadIO m) => m Bool

View File

@ -49,7 +49,7 @@ litmusTest name act sq tso pso = testGroup name
[ testDejafuWithSettings (set lmemtype SequentialConsistency (toSettings defaultWay)) "SQ" (gives' sq) act
, testDejafuWithSettings (set lmemtype TotalStoreOrder (toSettings defaultWay)) "TSO" (gives' tso) act
, testDejafuWithSettings (set lmemtype PartialStoreOrder (toSettings defaultWay)) "PSO" (gives' pso) act
, H.testProperty "dependency func." (prop_dep_fun act)
, H.testProperty "dependency func." (prop_dep_fun False act)
]
-- | Run a litmus test against the three different memory models, and

View File

@ -251,20 +251,22 @@ sctProps = toTestList
H.assert (SCT.canInterruptL ds tid (D.rewind act))
, testProperty "dependent ==> dependent'" $ do
safeIO <- H.forAll HGen.bool
ds <- H.forAll genDepState
tid1 <- H.forAll genThreadId
tid2 <- H.forAll genThreadId
ta1 <- H.forAll genThreadAction
ta2 <- H.forAll (HGen.filter (SCT.dependent ds tid1 ta1 tid2) genThreadAction)
H.assert (SCT.dependent' ds tid1 ta1 tid2 (D.rewind ta2))
ta2 <- H.forAll (HGen.filter (SCT.dependent safeIO ds tid1 ta1 tid2) genThreadAction)
H.assert (SCT.dependent' safeIO ds tid1 ta1 tid2 (D.rewind ta2))
, testProperty "dependent x y == dependent y x" $ do
safeIO <- H.forAll HGen.bool
ds <- H.forAll genDepState
tid1 <- H.forAll genThreadId
tid2 <- H.forAll genThreadId
ta1 <- H.forAll genThreadAction
ta2 <- H.forAll genThreadAction
SCT.dependent ds tid1 ta1 tid2 ta2 H.=== SCT.dependent ds tid2 ta2 tid1 ta1
SCT.dependent safeIO ds tid1 ta1 tid2 ta2 H.=== SCT.dependent safeIO ds tid2 ta2 tid1 ta1
, testProperty "dependentActions x y == dependentActions y x" $ do
ds <- H.forAll genDepState

View File

@ -7,6 +7,20 @@ standard Haskell versioning scheme.
.. _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)
---------------------

View File

@ -45,6 +45,7 @@ data Settings n a = Settings
, _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.

View File

@ -200,11 +200,11 @@ runSCTWithSettings settings conc = case _way settings of
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)

View File

@ -176,7 +176,7 @@ simplifyExecution settings run nTId nCRId res trace
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 @@ replay run = run (Scheduler (const sched)) where
-- | 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 @@ simplify memtype trc0 = loop (length trc0) (prepare trc0) where
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 @@ dropCommits memtype = go initialDepState where
-- 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 @@ pullBack memtype = go initialDepState where
| 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 @@ pullBack memtype = go initialDepState where
-- 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 @@ pushForward memtype = go initialDepState where
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

View File

@ -154,7 +154,9 @@ findSchedulePrefix dpor = case dporNext dpor of
-- | 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 @@ incorporateTrace :: HasCallStack
-- 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 @@ incorporateTrace memtype conservative trace dpor0 = grow initialDepState (initia
-- 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 @@ incorporateTrace memtype conservative trace dpor0 = grow initialDepState (initia
-- 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 @@ findBacktrackSteps
-> 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 @@ findBacktrackSteps memtype backtrack boundKill = go initialDepState S.empty init
-- 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 @@ backtrackAt toAll bs0 = backtrackAt' . nubBy ((==) `on` fst') . sortOn fst' wher
-- 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 @@ dporSched memtype boundf = Scheduler $ \prior threads s ->
[] ->
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 @@ dporSched memtype boundf = Scheduler $ \prior threads s ->
--
-- 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 @@ independent ds t1 a1 t2 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 :: 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 @@ dependent ds t1 a1 t2 a2 = case (a1, a2) of
(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 @@ dependent ds t1 a1 t2 a2 = case (a1, a2) of
--
-- 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

View File

@ -188,6 +188,20 @@ module Test.DejaFu.Settings
, 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 @@ fromWayAndMemType way memtype = Settings
, _earlyExit = Nothing
, _equality = Nothing
, _simplify = False
, _safeIO = False
}
-------------------------------------------------------------------------------
@ -409,6 +424,15 @@ lequality afb s = (\b -> s {_equality = b}) <$> afb (_equality s)
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

View File

@ -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 head
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

View File

@ -38,6 +38,9 @@ The available settings are:
* **Trace simplification**, rewriting execution traces into a simpler
form (particularly effective with the random testing).
* **Safe IO**, pruning needless schedules when your IO is only used to
manage thread-local state.
See the ``Test.DejaFu.Settings`` module for more information.

View File

@ -28,7 +28,7 @@ There are a few different packages under the Déjà Fu umbrella:
:header: "Package", "Version", "Summary"
":hackage:`concurrency`", "1.5.0.0", "Typeclasses, functions, and data types for concurrency and STM"
":hackage:`dejafu`", "1.10.0.0", "Systematic testing for Haskell concurrency"
":hackage:`dejafu`", "1.10.1.0", "Systematic testing for Haskell concurrency"
":hackage:`hunit-dejafu`", "1.2.0.5", "Déjà Fu support for the HUnit test framework"
":hackage:`tasty-dejafu`", "1.2.0.6", "Déjà Fu support for the tasty test framework"