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, isNothing, 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)
-> (Int -> (Int, g))
-> DPOR tid action
-> Maybe ([tid], Bool, Map tid action, g)
findSchedulePrefix predicate idx dpor0
| null allPrefixes = Nothing
| otherwise = let (i, g) = idx (length allPrefixes)
(ts, c, slp) = allPrefixes !! i
in Just (ts, c, slp, g)
where
allPrefixes = go (initialDPORThread dpor0) dpor0
go tid dpor =
let prefixes = concatMap go' (M.toList $ dporDone dpor) ++ here dpor
cmp = Down . preEmps tid dpor . (\(a,_,_) -> a)
sorted = sortBy (comparing cmp) prefixes
in if null prefixes
then []
else case partition (\(t:_,_,_) -> predicate t) sorted of
([], []) -> err "findSchedulePrefix" "empty prefix list!"
([], choices) -> choices
(choices, _) -> choices
go' (tid, dpor) = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> go tid dpor
here dpor = [([t], c, sleeps dpor) | (t, c) <- M.toList $ dporTodo 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 -> (tid, 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 dpor0 = grow stinit (initialDPORThread dpor0) trace dpor0 where
grow state tid trc@((d, _, a):rest) dpor =
let tid' = tidOf tid d
state' = ststep state (tid', a)
in case M.lookup tid' (dporDone dpor) of
Just dpor' ->
let done = M.insert tid' (grow state' tid' rest dpor') (dporDone dpor)
in dpor { dporDone = done }
Nothing ->
let taken = M.insert tid' a (dporTaken dpor)
sleep = dporSleep dpor `M.union` dporTaken dpor
done = M.insert tid' (subtree state' tid' sleep trc) (dporDone dpor)
in dpor { dporTaken = if conservative then dporTaken dpor else taken
, dporTodo = M.delete tid' (dporTodo dpor)
, dporDone = done
}
grow _ _ [] dpor = dpor
subtree state tid sleep ((_, _, a):rest) =
let state' = ststep state (tid, 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 _ _ _ [] = err "incorporateTrace" "subtree suffix empty!"
findBacktrackSteps :: Ord tid
=> s
-> (s -> (tid, action) -> s)
-> (s -> (tid, action) -> (tid, lookahead) -> Bool)
-> ([BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s])
-> Bool
-> Seq (NonEmpty (tid, lookahead), [tid])
-> Trace tid action lookahead
-> [BacktrackStep tid action lookahead s]
findBacktrackSteps _ _ _ _ _ bcktrck
| Sq.null bcktrck = const []
findBacktrackSteps stinit ststep dependency backtrack boundKill bcktrck = go stinit S.empty initialThread [] (Sq.viewl bcktrck) where
initialThread = case Sq.viewl bcktrck of
(((tid, _):|_, _):<_) -> tid
_ -> err "findBacktrack" "impossible case reached!"
go state allThreads tid bs ((e,i):<is) ((d,_,a):ts) =
let tid' = tidOf tid d
state' = ststep state (tid', 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 && boundKill
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
, schedBoundKill :: 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
, schedBoundKill 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
, schedBoundKill = False
, schedDepState = s
}
type BoundFunc tid action lookahead
= [(Decision tid, action)] -> (Decision tid, lookahead) -> Bool
trueBound :: BoundFunc tid action lookahead
trueBound _ _ = True
type BacktrackFunc tid action lookahead s
= [BacktrackStep tid action lookahead s] -> Int -> tid
-> [BacktrackStep tid action lookahead s]
backtrackAt :: Ord tid
=> (BacktrackStep tid action lookahead s -> Bool)
-> Bool
-> BacktrackFunc tid action lookahead s
backtrackAt toAll conservative bs i tid = go bs i where
go bx@(b:rest) 0
| not (toAll b) && tid `M.member` bcktRunnable b =
let val = M.lookup tid $ bcktBacktracks b
in if isNothing val || (val == Just False && conservative)
then b { bcktBacktracks = backtrackTo b } : rest
else bx
| otherwise = b { bcktBacktracks = backtrackAll b } : rest
go (b:rest) n = b : go rest (n1)
go [] _ = error "backtrackAt: Ran out of schedule whilst backtracking!"
backtrackTo = M.insert tid conservative . bcktBacktracks
backtrackAll = M.map (const conservative) . bcktRunnable
dporSched :: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s)
=> (action -> Bool)
-> (lookahead -> Bool)
-> (s -> (tid, action) -> (tid, action) -> Bool)
-> (s -> (tid, lookahead) -> NonEmpty tid -> Bool)
-> (s -> (tid, action) -> s)
-> BoundFunc tid action lookahead
-> DPORScheduler tid action lookahead s
dporSched didYield willYield dependency killsDaemons ststep inBound trc prior threads s = force schedule where
schedule = case schedPrefix s of
(d:ds) -> (Just d, (nextState []) { schedPrefix = ds })
[] ->
let choices = restrictToBound 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
sbkill' = not (null initialise) && null choices
in case choices' of
(nextTid:rest) -> (Just nextTid, (nextState rest) { schedSleep = ssleep' })
[] -> (Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill' })
nextState rest = s
{ schedBPoints = schedBPoints s |> (threads, rest)
, schedDepState = nextDepState
}
nextDepState = let ds = schedDepState s in maybe ds (ststep ds) prior
initialise = tryDaemons . yieldsToEnd $ case prior of
Just (tid, act)
| not (didYield act) && tid `elem` tids -> [tid]
_ -> tids'
tryDaemons ts
| any doesKill ts = filter (not . doesKill) tids' ++ filter doesKill ts
| otherwise = ts
doesKill t = killsDaemons nextDepState (t, action t) tids
restrictToBound = filter (\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 tids')
action t = fromJust $ lookup t threads'
tids = fst <$> threads
threads' = toList threads
tids' = toList tids
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 = digraph . go "L" where
digraph str = "digraph {\n" ++ str ++ "\n}"
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
err :: String -> String -> a
err func msg = error (func ++ ": (internal error) " ++ msg)