diff --git a/Control/Monad/Conc/SCT.hs b/Control/Monad/Conc/SCT.hs index 05aa4b2..7feee9a 100644 --- a/Control/Monad/Conc/SCT.hs +++ b/Control/Monad/Conc/SCT.hs @@ -80,11 +80,3 @@ sctRandom = makeSCT randomSched -- | A random scheduler with no pre-emption. sctRandomNP :: RandomGen g => SCTScheduler g sctRandomNP = makeSCT randomSchedNP - --- * Utils - --- | Check the pre-emption count of some scheduling decisions. -preEmpCount :: [Decision] -> Int -preEmpCount (SwitchTo _:ss) = 1 + preEmpCount ss -preEmpCount (_:ss) = preEmpCount ss -preEmpCount [] = 0 diff --git a/Control/Monad/Conc/SCT/Bounding.hs b/Control/Monad/Conc/SCT/Bounding.hs index f446e51..6efc575 100755 --- a/Control/Monad/Conc/SCT/Bounding.hs +++ b/Control/Monad/Conc/SCT/Bounding.hs @@ -42,6 +42,12 @@ pbOffspring lifts ((Continue, alts, ta):ds) pbOffspring lifts ((d, _, _):ds) = [d : n | n <- pbOffspring lifts ds, not $ null n] pbOffspring _ [] = [] +-- | Check the pre-emption count of some scheduling decisions. +preEmpCount :: [Decision] -> Int +preEmpCount (SwitchTo _:ss) = 1 + preEmpCount ss +preEmpCount (_:ss) = preEmpCount ss +preEmpCount [] = 0 + -- * Delay bounding -- | An SCT runner using a delay-bounding scheduler. Schedules are diff --git a/Control/Monad/Conc/SCT/Shrink.hs b/Control/Monad/Conc/SCT/Shrink.hs new file mode 100755 index 0000000..92d9bc4 --- /dev/null +++ b/Control/Monad/Conc/SCT/Shrink.hs @@ -0,0 +1,171 @@ +{-# LANGUAGE Rank2Types #-} + +-- | Functions for attempting to find maximally simple traces +-- producing a given result. +module Control.Monad.Conc.SCT.Shrink + ( -- * Trace shrinking + shrink + , shrink' + , shrinkIO + , shrinkIO' + + -- * Utilities + -- | If you wanted to implement your own shrinking logic, these are + -- the building blocks. + , candidates + , try + , tryIO + , essential + , simplest + ) where + +import Control.Applicative ((<$>)) +import Control.Monad.Conc.Fixed +import Control.Monad.Conc.SCT.Bounding +import Control.Monad.Conc.SCT.Internal +import Data.Function (on) +import Data.List (sortBy, isPrefixOf) +import Data.List.Extra +import Data.Maybe (fromJust, listToMaybe) +import Data.Ord (comparing) + +import qualified Control.Monad.Conc.Fixed.IO as CIO + +-- | Attempt to find a trace with a minimal number of pre-emptions +-- that gives rise to the desired output. +shrink :: Eq a => (Maybe a, SCTTrace) -> (forall t. Conc t a) -> SCTTrace +shrink (res, trc) = shrink' (res ==) trc + +-- | Variant of 'shrink' for 'IO'. See usual caveats about 'IO'. +shrinkIO :: Eq a => (Maybe a, SCTTrace) -> (forall t. CIO.Conc t a) -> IO SCTTrace +shrinkIO (res, trc) = shrinkIO' (res ==) trc + +-- | Variant of 'shrink' which takes a function to determine if the +-- result is erroneous in the same way. +shrink' :: (Maybe a -> Bool) -> SCTTrace -> (forall t. Conc t a) -> SCTTrace +shrink' p trace t = shrink'' [] trace where + shrink'' e trc = case nextscts of + -- No candidates for further shrinking found + [] -> trc + -- Attempt to shrink further. Safe because shrink'' will always + -- return at least one result. + ts -> fromJust . simplest $ map (uncurry shrink'') ts + + where + -- Get all candidate trace prefixes which start with the given + -- essential portion. + cands = filter (\(ds, _) -> e `isPrefixOf` ds) $ candidates trc + + -- Get traces for further shrinking, by finding the essential + -- prefixes out of the candidates + nextscts = concatMap step cands + + -- Pick a candidate for further simplification, and attempt to + -- identify a new essential trace prefix. + step (pref, tid) = + let tries = filter (/=trace) $ try p pref t + in case simplest tries of + -- No further candidates available. + Nothing -> [] + Just best -> + if essential (pref, tid) tries + -- If the pre-emption is essential, we have a new + -- essential prefix. + then [(pref ++ [SwitchTo tid], best)] + -- If not, just re-use the original prefix. + else [(e, best)] + + +-- | Variant of 'shrinkIO' which takes a function to determine if the +-- result is erroneous in the same way. See usual caveats about 'IO'. +shrinkIO' :: (Maybe a -> Bool) -> SCTTrace -> (forall t. CIO.Conc t a) -> IO SCTTrace +shrinkIO' p trace t = shrink'' [] trace where + shrink'' e trc = do + let cands = filter (\(ds, _) -> e `isPrefixOf` ds) $ candidates trc + nextscts <- concat <$> mapM step cands + + case nextscts of + [] -> return trc + ts -> fromJust . simplest <$> mapM (uncurry shrink'') ts + + where + step (pref, tid) = do + tries <- tryIO p pref t + return $ + case simplest tries of + Nothing -> [] + Just best -> + if essential (pref, tid) tries + then [(pref ++ [SwitchTo tid], best)] + else [(e, best)] + +-- | Generate all candidate trace prefixes from a trace. These are +-- produced by attempting to drop one pre-emption. Furthermore, the +-- 'ThreadId' of the thread which performed the dropped pre-emption is +-- also returned. +candidates :: SCTTrace -> [([Decision], ThreadId)] +candidates = candidates' [] where + candidates' _ [] = [] + candidates' ps ((SwitchTo i, _, _):ts) = (reverse ps, i) : candidates' (SwitchTo i : ps) ts + candidates' ps ((t, _, _):ts) = candidates' (t : ps) ts + +-- | Try all traces with a given trace prefix and return those which +-- satisfy the predicate. +try :: (Maybe a -> Bool) -> [Decision] -> (forall t. Conc t a) -> [SCTTrace] +try p pref c = map snd . filter (p . fst) $ sctPreBoundOffset pref c + +-- | Variant of 'try' for 'IO' See usual caveats about 'IO'. +tryIO :: (Maybe a -> Bool) -> [Decision] -> (forall t. CIO.Conc t a) -> IO [SCTTrace] +tryIO p pref c = map snd . filter (p . fst) <$> sctPreBoundOffsetIO pref c + +-- | Given a list of 'SCTTraces' which follow on from a given prefix, +-- determine if the removed pre-emption is \"essential\". That is, +-- every 'SCTTrace' starts with the prefix followed by a pre-emption +-- to the given thread. +essential :: ([Decision], ThreadId) -> [SCTTrace] -> Bool +essential (ds, tid) = all ((pref `isPrefixOf`) . unSCT) where + pref = ds ++ [SwitchTo tid] + +-- | Return the simplest 'SCTTrace' from a collection. Roughly, the +-- one with the fewest pre-emptions. If the list is empty, return +-- 'Nothing'. +simplest :: [SCTTrace] -> Maybe SCTTrace +simplest = listToMaybe . nubishBy (lexico `on` unSCT) . restrict contextSwitch . restrict preEmpCount where + + -- Favour schedules with fewer context switches if they have the + -- same number of pre-emptions. + contextSwitch (Start _:ss) = 1 + contextSwitch ss + contextSwitch (_:ss) = contextSwitch ss + contextSwitch [] = 0::Int -- Prevents a warning about defaulting. + + -- Favour shorter schedules with lexicographically "smaller" context + -- switches if all else is equal. + lexico (Continue:as) (b:bs) = b /= Continue || lexico as bs + lexico (Start i:_) (Start j:_) = i < j + lexico (SwitchTo i:_) (SwitchTo j:_) = i < j + lexico (_:as) (_:bs) = lexico as bs + lexico [] _ = True + lexico _ [] = False + + -- Find the best element(s) of the list and drop all worse ones. + restrict f xs = case sortBy (comparing $ f . unSCT) xs of + [] -> [] + ys -> let best = f . unSCT $ head ys in filter ((==best) . f . unSCT) ys + +-- | Like pre-emption bounding, but rather than starting from nothing, +-- use the given trace prefix. +sctPreBoundOffset :: [Decision] -> (forall t. Conc t a) -> [(Maybe a, SCTTrace)] +sctPreBoundOffset ds = runSCT' prefixSched (initialS', initialG) bTerm (bStep pbSiblings (pbOffspring False) pb) where + initialS' = initialS { _decisions = tail ds, _prefixlen = length ds - 1 } + pb = preEmpCount ds + 1 + +-- | Variant of 'sctPreBoundOffset' for 'IO'. See usual caveats about +-- 'IO'. +sctPreBoundOffsetIO :: [Decision] -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)] +sctPreBoundOffsetIO ds = runSCTIO' prefixSched (initialS', initialG) bTerm (bStep pbSiblings (pbOffspring False) pb) where + initialS' = initialS { _decisions = tail ds, _prefixlen = length ds - 1 } + pb = preEmpCount ds + 1 + +-- | Convert an 'SCTTrace' to a list of 'Decision's. +unSCT :: SCTTrace -> [Decision] +unSCT = map $ \(d, _, _) -> d diff --git a/Control/Monad/Conc/SCT/Tests.hs b/Control/Monad/Conc/SCT/Tests.hs index c97d34a..aeb74cb 100644 --- a/Control/Monad/Conc/SCT/Tests.hs +++ b/Control/Monad/Conc/SCT/Tests.hs @@ -34,8 +34,11 @@ import Control.Monad (when, void) import Control.Monad.Conc.Fixed import Control.Monad.Conc.SCT.Internal import Control.Monad.Conc.SCT.Bounding +import Control.Monad.Conc.SCT.Shrink +import Data.Function (on) +import Data.List (groupBy, foldl') import Data.List.Extra -import Data.Maybe (isJust, isNothing) +import Data.Maybe (mapMaybe, isJust, isNothing) import qualified Control.Monad.Conc.Fixed.IO as CIO @@ -70,7 +73,7 @@ doTest showf verbose (name, result) = do putStrLn ("\27[31m[fail]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")") let traces = let (rs, ts) = unzip . take 5 $ _failures result in rs `zip` simplify ts mapM_ (\(r, t) -> putStrLn $ "\t" ++ maybe "[deadlock]" showf r ++ " " ++ showtrc t) traces - when (length (_failures result) > 5) $ + when (moreThan (_failures result) 5) $ putStrLn "\t..." return $ _pass result @@ -124,21 +127,38 @@ instance Functor Result where fmap f r = r { _failures = map (first $ fmap f) $ _failures r } -- | Run a test using the pre-emption bounding scheduler, with a bound --- of 2. -runTest :: Predicate a -> (forall t. Conc t a) -> Result a +-- of 2, and attempt to shrink any failing traces. +runTest :: Eq a => Predicate a -> (forall t. Conc t a) -> Result a runTest = runTest' 2 -- | Variant of 'runTest' using 'IO'. See usual caveats about 'IO'. -runTestIO :: Predicate a -> (forall t. CIO.Conc t a) -> IO (Result a) +runTestIO :: Eq a => Predicate a -> (forall t. CIO.Conc t a) -> IO (Result a) runTestIO = runTestIO' 2 --- | Run a test using the pre-emption bounding scheduler. -runTest' :: Int -> Predicate a -> (forall t. Conc t a) -> Result a -runTest' pb predicate conc = predicate $ sctPreBound pb conc +-- | Run a test using the pre-emption bounding scheduler, and attempt +-- to shrink any failing traces. +runTest' :: Eq a => Int -> Predicate a -> (forall t. Conc t a) -> Result a +runTest' pb predicate conc = andShrink . predicate $ sctPreBound pb conc where + andShrink r + | null $ _failures r = r + | otherwise = r { _failures = uniques . map (\failure@(res, _) -> (res, shrink failure conc)) $ _failures r } -- | Variant of 'runTest'' using 'IO'. See usual caveats about 'IO'. -runTestIO' :: Int -> Predicate a -> (forall t. CIO.Conc t a) -> IO (Result a) -runTestIO' pb predicate conc = predicate <$> sctPreBoundIO pb conc +runTestIO' :: Eq a => Int -> Predicate a -> (forall t. CIO.Conc t a) -> IO (Result a) +runTestIO' pb predicate conc = (predicate <$> sctPreBoundIO pb conc) >>= andShrink where + andShrink r + | null $ _failures r = return r + | otherwise = (\fs -> r { _failures = uniques fs }) <$> + mapM (\failure@(res, _) -> (\trc' -> (res, trc')) <$> shrinkIO failure conc) (_failures r) + +-- | Find unique failures and return the simplest trace for each +-- failure. +uniques :: Eq a => [(Maybe a, SCTTrace)] -> [(Maybe a, SCTTrace)] +uniques = mapMaybe (foldl' simplest' Nothing) . groupBy ((==) `on` fst) where + simplest' Nothing r = Just r + simplest' r@(Just (_, trc)) s@(_, trc') + | simplest [trc, trc'] == Just trc = r + | otherwise = Just s -- * Predicates diff --git a/Data/List/Extra.hs b/Data/List/Extra.hs index 497b697..10dfc7e 100755 --- a/Data/List/Extra.hs +++ b/Data/List/Extra.hs @@ -23,6 +23,21 @@ commonPrefix ls = foldl1 commonPrefix2 ls where commonSuffix :: Eq a => [[a]] -> [a] commonSuffix = reverse . commonPrefix . map reverse +-- | Like 'nubBy', but only compare adjacent elements. +nubishBy :: (a -> a -> Bool) -> [a] -> [a] +nubishBy eq = nubish' Nothing where + nubish' _ [] = [] + nubish' Nothing (x:xs) = x : nubish' (Just x) xs + nubish' e'@(Just e) (x:xs) + | e `eq` x = nubish' e' xs + | otherwise = x : nubish' (Just x) xs + +-- | Check if a list has more than some number of elements. +moreThan :: [a] -> Int -> Bool +moreThan [] n = n < 0 +moreThan _ 0 = True +moreThan (_:xs) n = moreThan xs (n-1) + -- * Non-empty lists -- | This gets exposed to users of the library, so it has a bunch of -- classes which aren't actually used in the rest of the code to make diff --git a/monad-conc.cabal b/monad-conc.cabal index fc2b17b..b12dd26 100755 --- a/monad-conc.cabal +++ b/monad-conc.cabal @@ -53,6 +53,7 @@ library , Control.Monad.Conc.Fixed.IO , Control.Monad.Conc.Fixed.Schedulers , Control.Monad.Conc.SCT + , Control.Monad.Conc.SCT.Shrink , Control.Monad.Conc.SCT.Tests other-modules: Control.Monad.Conc.Fixed.Internal