Implement shrinking, and shrink test output.

Shrinking attempts to find a "maximally simple" trace which
exhibits the same bug as the original. Typically, this means that
the results are equal. Shrinking is implemented in terms of
recursively trying to find the simplest variant of the original
trace, where simplest in particular means:

1. A trace with fewer pre-emptions is simpler.
2. A trace with fewer non-pre-emptive context switches is simpler.
3. A trace lexicographically smaller is simpler.

These three criteria are applied in that order in order to determine
which the simplest trace out of a collection is.

For test output, there is a final set of simplification done at the end.
Shrinking attempts to reduce individual traces to their simplest variant,
which can result in multiple test failures having the same shrunk trace.
Thus, the test runner then filters out duplicate failures by only keeping
the simplest trace for a given result.

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

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

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

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
 

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

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