barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2024-12-26 15:02:20 +03:00
Code Issues Projects Releases Wiki Activity

Do not consider safe IO dependent

Browse Source
This commit is contained in:
Michael Walker 2018-06-17 12:39:55 +01:00
parent 0952b3799a
commit 92c8d941e7
6 changed files with 64 additions and 53 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
dejafu-tests/lib/Common.hs
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)

2
dejafu-tests/lib/Integration/Litmus.hs
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

8
dejafu-tests/lib/Unit/Properties.hs
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

6
dejafu/Test/DejaFu/SCT.hs
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)

43
dejafu/Test/DejaFu/SCT/Internal.hs
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

44
dejafu/Test/DejaFu/SCT/Internal/DPOR.hs
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