dpor (empty) → 0.1.0.0
raw patch · 6 files changed
+1229/−0 lines, 6 filesdep +basedep +containersdep +deepseqsetup-changed
Dependencies added: base, containers, deepseq, random, semigroups
Files
- LICENSE +20/−0
- Setup.hs +2/−0
- Test/DPOR.hs +484/−0
- Test/DPOR/Internal.hs +510/−0
- Test/DPOR/Schedule.hs +140/−0
- dpor.cabal +73/−0
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2016 Michael Walker++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Test/DPOR.hs view
@@ -0,0 +1,484 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++-- | Systematic testing of concurrent computations through dynamic+-- partial-order reduction and schedule bounding.+module Test.DPOR+ ( -- * Bounded dynamic partial-order reduction++ -- | We can characterise the state of a concurrent computation by+ -- considering the ordering of dependent events. This is a partial+ -- order: independent events can be performed in any order without+ -- affecting the result, and so are /not/ ordered.+ --+ -- Partial-order reduction is a technique for computing these+ -- partial orders, and only testing one total order for each partial+ -- order. This cuts down the amount of work to be done+ -- significantly. /Bounded/ partial-order reduction is a further+ -- optimisation, which only considers schedules within some bound.+ --+ -- This module provides a generic function for DPOR, parameterised+ -- by the actual (domain-specific) dependency function to use.+ --+ -- See /Bounded partial-order reduction/, K. Coons, M. Musuvathi,+ -- K. McKinley for more details.++ dpor+ , simpleDPOR+ , DPOR(..)++ -- ** Backtracking++ , BacktrackFunc+ , BacktrackStep(..)+ , backtrackAt++ -- ** Bounding++ , BoundFunc+ , (&+&)+ , trueBound++ -- *** Preemption++ -- | DPOR with preemption bounding. This adds conservative+ -- backtracking points at the prior context switch whenever a+ -- non-conervative backtracking point is added, as alternative+ -- decisions can influence the reachability of different states.+ --+ -- See the BPOR paper for more details.++ , PreemptionBound(..)+ , defaultPreemptionBound+ , preempBound+ , preempBacktrack+ , preempCount++ -- *** Fair++ -- | DPOR using fair bounding. This bounds the maximum difference+ -- between the number of yield operations different threads have+ -- performed.+ --+ -- See the DPOR paper for more details.++ , FairBound(..)+ , defaultFairBound+ , fairBound+ , fairBacktrack+ , yieldCount+ , maxYieldCountDiff++ -- *** Length++ -- | BPOR using length bounding. This bounds the maximum length (in+ -- terms of primitive actions) of an execution.++ , LengthBound(..)+ , defaultLengthBound+ , lenBound+ , lenBacktrack++ -- * Scheduling & execution traces++ -- | The partial-order reduction is driven by incorporating+ -- information gained from trial executions of the concurrent+ -- program.++ , DPORScheduler+ , SchedState+ , Trace++ , module Test.DPOR.Schedule+ ) where++import Control.DeepSeq (NFData)+import Data.List (nub)+import Data.Maybe (isNothing)+import qualified Data.Map.Strict as M++import Test.DPOR.Internal+import Test.DPOR.Schedule++-------------------------------------------------------------------------------+-- Bounded dynamic partial-order reduction++-- | Dynamic partial-order reduction.+--+-- This takes a lot of functional parameters because it's so generic,+-- but most are fairly simple.+--+-- Some state may be maintained when determining backtracking points,+-- which can then inform the dependency functions. This state is not+-- preserved between different schedules, and built up from scratch+-- each time.+--+-- The dependency functions must be consistent: if we can convert+-- between @action@ and @lookahead@, and supply some sensible default+-- state, then (1) == true implies that (2) is. In practice, (1) is+-- the most specific and (2) will be more pessimistic (due to,+-- typically, less information being available when merely looking+-- ahead).+dpor :: ( Ord tid+ , NFData tid+ , NFData action+ , NFData lookahead+ , NFData s+ , Monad m+ )+ => (action -> Bool)+ -- ^ Determine if a thread yielded.+ -> (lookahead -> Bool)+ -- ^ Determine if a thread will yield.+ -> s+ -- ^ The initial state for backtracking.+ -> (s -> action -> s)+ -- ^ The backtracking state step function.+ -> (s -> (tid, action) -> (tid, action) -> Bool)+ -- ^ The dependency (1) function.+ -> (s -> (tid, action) -> (tid, lookahead) -> Bool)+ -- ^ The dependency (2) function.+ -> tid+ -- ^ The initial thread.+ -> (tid -> Bool)+ -- ^ The thread partitioning function: when choosing what to+ -- execute, prefer threads which return true.+ -> BoundFunc tid action lookahead+ -- ^ The bounding function.+ -> BacktrackFunc tid action lookahead s+ -- ^ The backtracking function. Note that, for some bounding+ -- functions, this will need to add conservative backtracking+ -- points.+ -> (DPOR tid action -> DPOR tid action)+ -- ^ Some post-processing to do after adding the new to-do points.+ -> (DPORScheduler tid action lookahead s+ -> SchedState tid action lookahead s+ -> m (a, SchedState tid action lookahead s, Trace tid action lookahead))+ -- ^ The runner: given the scheduler and state, execute the+ -- computation under that scheduler.+ -> m [(a, Trace tid action lookahead)]+dpor didYield+ willYield+ stinit+ ststep+ dependency1+ dependency2+ initialTid+ predicate+ inBound+ backtrack+ transform+ run+ = go (initialState initialTid)++ where+ -- Repeatedly run the computation gathering all the results and+ -- traces into a list until there are no schedules remaining to+ -- try.+ go dp = case nextPrefix dp of+ Just (prefix, conservative, sleep) -> do+ (res, s, trace) <- run scheduler+ (initialSchedState stinit sleep prefix)++ let bpoints = findBacktracks s trace+ let newDPOR = addTrace conservative trace dp++ if schedIgnore s+ then go newDPOR+ else ((res, trace):) <$> go (transform $ addBacktracks bpoints newDPOR)++ Nothing -> pure []++ -- Find the next schedule prefix.+ nextPrefix = findSchedulePrefix predicate++ -- The DPOR scheduler.+ scheduler = dporSched didYield willYield dependency1 ststep inBound++ -- Find the new backtracking steps.+ findBacktracks = findBacktrackSteps stinit ststep dependency2 backtrack .+ schedBPoints++ -- Incorporate a trace into the DPOR tree.+ addTrace = incorporateTrace stinit ststep dependency1++ -- Incorporate the new backtracking steps into the DPOR tree.+ addBacktracks = incorporateBacktrackSteps inBound++-- | A much simplified DPOR function: no state, no preference between+-- threads, and no post-processing between iterations.+simpleDPOR :: ( Ord tid+ , NFData tid+ , NFData action+ , NFData lookahead+ , Monad m+ )+ => (action -> Bool)+ -- ^ Determine if a thread yielded.+ -> (lookahead -> Bool)+ -- ^ Determine if a thread will yield.+ -> ((tid, action) -> (tid, action) -> Bool)+ -- ^ The dependency (1) function.+ -> ((tid, action) -> (tid, lookahead) -> Bool)+ -- ^ The dependency (2) function.+ -> tid+ -- ^ The initial thread.+ -> BoundFunc tid action lookahead+ -- ^ The bounding function.+ -> BacktrackFunc tid action lookahead ()+ -- ^ The backtracking function. Note that, for some bounding+ -- functions, this will need to add conservative backtracking+ -- points.+ -> (DPORScheduler tid action lookahead ()+ -> SchedState tid action lookahead ()+ -> m (a, SchedState tid action lookahead (), Trace tid action lookahead))+ -- ^ The runner: given the scheduler and state, execute the+ -- computation under that scheduler.+ -> m [(a, Trace tid action lookahead)]+simpleDPOR didYield+ willYield+ dependency1+ dependency2+ initialTid+ inBound+ backtrack+ = dpor didYield+ willYield+ ()+ (\_ _ -> ())+ (const dependency1)+ (const dependency2)+ initialTid+ (const True)+ inBound+ backtrack+ id++-- | Add a backtracking point. If the thread isn't runnable, add all+-- runnable threads. If the backtracking point is already present,+-- don't re-add it UNLESS this would make it conservative.+backtrackAt :: Ord tid+ => (BacktrackStep tid action lookahead s -> Bool)+ -- ^ If this returns @True@, backtrack to all runnable threads,+ -- rather than just the given thread.+ -> Bool+ -- ^ Is this backtracking point conservative? Conservative points+ -- are always explored, whereas non-conservative ones might be+ -- skipped based on future information.+ -> BacktrackFunc tid action lookahead s+backtrackAt toAll conservative bs i tid = go bs i where+ go bx@(b:rest) 0+ -- If the backtracking point is already present, don't re-add it,+ -- UNLESS this would force it to backtrack (it's conservative)+ -- where before it might not.+ | 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 just backtrack to everything runnable.+ | otherwise = b { bcktBacktracks = backtrackAll b } : rest++ go (b:rest) n = b : go rest (n-1)+ go [] _ = error "backtrackAt: Ran out of schedule whilst backtracking!"++ -- Backtrack to a single thread+ backtrackTo = M.insert tid conservative . bcktBacktracks++ -- Backtrack to all runnable threads+ backtrackAll = M.map (const conservative) . bcktRunnable++-------------------------------------------------------------------------------+-- Bounds++-- | Combine two bounds into a larger bound, where both must be+-- satisfied.+(&+&) :: BoundFunc tid action lookahead+ -> BoundFunc tid action lookahead+ -> BoundFunc tid action lookahead+(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl++-- | The \"true\" bound, which allows everything.+trueBound :: BoundFunc tid action lookahead+trueBound _ _ = True++-------------------------------------------------------------------------------+-- Preemption bounding++newtype PreemptionBound = PreemptionBound Int+ deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)++-- | A sensible default preemption bound: 2.+--+-- See /Concurrency Testing Using Schedule Bounding: an Empirical Study/,+-- P. Thomson, A. F. Donaldson, A. Betts for justification.+defaultPreemptionBound :: PreemptionBound+defaultPreemptionBound = 2++-- | Preemption bound function+preempBound :: (action -> Bool)+ -- ^ Determine if a thread yielded.+ -> PreemptionBound+ -> BoundFunc tid action lookahead+preempBound didYield (PreemptionBound pb) ts dl =+ preempCount didYield ts dl <= pb++-- | Add a backtrack point, and also conservatively add one prior to+-- the most recent transition before that point. This may result in+-- the same state being reached multiple times, but is needed because+-- of the artificial dependency imposed by the bound.+preempBacktrack :: Ord tid+ => (action -> Bool)+ -- ^ If this is true of the action at a preemptive context switch,+ -- do NOT use that point for the conservative point, try earlier.+ -> BacktrackFunc tid action lookahead s+preempBacktrack ignore bs i tid =+ maybe id (\j' b -> backtrack True b j' tid) j $ backtrack False bs i tid++ where+ -- Index of the conservative point+ j = goJ . reverse . pairs $ zip [0..i-1] bs where+ goJ (((_,b1), (j',b2)):rest)+ | bcktThreadid b1 /= bcktThreadid b2+ && not (ignore . snd $ bcktDecision b1)+ && not (ignore . snd $ bcktDecision b2) = Just j'+ | otherwise = goJ rest+ goJ [] = Nothing++ -- List of adjacent pairs+ {-# INLINE pairs #-}+ pairs = zip <*> tail++ -- Add a backtracking point.+ backtrack = backtrackAt $ const False++-- | Count the number of preemptions in a schedule prefix.+preempCount :: (action -> Bool)+ -- ^ Determine if a thread yielded.+ -> [(Decision tid, action)]+ -- ^ The schedule prefix.+ -> (Decision tid, lookahead)+ -- ^ The to-do point.+ -> Int+preempCount didYield ts (d, _) = go Nothing ts where+ go p ((d', a):rest) = preempC p d' + go (Just a) rest+ go p [] = preempC p d++ preempC (Just act) (SwitchTo _) | didYield act = 0+ preempC _ (SwitchTo _) = 1+ preempC _ _ = 0++-------------------------------------------------------------------------------+-- Fair bounding++newtype FairBound = FairBound Int+ deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)++-- | A sensible default fair bound: 5.+--+-- This comes from playing around myself, but there is probably a+-- better default.+defaultFairBound :: FairBound+defaultFairBound = 5++-- | Fair bound function+fairBound :: Eq tid+ => (action -> Bool)+ -- ^ Determine if a thread yielded.+ -> (lookahead -> Bool)+ -- ^ Determine if a thread will yield.+ -> (action -> [tid])+ -- ^ The new threads an action causes to come into existence.+ -> FairBound -> BoundFunc tid action lookahead+fairBound didYield willYield forkTids (FairBound fb) ts dl =+ maxYieldCountDiff didYield willYield forkTids ts dl <= fb++-- | Add a backtrack point. If the thread isn't runnable, or performs+-- a release operation, add all runnable threads.+fairBacktrack :: Ord tid+ => (lookahead -> Bool)+ -- ^ Determine if an action is a release operation: if it could+ -- cause other threads to become runnable.+ -> BacktrackFunc tid action lookahead s+fairBacktrack willRelease bs i t = backtrackAt check False bs i t where+ -- True if a release operation is performed.+ check b = Just True == (willRelease <$> M.lookup t (bcktRunnable b))++-- | Count the number of yields by a thread in a schedule prefix.+yieldCount :: Eq tid+ => (action -> Bool)+ -- ^ Determine if a thread yielded.+ -> (lookahead -> Bool)+ -- ^ Determine if a thread will yield.+ -> tid+ -- ^ The thread to count yields for.+ -> [(Decision tid, action)] -> (Decision tid, lookahead) -> Int+yieldCount didYield willYield tid ts (ld, l) = go initialThread ts where+ go t ((Start t', act):rest)+ | t == tid && didYield act = 1 + go t' rest+ | otherwise = go t' rest+ go t ((SwitchTo t', act):rest)+ | t == tid && didYield act = 1 + go t' rest+ | otherwise = go t' rest+ go t ((Continue, act):rest)+ | t == tid && didYield act = 1 + go t rest+ | otherwise = go t rest+ go t []+ | t == tid && willYield l = 1+ | otherwise = 0++ -- The initial thread ID+ initialThread = case (ts, ld) of+ ((Start t, _):_, _) -> t+ ([], Start t) -> t+ _ -> error "yieldCount: unknown initial thread."++-- | Get the maximum difference between the yield counts of all+-- threads in this schedule prefix.+maxYieldCountDiff :: Eq tid+ => (action -> Bool)+ -- ^ Determine if a thread yielded.+ -> (lookahead -> Bool)+ -- ^ Determine if a thread will yield.+ -> (action -> [tid])+ -- ^ The new threads an action causes to come into existence.+ -> [(Decision tid, action)] -> (Decision tid, lookahead) -> Int+maxYieldCountDiff didYield willYield forkTids ts dl = maximum yieldCountDiffs+ where+ yieldsBy tid = yieldCount didYield willYield tid ts dl+ yieldCounts = [yieldsBy tid | tid <- nub $ allTids ts]+ yieldCountDiffs = [y1 - y2 | y1 <- yieldCounts, y2 <- yieldCounts]++ -- 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]++ -- The initial thread ID+ initialThread = case (ts, dl) of+ ((Start t, _):_, _) -> t+ ([], (Start t, _)) -> t+ _ -> error "maxYieldCountDiff: unknown initial thread."++-------------------------------------------------------------------------------+-- Length bounding++newtype LengthBound = LengthBound Int+ deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)++-- | A sensible default length bound: 250.+--+-- Based on the assumption that anything which executes for much+-- longer (or even this long) will take ages to test.+defaultLengthBound :: LengthBound+defaultLengthBound = 250++-- | Length bound function+lenBound :: LengthBound -> BoundFunc tid action lookahead+lenBound (LengthBound lb) ts _ = length ts < lb++-- | Add a backtrack point. If the thread isn't runnable, add all+-- runnable threads.+lenBacktrack :: Ord tid => BacktrackFunc tid action lookahead s+lenBacktrack = backtrackAt (const False) False
+ Test/DPOR/Internal.hs view
@@ -0,0 +1,510 @@+-- | Internal types and functions for dynamic partial-order reduction.+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, 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)++-------------------------------------------------------------------------------+-- * Dynamic partial-order reduction++-- | DPOR execution is represented as a tree of states, characterised+-- by the decisions that lead to that state.+data DPOR tid action = DPOR+ { dporRunnable :: Set tid+ -- ^ What threads are runnable at this step.+ , dporTodo :: Map tid Bool+ -- ^ Follow-on decisions still to make, and whether that decision+ -- was added conservatively due to the bound.+ , dporDone :: Map tid (DPOR tid action)+ -- ^ Follow-on decisions that have been made.+ , dporSleep :: Map tid action+ -- ^ Transitions to ignore (in this node and children) until a+ -- dependent transition happens.+ , dporTaken :: Map tid action+ -- ^ Transitions which have been taken, excluding+ -- conservatively-added ones. This is used in implementing sleep+ -- sets.+ , dporAction :: Maybe action+ -- ^ What happened at this step. This will be 'Nothing' at the root,+ -- 'Just' everywhere else.+ }++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+ )++-- | One step of the execution, including information for backtracking+-- purposes. This backtracking information is used to generate new+-- schedules.+data BacktrackStep tid action lookahead state = BacktrackStep+ { bcktThreadid :: tid+ -- ^ The thread running at this step+ , bcktDecision :: (Decision tid, action)+ -- ^ What happened at this step.+ , bcktRunnable :: Map tid lookahead+ -- ^ The threads runnable at this step+ , bcktBacktracks :: Map tid Bool+ -- ^ The list of alternative threads to run, and whether those+ -- alternatives were added conservatively due to the bound.+ , bcktState :: state+ -- ^ Some domain-specific state at this point.+ } 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+ )++-- | Initial DPOR state, given an initial thread ID. This initial+-- thread should exist and be runnable at the start of execution.+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+ }++-- | Produce a new schedule prefix from a @DPOR@ tree. If there are no new+-- prefixes remaining, return 'Nothing'. Also returns whether the+-- decision was added conservatively, and the sleep set at the point+-- where divergence happens.+--+-- A schedule prefix is a possibly empty sequence of decisions that+-- have already been made, terminated by a single decision from the+-- to-do set. The intent is to put the system into a new state when+-- executed with this initial sequence of scheduling decisions.+--+-- 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.+findSchedulePrefix :: Ord tid+ => (tid -> Bool)+ -- ^ Some partitioning function, applied to the to-do decisions. If+ -- there is an identifier which passes the test, it will be used,+ -- rather than any which fail it. This allows a very basic way of+ -- domain-specific prioritisation between otherwise equal choices,+ -- which may be useful in some cases.+ -> DPOR tid action+ -> Maybe ([tid], Bool, Map tid action)+findSchedulePrefix predicate dporRoot = go (initialDPORThread dporRoot) dporRoot where+ go tid dpor =+ -- All the possible prefix traces from this point, with+ -- updated DPOR subtrees if taken from the done list.+ let prefixes = mapMaybe go' (M.toList $ dporDone dpor) ++ [([t], c, sleeps dpor) | (t, c) <- M.toList $ dporTodo dpor]+ -- Sort by number of preemptions, in descending order.+ cmp = Down . preEmps tid dpor . (\(a,_,_) -> a)++ in if null prefixes+ then Nothing+ else case partition (\(t:_,_,_) -> predicate t) $ sortBy (comparing cmp) prefixes of+ (choice:_, _) -> Just choice+ ([], choice:_) -> Just choice+ ([], []) -> error "findSchedulePrefix: (internal error) empty prefix list!" ++ go' (tid, dpor) = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> go tid dpor++ -- The new sleep set is the union of the sleep set of the node we're+ -- branching from, plus all the decisions we've already explored.+ sleeps dpor = dporSleep dpor `M.union` dporTaken dpor++ -- The number of pre-emptive context switches+ 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++-- | One of the outputs of the runner is a @Trace@, which is a log of+-- decisions made, all the runnable threads and what they would do,+-- and the action a thread took in its step.+type Trace tid action lookahead = [(Decision tid, [(tid, NonEmpty lookahead)], action)]++-- | Add a new trace to the tree, creating a new subtree branching off+-- at the point where the \"to-do\" decision was made.+incorporateTrace :: Ord tid+ => state+ -- ^ Initial state+ -> (state -> action -> state)+ -- ^ State step function+ -> (state -> (tid, action) -> (tid, action) -> Bool)+ -- ^ Dependency function+ -> Bool+ -- ^ Whether the \"to-do\" point which was used to create this new+ -- execution was conservative or not.+ -> Trace tid action lookahead+ -- ^ The execution trace: the decision made, the runnable threads,+ -- and the action performed.+ -> DPOR tid action+ -> DPOR tid action+incorporateTrace stinit ststep dependency conservative trace dporRoot = grow stinit (initialDPORThread dporRoot) trace dporRoot where+ grow state tid trc@((d, _, a):rest) dpor =+ let tid' = tidOf tid d+ state' = ststep state a+ in case M.lookup tid' $ dporDone dpor of+ Just dpor' -> dpor { dporDone = M.insert tid' (grow state' tid' rest dpor') $ dporDone dpor }+ Nothing -> dpor { dporTaken = if conservative then dporTaken dpor else M.insert tid' a $ dporTaken dpor+ , dporTodo = M.delete tid' $ dporTodo dpor+ , dporDone = M.insert tid' (subtree state' tid' (dporSleep dpor `M.union` dporTaken dpor) trc) $ dporDone dpor }+ grow _ _ [] dpor = dpor++ -- Construct a new subtree corresponding to a trace suffix.+ subtree state tid sleep ((_, _, a):rest) =+ let state' = ststep state 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 _ _ _ [] = error "incorporateTrace: (internal error) subtree suffix empty!"++-- | Produce a list of new backtracking points from an execution+-- trace. These are then used to inform new \"to-do\" points in the+-- @DPOR@ tree.+--+-- Two traces are passed in to this function: the first is generated+-- from the special DPOR scheduler, the other from the execution of+-- the concurrent program.+--+-- If the trace ends with any threads other than the initial one still+-- runnable, a dependency is imposed between this final action and+-- everything else.+findBacktrackSteps :: Ord tid+ => s+ -- ^ Initial state.+ -> (s -> action -> s)+ -- ^ State step function.+ -> (s -> (tid, action) -> (tid, lookahead) -> Bool)+ -- ^ Dependency function.+ -> ([BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s])+ -- ^ Backtracking function. Given a list of backtracking points, and+ -- a thread to backtrack to at a specific point in that list, add+ -- the new backtracking points. There will be at least one: this+ -- chosen one, but the function may add others.+ -> Seq (NonEmpty (tid, lookahead), [tid])+ -- ^ A sequence of threads at each step: the nonempty list of+ -- runnable 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.+ -> Trace tid action lookahead+ -- ^ The execution trace.+ -> [BacktrackStep tid action lookahead s]+findBacktrackSteps stinit ststep dependency backtrack bcktrck = go stinit S.empty initialThread [] (Sq.viewl bcktrck) where+ -- Get the initial thread ID+ initialThread = case Sq.viewl bcktrck of+ (((tid, _):|_, _):<_) -> tid+ _ -> error "findBacktrack: empty backtracking sequence."++ -- Walk through the traces one step at a time, building up a list of+ -- new backtracking points.+ go state allThreads tid bs ((e,i):<is) ((d,_,a):ts) =+ let tid' = tidOf tid d+ state' = ststep state 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 && any (/=initialThread) runnable+ in go state' allThreads' tid' bs' (Sq.viewl is) ts+ go _ _ _ bs _ _ = bs++ -- Find the prior actions dependent with this one and add+ -- backtracking points.+ 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++-- | Add new backtracking points, if they have not already been+-- visited, fit into the bound, and aren't in the sleep set.+incorporateBacktrackSteps :: Ord tid+ => ([(Decision tid, action)] -> (Decision tid, lookahead) -> Bool)+ -- ^ Bound function: returns true if that schedule prefix terminated+ -- with the lookahead decision fits within the bound.+ -> [BacktrackStep tid action lookahead s]+ -- ^ Backtracking steps identified by 'findBacktrackSteps'.+ -> 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' }++-------------------------------------------------------------------------------+-- * DPOR scheduler++-- | A @Scheduler@ where the state is a @SchedState@.+type DPORScheduler tid action lookahead s = Scheduler tid action lookahead (SchedState tid action lookahead s)++-- | The scheduler state+data SchedState tid action lookahead s = SchedState+ { schedSleep :: Map tid action+ -- ^ The sleep set: decisions not to make until something dependent+ -- with them happens.+ , schedPrefix :: [tid]+ -- ^ Decisions still to make+ , schedBPoints :: Seq (NonEmpty (tid, lookahead), [tid])+ -- ^ Which threads are runnable 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+ -- sleep set, as then everything in this execution is covered by+ -- another.+ , schedDepState :: s+ -- ^ State used by the dependency function to determine when to+ -- remove decisions from the sleep set.+ } 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+ , schedDepState s+ )++-- | Initial scheduler state for a given prefix+initialSchedState :: s+ -- ^ The initial dependency function state.+ -> Map tid action+ -- ^ The initial sleep set.+ -> [tid]+ -- ^ The schedule prefix.+ -> SchedState tid action lookahead s+initialSchedState s sleep prefix = SchedState+ { schedSleep = sleep+ , schedPrefix = prefix+ , schedBPoints = Sq.empty+ , schedIgnore = False+ , schedDepState = s+ }++-- | 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 tid action lookahead = [(Decision tid, action)] -> (Decision tid, lookahead) -> Bool++-- | A backtracking step is a point in the execution where another+-- decision needs to be made, in order to explore interesting new+-- schedules. A backtracking /function/ takes the steps identified so+-- far and a point and a thread to backtrack to, and inserts at least+-- that backtracking point. More may be added to compensate for the+-- effects of the bounding function. For example, under pre-emption+-- bounding a conservative backtracking point is added at the prior+-- context switch.+--+-- In general, a backtracking function should identify one or more+-- backtracking points, and then use @backtrackAt@ to do the actual+-- work.+type BacktrackFunc tid action lookahead s = [BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s]++-- | DPOR 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.+--+-- After the initial decisions are exhausted, this prefers choosing+-- the prior thread if it's (1) still runnable and (2) hasn't just+-- yielded. Furthermore, threads which /will/ yield are ignored in+-- preference of those which will not.+--+-- This forces full evaluation of the result every step, to avoid any+-- possible space leaks.+dporSched :: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s)+ => (action -> Bool)+ -- ^ Determine if a thread yielded.+ -> (lookahead -> Bool)+ -- ^ Determine if a thread will yield.+ -> (s -> (tid, action) -> (tid, action) -> Bool)+ -- ^ Dependency function.+ -> (s -> action -> s)+ -- ^ Dependency function's state step function.+ -> BoundFunc tid action lookahead+ -- ^ Bound function: returns true if that schedule prefix terminated+ -- with the lookahead decision fits within the bound.+ -> DPORScheduler tid action lookahead s+dporSched didYield willYield dependency ststep inBound trc prior threads s = force 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 })++ -- 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 = 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+ in case choices' of+ (nextTid:rest) -> (Just nextTid, (nextState rest) { schedSleep = ssleep' })+ [] -> (Nothing, (nextState []) { schedIgnore = signore' })++ -- The next scheduler state+ nextState rest = s+ { schedBPoints = schedBPoints s |> (threads, rest)+ , schedDepState = case prior of+ Just (_, act) -> ststep (schedDepState s) act+ Nothing -> schedDepState s+ }++ -- Pick a new thread to run, which does not exceed the bound. Choose+ -- the current thread if available and it hasn't just yielded,+ -- otherwise add all runnable threads.+ initialise = restrictToBound . yieldsToEnd $ case prior of+ Just (tid, act)+ | didYield act -> map fst (toList threads)+ | any (\(t, _) -> t == tid) threads -> [tid]+ _ -> map fst (toList threads)++ -- Restrict the possible decisions to those in the bound.+ restrictToBound = fst . partition (\t -> inBound trc (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 $ map fst threads')++ -- Get the action of a thread+ action t = fromJust $ lookup t threads'++ -- The runnable threads as a normal list.+ threads' = toList threads++-------------------------------------------------------------------------------+-- * Utilities++-- The initial thread of a DPOR tree.+initialDPORThread :: DPOR tid action -> tid+initialDPORThread = S.elemAt 0 . dporRunnable++-- | Render a 'DPOR' value as a graph in GraphViz \"dot\" format.+toDot :: (tid -> String)+ -- ^ Show a @tid@ - this should produce a string suitable for+ -- use as a node identifier.+ -> (action -> String)+ -- ^ Show a @action@.+ -> DPOR tid action+ -> String+toDot = toDotFiltered (\_ _ -> True)++-- | Render a 'DPOR' value as a graph in GraphViz \"dot\" format, with+-- a function to determine if a subtree should be included or not.+toDotFiltered :: (tid -> DPOR tid action -> Bool)+ -- ^ Subtree predicate.+ -> (tid -> String)+ -> (action -> String)+ -> DPOR tid action+ -> String+toDotFiltered check showTid showAct dpor = "digraph {\n" ++ go "L" dpor ++ "\n}" where+ go l b = unlines $ node l b : edges l b++ -- Display a labelled node.+ node n b = n ++ " [label=\"" ++ label b ++ "\"]"++ -- Display the edges.+ edges l b = [ edge l l' i ++ go l' b'+ | (i, b') <- M.toList (dporDone b)+ , check i b'+ , let l' = l ++ tidId i+ ]++ -- A node label, summary of the DPOR state at that node.+ 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)+ ]++ -- Display a labelled edge+ edge n1 n2 l = n1 ++ "-> " ++ n2 ++ " [label=\"" ++ showTid l ++ "\"]\n"++ -- Show a list of values+ showLst showf xs = "[" ++ intercalate ", " (map showf xs) ++ "]"++ -- Generate a graphviz-friendly identifier from a tid.+ tidId = concatMap (show . ord) . showTid
+ Test/DPOR/Schedule.hs view
@@ -0,0 +1,140 @@+-- | Scheduling for concurrent computations.+module Test.DPOR.Schedule+ ( -- * Scheduling+ Scheduler++ , Decision(..)+ , tidOf+ , decisionOf++ , NonEmpty(..)++ -- ** Preemptive+ , randomSched+ , roundRobinSched++ -- ** Non-preemptive+ , randomSchedNP+ , roundRobinSchedNP++ -- * Utilities+ , makeNonPreemptive+ ) where++import Control.DeepSeq (NFData(..))+import Data.List.NonEmpty (NonEmpty(..), toList)+import System.Random (RandomGen, randomR)++-- | A @Scheduler@ drives the execution of a concurrent program. The+-- parameters it takes are:+--+-- 1. The trace so far.+--+-- 2. The last thread executed (if this is the first invocation, this+-- is @Nothing@).+--+-- 3. The runnable threads at this point.+--+-- 4. The state.+--+-- It returns a thread to execute, or @Nothing@ if execution should+-- abort here, and also a new state.+type Scheduler tid action lookahead s+ = [(Decision tid, action)]+ -> Maybe (tid, action)+ -> NonEmpty (tid, lookahead)+ -> s+ -> (Maybe tid, s)++-------------------------------------------------------------------------------+-- Scheduling decisions++-- | Scheduling decisions are based on the state of the running+-- program, and so we can capture some of that state in recording what+-- specific decision we made.+data Decision tid =+ Start tid+ -- ^ Start a new thread, because the last was blocked (or it's the+ -- start of computation).+ | Continue+ -- ^ Continue running the last thread for another step.+ | SwitchTo tid+ -- ^ Pre-empt the running thread, and switch to another.+ deriving (Eq, Show)++instance NFData tid => NFData (Decision tid) where+ rnf (Start tid) = rnf tid+ rnf (SwitchTo tid) = rnf tid+ rnf d = d `seq` ()++-- | Get the resultant thread identifier of a 'Decision', with a default case+-- for 'Continue'.+tidOf :: tid -> Decision tid -> tid+tidOf _ (Start t) = t+tidOf _ (SwitchTo t) = t+tidOf tid _ = tid++-- | Get the 'Decision' that would have resulted in this thread identifier,+-- given a prior thread (if any) and list of runnable threads.+decisionOf :: (Eq tid, Foldable f)+ => Maybe tid+ -- ^ The prior thread.+ -> f tid+ -- ^ The runnable threads.+ -> tid+ -- ^ The current thread.+ -> Decision tid+decisionOf Nothing _ chosen = Start chosen+decisionOf (Just prior) runnable chosen+ | prior == chosen = Continue+ | prior `elem` runnable = SwitchTo chosen+ | otherwise = Start chosen++-------------------------------------------------------------------------------+-- Preemptive++-- | A simple random scheduler which, at every step, picks a random+-- thread to run.+randomSched :: RandomGen g => Scheduler tid action lookahead g+randomSched _ _ threads g = (Just $ threads' !! choice, g') where+ (choice, g') = randomR (0, length threads' - 1) g+ threads' = map fst $ toList threads++-- | A round-robin scheduler which, at every step, schedules the+-- thread with the next 'ThreadId'.+roundRobinSched :: Ord tid => Scheduler tid action lookahead ()+roundRobinSched _ Nothing ((tid,_):|_) _ = (Just tid, ())+roundRobinSched _ (Just (prior, _)) threads _+ | prior >= maximum threads' = (Just $ minimum threads', ())+ | otherwise = (Just . minimum $ filter (>prior) threads', ())++ where+ threads' = map fst $ toList threads++-------------------------------------------------------------------------------+-- Non-preemptive++-- | A random scheduler which doesn't preempt the running+-- thread. That is, if the last thread scheduled is still runnable,+-- run that, otherwise schedule randomly.+randomSchedNP :: (RandomGen g, Eq tid) => Scheduler tid action lookahead g+randomSchedNP = makeNonPreemptive randomSched++-- | A round-robin scheduler which doesn't preempt the running+-- thread.+roundRobinSchedNP :: Ord tid => Scheduler tid action lookahead ()+roundRobinSchedNP = makeNonPreemptive roundRobinSched++-------------------------------------------------------------------------------+-- Utilities++-- | Turn a potentially preemptive scheduler into a non-preemptive+-- one.+makeNonPreemptive :: Eq tid+ => Scheduler tid action lookahead s+ -> Scheduler tid action lookahead s+makeNonPreemptive sched = newsched where+ newsched trc p@(Just (prior, _)) threads s+ | prior `elem` map fst (toList threads) = (Just prior, s)+ | otherwise = sched trc p threads s+ newsched trc Nothing threads s = sched trc Nothing threads s
+ dpor.cabal view
@@ -0,0 +1,73 @@+-- Initial dpor.cabal generated by cabal init. For further documentation, +-- see http://haskell.org/cabal/users-guide/++name: dpor+version: 0.1.0.0+synopsis: A generic implementation of dynamic partial-order reduction (DPOR) for testing arbitrary models of concurrency.++description:+ We can characterise the state of a concurrent computation by+ considering the ordering of dependent events. This is a partial+ order: independent events can be performed in any order without+ affecting the result. DPOR is a technique for computing these+ partial orders at run-time, and only testing one total order for+ each partial order. This cuts down the amount of work to be done+ significantly. In particular, this package implemented bounded+ partial-order reduction, which is a further optimisation. Only+ schedules within some *bound* are considered.+ .+ * DPOR with no schedule bounding is __complete__, it /will/ find all+ distinct executions!+ .+ * DPOR with schedule bounding is __incomplete__, it will only find+ all distinct executions /within the bound/!+ .+ __Caution:__ The fundamental assumption behind DPOR is that the+ *only* source of nondeterminism in your program is the+ scheduler. Or, to put it another way, if you execute the same+ program with the same schedule twice, you get the same result. If+ you are using this library in combination with something which+ performs I/O, be *very* certain that this is the case!+ .+ See the <https://github.com/barrucadu/dejafu README> for more+ details.+ .+ For details on the algorithm, albeit presented in a very imperative+ way, see /Bounded partial-order reduction/, K. Coons, M. Musuvathi,+ and K. McKinley (2013), available at+ <http://research.microsoft.com/pubs/202164/bpor-oopsla-2013.pdf>++homepage: https://github.com/barrucadu/dejafu+license: MIT+license-file: LICENSE+author: Michael Walker+maintainer: mike@barrucadu.co.uk+-- copyright: +category: Testing+build-type: Simple+-- extra-source-files: +cabal-version: >=1.10++source-repository head+ type: git+ location: https://github.com/barrucadu/dejafu.git++source-repository this+ type: git+ location: https://github.com/barrucadu/dejafu.git+ tag: dpor-0.1.0.0++library+ exposed-modules: Test.DPOR+ , Test.DPOR.Internal+ , Test.DPOR.Schedule+ -- other-modules: + -- other-extensions: + build-depends: base >=4.8 && <4.9+ , containers+ , deepseq+ , random+ , semigroups+ -- hs-source-dirs: + default-language: Haskell2010+ ghc-options: -Wall