From c4eefd4849a5a8ff66d7b6ea3cffb1268cf24e4c Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Mon, 20 Jul 2015 15:19:51 +0100 Subject: [PATCH] Avoid decisions which will immediately block. If a decision will immediately block without changing the global state, then there is no point in making it: no state will become reachable from it which isn't reachable through some other option we have available. This has three parts: - When the prefix runs out and the scheduler is making decisions, it filters out decisions which will immediately block. - When a subtree is being added, it records which decisions will immediately block. - When backtracking points are being added, it filters out ones in this block list. This optimisation is likely to only be useful when threads are communicating a lot. For instance, a `parMap id` is totally unaffected by this, but the test cases drop from an average of 64 runs to 42. --- Test/DejaFu/SCT.hs | 34 +++++++++++++++++++++----- Test/DejaFu/SCT/Internal.hs | 48 ++++++++++++++++++++++++++++++------- 2 files changed, 67 insertions(+), 15 deletions(-) diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs index 0b4c4f1..99cbf42 100755 --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -32,10 +32,14 @@ module Test.DejaFu.SCT , decisionOf , activeTid , preEmpCount + , initialCVState + , updateCVState + , willBlock ) where import Control.Applicative ((<$>), (<*>)) import Control.DeepSeq (force) +import Data.Maybe (maybeToList) import Test.DejaFu.Deterministic import Test.DejaFu.Deterministic.IO (ConcIO, runConcIO) import Test.DejaFu.SCT.Internal @@ -105,7 +109,7 @@ sctBounded bv backtrack initialise c = go initialState where go bpor = case next bpor of Just (sched, conservative, bpor') -> -- Run the computation - let (res, (_, bs), trace) = runConc (bporSched initialise) (sched, []) c + let (res, (_, bs, _), trace) = runConc (bporSched initialise) (initialSchedState sched) c -- Identify the backtracking points bpoints = findBacktrack backtrack bs trace -- Add new nodes to the tree @@ -125,7 +129,7 @@ sctBoundedIO :: ([Decision] -> Bool) sctBoundedIO bv backtrack initialise c = go initialState where go bpor = case next bpor of Just (sched, conservative, bpor') -> do - (res, (_, bs), trace) <- runConcIO (bporSched initialise) (sched, []) c + (res, (_, bs, _), trace) <- runConcIO (bporSched initialise) (initialSchedState sched) c let bpoints = findBacktrack backtrack bs trace let bpor'' = grow conservative trace bpor' @@ -135,16 +139,34 @@ sctBoundedIO bv backtrack initialise c = go initialState where Nothing -> return [] +-- | Initial scheduler state for a given prefix +initialSchedState :: [ThreadId] -> ([ThreadId], [(NonEmpty (ThreadId, ThreadAction'), [ThreadId])], [(ThreadId, Bool)]) +initialSchedState prefix = (prefix, [], initialCVState) + -- | BPOR 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. bporSched :: (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, ThreadAction') -> NonEmpty ThreadId) - -> Scheduler ([ThreadId], [(NonEmpty (ThreadId, ThreadAction'), [ThreadId])]) + -> Scheduler ([ThreadId], [(NonEmpty (ThreadId, ThreadAction'), [ThreadId])], [(ThreadId, Bool)]) bporSched initialise = force sched where -- If there is a decision available, make it - sched (d:ds, bs) _ threads = (d, (ds, bs ++ [(threads, [])])) + sched (d:ds, bs, cvstate) prior threads = + let cvstate' = maybe cvstate (updateCVState cvstate . snd) prior + in (d, (ds, bs ++ [(threads, [])], cvstate')) -- Otherwise query the initialise function for a list of possible -- choices, and make one of them arbitrarily (recording the others). - sched ([], bs) prior threads = case initialise prior threads of - (next:|rest) -> (next, ([], bs ++ [(threads, rest)])) + sched ([], bs, cvstate) prior threads = + let choices = initialise prior threads + cvstate' = maybe cvstate (updateCVState cvstate . snd) prior + choices' = [t + | t <- toList choices + , a <- maybeToList $ lookup t (toList threads) + , not $ willBlock cvstate' a + ] + in case choices' of + (next:rest) -> (next, ([], bs ++ [(threads, rest)], cvstate')) + + -- TODO: abort the execution here. + [] -> case choices of + (next:|_) -> (next, ([], bs ++ [(threads, [])], cvstate')) diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs index 9a4e57b..07157fb 100755 --- a/Test/DejaFu/SCT/Internal.hs +++ b/Test/DejaFu/SCT/Internal.hs @@ -37,6 +37,11 @@ data BPOR = BPOR , _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)] @@ -54,6 +59,7 @@ initialState :: BPOR initialState = BPOR { _brunnable = [0] , _btodo = [(0, False)] + , _bignore = [] , _bdone = M.empty , _bsleep = [] , _btaken = [] @@ -120,24 +126,27 @@ findBacktrack backtrack = go [] where -- | Add a new trace to the tree, creating a new subtree. grow :: Bool -> Trace -> BPOR -> BPOR -grow conservative = grow' 0 where - grow' tid trc@((d, _, a):rest) bpor = - let tid' = tidOf tid d +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' tid' rest bpor') $ _bdone bpor } + 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 tid' (_bsleep bpor ++ _btaken bpor) trc) $ _bdone bpor } - grow' _ [] bpor = bpor + , _bdone = M.insert tid' (subtree cvstate' tid' (_bsleep bpor ++ _btaken bpor) trc) $ _bdone bpor } + grow' _ _ [] bpor = bpor - subtree tid sleep ((d, ts, a):rest) = - let sleep' = filter (not . dependent a) sleep + 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,a) <- ts, willBlock cvstate' a] , _bdone = M.fromList $ case rest of ((d', _, _):_) -> let tid' = tidOf tid d' - in [(tid', subtree tid' sleep' rest)] + in [(tid', subtree cvstate' tid' sleep' rest)] [] -> [] , _bsleep = sleep' , _btaken = case rest of @@ -169,6 +178,7 @@ todo bv = go 0 [] where | (t,c) <- _backtrack b , bv $ pref ++ [decisionOf (Just $ activeTid pref) (_brunnable bpor) t] , t `notElem` M.keys (_bdone bpor) + , t `notElem` _bignore bpor , c || t `notElem` map fst (_bsleep bpor) ] in bpor { _btodo = todo' } @@ -277,3 +287,23 @@ dependent' d1 (_, d2) = cref || cvar || ctvar where 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