mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-18 19:11:37 +03:00
Implement sleep sets for BPOR.
This further improves performance in all cases, although it's still far worse on some of the included tests, and I have yet to figure out why. See also: "Partial-Order Methods for the Verication of Concurrent Systems" [Godefroid 1996]
This commit is contained in:
Michael Walker
parent
c12cbcf707
commit
aadb27ea1f
@ -35,17 +35,11 @@ module Test.DejaFu.SCT
|
||||
) where
|
||||
|
||||
import Control.Applicative ((<$>), (<*>))
|
||||
import Control.Arrow (first)
|
||||
import Control.DeepSeq (NFData(..), force)
|
||||
import Data.List (nub)
|
||||
import Data.Map (Map)
|
||||
import Data.Maybe (mapMaybe, fromJust)
|
||||
import Control.DeepSeq (force)
|
||||
import Test.DejaFu.Deterministic
|
||||
import Test.DejaFu.Deterministic.IO (ConcIO, runConcIO)
|
||||
import Test.DejaFu.SCT.Internal
|
||||
|
||||
import qualified Data.Map as M
|
||||
|
||||
-- * Pre-emption bounding
|
||||
|
||||
-- | An SCT runner using a pre-emption bounding scheduler.
|
||||
@ -65,14 +59,14 @@ pbBv pb ds = preEmpCount ds <= pb
|
||||
-- the same state being reached multiple times, but is needed because
|
||||
-- of the artificial dependency imposed by the bound.
|
||||
pbBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]
|
||||
pbBacktrack bs i tid = backtrack (backtrack bs i tid) (maximum js) tid where
|
||||
js = 0:[j | ((_,t1), (j,t2)) <- (zip <*> tail) . zip [0..] $ tidTag (fst . _decision) 0 bs, t1 /= t2, j < i]
|
||||
pbBacktrack bs i tid = backtrack True (backtrack False bs i tid) (maximum js) tid where
|
||||
js = 0:[j | ((_,(t1,_)), (j,(t2,_))) <- (zip <*> tail) . zip [0..] $ tidTag (fst . _decision) 0 bs, t1 /= t2, j < i]
|
||||
|
||||
backtrack (b:bs) 0 t
|
||||
| t `elem` _runnable b = b { _backtrack = nub $ t : _backtrack b } : bs
|
||||
| otherwise = b { _backtrack = _runnable b } : bs
|
||||
backtrack (b:bs) n t = b : backtrack bs (n-1) t
|
||||
backtrack [] _ _ = error "Ran out of schedule whilst backtracking!"
|
||||
backtrack c (b:bs) 0 t
|
||||
| t `elem` _runnable b = b { _backtrack = (if any ((==t) . fst) $ _backtrack b then id else (++[(t,c)])) $ _backtrack b } : bs
|
||||
| otherwise = b { _backtrack = [(t,c) | t <- _runnable b] } : bs
|
||||
backtrack c (b:bs) n t = b : backtrack c bs (n-1) t
|
||||
backtrack _ [] _ _ = error "Ran out of schedule whilst backtracking!"
|
||||
|
||||
-- | Pick a new thread to run. Choose the current thread if available,
|
||||
-- otherwise add all runnable threads.
|
||||
@ -109,13 +103,13 @@ sctBounded :: ([Decision] -> Bool)
|
||||
-> (forall t. Conc t a) -> [(Either Failure a, Trace)]
|
||||
sctBounded bv backtrack initialise c = go initialState where
|
||||
go bpor = case next bpor of
|
||||
Just (sched, bpor') ->
|
||||
Just (sched, conservative, bpor') ->
|
||||
-- Run the computation
|
||||
let (res, (_, bs), trace) = runConc (bporSched initialise) (sched, []) c
|
||||
-- Identify the backtracking points
|
||||
bpoints = findBacktrack False backtrack bs trace
|
||||
bpoints = findBacktrack backtrack bs trace
|
||||
-- Add new nodes to the tree
|
||||
bpor'' = grow trace bpor'
|
||||
bpor'' = grow conservative trace bpor'
|
||||
-- Add new backtracking information
|
||||
bpor''' = todo bv bpoints bpor''
|
||||
-- Loop
|
||||
@ -130,11 +124,11 @@ sctBoundedIO :: ([Decision] -> Bool)
|
||||
-> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]
|
||||
sctBoundedIO bv backtrack initialise c = go initialState where
|
||||
go bpor = case next bpor of
|
||||
Just (sched, bpor') -> do
|
||||
Just (sched, conservative, bpor') -> do
|
||||
(res, (_, bs), trace) <- runConcIO (bporSched initialise) (sched, []) c
|
||||
|
||||
let bpoints = findBacktrack True backtrack bs trace
|
||||
let bpor'' = grow trace bpor'
|
||||
let bpoints = findBacktrack backtrack bs trace
|
||||
let bpor'' = grow conservative trace bpor'
|
||||
let bpor''' = todo bv bpoints bpor''
|
||||
|
||||
((res, trace):) <$> go bpor'''
|
||||
|
||||
@ -2,7 +2,6 @@
|
||||
module Test.DejaFu.SCT.Internal where
|
||||
|
||||
import Control.Applicative ((<$>), (<*>))
|
||||
import Control.Arrow (first)
|
||||
import Control.DeepSeq (NFData(..))
|
||||
import Data.List (foldl', nub, sortBy)
|
||||
import Data.Ord (Down(..), comparing)
|
||||
@ -22,8 +21,9 @@ data BacktrackStep = BacktrackStep
|
||||
-- ^ What happened at this step.
|
||||
, _runnable :: [ThreadId]
|
||||
-- ^ The threads runnable at this step
|
||||
, _backtrack :: [ThreadId]
|
||||
-- ^ The list of alternative threads to run.
|
||||
, _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
|
||||
@ -34,43 +34,56 @@ instance NFData BacktrackStep where
|
||||
data BPOR = BPOR
|
||||
{ _brunnable :: [ThreadId]
|
||||
-- ^ What threads are runnable at this step.
|
||||
, _btodo :: [ThreadId]
|
||||
-- ^ Follow-on decisions still to make.
|
||||
, _btodo :: [(ThreadId, Bool)]
|
||||
-- ^ Follow-on decisions still to make, and whether that decision
|
||||
-- was added conservatively due to the bound.
|
||||
, _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]
|
||||
, _btodo = [(0, False)]
|
||||
, _bdone = M.empty
|
||||
, _bsleep = []
|
||||
, _btaken = []
|
||||
}
|
||||
|
||||
-- | Produce a new schedule from a BPOR tree. If there are no new
|
||||
-- schedules remaining, return 'Nothing'.
|
||||
-- schedules remaining, return 'Nothing'. Also returns whether the
|
||||
-- decision made was added conservatively.
|
||||
--
|
||||
-- This returns the prefix with the most preemptions in, on the
|
||||
-- assumption that preemptions are likely to exhibit bugs, and so lead
|
||||
-- to earlier test failures.
|
||||
next :: BPOR -> Maybe ([ThreadId], BPOR)
|
||||
-- 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 (:[]) fst) prefixes
|
||||
sorted = sortBy (comparing $ Down . preEmps tid bpor . either (\(a,_) -> [a]) (\(a,_,_) -> a)) prefixes
|
||||
|
||||
in case sorted of
|
||||
-- If the schedule with the most preemptions is from the done list, update that.
|
||||
(Right (ts@(t:_), b):_) -> Just (ts, bpor { _bdone = M.insert t b $ _bdone bpor })
|
||||
-- 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:_) -> Just ([t], bpor { _btodo = filter (/=t) $ _btodo bpor })
|
||||
(Left (t,c):_) -> Just ([t], c, bpor { _btodo = filter (/=(t,c)) $ _btodo bpor })
|
||||
|
||||
_ -> Nothing
|
||||
|
||||
go' (tid, bpor) = Right . first (tid:) <$> go tid bpor
|
||||
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
|
||||
@ -79,14 +92,13 @@ next = go 0 where
|
||||
|
||||
-- | Produce a list of new backtracking points from an execution
|
||||
-- trace.
|
||||
findBacktrack :: Bool
|
||||
-> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])
|
||||
findBacktrack :: ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])
|
||||
-> [(NonEmpty (ThreadId, ThreadAction'), [ThreadId])]
|
||||
-> Trace
|
||||
-> [BacktrackStep]
|
||||
findBacktrack deplifts backtrack = go [] where
|
||||
findBacktrack backtrack = go [] where
|
||||
go bs ((e,i):is) ((d,_,a):ts) =
|
||||
let this = BacktrackStep { _decision = (d, a), _runnable = map fst . toList $ e, _backtrack = i }
|
||||
let this = BacktrackStep { _decision = (d, a), _runnable = map fst . toList $ e, _backtrack = map (\i' -> (i', False)) i }
|
||||
bs' = doBacktrack (toList e) bs
|
||||
in go (bs' ++ [this]) is ts
|
||||
go bs _ _ = bs
|
||||
@ -99,7 +111,7 @@ findBacktrack deplifts backtrack = go [] where
|
||||
, let is = [ i
|
||||
| (i, (t, b)) <- zip [0..] $ tidTag (fst . _decision) 0 bs
|
||||
, t == v
|
||||
, dependent deplifts (snd $ _decision b) (u, n)
|
||||
, dependent' (snd $ _decision b) (u, n)
|
||||
]
|
||||
, not $ null is] :: [(Int, ThreadId)]
|
||||
in foldl' (\bs (i, u) -> backtrack bs i u) bs idxs
|
||||
@ -107,22 +119,29 @@ findBacktrack deplifts backtrack = go [] where
|
||||
allThreads = nub . concatMap _runnable
|
||||
|
||||
-- | Add a new trace to the tree, creating a new subtree.
|
||||
grow :: Trace -> BPOR -> BPOR
|
||||
grow = grow' 0 where
|
||||
grow' tid trc@((d, _, _):rest) bpor =
|
||||
grow :: Bool -> Trace -> BPOR -> BPOR
|
||||
grow conservative = grow' 0 where
|
||||
grow' tid trc@((d, _, a):rest) bpor =
|
||||
let tid' = tidOf tid d
|
||||
in case M.lookup tid' $ _bdone bpor of
|
||||
Just bpor' -> bpor { _bdone = M.insert tid' (grow' tid' rest bpor') $ _bdone bpor }
|
||||
Nothing -> bpor { _bdone = M.insert tid' (subtree tid' trc) $ _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
|
||||
|
||||
subtree tid ((d, ts, a):rest) = BPOR
|
||||
subtree tid sleep ((d, ts, a):rest) =
|
||||
let sleep' = filter (not . dependent a) sleep
|
||||
in BPOR
|
||||
{ _brunnable = tids tid d a ts
|
||||
, _btodo = []
|
||||
, _bdone = M.fromList $ case rest of
|
||||
((d', _, _):_) ->
|
||||
let tid' = tidOf tid d'
|
||||
in [(tid', subtree tid' rest)]
|
||||
in [(tid', subtree tid' sleep' rest)]
|
||||
[] -> []
|
||||
, _bsleep = sleep'
|
||||
, _btaken = case rest of
|
||||
((d', _, a'):_) -> [(tidOf tid d', a')]
|
||||
[] -> []
|
||||
}
|
||||
|
||||
@ -136,7 +155,7 @@ grow = grow' 0 where
|
||||
tids tid d _ ts = tidOf tid d : map (tidOf tid . fst) ts
|
||||
|
||||
-- | Add new backtracking points, if they have not already been
|
||||
-- visited and fit into the bound.
|
||||
-- visited, fit into the bound, and aren't in the sleep set.
|
||||
todo :: ([Decision] -> Bool) -> [BacktrackStep] -> BPOR -> BPOR
|
||||
todo bv = go 0 [] where
|
||||
go tid pref (b:bs) bpor =
|
||||
@ -146,10 +165,11 @@ todo bv = go 0 [] where
|
||||
go _ _ _ bpor = bpor
|
||||
|
||||
backtrack pref b bpor =
|
||||
let todo' = nub $ _btodo bpor ++ [ t
|
||||
| t <- _backtrack b
|
||||
let todo' = nub $ _btodo bpor ++ [ (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)
|
||||
]
|
||||
in bpor { _btodo = todo' }
|
||||
|
||||
@ -196,10 +216,36 @@ 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 :: Bool -> ThreadAction -> (ThreadId, ThreadAction') -> Bool
|
||||
dependent deplifts Lift (_, Lift') = deplifts
|
||||
dependent _ (ThrowTo t) (t2, _) = t == t2
|
||||
dependent _ d1 (_, d2) = cref || cvar || ctvar where
|
||||
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)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user