dejafu-2.0.0.0: Test/DejaFu/SCT/Internal/DPOR.hs
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ViewPatterns #-}
-- |
-- Module : Test.DejaFu.SCT.Internal.DPOR
-- Copyright : (c) 2015--2018 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : DeriveAnyClass, DeriveGeneric, FlexibleContexts, ViewPatterns
--
-- Internal types and functions for SCT via dynamic partial-order
-- reduction. This module is NOT considered to form part of the
-- public interface of this library.
module Test.DejaFu.SCT.Internal.DPOR where
import Control.Applicative ((<|>))
import Control.DeepSeq (NFData)
import qualified Data.Foldable as F
import Data.Function (on)
import Data.List (nubBy, partition, sortOn)
import Data.List.NonEmpty (toList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
import Data.Maybe (isJust, isNothing, listToMaybe,
maybeToList)
import Data.Sequence (Seq, (|>))
import qualified Data.Sequence as Sq
import Data.Set (Set)
import qualified Data.Set as S
import GHC.Generics (Generic)
import GHC.Stack (HasCallStack)
import Test.DejaFu.Internal
import Test.DejaFu.Schedule (Scheduler(..))
import Test.DejaFu.Types
import Test.DejaFu.Utils (decisionOf, tidOf)
-------------------------------------------------------------------------------
-- * Dynamic partial-order reduction
-- | DPOR execution is represented as a tree of states, characterised
-- by the decisions that lead to that state.
data DPOR = DPOR
{ dporRunnable :: Set ThreadId
-- ^ What threads are runnable at this step.
, dporTodo :: Map ThreadId Bool
-- ^ Follow-on decisions still to make, and whether that decision
-- was added conservatively due to the bound.
, dporNext :: Maybe (ThreadId, DPOR)
-- ^ The next decision made. Executions are explored in a
-- depth-first fashion, so this changes as old subtrees are
-- exhausted and new ones explored.
, dporDone :: Set ThreadId
-- ^ All transitions which have been taken from this point,
-- including conservatively-added ones.
, dporSleep :: Map ThreadId ThreadAction
-- ^ Transitions to ignore (in this node and children) until a
-- dependent transition happens.
, dporTaken :: Map ThreadId ThreadAction
-- ^ Transitions which have been taken, excluding
-- conservatively-added ones. This is used in implementing sleep
-- sets.
} deriving (Eq, Show, Generic, NFData)
-- | Check the DPOR data invariants and raise an error if any are
-- broken.
--
-- This is a reasonable thing to do, because if the state is corrupted
-- then nothing sensible can happen anyway.
validateDPOR :: HasCallStack => DPOR -> DPOR
validateDPOR dpor
| not (todo `S.isSubsetOf` runnable) = fatal "thread exists in todo set but not runnable set"
| not (done `S.isSubsetOf` runnable) = fatal "thread exists in done set but not runnable set"
| not (taken `S.isSubsetOf` done) = fatal "thread exists in taken set but not done set"
| not (todo `disjoint` done) = fatal "thread exists in both taken set and done set"
| not (maybe True (`S.member` done) next) = fatal "taken thread does not exist in done set"
| otherwise = dpor
where
done = dporDone dpor
next = fst <$> dporNext dpor
runnable = dporRunnable dpor
taken = S.fromList (M.keys (dporTaken dpor))
todo = S.fromList (M.keys (dporTodo dpor))
disjoint s1 s2 = S.null (S.intersection s1 s2)
-- | One step of the execution, including information for backtracking
-- purposes. This backtracking information is used to generate new
-- schedules.
data BacktrackStep = BacktrackStep
{ bcktThreadid :: ThreadId
-- ^ The thread running at this step
, bcktDecision :: Decision
-- ^ What was decided at this step.
, bcktAction :: ThreadAction
-- ^ What happened at this step.
, bcktRunnable :: Map ThreadId Lookahead
-- ^ The threads runnable at this step
, bcktBacktracks :: Map ThreadId Bool
-- ^ The list of alternative threads to run, and whether those
-- alternatives were added conservatively due to the bound.
, bcktState :: ConcurrencyState
-- ^ Some domain-specific state at this point.
} deriving (Eq, Show, Generic, NFData)
-- | Initial DPOR state, given an initial thread ID. This initial
-- thread should exist and be runnable at the start of execution.
--
-- The main thread must be in the list of initially runnable threads.
initialState :: [ThreadId] -> DPOR
initialState threads
| initialThread `elem` threads = DPOR
{ dporRunnable = S.fromList threads
, dporTodo = M.singleton initialThread False
, dporNext = Nothing
, dporDone = S.empty
, dporSleep = M.empty
, dporTaken = M.empty
}
| otherwise = fatal "initialState" "Initial thread is not in initially runnable set"
-- | Produce a new schedule prefix from a @DPOR@ tree. If there are no new
-- prefixes remaining, return 'Nothing'. Also returns whether the
-- decision was added conservatively, and the sleep set at the point
-- where divergence happens.
--
-- A schedule prefix is a possibly empty sequence of decisions that
-- have already been made, terminated by a single decision from the
-- to-do set. The intent is to put the system into a new state when
-- executed with this initial sequence of scheduling decisions.
findSchedulePrefix
:: DPOR
-> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
findSchedulePrefix dpor = case dporNext dpor of
Just (tid, child) -> go tid child <|> here
Nothing -> here
where
go tid child = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> findSchedulePrefix child
-- Prefix traces terminating with a to-do decision at this point.
here =
let todos = [([t], c, sleeps) | (t, c) <- M.toList $ dporTodo dpor]
(best, worst) = partition (\([t],_,_) -> t >= initialThread) todos
in listToMaybe best <|> listToMaybe worst
-- The new sleep set is the union of the sleep set of the node
-- we're branching from, plus all the decisions we've already
-- explored.
sleeps = dporSleep dpor `M.union` dporTaken dpor
-- | Add a new trace to the stack. This won't work if to-dos aren't explored depth-first.
incorporateTrace :: HasCallStack
=> 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.
-> Trace
-- ^ The execution trace: the decision made, the runnable threads,
-- and the action performed.
-> ConcurrencyState
-- ^ The initial concurrency state
-> DPOR
-> DPOR
incorporateTrace safeIO memtype conservative trace state0 dpor0 = grow state0 (initialDPORThread dpor0) trace dpor0 where
grow state tid trc@((d, _, a):rest) dpor =
let tid' = tidOf tid d
state' = updateCState memtype state tid' a
in case dporNext dpor of
Just (t, child)
| t == tid' ->
validateDPOR $ dpor { dporNext = Just (tid', grow state' tid' rest child) }
| hasTodos child -> fatal "replacing child with todos!"
_ -> validateDPOR $
let taken = M.insert tid' a (dporTaken dpor)
sleep = dporSleep dpor `M.union` dporTaken dpor
in dpor { dporTaken = if conservative then dporTaken dpor else taken
, dporTodo = M.delete tid' (dporTodo dpor)
, dporNext = Just (tid', subtree state' tid' sleep trc)
, dporDone = S.insert tid' (dporDone dpor)
}
grow _ _ [] _ = fatal "trace exhausted without reading a to-do point!"
-- check if there are to-do points in a tree
hasTodos dpor = not (M.null (dporTodo dpor)) || (case dporNext dpor of Just (_, dpor') -> hasTodos dpor'; _ -> False)
-- Construct a new subtree corresponding to a trace suffix.
subtree state tid sleep ((_, _, a):rest) = validateDPOR $
let state' = updateCState memtype state tid a
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
[] -> []
, dporTodo = M.empty
, dporNext = case rest of
((d', _, _):_) ->
let tid' = tidOf tid d'
in Just (tid', subtree state' tid' sleep' rest)
[] -> Nothing
, dporDone = case rest of
((d', _, _):_) -> S.singleton (tidOf tid d')
[] -> S.empty
, dporSleep = sleep'
, dporTaken = case rest of
((d', _, a'):_) -> M.singleton (tidOf tid d') a'
[] -> M.empty
}
subtree _ _ _ [] = fatal "subtree suffix empty!"
-- | Produce a list of new backtracking points from an execution
-- trace. These are then used to inform new \"to-do\" points in the
-- @DPOR@ tree.
--
-- Two traces are passed in to this function: the first is generated
-- from the special DPOR scheduler, the other from the execution of
-- the concurrent program.
--
-- If the trace ends with any threads other than the initial one still
-- runnable, a dependency is imposed between this final action and
-- everything else.
findBacktrackSteps
:: 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
-- the new backtracking points. There will be at least one: this
-- chosen one, but the function may add others.
-> Bool
-- ^ Whether the computation was aborted due to no decisions being
-- in-bounds.
-> ConcurrencyState
-- ^ The initial concurrency state.
-> Seq ([(ThreadId, Lookahead)], [ThreadId])
-- ^ A sequence of threads at each step: the list of runnable
-- in-bound threads (with lookahead values), and the list of threads
-- still to try. The reason for the two separate lists is because
-- the threads chosen to try will be dependent on the specific
-- domain.
-> Trace
-- ^ The execution trace.
-> [BacktrackStep]
findBacktrackSteps safeIO memtype backtrack boundKill state0 = go state0 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) =
let tid' = tidOf tid d
state' = updateCState memtype state tid' a
this = BacktrackStep
{ bcktThreadid = tid'
, bcktDecision = d
, bcktAction = a
, bcktRunnable = M.fromList e
, bcktBacktracks = M.fromList $ map (\i' -> (i', False)) i
, bcktState = state
}
bs' = doBacktrack killsEarly allThreads' e (bs++[this])
runnable = S.fromList (M.keys $ bcktRunnable this)
allThreads' = allThreads `S.union` runnable
killsEarly = null ts && boundKill
in go state' allThreads' tid' bs' is ts
go _ _ _ bs _ _ = bs
-- Find the prior actions dependent with this one and add
-- backtracking points.
doBacktrack killsEarly allThreads enabledThreads bs =
let tagged = reverse $ zip [0..] bs
idxs = [ (i, False, u)
| (u, n) <- enabledThreads
, v <- S.toList allThreads
, u /= v
, i <- maybeToList (findIndex u n v tagged)]
findIndex u n v = go' where
{-# INLINE go' #-}
go' ((i,b):rest)
-- If this is the final action in the trace and the
-- execution was killed due to nothing being within bounds
-- (@killsEarly == True@) assume worst-case dependency.
| bcktThreadid b == v && (killsEarly || isDependent b) = Just i
| otherwise = go' rest
go' [] = Nothing
{-# INLINE isDependent #-}
isDependent b
-- Don't impose a dependency if the other thread will
-- immediately block already. This is safe because a
-- context switch will occur anyway so there's no point
-- 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' safeIO (bcktState b) (bcktThreadid b) (bcktAction b) u n
in backtrack bs idxs
-- | Add new backtracking points, if they have not already been
-- visited and aren't in the sleep set.
incorporateBacktrackSteps :: HasCallStack
=> [BacktrackStep] -> DPOR -> DPOR
incorporateBacktrackSteps (b:bs) dpor = validateDPOR dpor' where
tid = bcktThreadid b
dpor' = dpor
{ dporTodo = dporTodo dpor `M.union` M.fromList todo
, dporNext = Just (tid, child)
}
todo =
[ x
| x@(t,c) <- M.toList $ bcktBacktracks b
, Just t /= (fst <$> dporNext dpor)
, S.notMember t (dporDone dpor)
, c || M.notMember t (dporSleep dpor)
]
child = case dporNext dpor of
Just (t, d)
| t /= tid -> fatal "incorporating wrong trace!"
| otherwise -> incorporateBacktrackSteps bs d
Nothing -> fatal "child is missing!"
incorporateBacktrackSteps [] dpor = dpor
-------------------------------------------------------------------------------
-- * DPOR scheduler
-- | The scheduler state
data DPORSchedState k = DPORSchedState
{ schedSleep :: Map ThreadId ThreadAction
-- ^ The sleep set: decisions not to make until something dependent
-- with them happens.
, schedPrefix :: [ThreadId]
-- ^ Decisions still to make
, schedBPoints :: Seq ([(ThreadId, Lookahead)], [ThreadId])
-- ^ Which threads are runnable and in-bound at each step, and the
-- alternative decisions still to make.
, schedIgnore :: Bool
-- ^ Whether to ignore this execution or not: @True@ if the
-- execution is aborted due to all possible decisions being in the
-- sleep set, as then everything in this execution is covered by
-- another.
, schedBoundKill :: Bool
-- ^ Whether the execution was terminated due to all decisions being
-- out of bounds.
, schedCState :: ConcurrencyState
-- ^ State used by the dependency function to determine when to
-- remove decisions from the sleep set.
, schedBState :: Maybe k
-- ^ State used by the incremental bounding function.
} deriving (Eq, Show, Generic, NFData)
-- | Initial DPOR scheduler state for a given prefix
initialDPORSchedState :: Map ThreadId ThreadAction
-- ^ The initial sleep set.
-> [ThreadId]
-- ^ The schedule prefix.
-> ConcurrencyState
-- ^ The initial concurrency state.
-> DPORSchedState k
initialDPORSchedState sleep prefix state0 = DPORSchedState
{ schedSleep = sleep
, schedPrefix = prefix
, schedBPoints = Sq.empty
, schedIgnore = False
, schedBoundKill = False
, schedCState = state0
, schedBState = Nothing
}
-- | An incremental bounding function is a stateful function that
-- takes the last and next decisions, and returns a new state only if
-- the next decision is within the bound.
type IncrementalBoundFunc k
= Maybe k -> Maybe (ThreadId, ThreadAction) -> (Decision, Lookahead) -> Maybe k
-- | A backtracking step is a point in the execution where another
-- decision needs to be made, in order to explore interesting new
-- schedules. A backtracking /function/ takes the steps identified so
-- far and a list of points and thread at that point to backtrack
-- to. More points be added to compensate for the effects of the
-- bounding function. For example, under pre-emption bounding a
-- conservative backtracking point is added at the prior context
-- switch. The bool is whether the point is conservative. Conservative
-- points are always explored, whereas non-conservative ones might be
-- skipped based on future information.
--
-- In general, a backtracking function should identify one or more
-- backtracking points, and then use @backtrackAt@ to do the actual
-- work.
type BacktrackFunc
= [BacktrackStep] -> [(Int, Bool, ThreadId)] -> [BacktrackStep]
-- | Add a backtracking point. If the thread isn't runnable, add all
-- runnable threads. If the backtracking point is already present,
-- don't re-add it UNLESS this would make it conservative.
backtrackAt :: HasCallStack
=> (ThreadId -> BacktrackStep -> Bool)
-- ^ If this returns @True@, backtrack to all runnable threads,
-- rather than just the given thread.
-> BacktrackFunc
backtrackAt toAll bs0 = backtrackAt' . nubBy ((==) `on` fst') . sortOn fst' where
fst' (x,_,_) = x
backtrackAt' ((i,c,t):is) = go i bs0 i c t is
backtrackAt' [] = bs0
go i0 (b:bs) 0 c tid is
-- If the backtracking point is already present, don't re-add it,
-- UNLESS this would force it to backtrack (it's conservative)
-- where before it might not.
| not (toAll tid b) && tid `M.member` bcktRunnable b =
let val = M.lookup tid $ bcktBacktracks b
b' = if isNothing val || (val == Just False && c)
then b { bcktBacktracks = backtrackTo tid c b }
else b
in b' : case is of
((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is'
[] -> bs
-- Otherwise just backtrack to everything runnable.
| otherwise =
let b' = b { bcktBacktracks = backtrackAll c b }
in b' : case is of
((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is'
[] -> bs
go i0 (b:bs) i c tid is = b : go i0 bs (i-1) c tid is
go _ [] _ _ _ _ = fatal "ran out of schedule whilst backtracking!"
-- Backtrack to a single thread
backtrackTo tid c = M.insert tid c . bcktBacktracks
-- Backtrack to all runnable threads
backtrackAll c = M.map (const c) . bcktRunnable
-- | DPOR scheduler: takes a list of decisions, and maintains a trace
-- including the runnable threads, and the alternative choices allowed
-- by the bound-specific initialise function.
--
-- After the initial decisions are exhausted, this prefers choosing
-- the prior thread if it's (1) still runnable and (2) hasn't just
-- yielded. Furthermore, threads which /will/ yield are ignored in
-- preference of those which will not.
dporSched :: HasCallStack
=> Bool
-- ^ True if all IO is thread safe.
-> IncrementalBoundFunc k
-- ^ Bound function: returns true if that schedule prefix terminated
-- with the lookahead decision fits within the bound.
-> Scheduler (DPORSchedState k)
dporSched safeIO boundf = Scheduler $ \prior threads cstate s ->
let
-- The next scheduler state
nextState rest = s
{ schedBPoints = schedBPoints s |> (restrictToBound fst threads', rest)
-- we only update this after using the current value; so in
-- effect this field is the depstate *before* the action which
-- just happened, we need this because we need to know if the
-- prior action (in the state we did it from) is dependent with
-- anything in the sleep set.
, schedCState = cstate
}
-- Pick a new thread to run, not considering bounds. Choose the
-- current thread if available and it hasn't just yielded,
-- otherwise add all runnable threads.
initialise = tryDaemons . yieldsToEnd $ case prior of
Just (tid, act)
| not (didYield act) && tid `elem` tids && isInBound tid -> [tid]
_ -> tids
-- If one of the chosen actions will kill the computation, and
-- there are daemon threads, try them instead.
--
-- This is necessary if the killing action is NOT dependent with
-- every other action, according to the dependency function. This
-- is, strictly speaking, wrong; an action that kills another
-- thread is definitely dependent with everything in that
-- thread. HOWEVER, implementing it that way leads to an explosion
-- of schedules tried. Really, all that needs to happen is for the
-- thread-that-would-be-killed to be executed fully ONCE, and then
-- the normal dependency mechanism will identify any other
-- backtracking points that should be tried. This is achieved by
-- adding every thread that would be killed to the to-do list.
-- Furthermore, these threads MUST be ahead of the killing thread,
-- or the killing thread will end up in the sleep set and so the
-- killing action not performed. This is, again, because of the
-- lack of the dependency messing things up in the name of
-- performance.
--
-- See commits a056f54 and 8554ce9, and my 4th June comment in
-- issue #52.
tryDaemons ts
| any doesKill ts = case partition doesKill tids of
(kills, nokills) -> nokills ++ kills
| otherwise = ts
doesKill t = killsDaemons t (action t)
-- Restrict the possible decisions to those in the bound.
restrictToBound f = filter (isInBound . f)
isInBound t = isJust $ boundf (schedBState s) prior (decision t, action t)
-- Move the threads which will immediately yield to the end of the list
yieldsToEnd ts = case partition (willYield . action) ts of
(yields, noyields) -> noyields ++ yields
-- Get the decision that will lead to a thread being scheduled.
decision = decisionOf (fst <$> prior) (S.fromList tids)
-- Get the action of a thread
action t = efromJust (lookup t threads')
-- The runnable thread IDs
tids = map fst threads'
-- The runnable threads as a normal list.
threads' = toList threads
in case schedPrefix s of
-- If there is a decision available, make it
(t:ts) ->
let bstate' = boundf (schedBState s) prior (decision t, action t)
in (Just t, (nextState []) { schedPrefix = ts, schedBState = bstate' })
-- Otherwise query the initialise function for a list of possible
-- choices, filter out anything in the sleep set, and make one of
-- them arbitrarily (recording the others).
[] ->
let choices = restrictToBound id initialise
checkDep t a = case prior of
Just (tid, act) -> dependent safeIO (schedCState 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
signore' = not (null choices) && all (`elem` M.keys ssleep') choices
sbkill' = not (null initialise) && null choices
in case choices' of
(nextTid:rest) ->
let bstate' = boundf (schedBState s) prior (decision nextTid, action nextTid)
in (Just nextTid, (nextState rest) { schedSleep = ssleep', schedBState = bstate' })
[] ->
(Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill', schedBState = Nothing })
-------------------------------------------------------------------------------
-- * Dependency function
-- | Check if two actions commute.
--
-- This implements a stronger check that @not (dependent ...)@, as it
-- handles some cases which 'dependent' doesn't need to care about.
independent :: Bool -> ConcurrencyState -> 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 safeIO ds t1 a1 t2 a2)
where
-- can't re-order any action of a thread with the fork which
-- created it.
check _ (Fork t) tid _ | t == tid = True
check _ (ForkOS t) tid _ | t == tid = True
-- because we can't easily tell if this will terminate the other
-- thread, we just can't re-order asynchronous exceptions at all
-- :(
--
-- See #191 / #190
check _ (ThrowTo t _) tid _ | t == tid = True
check _ (BlockedThrowTo t) tid _ | t == tid = True
-- can't re-order an unsynchronised write with something which synchronises that IORef.
check _ (simplifyAction -> UnsynchronisedWrite r) _ (simplifyAction -> a) | synchronises a r = True
check _ _ _ _ = False
-- | Check if an action is dependent on another.
--
-- 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 :: Bool -> ConcurrencyState -> 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
-- pessimistic in this case.
(ThrowTo t _, ThrowTo u _)
| t == t2 && u == t1 -> canInterrupt ds t1 a1 || canInterrupt ds t2 a2
(ThrowTo t _, _) | t == t2 -> canInterrupt ds t2 a2 && a2 /= Stop
(_, ThrowTo t _) | t == t1 -> canInterrupt ds t1 a1 && a1 /= Stop
-- Dependency of STM transactions can be /greatly/ improved here, as
-- the 'Lookahead' does not know which @TVar@s will be touched, and
-- so has to assume all transactions are dependent.
(STM _ _, STM _ _) -> checkSTM
(STM _ _, BlockedSTM _) -> checkSTM
(BlockedSTM _, STM _ _) -> checkSTM
(BlockedSTM _, BlockedSTM _) -> checkSTM
_ -> 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
-- touched, or vice versa.
checkSTM = checkSTM' a1 a2 || checkSTM' a2 a1
checkSTM' a b = not . S.null $ tvarsWritten a `S.intersection` tvarsOf b
-- | Variant of 'dependent' to handle 'Lookahead'.
--
-- Termination of the initial thread is handled specially in the DPOR
-- implementation.
dependent' :: Bool -> ConcurrencyState -> 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) -> not safeIO
-- Throwing an exception is only dependent with actions in that
-- thread and if the actions can be interrupted. We can also
-- slightly improve on that by not considering interrupting the
-- normal termination of a thread: it doesn't make a difference.
(ThrowTo t _, WillThrowTo u)
| t == t2 && u == t1 -> canInterrupt ds t1 a1 || canInterruptL ds t2 l2
(ThrowTo t _, _) | t == t2 -> canInterruptL ds t2 l2 && l2 /= WillStop
(_, WillThrowTo t) | t == t1 -> canInterrupt ds t1 a1 && a1 /= Stop
-- Another worst-case: assume all STM is dependent.
(STM _ _, WillSTM) -> True
(BlockedSTM _, WillSTM) -> True
-- the number of capabilities is essentially a global shared
-- variable
(GetNumCapabilities _, WillSetNumCapabilities _) -> True
(SetNumCapabilities _, WillGetNumCapabilities) -> True
(SetNumCapabilities _, WillSetNumCapabilities _) -> True
_ -> dependentActions ds (simplifyAction a1) (simplifyLookahead l2)
-- | Check if two 'ActionType's are dependent. Note that this is not
-- sufficient to know if two 'ThreadAction's are dependent, without
-- being so great an over-approximation as to be useless!
dependentActions :: ConcurrencyState -> ActionType -> ActionType -> Bool
dependentActions ds a1 a2 = case (a1, a2) of
(UnsynchronisedRead _, UnsynchronisedRead _) -> False
-- Unsynchronised writes and synchronisation where the buffer is not
-- empty.
--
-- See [RMMVerification], lemma 5.25.
(UnsynchronisedWrite r1, PartiallySynchronisedCommit r2) | r1 == r2 && isBuffered ds r1 -> False
(PartiallySynchronisedCommit r1, UnsynchronisedWrite r2) | r1 == r2 && isBuffered ds r1 -> False
-- Unsynchronised reads where a memory barrier would flush a
-- buffered write
(UnsynchronisedRead r1, _) | isBarrier a2 && isBuffered ds r1 -> True
(_, UnsynchronisedRead r2) | isBarrier a1 && isBuffered ds r2 -> True
-- Commits and memory barriers must be dependent, as memory barriers
-- (currently) flush in a consistent order. Alternative orders need
-- to be explored as well. Perhaps a better implementation of
-- memory barriers would just block every non-commit thread while
-- any buffer is nonempty.
(PartiallySynchronisedCommit r1, _) | synchronises a2 r1 -> True
(_, PartiallySynchronisedCommit r2) | synchronises a1 r2 -> True
-- Two @MVar@ puts are dependent if they're to the same empty
-- @MVar@, and two takes are dependent if they're to the same full
-- @MVar@.
(SynchronisedWrite v1, SynchronisedWrite v2) | v1 == v2 -> not (isFull ds v1)
(SynchronisedRead v1, SynchronisedRead v2) | v1 == v2 -> isFull ds v1
(SynchronisedWrite v1, SynchronisedRead v2) | v1 == v2 -> True
(SynchronisedRead v1, SynchronisedWrite v2) | v1 == v2 -> True
(_, _) -> maybe False (\r -> Just r == iorefOf a2) (iorefOf a1)
-------------------------------------------------------------------------------
-- * Utilities
-- The initial thread of a DPOR tree.
initialDPORThread :: DPOR -> ThreadId
initialDPORThread = S.elemAt 0 . dporRunnable
-- | Check if a thread yielded.
didYield :: ThreadAction -> Bool
didYield Yield = True
didYield (ThreadDelay _) = True
didYield _ = False
-- | Check if a thread will yield.
willYield :: Lookahead -> Bool
willYield WillYield = True
willYield (WillThreadDelay _) = True
willYield _ = False
-- | Check if an action will kill daemon threads.
killsDaemons :: ThreadId -> Lookahead -> Bool
killsDaemons t WillStop = t == initialThread
killsDaemons _ _ = False