module Test.DPOR.Internal where
import Control.DeepSeq (NFData(..), force)
import Data.Char (ord)
import Data.List (foldl', intercalate, partition, sortBy)
import Data.List.NonEmpty (NonEmpty(..), toList)
import Data.Ord (Down(..), comparing)
import Data.Map.Strict (Map)
import Data.Maybe (fromJust, mapMaybe)
import qualified Data.Map.Strict as M
import Data.Set (Set)
import qualified Data.Set as S
import Data.Sequence (Seq, ViewL(..), (|>))
import qualified Data.Sequence as Sq
import Test.DPOR.Schedule (Decision(..), Scheduler, decisionOf, tidOf)
data DPOR tid action = DPOR
{ dporRunnable :: Set tid
, dporTodo :: Map tid Bool
, dporDone :: Map tid (DPOR tid action)
, dporSleep :: Map tid action
, dporTaken :: Map tid action
, dporAction :: Maybe action
}
instance (NFData tid, NFData action) => NFData (DPOR tid action) where
rnf dpor = rnf ( dporRunnable dpor
, dporTodo dpor
, dporDone dpor
, dporSleep dpor
, dporTaken dpor
, dporAction dpor
)
data BacktrackStep tid action lookahead state = BacktrackStep
{ bcktThreadid :: tid
, bcktDecision :: (Decision tid, action)
, bcktRunnable :: Map tid lookahead
, bcktBacktracks :: Map tid Bool
, bcktState :: state
} deriving Show
instance ( NFData tid
, NFData action
, NFData lookahead
, NFData state
) => NFData (BacktrackStep tid action lookahead state) where
rnf b = rnf ( bcktThreadid b
, bcktDecision b
, bcktRunnable b
, bcktBacktracks b
, bcktState b
)
initialState :: Ord tid => tid -> DPOR tid action
initialState initialThread = DPOR
{ dporRunnable = S.singleton initialThread
, dporTodo = M.singleton initialThread False
, dporDone = M.empty
, dporSleep = M.empty
, dporTaken = M.empty
, dporAction = Nothing
}
findSchedulePrefix :: Ord tid
=> (tid -> Bool)
-> DPOR tid action
-> Maybe ([tid], Bool, Map tid action)
findSchedulePrefix predicate dporRoot = go (initialDPORThread dporRoot) dporRoot where
go tid dpor =
let prefixes = mapMaybe go' (M.toList $ dporDone dpor) ++ [([t], c, sleeps dpor) | (t, c) <- M.toList $ dporTodo dpor]
cmp = Down . preEmps tid dpor . (\(a,_,_) -> a)
in if null prefixes
then Nothing
else case partition (\(t:_,_,_) -> predicate t) $ sortBy (comparing cmp) prefixes of
(choice:_, _) -> Just choice
([], choice:_) -> Just choice
([], []) -> error "findSchedulePrefix: (internal error) empty prefix list!"
go' (tid, dpor) = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> go tid dpor
sleeps dpor = dporSleep dpor `M.union` dporTaken dpor
preEmps tid dpor (t:ts) =
let rest = preEmps t (fromJust . M.lookup t $ dporDone dpor) ts
in if tid `S.member` dporRunnable dpor then 1 + rest else rest
preEmps _ _ [] = 0::Int
type Trace tid action lookahead = [(Decision tid, [(tid, NonEmpty lookahead)], action)]
incorporateTrace :: Ord tid
=> state
-> (state -> action -> state)
-> (state -> (tid, action) -> (tid, action) -> Bool)
-> Bool
-> Trace tid action lookahead
-> DPOR tid action
-> DPOR tid action
incorporateTrace stinit ststep dependency conservative trace dporRoot = grow stinit (initialDPORThread dporRoot) trace dporRoot where
grow state tid trc@((d, _, a):rest) dpor =
let tid' = tidOf tid d
state' = ststep state a
in case M.lookup tid' $ dporDone dpor of
Just dpor' -> dpor { dporDone = M.insert tid' (grow state' tid' rest dpor') $ dporDone dpor }
Nothing -> dpor { dporTaken = if conservative then dporTaken dpor else M.insert tid' a $ dporTaken dpor
, dporTodo = M.delete tid' $ dporTodo dpor
, dporDone = M.insert tid' (subtree state' tid' (dporSleep dpor `M.union` dporTaken dpor) trc) $ dporDone dpor }
grow _ _ [] dpor = dpor
subtree state tid sleep ((_, _, a):rest) =
let state' = ststep state a
sleep' = M.filterWithKey (\t a' -> not $ dependency state' (tid, a) (t,a')) sleep
in DPOR
{ dporRunnable = S.fromList $ case rest of
((_, runnable, _):_) -> map fst runnable
[] -> []
, dporTodo = M.empty
, dporDone = M.fromList $ case rest of
((d', _, _):_) ->
let tid' = tidOf tid d'
in [(tid', subtree state' tid' sleep' rest)]
[] -> []
, dporSleep = sleep'
, dporTaken = case rest of
((d', _, a'):_) -> M.singleton (tidOf tid d') a'
[] -> M.empty
, dporAction = Just a
}
subtree _ _ _ [] = error "incorporateTrace: (internal error) subtree suffix empty!"
findBacktrackSteps :: Ord tid
=> s
-> (s -> action -> s)
-> (s -> (tid, action) -> (tid, lookahead) -> Bool)
-> ([BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s])
-> Seq (NonEmpty (tid, lookahead), [tid])
-> Trace tid action lookahead
-> [BacktrackStep tid action lookahead s]
findBacktrackSteps stinit ststep dependency backtrack bcktrck = go stinit S.empty initialThread [] (Sq.viewl bcktrck) where
initialThread = case Sq.viewl bcktrck of
(((tid, _):|_, _):<_) -> tid
_ -> error "findBacktrack: empty backtracking sequence."
go state allThreads tid bs ((e,i):<is) ((d,_,a):ts) =
let tid' = tidOf tid d
state' = ststep state a
this = BacktrackStep
{ bcktThreadid = tid'
, bcktDecision = (d, a)
, bcktRunnable = M.fromList . toList $ e
, bcktBacktracks = M.fromList $ map (\i' -> (i', False)) i
, bcktState = state'
}
bs' = doBacktrack killsEarly allThreads' (toList e) (bs++[this])
runnable = S.fromList (M.keys $ bcktRunnable this)
allThreads' = allThreads `S.union` runnable
killsEarly = null ts && any (/=initialThread) runnable
in go state' allThreads' tid' bs' (Sq.viewl is) ts
go _ _ _ bs _ _ = bs
doBacktrack killsEarly allThreads enabledThreads bs =
let tagged = reverse $ zip [0..] bs
idxs = [ (head is, u)
| (u, n) <- enabledThreads
, v <- S.toList allThreads
, u /= v
, let is = idxs' u n v tagged
, not $ null is]
idxs' u n v = mapMaybe go' where
go' (i, b)
| bcktThreadid b == v && (killsEarly || isDependent b) = Just i
| otherwise = Nothing
isDependent b = dependency (bcktState b) (bcktThreadid b, snd $ bcktDecision b) (u, n)
in foldl' (\b (i, u) -> backtrack b i u) bs idxs
incorporateBacktrackSteps :: Ord tid
=> ([(Decision tid, action)] -> (Decision tid, lookahead) -> Bool)
-> [BacktrackStep tid action lookahead s]
-> DPOR tid action
-> DPOR tid action
incorporateBacktrackSteps bv = go Nothing [] where
go priorTid pref (b:bs) bpor =
let bpor' = doBacktrack priorTid pref b bpor
tid = bcktThreadid b
pref' = pref ++ [bcktDecision b]
child = go (Just tid) pref' bs . fromJust $ M.lookup tid (dporDone bpor)
in bpor' { dporDone = M.insert tid child $ dporDone bpor' }
go _ _ [] bpor = bpor
doBacktrack priorTid pref b bpor =
let todo' = [ x
| x@(t,c) <- M.toList $ bcktBacktracks b
, let decision = decisionOf priorTid (dporRunnable bpor) t
, let lahead = fromJust . M.lookup t $ bcktRunnable b
, bv pref (decision, lahead)
, t `notElem` M.keys (dporDone bpor)
, c || M.notMember t (dporSleep bpor)
]
in bpor { dporTodo = dporTodo bpor `M.union` M.fromList todo' }
type DPORScheduler tid action lookahead s = Scheduler tid action lookahead (SchedState tid action lookahead s)
data SchedState tid action lookahead s = SchedState
{ schedSleep :: Map tid action
, schedPrefix :: [tid]
, schedBPoints :: Seq (NonEmpty (tid, lookahead), [tid])
, schedIgnore :: Bool
, schedDepState :: s
} deriving Show
instance ( NFData tid
, NFData action
, NFData lookahead
, NFData s
) => NFData (SchedState tid action lookahead s) where
rnf s = rnf ( schedSleep s
, schedPrefix s
, schedBPoints s
, schedIgnore s
, schedDepState s
)
initialSchedState :: s
-> Map tid action
-> [tid]
-> SchedState tid action lookahead s
initialSchedState s sleep prefix = SchedState
{ schedSleep = sleep
, schedPrefix = prefix
, schedBPoints = Sq.empty
, schedIgnore = False
, schedDepState = s
}
type BoundFunc tid action lookahead = [(Decision tid, action)] -> (Decision tid, lookahead) -> Bool
type BacktrackFunc tid action lookahead s = [BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s]
dporSched :: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s)
=> (action -> Bool)
-> (lookahead -> Bool)
-> (s -> (tid, action) -> (tid, action) -> Bool)
-> (s -> action -> s)
-> BoundFunc tid action lookahead
-> DPORScheduler tid action lookahead s
dporSched didYield willYield dependency ststep inBound trc prior threads s = force schedule where
schedule = case schedPrefix s of
(d:ds) -> (Just d, (nextState []) { schedPrefix = ds })
[] ->
let choices = initialise
checkDep t a = case prior of
Just (tid, act) -> dependency (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
signore' = not (null choices) && all (`elem` M.keys ssleep') choices
in case choices' of
(nextTid:rest) -> (Just nextTid, (nextState rest) { schedSleep = ssleep' })
[] -> (Nothing, (nextState []) { schedIgnore = signore' })
nextState rest = s
{ schedBPoints = schedBPoints s |> (threads, rest)
, schedDepState = case prior of
Just (_, act) -> ststep (schedDepState s) act
Nothing -> schedDepState s
}
initialise = restrictToBound . yieldsToEnd $ case prior of
Just (tid, act)
| didYield act -> map fst (toList threads)
| any (\(t, _) -> t == tid) threads -> [tid]
_ -> map fst (toList threads)
restrictToBound = fst . partition (\t -> inBound trc (decision t, action t))
yieldsToEnd ts = case partition (willYield . action) ts of
(yields, noyields) -> noyields ++ yields
decision = decisionOf (fst <$> prior) (S.fromList $ map fst threads')
action t = fromJust $ lookup t threads'
threads' = toList threads
initialDPORThread :: DPOR tid action -> tid
initialDPORThread = S.elemAt 0 . dporRunnable
toDot :: (tid -> String)
-> (action -> String)
-> DPOR tid action
-> String
toDot = toDotFiltered (\_ _ -> True)
toDotFiltered :: (tid -> DPOR tid action -> Bool)
-> (tid -> String)
-> (action -> String)
-> DPOR tid action
-> String
toDotFiltered check showTid showAct dpor = "digraph {\n" ++ go "L" dpor ++ "\n}" where
go l b = unlines $ node l b : edges l b
node n b = n ++ " [label=\"" ++ label b ++ "\"]"
edges l b = [ edge l l' i ++ go l' b'
| (i, b') <- M.toList (dporDone b)
, check i b'
, let l' = l ++ tidId i
]
label b = showLst id
[ maybe "Nothing" (("Just " ++) . showAct) $ dporAction b
, "Run:" ++ showLst showTid (S.toList $ dporRunnable b)
, "Tod:" ++ showLst showTid (M.keys $ dporTodo b)
, "Slp:" ++ showLst (\(t,a) -> "(" ++ showTid t ++ ", " ++ showAct a ++ ")")
(M.toList $ dporSleep b)
]
edge n1 n2 l = n1 ++ "-> " ++ n2 ++ " [label=\"" ++ showTid l ++ "\"]\n"
showLst showf xs = "[" ++ intercalate ", " (map showf xs) ++ "]"
tidId = concatMap (show . ord) . showTid