commit ghc-dpor for openSUSE:Factory

Hello community, here is the log from the commit of package ghc-dpor for openSUSE:Factory checked in at 2017-04-11 09:37:37 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/ghc-dpor (Old) and /work/SRC/openSUSE:Factory/.ghc-dpor.new (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Package is "ghc-dpor" Tue Apr 11 09:37:37 2017 rev:2 rq:483922 version:0.2.0.0 Changes: -------- --- /work/SRC/openSUSE:Factory/ghc-dpor/ghc-dpor.changes 2017-03-24 01:54:49.627884853 +0100 +++ /work/SRC/openSUSE:Factory/.ghc-dpor.new/ghc-dpor.changes 2017-04-11 09:37:40.248584807 +0200 @@ -1,0 +2,5 @@ +Thu Sep 15 06:34:19 UTC 2016 - psimons@suse.com + +- Update to version 0.2.0.0 revision 0 with cabal2obs. + +------------------------------------------------------------------- Old: ---- dpor-0.1.0.1.tar.gz New: ---- dpor-0.2.0.0.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ ghc-dpor.spec ++++++ --- /var/tmp/diff_new_pack.8k97xS/_old 2017-04-11 09:37:40.752513620 +0200 +++ /var/tmp/diff_new_pack.8k97xS/_new 2017-04-11 09:37:40.756513055 +0200 @@ -1,7 +1,7 @@ # # spec file for package ghc-dpor # -# Copyright (c) 2016 SUSE LINUX GmbH, Nuernberg, Germany. +# Copyright (c) 2017 SUSE LINUX GmbH, Nuernberg, Germany. # # All modifications and additions to the file contributed by third parties # remain the property of their copyright owners, unless otherwise agreed @@ -18,22 +18,20 @@ %global pkg_name dpor Name: ghc-%{pkg_name} -Version: 0.1.0.1 +Version: 0.2.0.0 Release: 0 Summary: A generic implementation of dynamic partial-order reduction (DPOR) for testing arbitrary models of concurrency License: MIT -Group: System/Libraries +Group: Development/Languages/Other Url: https://hackage.haskell.org/package/%{pkg_name} Source0: https://hackage.haskell.org/package/%{pkg_name}-%{version}/%{pkg_name}-%{version}.tar.gz BuildRequires: ghc-Cabal-devel -# Begin cabal-rpm deps: BuildRequires: ghc-containers-devel BuildRequires: ghc-deepseq-devel BuildRequires: ghc-random-devel BuildRequires: ghc-rpm-macros BuildRequires: ghc-semigroups-devel BuildRoot: %{_tmppath}/%{name}-%{version}-build -# End cabal-rpm deps %description We can characterise the state of a concurrent computation by considering the @@ -78,15 +76,12 @@ %prep %setup -q -n %{pkg_name}-%{version} - %build %ghc_lib_build - %install %ghc_lib_install - %post devel %ghc_pkg_recache ++++++ dpor-0.1.0.1.tar.gz -> dpor-0.2.0.0.tar.gz ++++++ diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/dpor-0.1.0.1/Test/DPOR/Internal.hs new/dpor-0.2.0.0/Test/DPOR/Internal.hs --- old/dpor-0.1.0.1/Test/DPOR/Internal.hs 2016-05-26 13:22:12.000000000 +0200 +++ new/dpor-0.2.0.0/Test/DPOR/Internal.hs 2016-06-06 21:04:03.000000000 +0200 @@ -1,4 +1,14 @@ --- | Internal types and functions for dynamic partial-order reduction. +-- | +-- Module : Test.DPOR.Internal +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : portable +-- +-- Internal types and functions for dynamic partial-order +-- reduction. This module is NOT considered to form part of the public +-- interface of this library. module Test.DPOR.Internal where import Control.DeepSeq (NFData(..), force) @@ -7,7 +17,7 @@ import Data.List.NonEmpty (NonEmpty(..), toList) import Data.Ord (Down(..), comparing) import Data.Map.Strict (Map) -import Data.Maybe (fromJust, mapMaybe) +import Data.Maybe (fromJust, isNothing, mapMaybe) import qualified Data.Map.Strict as M import Data.Set (Set) import qualified Data.Set as S @@ -100,10 +110,6 @@ -- 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 @@ -111,38 +117,50 @@ -- 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. + -> (Int -> (Int, g)) + -- ^ List indexing function, used to select which schedule to + -- return. Takes the length of the list, and returns an index and + -- some generator state. The index returned MUST be in range! -> DPOR tid action - -> Maybe ([tid], Bool, Map tid action) -findSchedulePrefix predicate dpor0 = go (initialDPORThread dpor0) dpor0 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) ++ here dpor - -- Sort by number of preemptions, in descending order. - cmp = Down . preEmps tid dpor . (\(a,_,_) -> a) - sorted = sortBy (comparing cmp) prefixes - - in if null prefixes - then Nothing - else case partition (\(t:_,_,_) -> predicate t) sorted of - (choice:_, _) -> Just choice - ([], choice:_) -> Just choice - ([], []) -> err "findSchedulePrefix" "empty prefix list!" - - go' (tid, dpor) = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> go tid dpor - - -- Prefix traces terminating with a to-do decision at this point. - here dpor = [([t], c, sleeps dpor) | (t, c) <- M.toList $ dporTodo 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 + -> Maybe ([tid], Bool, Map tid action, g) +findSchedulePrefix predicate idx dpor0 + | null allPrefixes = Nothing + | otherwise = let (i, g) = idx (length allPrefixes) + (ts, c, slp) = allPrefixes !! i + in Just (ts, c, slp, g) + where + allPrefixes = go (initialDPORThread dpor0) dpor0 + + go tid dpor = + -- All the possible prefix traces from this point, with + -- updated DPOR subtrees if taken from the done list. + let prefixes = concatMap go' (M.toList $ dporDone dpor) ++ here dpor + -- Sort by number of preemptions, in descending order. + cmp = Down . preEmps tid dpor . (\(a,_,_) -> a) + sorted = sortBy (comparing cmp) prefixes + + in if null prefixes + then [] + else case partition (\(t:_,_,_) -> predicate t) sorted of + ([], []) -> err "findSchedulePrefix" "empty prefix list!" + ([], choices) -> choices + (choices, _) -> choices + + go' (tid, dpor) = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> go tid dpor + + -- Prefix traces terminating with a to-do decision at this point. + here dpor = [([t], c, sleeps dpor) | (t, c) <- M.toList $ dporTodo 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, @@ -155,7 +173,7 @@ incorporateTrace :: Ord tid => state -- ^ Initial state - -> (state -> action -> state) + -> (state -> (tid, action) -> state) -- ^ State step function -> (state -> (tid, action) -> (tid, action) -> Bool) -- ^ Dependency function @@ -170,7 +188,7 @@ incorporateTrace stinit ststep dependency conservative trace dpor0 = grow stinit (initialDPORThread dpor0) trace dpor0 where grow state tid trc@((d, _, a):rest) dpor = let tid' = tidOf tid d - state' = ststep state a + state' = ststep state (tid', a) in case M.lookup tid' (dporDone dpor) of Just dpor' -> let done = M.insert tid' (grow state' tid' rest dpor') (dporDone dpor) @@ -187,7 +205,7 @@ -- Construct a new subtree corresponding to a trace suffix. subtree state tid sleep ((_, _, a):rest) = - let state' = ststep state a + let state' = ststep state (tid, a) sleep' = M.filterWithKey (\t a' -> not $ dependency state' (tid, a) (t,a')) sleep in DPOR { dporRunnable = S.fromList $ case rest of @@ -221,7 +239,7 @@ findBacktrackSteps :: Ord tid => s -- ^ Initial state. - -> (s -> action -> s) + -> (s -> (tid, action) -> s) -- ^ State step function. -> (s -> (tid, action) -> (tid, lookahead) -> Bool) -- ^ Dependency function. @@ -230,6 +248,9 @@ -- 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. + -> Bool + -- ^ Whether the computation was aborted due to no decisions being + -- in-bounds. -> 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 @@ -239,9 +260,9 @@ -> Trace tid action lookahead -- ^ The execution trace. -> [BacktrackStep tid action lookahead s] -findBacktrackSteps _ _ _ _ bcktrck +findBacktrackSteps _ _ _ _ _ bcktrck | Sq.null bcktrck = const [] -findBacktrackSteps stinit ststep dependency backtrack bcktrck = go stinit S.empty initialThread [] (Sq.viewl bcktrck) where +findBacktrackSteps stinit ststep dependency backtrack boundKill bcktrck = go stinit S.empty initialThread [] (Sq.viewl bcktrck) where -- Get the initial thread ID initialThread = case Sq.viewl bcktrck of (((tid, _):|_, _):<_) -> tid @@ -251,7 +272,7 @@ -- new backtracking points. go state allThreads tid bs ((e,i): NFData (SchedState tid action lookahead s) where - rnf s = rnf ( schedSleep s - , schedPrefix s - , schedBPoints s - , schedIgnore s - , schedDepState s + rnf s = rnf ( schedSleep s + , schedPrefix s + , schedBPoints s + , schedIgnore s + , schedBoundKill s + , schedDepState s ) -- | Initial scheduler state for a given prefix @@ -364,11 +392,12 @@ -- ^ The schedule prefix. -> SchedState tid action lookahead s initialSchedState s sleep prefix = SchedState - { schedSleep = sleep - , schedPrefix = prefix - , schedBPoints = Sq.empty - , schedIgnore = False - , schedDepState = s + { schedSleep = sleep + , schedPrefix = prefix + , schedBPoints = Sq.empty + , schedIgnore = False + , schedBoundKill = False + , schedDepState = s } -- | A bounding function takes the scheduling decisions so far and a @@ -377,6 +406,10 @@ type BoundFunc tid action lookahead = [(Decision tid, action)] -> (Decision tid, lookahead) -> Bool +-- | The \"true\" bound, which allows everything. +trueBound :: BoundFunc tid action lookahead +trueBound _ _ = True + -- | 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 @@ -393,6 +426,41 @@ = [BacktrackStep tid action lookahead s] -> Int -> tid -> [BacktrackStep tid action lookahead s] +-- | 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 + -- | 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. @@ -411,13 +479,15 @@ -- ^ Determine if a thread will yield. -> (s -> (tid, action) -> (tid, action) -> Bool) -- ^ Dependency function. - -> (s -> action -> s) + -> (s -> (tid, lookahead) -> NonEmpty tid -> Bool) + -- ^ Daemon-termination predicate. + -> (s -> (tid, 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 +dporSched didYield willYield dependency killsDaemons 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 @@ -427,49 +497,59 @@ -- choices, filter out anything in the sleep set, and make one of -- them arbitrarily (recording the others). [] -> - let choices = initialise + let choices = restrictToBound 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 + sbkill' = not (null initialise) && null choices in case choices' of (nextTid:rest) -> (Just nextTid, (nextState rest) { schedSleep = ssleep' }) - [] -> (Nothing, (nextState []) { schedIgnore = signore' }) + [] -> (Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill' }) -- 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 + , schedDepState = nextDepState } + nextDepState = let ds = schedDepState s in maybe ds (ststep ds) prior - -- 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 + -- Pick a new thread to run, not considering bounds. Choose the + -- current thread if available and it hasn't just yielded, otherwise + -- add all runnable threads. + initialise = tryDaemons . yieldsToEnd $ case prior of Just (tid, act) - | didYield act -> map fst (toList threads) - | any (\(t, _) -> t == tid) threads -> [tid] - _ -> map fst (toList threads) + | not (didYield act) && tid `elem` tids -> [tid] + _ -> tids' + + -- If one of the chosen actions will kill the computation, and there + -- are daemon threads, try them instead. + tryDaemons ts + | any doesKill ts = filter (not . doesKill) tids' ++ filter doesKill ts + | otherwise = ts + doesKill t = killsDaemons nextDepState (t, action t) tids -- Restrict the possible decisions to those in the bound. - restrictToBound = fst . partition (\t -> inBound trc (decision t, action t)) + restrictToBound = filter (\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') + 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 + -- The runnable threads as a normal list. threads' = toList threads + tids' = toList tids ------------------------------------------------------------------------------- -- * Utilities diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/dpor-0.1.0.1/Test/DPOR/Random.hs new/dpor-0.2.0.0/Test/DPOR/Random.hs --- old/dpor-0.1.0.1/Test/DPOR/Random.hs 1970-01-01 01:00:00.000000000 +0100 +++ new/dpor-0.2.0.0/Test/DPOR/Random.hs 2016-06-06 21:04:03.000000000 +0200 @@ -0,0 +1,204 @@ +-- | +-- Module : Test.DPOR.Random +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : portable +-- +-- Random and incomplete techniques for when complete testing is +-- infeasible. +module Test.DPOR.Random + ( -- * Randomness and partial-order reduction + randomDPOR + + -- * Non-POR techniques + + -- | These algorithms do not make use of partial-order reduction to + -- systematically prune the search space and search for interesting + -- interleavings. Instead, the exploration is driven entirely by + -- random choice, with optional bounds. However, the same schedule + -- will never be explored twice. + , boundedRandom + ) where + +import Control.DeepSeq (NFData) +import Data.List.NonEmpty (NonEmpty) +import Data.Maybe (fromMaybe) +import System.Random (RandomGen, randomR) + +import Test.DPOR.Internal + +------------------------------------------------------------------------------- +-- Randomness and partial-order reduction + +-- | Random dynamic partial-order reduction. +-- +-- This is the 'dpor' algorithm in "Test.DPOR", however it does not +-- promise to test every distinct schedule: instead, an execution +-- limit is passed in, and a PRNG used to decide which actual +-- schedules to test. Testing terminates when either the execution +-- limit is reached, or when there are no distinct schedules +-- remaining. +-- +-- Despite being \"random\", this still uses the normal partial-order +-- reduction and schedule bounding machinery, and so will prune the +-- search space to \"interesting\" cases, and will never try the same +-- schedule twice. Additionally, the thread partitioning function +-- still applies when selecting schedules. +randomDPOR :: ( Ord tid + , NFData tid + , NFData action + , NFData lookahead + , NFData s + , Monad m + , RandomGen g + ) + => (action -> Bool) + -- ^ Determine if a thread yielded. + -> (lookahead -> Bool) + -- ^ Determine if a thread will yield. + -> s + -- ^ The initial state for backtracking. + -> (s -> (tid, 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. + -> (s -> (tid, lookahead) -> NonEmpty tid -> Bool) + -- ^ The daemon-termination predicate. + -> 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. + -> g + -- ^ Random number generator, used to determine which schedules to + -- try. + -> Int + -- ^ Execution limit, used to abort the execution whilst schedules + -- still remain. + -> m [(a, Trace tid action lookahead)] +randomDPOR didYield + willYield + stinit + ststep + dependency1 + dependency2 + killsDaemons + 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 _ _ 0 = pure [] + go dp g elim = case nextPrefix g dp of + Just (prefix, conservative, sleep, g') -> do + (res, s, trace) <- run scheduler + (initialSchedState stinit sleep prefix) + + let bpoints = findBacktracks (schedBoundKill s) (schedBPoints s) trace + let newDPOR = addTrace conservative trace dp + let newDPOR' = transform (addBacktracks bpoints newDPOR) + + if schedIgnore s + then go newDPOR g' (elim-1) + else ((res, trace):) <$> go newDPOR' g' (elim-1) + + Nothing -> pure [] + + -- Generate a random value from a range + gen g hi = randomR (0, hi - 1) g + + -- Find the next schedule prefix. + nextPrefix = findSchedulePrefix predicate . gen + + -- The DPOR scheduler. + scheduler = dporSched didYield willYield dependency1 killsDaemons ststep inBound + + -- Find the new backtracking steps. + findBacktracks = findBacktrackSteps stinit ststep dependency2 backtrack + + -- Incorporate a trace into the DPOR tree. + addTrace = incorporateTrace stinit ststep dependency1 + + -- Incorporate the new backtracking steps into the DPOR tree. + addBacktracks = incorporateBacktrackSteps inBound + +------------------------------------------------------------------------------- +-- Unsystematic techniques + +-- | Pure random scheduling. Like 'randomDPOR' but all actions are +-- dependent and the bounds are optional. +boundedRandom :: ( Ord tid + , NFData tid + , NFData action + , NFData lookahead + , Monad m + , RandomGen g + ) + => (action -> Bool) + -- ^ Determine if a thread yielded. + -> (lookahead -> Bool) + -- ^ Determine if a thread will yield. + -> tid + -- ^ The initial thread. + -> Maybe (BoundFunc tid action lookahead) + -- ^ The bounding function. If no function is provided, 'trueBound' + -- is used. + -> (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. + -> g + -- ^ Random number generator, used to determine which schedules to + -- try. + -> Int + -- ^ Execution limit, used to abort the execution whilst schedules + -- still remain. + -> m [(a, Trace tid action lookahead)] +boundedRandom didYield willYield initialTid inBoundm + = randomDPOR didYield + willYield + stinit + ststep + dependency1 + dependency2 + killsDaemons + initialTid + predicate + inBound + backtrack + transform + where + stinit = () + ststep _ _ = () + dependency1 _ _ _ = True + dependency2 _ _ _ = True + killsDaemons _ _ _ = True + predicate _ = True + inBound = fromMaybe trueBound inBoundm + backtrack = backtrackAt (const False) False + transform = id diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/dpor-0.1.0.1/Test/DPOR/Schedule.hs new/dpor-0.2.0.0/Test/DPOR/Schedule.hs --- old/dpor-0.1.0.1/Test/DPOR/Schedule.hs 2016-05-26 13:22:18.000000000 +0200 +++ new/dpor-0.2.0.0/Test/DPOR/Schedule.hs 2016-06-06 21:04:03.000000000 +0200 @@ -1,4 +1,12 @@ --- | Scheduling for concurrent computations. +-- | +-- Module : Test.DPOR.Schedule +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : portable +-- +-- Scheduling for concurrent computations. module Test.DPOR.Schedule ( -- * Scheduling Scheduler diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/dpor-0.1.0.1/Test/DPOR.hs new/dpor-0.2.0.0/Test/DPOR.hs --- old/dpor-0.1.0.1/Test/DPOR.hs 2016-05-26 13:22:16.000000000 +0200 +++ new/dpor-0.2.0.0/Test/DPOR.hs 2016-06-06 21:04:03.000000000 +0200 @@ -1,6 +1,14 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} --- | Systematic testing of concurrent computations through dynamic +-- | +-- Module : Test.DPOR +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : GeneralizedNewtypeDeriving +-- +-- Systematic testing of concurrent computations through dynamic -- partial-order reduction and schedule bounding. module Test.DPOR ( -- * Bounded dynamic partial-order reduction @@ -78,6 +86,9 @@ , lenBound , lenBacktrack + -- * Random approaches + , module Test.DPOR.Random + -- * Scheduling & execution traces -- | The partial-order reduction is driven by incorporating @@ -93,10 +104,11 @@ import Control.DeepSeq (NFData) import Data.List (nub) -import Data.Maybe (isNothing) +import Data.List.NonEmpty (NonEmpty) import qualified Data.Map.Strict as M import Test.DPOR.Internal +import Test.DPOR.Random import Test.DPOR.Schedule ------------------------------------------------------------------------------- @@ -118,6 +130,14 @@ -- the most specific and (2) will be more pessimistic (due to, -- typically, less information being available when merely looking -- ahead). +-- +-- The daemon-termination predicate returns @True@ if the action being +-- looked at will cause the entire computation to terminate, +-- regardless of the other runnable threads (which are passed in the +-- 'NonEmpty' list). Such actions will then be put off for as long as +-- possible. This allows supporting concurrency models with daemon +-- threads without doing something as drastic as imposing a dependency +-- between the program-terminating action and /everything/ else. dpor :: ( Ord tid , NFData tid , NFData action @@ -131,12 +151,14 @@ -- ^ Determine if a thread will yield. -> s -- ^ The initial state for backtracking. - -> (s -> action -> s) + -> (s -> (tid, 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. + -> (s -> (tid, lookahead) -> NonEmpty tid -> Bool) + -- ^ The daemon-termination predicate. -> tid -- ^ The initial thread. -> (tid -> Bool) @@ -162,6 +184,7 @@ ststep dependency1 dependency2 + killsDaemons initialTid predicate inBound @@ -175,11 +198,11 @@ -- traces into a list until there are no schedules remaining to -- try. go dp = case nextPrefix dp of - Just (prefix, conservative, sleep) -> do + Just (prefix, conservative, sleep, ()) -> do (res, s, trace) <- run scheduler (initialSchedState stinit sleep prefix) - let bpoints = findBacktracks s trace + let bpoints = findBacktracks (schedBoundKill s) (schedBPoints s) trace let newDPOR = addTrace conservative trace dp if schedIgnore s @@ -189,14 +212,13 @@ Nothing -> pure [] -- Find the next schedule prefix. - nextPrefix = findSchedulePrefix predicate + nextPrefix = findSchedulePrefix predicate (const (0, ())) -- The DPOR scheduler. - scheduler = dporSched didYield willYield dependency1 ststep inBound + scheduler = dporSched didYield willYield dependency1 killsDaemons ststep inBound -- Find the new backtracking steps. - findBacktracks = findBacktrackSteps stinit ststep dependency2 backtrack . - schedBPoints + findBacktracks = findBacktrackSteps stinit ststep dependency2 backtrack -- Incorporate a trace into the DPOR tree. addTrace = incorporateTrace stinit ststep dependency1 @@ -220,6 +242,8 @@ -- ^ The dependency (1) function. -> ((tid, action) -> (tid, lookahead) -> Bool) -- ^ The dependency (2) function. + -> ((tid, lookahead) -> NonEmpty tid -> Bool) + -- ^ The daemon-termination predicate. -> tid -- ^ The initial thread. -> BoundFunc tid action lookahead @@ -238,6 +262,7 @@ willYield dependency1 dependency2 + killsDaemons initialTid inBound backtrack @@ -247,47 +272,13 @@ (\_ _ -> ()) (const dependency1) (const dependency2) + (const killsDaemons) 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 @@ -298,10 +289,6 @@ -> 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 diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/dpor-0.1.0.1/dpor.cabal new/dpor-0.2.0.0/dpor.cabal --- old/dpor-0.1.0.1/dpor.cabal 2016-05-26 13:30:01.000000000 +0200 +++ new/dpor-0.2.0.0/dpor.cabal 2016-06-06 21:04:03.000000000 +0200 @@ -2,7 +2,7 @@ -- see http://haskell.org/cabal/users-guide/ name: dpor -version: 0.1.0.1 +version: 0.2.0.0 synopsis: A generic implementation of dynamic partial-order reduction (DPOR) for testing arbitrary models of concurrency. description: @@ -55,11 +55,12 @@ source-repository this type: git location: https://github.com/barrucadu/dejafu.git - tag: dpor-0.1.0.1 + tag: dpor-0.2.0.0 library exposed-modules: Test.DPOR , Test.DPOR.Internal + , Test.DPOR.Random , Test.DPOR.Schedule -- other-modules: -- other-extensions: