diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/Test/DPOR.hs b/Test/DPOR.hs new file mode 100644 --- /dev/null +++ b/Test/DPOR.hs @@ -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 diff --git a/Test/DPOR/Internal.hs b/Test/DPOR/Internal.hs new file mode 100644 --- /dev/null +++ b/Test/DPOR/Internal.hs @@ -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): (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 diff --git a/Test/DPOR/Schedule.hs b/Test/DPOR/Schedule.hs new file mode 100644 --- /dev/null +++ b/Test/DPOR/Schedule.hs @@ -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 diff --git a/dpor.cabal b/dpor.cabal new file mode 100644 --- /dev/null +++ b/dpor.cabal @@ -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 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 + + +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