barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2024-12-18 02:51:42 +03:00
Code Issues Projects Releases Wiki Activity

Incrementally compute bounds state

Browse Source 
Closes #104
Closes #105
This commit is contained in:
Michael Walker 2017-09-05 14:00:47 +01:00
parent 915233fec8
commit 36d2a1b2e4
3 changed files with 149 additions and 125 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
dejafu/CHANGELOG.markdown
View File

@ -7,9 +7,20 @@ This project is versioned according to the [Package Versioning Policy](https://p
*de facto* standard Haskell versioning scheme.
0.7.1.2
unreleased
----------
### Miscellaneous
- Slightly improved run-time of systematic testing.
---------------------------------------------------------------------------------------------------
0.7.1.2
-------
- **Date** 2017-08-21
- **Git tag** [dejafu-0.7.1.2][]
- **Hackage** https://hackage.haskell.org/package/dejafu-0.7.1.2

132
dejafu/Test/DejaFu/SCT.hs
View File

@ -111,6 +111,7 @@ import Control.DeepSeq (NFData(..), force)
import Control.Monad.Ref (MonadRef)
import Data.List (foldl')
import qualified Data.Map.Strict as M
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import qualified Data.Set as S
import System.Random (RandomGen, randomR)
@ -354,11 +355,11 @@ noBounds = Bounds
}
-- | Combination bound function
cBound :: Bounds -> BoundFunc
cBound :: Bounds -> IncrementalBoundFunc (((Int, Maybe ThreadId), M.Map ThreadId Int), Int)
cBound (Bounds pb fb lb) =
maybe trueBound pBound pb &+&
maybe trueBound fBound fb &+&
maybe trueBound lBound lb
maybe (trueBound (0, Nothing)) pBound pb &+&
maybe (trueBound M.empty) fBound fb &+&
maybe (trueBound 0) lBound lb
-- | Combination backtracking function. Add all backtracking points
-- corresponding to enabled bound functions.
@ -384,8 +385,10 @@ instance NFData PreemptionBound where
-- | Pre-emption bound function. This does not count pre-emptive
-- context switches to a commit thread.
pBound :: PreemptionBound -> BoundFunc
pBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb
pBound :: PreemptionBound -> IncrementalBoundFunc (Int, Maybe ThreadId)
pBound (PreemptionBound pb) k prior lhead =
let k'@(pcount, _) = preEmpCountInc (fromMaybe (0, Nothing) k) prior lhead
in if pcount <= pb then Just k' else Nothing
-- | Add a backtrack point, and also conservatively add one prior to
-- the most recent transition before that point. This may result in
@ -420,8 +423,10 @@ instance NFData FairBound where
rnf (FairBound i) = rnf i
-- | Fair bound function
fBound :: FairBound -> BoundFunc
fBound (FairBound fb) ts (_, l) = maxYieldCountDiff ts l <= fb
fBound :: FairBound -> IncrementalBoundFunc (M.Map ThreadId Int)
fBound (FairBound fb) k prior lhead =
let k' = yieldCountInc (fromMaybe M.empty k) prior lhead
in if maxDiff (M.elems k') <= fb then Just k' else Nothing
-- | Add a backtrack point. If the thread isn't runnable, or performs
-- a release operation, add all runnable threads.
@ -443,8 +448,10 @@ instance NFData LengthBound where
rnf (LengthBound i) = rnf i
-- | Length bound function
lBound :: LengthBound -> BoundFunc
lBound (LengthBound lb) ts _ = length ts < lb
lBound :: LengthBound -> IncrementalBoundFunc Int
lBound (LengthBound lb) len _ _ =
let len' = maybe 1 (+1) len
in if len' < lb then Just len' else Nothing
-- | Add a backtrack point. If the thread isn't runnable, add all
-- runnable threads.
@ -505,7 +512,7 @@ sctBoundDiscard discard memtype cb conc = go initialState where
if schedIgnore s
then go (force newDPOR)
else checkDiscard discard res trace $ go (force (addBacktracks bpoints newDPOR))
else checkDiscard discard res trace $ go (force (incorporateBacktrackSteps bpoints newDPOR))
Nothing -> pure []
@ -518,9 +525,6 @@ sctBoundDiscard discard memtype cb conc = go initialState where
-- Incorporate a trace into the DPOR tree.
addTrace = incorporateTrace memtype
-- Incorporate the new backtracking steps into the DPOR tree.
addBacktracks = incorporateBacktrackSteps (cBound cb)
-- | SCT via uniform random scheduling.
--
-- Schedules are generated by assigning to each new thread a random
@ -619,63 +623,71 @@ sctWeightedRandomDiscard discard memtype g0 lim0 use0 conc = go g0 (max 0 lim0)
-------------------------------------------------------------------------------
-- Utilities
-- | An incremental version of 'preEmpCount', going one step at a time.
preEmpCountInc
:: (Int, Maybe ThreadId)
-- ^ The number of preemptions so far and, if currently executing a
-- commit thread, what the prior thread was.
-> Maybe (ThreadId, ThreadAction)
-- ^ What just happened.
-> (Decision, a)
-- ^ What's coming up.
-> (Int, Maybe ThreadId)
preEmpCountInc (sofar, lastnoncommit) prior (d, _) = case (prior, d) of
(Just (tid, _), Start tnext) -> cswitch tid tnext False
(Just (tid, act), SwitchTo tnext) -> cswitch tid tnext (not (didYield act))
(_, Continue) -> (sofar, lastnoncommit)
(Nothing, _) -> (sofar, lastnoncommit)
where
cswitch tid tnext isPreemptive
| isCommitThread tnext = (sofar, if isCommitThread tid then lastnoncommit else Just tid)
| isCommitThread tid = (if lastnoncommit == Just tnext then sofar else sofar + 1, Nothing)
| otherwise = (if isPreemptive then sofar + 1 else sofar, Nothing)
isCommitThread = (< initialThread)
-- | An incremental count of yields, going one step at a time.
yieldCountInc
:: M.Map ThreadId Int
-- ^ The number of yields of each thread so far
-> Maybe (ThreadId, a)
-- ^ What just happened.
-> (Decision, Lookahead)
-- ^ What's coming up.
-> M.Map ThreadId Int
yieldCountInc sofar prior (d, lnext) = case prior of
Just (tid, _) -> ycount (tidOf tid d)
Nothing -> ycount initialThread
where
ycount tnext = case lnext of
WillYield -> M.alter (Just . maybe 1 (+1)) tnext sofar
_ -> M.alter (Just . maybe 0 id) tnext sofar
-- | Determine if an action is a commit or not.
isCommitRef :: ThreadAction -> Bool
isCommitRef (CommitCRef _ _) = True
isCommitRef _ = False
-- | Extra threads created in a fork.
forkTids :: ThreadAction -> [ThreadId]
forkTids (Fork t) = [t]
forkTids _ = []
-- | Count the number of yields by a thread in a schedule prefix.
yieldCount :: ThreadId
-- ^ The thread to count yields for.
-> [(Decision, ThreadAction)]
-> Lookahead
-> Int
yieldCount tid ts l = go initialThread ts where
go t ((Start t', act):rest) = go' t t' act rest
go t ((SwitchTo t', act):rest) = go' t t' act rest
go t ((Continue, act):rest) = go' t t act rest
go t []
| t == tid && willYield l = 1
| otherwise = 0
{-# INLINE go' #-}
go' t t' act rest
| t == tid && didYield act = 1 + go t' rest
| otherwise = go t' rest
-- | Get the maximum difference between the yield counts of all
-- threads in this schedule prefix.
maxYieldCountDiff :: [(Decision, ThreadAction)]
-> Lookahead
-> Int
maxYieldCountDiff ts l = go 0 yieldCounts where
go m (yc:ycs) =
let m' = m `max` foldl' (go' yc) 0 ycs
in go m' ycs
-- | Get the maximum difference between two ints in a list.
maxDiff :: [Int] -> Int
maxDiff = go 0 where
go m (x:xs) =
let m' = m `max` foldl' (go' x) 0 xs
in go m' xs
go m [] = m
go' yc0 m yc = m `max` abs (yc0 - yc)
yieldCounts = [yieldCount t ts l | t <- allTids ts]
-- All the threads created during the lifetime of the system.
allTids ((_, act):rest) =
let tids' = forkTids act
in if null tids' then allTids rest else tids' ++ allTids rest
allTids [] = [initialThread]
go' x0 m x = m `max` abs (x0 - x)
-- | The \"true\" bound, which allows everything.
trueBound :: BoundFunc
trueBound _ _ = True
trueBound :: k -> IncrementalBoundFunc k
trueBound k _ _ _ = Just k
-- | Combine two bounds into a larger bound, where both must be
-- satisfied.
(&+&) :: BoundFunc -> BoundFunc -> BoundFunc
(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl
(&+&) :: IncrementalBoundFunc k1 -> IncrementalBoundFunc k2 -> IncrementalBoundFunc (k1, k2)
(&+&) f1 f2 ks prior lhead =
let k1' = f1 (fst <$> ks) prior lhead
k2' = f2 (snd <$> ks) prior lhead
in (,) <$> k1' <*> k2'
-- | Apply the discard function.
checkDiscard :: Functor f => (a -> Maybe Discard) -> a -> [b] -> f [(a, [b])] -> f [(a, [b])]

129
dejafu/Test/DejaFu/SCT/Internal.hs
View File

@ -1,10 +1,12 @@
{-# LANGUAGE TupleSections #-}
-- |
-- Module : Test.DejaFu.SCT.Internal
-- Copyright : (c) 2016 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : portable
-- Portability : TupleSections
--
-- Internal types and functions for dynamic partial-order
-- reduction. This module is NOT considered to form part of the public
@ -17,7 +19,7 @@ import Control.Exception (MaskingState(..))
import qualified Data.Foldable as F
import Data.Function (on)
import Data.List (nubBy, partition, sortOn)
import Data.List.NonEmpty (NonEmpty(..), toList)
import Data.List.NonEmpty (toList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
import Data.Maybe (catMaybes, fromJust, fromMaybe, isJust,
@ -216,9 +218,9 @@ findBacktrackSteps
-> Bool
-- ^ Whether the computation was aborted due to no decisions being
-- in-bounds.
-> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])
-- ^ A sequence of threads at each step: the nonempty list of
-- runnable threads (with lookahead values), and the list of threads
-> Seq ([(ThreadId, Lookahead)], [ThreadId])
-- ^ A sequence of threads at each step: the list of runnable
-- in-bound threads (with lookahead values), and the list of threads
-- still to try. The reason for the two separate lists is because
-- the threads chosen to try will be dependent on the specific
-- domain.
@ -235,11 +237,11 @@ findBacktrackSteps memtype backtrack boundKill = go initialDepState S.empty init
{ bcktThreadid = tid'
, bcktDecision = d
, bcktAction = a
, bcktRunnable = M.fromList . toList $ e
, bcktRunnable = M.fromList e
, bcktBacktracks = M.fromList $ map (\i' -> (i', False)) i
, bcktState = state'
}
bs' = doBacktrack killsEarly allThreads' (toList e) (bs++[this])
bs' = doBacktrack killsEarly allThreads' e (bs++[this])
runnable = S.fromList (M.keys $ bcktRunnable this)
allThreads' = allThreads `S.union` runnable
killsEarly = null ts && boundKill
@ -280,53 +282,44 @@ findBacktrackSteps memtype backtrack boundKill = go initialDepState S.empty init
in backtrack bs idxs
-- | Add new backtracking points, if they have not already been
-- visited, fit into the bound, and aren't in the sleep set.
incorporateBacktrackSteps
:: ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool)
-- ^ Bound function: returns true if that schedule prefix terminated
-- with the lookahead decision fits within the bound.
-> [BacktrackStep]
-- ^ Backtracking steps identified by 'findBacktrackSteps'.
-> DPOR
-> DPOR
incorporateBacktrackSteps bv = go Nothing [] where
go priorTid pref (b:bs) dpor =
let dpor' = doBacktrack priorTid pref b dpor
tid = bcktThreadid b
pref' = pref ++ [(bcktDecision b, bcktAction b)]
child = case dporNext dpor of
Just (t, d)
| t /= tid -> err "incorporateBacktrackSteps" "incorporating wrong trace!"
| otherwise -> go (Just t) pref' bs d
Nothing -> err "incorporateBacktrackSteps" "child is missing!"
in dpor' { dporNext = Just (tid, child) }
go _ _ [] dpor = dpor
-- visited and aren't in the sleep set.
incorporateBacktrackSteps :: [BacktrackStep] -> DPOR -> DPOR
incorporateBacktrackSteps (b:bs) dpor = dpor' where
tid = bcktThreadid b
doBacktrack priorTid pref b dpor =
let todo' = [ x
| x@(t,c) <- M.toList $ bcktBacktracks b
, let decision = decisionOf priorTid (dporRunnable dpor) t
, let lahead = fromJust . M.lookup t $ bcktRunnable b
, bv pref (decision, lahead)
, Just t /= (fst <$> dporNext dpor)
, S.notMember t (dporDone dpor)
, c || M.notMember t (dporSleep dpor)
]
in dpor { dporTodo = dporTodo dpor `M.union` M.fromList todo' }
dpor' = dpor
{ dporTodo = dporTodo dpor `M.union` M.fromList todo
, dporNext = Just (tid, child)
}
todo =
[ x
| x@(t,c) <- M.toList $ bcktBacktracks b
, Just t /= (fst <$> dporNext dpor)
, S.notMember t (dporDone dpor)
, c || M.notMember t (dporSleep dpor)
]
child = case dporNext dpor of
Just (t, d)
| t /= tid -> err "incorporateBacktrackSteps" "incorporating wrong trace!"
| otherwise -> incorporateBacktrackSteps bs d
Nothing -> err "incorporateBacktrackSteps" "child is missing!"
incorporateBacktrackSteps [] dpor = dpor
-------------------------------------------------------------------------------
-- * DPOR scheduler
-- | The scheduler state
data DPORSchedState = DPORSchedState
data DPORSchedState k = DPORSchedState
{ schedSleep :: Map ThreadId ThreadAction
-- ^ The sleep set: decisions not to make until something dependent
-- with them happens.
, schedPrefix :: [ThreadId]
-- ^ Decisions still to make
, schedBPoints :: Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])
-- ^ Which threads are runnable at each step, and the alternative
-- decisions still to make.
, schedBPoints :: Seq ([(ThreadId, Lookahead)], [ThreadId])
-- ^ Which threads are runnable and in-bound at each step, and the
-- alternative decisions still to make.
, schedIgnore :: Bool
-- ^ Whether to ignore this execution or not: @True@ if the
-- execution is aborted due to all possible decisions being in the
@ -338,15 +331,18 @@ data DPORSchedState = DPORSchedState
, schedDepState :: DepState
-- ^ State used by the dependency function to determine when to
-- remove decisions from the sleep set.
, schedBState :: Maybe k
-- ^ State used by the incremental bounding function.
} deriving (Eq, Show)
instance NFData DPORSchedState where
instance NFData k => NFData (DPORSchedState k) where
rnf s = rnf ( schedSleep s
, schedPrefix s
, schedBPoints s
, schedIgnore s
, schedBoundKill s
, schedDepState s
, schedBState s
)
-- | Initial DPOR scheduler state for a given prefix
@ -354,7 +350,7 @@ initialDPORSchedState :: Map ThreadId ThreadAction
-- ^ The initial sleep set.
-> [ThreadId]
-- ^ The schedule prefix.
-> DPORSchedState
-> DPORSchedState k
initialDPORSchedState sleep prefix = DPORSchedState
{ schedSleep = sleep
, schedPrefix = prefix
@ -362,13 +358,14 @@ initialDPORSchedState sleep prefix = DPORSchedState
, schedIgnore = False
, schedBoundKill = False
, schedDepState = initialDepState
, schedBState = Nothing
}
-- | A bounding function takes the scheduling decisions so far and a
-- decision chosen to come next, and returns if that decision is
-- within the bound.
type BoundFunc
= [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool
-- | An incremental bounding function is a stateful function that
-- takes the last and next decisions, and returns a new state only if
-- the next decision is within the bound.
type IncrementalBoundFunc k
= Maybe k -> Maybe (ThreadId, ThreadAction) -> (Decision, Lookahead) -> Maybe k
-- | A backtracking step is a point in the execution where another
-- decision needs to be made, in order to explore interesting new
@ -439,21 +436,23 @@ backtrackAt toAll bs0 = backtrackAt' . nubBy ((==) `on` fst') . sortOn fst' wher
dporSched
:: MemType
-- ^ Memory model.
-> BoundFunc
-> IncrementalBoundFunc k
-- ^ Bound function: returns true if that schedule prefix terminated
-- with the lookahead decision fits within the bound.
-> Scheduler DPORSchedState
dporSched memtype inBound trc prior threads s = schedule where
-> Scheduler (DPORSchedState k)
dporSched memtype boundf _ prior threads s = schedule where
-- Pick a thread to run.
schedule = case schedPrefix s of
-- If there is a decision available, make it
(d:ds) -> (Just d, (nextState []) { schedPrefix = ds })
(t:ts) ->
let bstate' = boundf (schedBState s) prior (decision t, action t)
in (Just t, (nextState []) { schedPrefix = ts, schedBState = bstate' })
-- Otherwise query the initialise function for a list of possible
-- choices, filter out anything in the sleep set, and make one of
-- them arbitrarily (recording the others).
[] ->
let choices = restrictToBound initialise
let choices = restrictToBound id initialise
checkDep t a = case prior of
Just (tid, act) -> dependent memtype (schedDepState s) tid act t a
Nothing -> False
@ -462,12 +461,15 @@ dporSched memtype inBound trc prior threads s = schedule where
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' })
(nextTid:rest) ->
let bstate' = boundf (schedBState s) prior (decision nextTid, action nextTid)
in (Just nextTid, (nextState rest) { schedSleep = ssleep', schedBState = bstate' })
[] ->
(Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill', schedBState = Nothing })
-- The next scheduler state
nextState rest = s
{ schedBPoints = schedBPoints s |> (threads, rest)
{ schedBPoints = schedBPoints s |> (restrictToBound fst threads', rest)
, schedDepState = nextDepState
}
nextDepState = let ds = schedDepState s in maybe ds (uncurry $ updateDepState ds) prior
@ -478,7 +480,7 @@ dporSched memtype inBound trc prior threads s = schedule where
initialise = tryDaemons . yieldsToEnd $ case prior of
Just (tid, act)
| not (didYield act) && tid `elem` tids -> [tid]
_ -> tids'
_ -> tids
-- If one of the chosen actions will kill the computation, and there
-- are daemon threads, try them instead.
@ -501,30 +503,29 @@ dporSched memtype inBound trc prior threads s = schedule where
-- See commits a056f54 and 8554ce9, and my 4th June comment in issue
-- #52.
tryDaemons ts
| any doesKill ts = case partition doesKill tids' of
| any doesKill ts = case partition doesKill tids of
(kills, nokills) -> nokills ++ kills
| otherwise = ts
doesKill t = killsDaemons t (action t)
-- Restrict the possible decisions to those in the bound.
restrictToBound = filter (\t -> inBound trc (decision t, action t))
restrictToBound f = filter (\x -> let t = f x in isJust $ boundf (schedBState s) prior (decision t, action t))
-- Move the threads which will immediately yield to the end of the list
yieldsToEnd ts = case partition (willYield . action) ts of
(yields, noyields) -> noyields ++ yields
-- Get the decision that will lead to a thread being scheduled.
decision = decisionOf (fst <$> prior) (S.fromList tids')
decision = decisionOf (fst <$> prior) (S.fromList tids)
-- Get the action of a thread
action t = fromJust $ lookup t threads'
-- The runnable thread IDs
tids = fst <$> threads
tids = map fst threads'
-- The runnable threads as a normal list.
threads' = toList threads
tids' = toList tids
-------------------------------------------------------------------------------
-- Weighted random scheduler