dejafu/Test/DejaFu/SCT/Internal.hs

-- | Internal utilities and types for BPOR.
module Test.DejaFu.SCT.Internal where

import Control.Applicative ((<$>), (<*>))
import Control.DeepSeq (NFData(..))
import Data.List (foldl', nub, partition, sortBy)
import Data.Ord (Down(..), comparing)
import Data.Map (Map)
import Data.Maybe (mapMaybe, fromJust)
import Test.DejaFu.Deterministic

import qualified Data.Map as M

-- * BPOR state

-- | One step of the execution, including information for backtracking
-- purposes. This backtracking information is used to generate new
-- schedules.
data BacktrackStep = BacktrackStep
  { _decision  :: (Decision, ThreadAction)
  -- ^ What happened at this step.
  , _runnable  :: [ThreadId]
  -- ^ The threads runnable at this step
  , _backtrack :: [(ThreadId, Bool)]
  -- ^ The list of alternative threads to run, and whether those
  -- alternatives were added conservatively due to the bound.
  } deriving (Eq, Show)

instance NFData BacktrackStep where
  rnf b = rnf (_decision b, _runnable b, _backtrack b)

-- | BPOR execution is represented as a tree of states, characterised
-- by the decisions that lead to that state.
data BPOR = BPOR
  { _brunnable :: [ThreadId]
  -- ^ What threads are runnable at this step.
  , _btodo     :: [(ThreadId, Bool)]
  -- ^ Follow-on decisions still to make, and whether that decision
  -- was added conservatively due to the bound.
  , _bignore :: [ThreadId]
  -- ^ Follow-on decisions never to make, because they will result in
  -- the chosen thread immediately blocking without achieving
  -- anything, which can't have any effect on the result of the
  -- program.
  , _bdone     :: Map ThreadId BPOR
  -- ^ Follow-on decisions that have been made.
  , _bsleep    :: [(ThreadId, ThreadAction)]
  -- ^ Transitions to ignore (in this node and children) until a
  -- dependent transition happens.
  , _btaken    :: [(ThreadId, ThreadAction)]
  -- ^ Transitions which have been taken, excluding
  -- conservatively-added ones, in the (reverse) order that they were
  -- taken, as the 'Map' doesn't preserve insertion order. This is
  -- used in implementing sleep sets.
  }

-- | Initial BPOR state.
initialState :: BPOR
initialState = BPOR
  { _brunnable = [0]
  , _btodo     = [(0, False)]
  , _bignore   = []
  , _bdone     = M.empty
  , _bsleep    = []
  , _btaken    = []
  }

-- | Produce a new schedule from a BPOR tree. If there are no new
-- schedules remaining, return 'Nothing'. Also returns whether the
-- decision made was added conservatively.
--
-- This returns the longest prefix, on the assumption that this will
-- lead to lots of backtracking points being identified before
-- higher-up decisions are reconsidered, so enlarging the sleep sets.
next :: BPOR -> Maybe ([ThreadId], Bool, BPOR)
next = go 0 where
  go tid bpor =
        -- All the possible prefix traces from this point, with
        -- updated BPOR subtrees if taken from the done list.
    let prefixes = [Left t | t <- _btodo bpor] ++ mapMaybe go' (M.toList $ _bdone bpor)
        -- Sort by number of preemptions, in descending order.
        sorted   = sortBy (comparing $ Down . preEmps tid bpor . either (\(a,_) -> [a]) (\(a,_,_) -> a)) prefixes

    in case sorted of
         -- If the prefix with the most preemptions is from the done list, update that.
         (Right (ts@(t:_), c, b):_) -> Just (ts, c, bpor { _bdone = M.insert t b $ _bdone bpor })
         -- If from the todo list, remove it.
         (Left (t,c):_) -> Just ([t], c, bpor { _btodo = filter (/=(t,c)) $ _btodo bpor })

         _ -> Nothing

  go' (tid, bpor) = (\(ts,c,b) -> Right (tid:ts, c, b)) <$> next bpor

  preEmps tid bpor (t:ts) =
    let rest = preEmps t (fromJust . M.lookup t $ _bdone bpor) ts
    in  if tid /= t && tid `elem` _brunnable bpor then 1 + rest else rest
  preEmps _ _ [] = 0::Int

-- | Produce a list of new backtracking points from an execution
-- trace.
findBacktrack :: ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])
              -> [(NonEmpty (ThreadId, ThreadAction'), [ThreadId])]
              -> Trace'
              -> [BacktrackStep]
findBacktrack backtrack = go [] [] where
  go allThreads bs ((e,i):is) ((d,_,a):ts) =
    let this        = BacktrackStep { _decision = (d, a), _runnable = map fst . toList $ e, _backtrack = map (\i' -> (i', False)) i }
        bs'         = doBacktrack allThreads (toList e) bs
        allThreads' = nub $ allThreads ++ _runnable this
    in go allThreads' (bs' ++ [this]) is ts
  go _ bs _ _ = bs

  doBacktrack allThreads enabledThreads bs =
    let tagged = zip [0..] $ tidTag (fst . _decision) 0 bs
        idxs   = [ (maximum is, u)
                 | (u, n) <- enabledThreads
                 , v <- allThreads
                 , u /= v
                 , let is = [ i
                            | (i, (t, b)) <- tagged
                            , t == v
                            , dependent' (snd $ _decision b) (u, n)
                            ]
                 , not $ null is] :: [(Int, ThreadId)]
    in foldl' (\bs (i, u) -> backtrack bs i u) bs idxs

-- | Add a new trace to the tree, creating a new subtree.
grow :: Bool -> Trace' -> BPOR -> BPOR
grow conservative = grow' initialCVState 0 where
  grow' cvstate tid trc@((d, _, a):rest) bpor =
    let tid'     = tidOf tid d
        cvstate' = updateCVState cvstate a
    in  case M.lookup tid' $ _bdone bpor of
          Just bpor' -> bpor { _bdone  = M.insert tid' (grow' cvstate' tid' rest bpor') $ _bdone bpor }
          Nothing    -> bpor { _btaken = if conservative then _btaken bpor else (tid', a) : _btaken bpor
                            , _bdone  = M.insert tid' (subtree cvstate' tid' (_bsleep bpor ++ _btaken bpor) trc) $ _bdone bpor }
  grow' _ _ [] bpor = bpor

  subtree cvstate tid sleep ((d, ts, a):rest) =
    let cvstate' = updateCVState cvstate a
        sleep'   = filter (not . dependent a) sleep
    in BPOR
        { _brunnable = tids tid d a ts
        , _btodo     = []
        , _bignore   = [tidOf tid d | (d,as) <- ts, willBlockSafely cvstate' $ toList as]
        , _bdone     = M.fromList $ case rest of
          ((d', _, _):_) ->
            let tid' = tidOf tid d'
            in  [(tid', subtree cvstate' tid' sleep' rest)]
          [] -> []
        , _bsleep = sleep'
        , _btaken = case rest of
          ((d', _, a'):_) -> [(tidOf tid d', a')]
          [] -> []
        }

  tids tid d (Fork t)           ts = tidOf tid d : t : map (tidOf tid . fst) ts
  tids tid _ (BlockedPut _)     ts = map (tidOf tid . fst) ts
  tids tid _ (BlockedRead _)    ts = map (tidOf tid . fst) ts
  tids tid _ (BlockedTake _)    ts = map (tidOf tid . fst) ts
  tids tid _ BlockedSTM         ts = map (tidOf tid . fst) ts
  tids tid _ (BlockedThrowTo _) ts = map (tidOf tid . fst) ts
  tids tid _ Stop               ts = map (tidOf tid . fst) ts
  tids tid d _ ts = tidOf tid d : map (tidOf tid . fst) ts

-- | Add new backtracking points, if they have not already been
-- visited, fit into the bound, and aren't in the sleep set.
todo :: ([Decision] -> Bool) -> [BacktrackStep] -> BPOR -> BPOR
todo bv = step where
  step bs bpor =
    let (bpor', bs') = go 0 [] Nothing bs bpor
    in  if all (null . _backtrack) bs'
        then bpor'
        else step bs' bpor'

  go tid pref lastb (b:bs) bpor =
    let (bpor', blocked) = backtrack pref b bpor
        tid'   = tidOf tid . fst $ _decision b
        (child, blocked')  = go tid' (pref++[fst $ _decision b]) (Just b) bs . fromJust $ M.lookup tid' (_bdone bpor)
        bpor'' = bpor' { _bdone = M.insert tid' child $ _bdone bpor' }
    in  case lastb of
         Just b' -> (bpor'', b' { _backtrack = blocked } : blocked')
         Nothing -> (bpor'', blocked')

  go _ _ (Just b') _ bpor = (bpor, [b' { _backtrack = [] }])
  go _ _ Nothing   _ bpor = (bpor, [])

  backtrack pref b bpor =
    let todo' = [ (t,c)
                | (t,c) <- _backtrack b
                , bv $ pref ++ [decisionOf (Just $ activeTid pref) (_brunnable bpor) t]
                , t `notElem` M.keys (_bdone bpor)
                , c || t `notElem` map fst (_bsleep bpor)
                ]
        (blocked, next) = partition (\(t,_) -> t `elem` _bignore bpor) todo'
    in  (bpor { _btodo = nub $ _btodo bpor ++ next }, blocked)

-- * Utilities

-- | Get the resultant 'ThreadId' of a 'Decision', with a default case
-- for 'Continue'.
tidOf :: ThreadId -> Decision -> ThreadId
tidOf _ (Start t)    = t
tidOf _ (SwitchTo t) = t
tidOf tid Continue   = tid

-- | Tag a list of items encapsulating 'Decision's with 'ThreadId's,
-- with an initial default case for 'Continue'.
tidTag :: (a -> Decision) -> ThreadId -> [a] -> [(ThreadId, a)]
tidTag df = go where
  go t (a:as) =
    let t' = tidOf t $ df a
    in (t', a) : go t' as
  go _ [] = []

-- | Get the 'Decision' that would have resulted in this 'ThreadId',
-- given a prior 'ThreadId' (if any) and list of runnable threds.
decisionOf :: Maybe ThreadId -> [ThreadId] -> ThreadId -> Decision
decisionOf prior runnable chosen
  | prior == Just chosen = Continue
  | prior `elem` map Just runnable = SwitchTo chosen
  | otherwise = Start chosen

-- | Get the tid of the currently active thread after executing a
-- series of decisions. The list MUST begin with a 'Start'.
activeTid :: [Decision] -> ThreadId
activeTid = foldl' go 0 where
  go _ (Start t)    = t
  go _ (SwitchTo t) = t
  go t Continue     = t

-- | Count the number of preemptions in a schedule
preEmpCount :: [Decision] -> Int
preEmpCount (SwitchTo _:ds) = 1 + preEmpCount ds
preEmpCount (_:ds) = preEmpCount ds
preEmpCount [] = 0

-- | Check if an action is dependent on another, assumes the actions
-- are from different threads (two actions in the same thread are
-- always dependent).
dependent :: ThreadAction -> (ThreadId, ThreadAction) -> Bool
dependent Lift (_, Lift) = True
dependent (ThrowTo t) (t2, _) = t == t2
dependent d1 (_, d2) = cref || cvar || ctvar where
  cref = Just True == ((\(r1, w1) (r2, w2) -> r1 == r2 && (w1 || w2)) <$> cref' d1 <*> cref' d2)
  cref'  (ReadRef  r) = Just (r, False)
  cref'  (ModRef   r) = Just (r, True)
  cref'  _ = Nothing

  cvar = Just True == ((==) <$> cvar' d1 <*> cvar' d2)
  cvar'  (BlockedPut  _) = Nothing
  cvar'  (BlockedRead _) = Nothing
  cvar'  (BlockedTake _) = Nothing
  cvar'  (TryPut  c _ _) = Just c
  cvar'  (TryTake c _ _) = Just c
  cvar'  (Put  c _) = Just c
  cvar'  (Read c)   = Just c
  cvar'  (Take c _) = Just c
  cvar'  _ = Nothing

  ctvar = ctvar' d1 && ctvar' d2
  ctvar' (STM _)    = True
  ctvar' BlockedSTM = False
  ctvar' _ = False

-- | Variant of 'dependent' to handle 'ThreadAction''s
dependent' :: ThreadAction -> (ThreadId, ThreadAction') -> Bool
dependent' Lift (_, Lift') = True
dependent' (ThrowTo t) (t2, _) = t == t2
dependent' d1 (_, d2) = cref || cvar || ctvar where
  cref = Just True == ((\(r1, w1) (r2, w2) -> r1 == r2 && (w1 || w2)) <$> cref' d1 <*> cref'' d2)
  cref'  (ReadRef  r) = Just (r, False)
  cref'  (ModRef   r) = Just (r, True)
  cref'  _ = Nothing
  cref'' (ReadRef' r) = Just (r, False)
  cref'' (ModRef'  r) = Just (r, True)
  cref'' _ = Nothing

  cvar = Just True == ((==) <$> cvar' d1 <*> cvar'' d2)
  cvar'  (BlockedPut  _) = Nothing
  cvar'  (BlockedRead _) = Nothing
  cvar'  (BlockedTake _) = Nothing
  cvar'  (TryPut  c _ _) = Just c
  cvar'  (TryTake c _ _) = Just c
  cvar'  (Put  c _) = Just c
  cvar'  (Read c)   = Just c
  cvar'  (Take c _) = Just c
  cvar'  _ = Nothing
  cvar'' (TryPut'  c) = Just c
  cvar'' (TryTake' c) = Just c
  cvar'' (Put'  c) = Just c
  cvar'' (Read' c) = Just c
  cvar'' (Take' c) = Just c
  cvar'' _ = Nothing

  ctvar = ctvar' d1 && ctvar'' d2
  ctvar' (STM _)    = True
  ctvar' BlockedSTM = False
  ctvar' _ = False
  ctvar'' STM' = True
  ctvar'' _ = False

-- * Keeping track of 'CVar' full/empty states

-- | Initial global 'CVar' state
initialCVState :: [(CVarId, Bool)]
initialCVState = []

-- | Update the 'CVar' state with the action that has just happened.
updateCVState :: [(CVarId, Bool)] -> ThreadAction -> [(CVarId, Bool)]
updateCVState cvstate (Put  c _) = (c,True)  : filter (/=(c,False)) cvstate
updateCVState cvstate (Take c _) = (c,False) : filter (/=(c,True))  cvstate
updateCVState cvstate (TryPut  c True _) = (c,True)  : filter (/=(c,False)) cvstate
updateCVState cvstate (TryTake c True _) = (c,False) : filter (/=(c,True))  cvstate
updateCVState cvstate _ = cvstate

-- | Check if an action will block.
willBlock :: [(CVarId, Bool)] -> ThreadAction' -> Bool
willBlock cvstate (Put'  c) = (c, True)  `elem` cvstate
willBlock cvstate (Take' c) = (c, False) `elem` cvstate
willBlock _ _ = False

-- | Check if a list of actions will block safely (without modifying
-- any global state). This allows further lookahead at, say, the
-- 'spawn' of a thread (which always starts with 'KnowsAbout'.
willBlockSafely :: [(CVarId, Bool)] -> [ThreadAction'] -> Bool
willBlockSafely cvstate (KnowsAbout':as) = willBlockSafely cvstate as
willBlockSafely cvstate (Forgets':as)    = willBlockSafely cvstate as
willBlockSafely cvstate (AllKnown':as)   = willBlockSafely cvstate as
willBlockSafely cvstate (Put'  c:_) = willBlock cvstate (Put'  c)
willBlockSafely cvstate (Take' c:_) = willBlock cvstate (Take' c)
willBlockSafely _ _ = False