Use schedule bounding as the primary SCT approach.

This allows results to be naturally reported as lazy trees, rather
than as lists representing a tree traversal. This in turn means
that the actual bound can be moved outwards to the testing code, and
not used at all in the runner. Trees let us do nice things with
shrinking and short-circuiting, if we make the (fairly reasonable)
assumption that the children of a buggy result will exhibit the same
bug.

Storing results as trees does complicate the predicate helper
functions somewhat, but I think the clarity gained in the actual
SCT code is well worth it.
This commit is contained in:
Michael Walker 2015-06-19 16:50:51 +01:00
parent 1d085f4ea9
commit 8944ea97a5
9 changed files with 294 additions and 476 deletions

View File

@ -2,28 +2,15 @@
module Data.List.Extra where
import Control.DeepSeq (NFData(..))
import Data.List (foldl')
-- * Regular lists
-- | Split a list at an index and transform the two halves.
splitAtF :: ([a] -> b) -> ([a] -> c) -> Int -> [a] -> (b, c)
splitAtF f g i xs = let (l, r) = splitAt i xs in (f l, g r)
-- | 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)
-- | For all sets of mutually comparable elements (hence the partial
-- ordering), remove all non-minimal ones.
sortNubBy :: (a -> a -> Maybe Ordering) -> [a] -> [a]
sortNubBy cmp = foldl' (flip insert) [] where
insert x xs
| any (\a -> a `cmp` x == Just LT) xs = xs
| otherwise = x : filter (\a -> a `cmp` x /= Just GT) xs
-- * Non-empty lists
-- This gets exposed to users of the library, so it has a bunch of
@ -42,15 +29,3 @@ instance NFData a => NFData (NonEmpty a) where
-- | Convert a 'NonEmpty' to a regular non-empty list.
toList :: NonEmpty a -> [a]
toList (a :| as) = a : as
-- * Tagged streams
-- | Data type representing a chunky, tagged, stream of data.
data Stream t a = Stream (t, NonEmpty a) (Stream t a) | Empty t
-- | Prepend a value onto a lazy stream.
(+|) :: (t, [a]) -> Stream t a -> Stream t a
(_, []) +| l = l
(t, x:xs) +| l = Stream (t, x:|xs) l
infixr +|

View File

@ -84,15 +84,13 @@ module Test.DejaFu
, alwaysTrue
, alwaysTrue2
, somewhereTrue
, somewhereTrue2
) where
import Control.Applicative ((<$>))
import Control.Arrow (first)
import Control.DeepSeq (NFData(..))
import Control.Monad (when)
import Data.List (nub)
import Data.List.Extra
import Data.Monoid (mconcat)
import Test.DejaFu.Deterministic
import Test.DejaFu.Deterministic.IO (ConcIO)
import Test.DejaFu.SCT
@ -118,8 +116,8 @@ dejafus = dejafus' 2
-- | Variant of 'dejafus' which takes a pre-emption bound.
dejafus' :: (Eq a, Show a) => Int -> (forall t. Conc t a) -> [(String, Predicate a)] -> IO Bool
dejafus' pb conc tests = do
let traces = sctPreBound pb conc
results <- mapM (\(name, test) -> doTest name $ runTest'' test traces) tests
let traces = sctPreBound conc
results <- mapM (\(name, test) -> doTest name $ runTest'' pb test traces) tests
return $ and results
-- | Variant of 'dejafus' for computations which do 'IO'.
@ -129,8 +127,9 @@ dejafusIO = dejafusIO' 2
-- | Variant of 'dejafus'' for computations which do 'IO'.
dejafusIO' :: (Eq a, Show a) => Int -> (forall t. ConcIO t a) -> [(String, Predicate a)] -> IO Bool
dejafusIO' pb concio tests = do
traces <- sctPreBoundIO pb concio
results <- mapM (\(name, test) -> doTest name $ runTest'' test traces) tests
traces <- sctPreBoundIO concio
traces' <- mapM (sequenceIOTree $ Just pb) traces
results <- mapM (\(name, test) -> doTest name $ runTest'' pb test traces') tests
return $ and results
-- | Automatically test a computation. In particular, look for
@ -152,23 +151,19 @@ autocheckIO concio = dejafusIO concio cases where
-- * Test cases
-- | The results of a test, including information on the number of
-- cases checked, and number of total cases. Be careful if using the
-- total number of cases, as that value may be very big, and (due to
-- laziness) will actually force a lot more computation!.
-- | The results of a test, including the number of cases checked to
-- determine the final boolean outcome.
data Result a = Result
{ _pass :: Bool
-- ^ Whether the test passed or not.
, _casesChecked :: Int
-- ^ The number of cases checked.
, _casesTotal :: Int
-- ^ The total number of cases.
, _failures :: [(Either Failure a, Trace)]
-- ^ The failed cases, if any.
} deriving (Show, Eq)
instance NFData a => NFData (Result a) where
rnf r = rnf (_pass r, _casesChecked r, _casesTotal r, _failures r)
rnf r = rnf (_pass r, _casesChecked r, _failures r)
instance Functor Result where
fmap f r = r { _failures = map (first $ fmap f) $ _failures r }
@ -189,54 +184,25 @@ runTestIO = runTestIO' 2
-- | Variant of 'runTest' which takes a pre-emption bound.
runTest' :: Eq a => Int -> Predicate a -> (forall t. Conc t a) -> Result a
runTest' pb predicate conc = runTest'' predicate $ sctPreBound pb conc
runTest' pb predicate conc = runTest'' pb predicate $ sctPreBound conc
-- | Variant of 'runTest'' which takes a list of results.
runTest'' :: Eq a => Predicate a -> [(Either Failure a, Trace)] -> Result a
runTest'' predicate results = r { _failures = uniques $ _failures r } where
r = predicate results
-- | Variant of 'runTest'' which takes a tree of results and a depth limit.
runTest'' :: Eq a => Int -> Predicate a -> [SCTTree a] -> Result a
runTest'' pb predicate results = predicate $ map (bound pb) results where
bound 0 (SCTTree a t _) = SCTTree a t []
bound n (SCTTree a t os) = SCTTree a t $ map (bound $ n - 1) os
-- | Variant of 'runTest'' for computations which do 'IO'.
runTestIO' :: Eq a => Int -> Predicate a -> (forall t. ConcIO t a) -> IO (Result a)
runTestIO' pb predicate conc = do
results <- sctPreBoundIO pb conc
return $ runTest'' predicate results
-- | Strip out duplicates
uniques :: Eq a => [(a, Trace)] -> [(a, Trace)]
uniques = nub . sortNubBy simplicity
-- | Determine which of two failures is simpler, if they are comparable.
simplicity :: Eq a => (a, Trace) -> (a, Trace) -> Maybe Ordering
simplicity (r, t) (s, u)
| r /= s = Nothing
| otherwise = Just $ mconcat
[ preEmpCount t' `compare` preEmpCount u'
, contextSwitchCount t' `compare` contextSwitchCount u'
, lexicographic t' u'
]
where
t' = map (\(d,_,_) -> d) t
u' = map (\(d,_,_) -> d) u
contextSwitchCount (Start _:ss) = 1 + contextSwitchCount ss
contextSwitchCount (_:ss) = contextSwitchCount ss
contextSwitchCount _ = 0::Int
lexicographic (SwitchTo i:_) (SwitchTo j:_) = i `compare` j
lexicographic (Start i:_) (Start j:_) = i `compare` j
lexicographic (Continue:as) (b:bs) = if b /= Continue then LT else lexicographic as bs
lexicographic (_:as) (_:bs) = lexicographic as bs
lexicographic [] [] = EQ
lexicographic [] _ = LT
lexicographic _ [] = GT
results <- sctPreBoundIO conc
runTest'' pb predicate <$> mapM (sequenceIOTree $ Just pb) results
-- * Predicates
-- | A @Predicate@ is a function which collapses a list of results
-- into a 'Result'.
type Predicate a = [(Either Failure a, Trace)] -> Result a
type Predicate a = [SCTTree a] -> Result a
-- | Check that a computation never deadlocks.
deadlocksNever :: Predicate a
@ -270,71 +236,69 @@ alwaysSame = alwaysTrue2 (==)
-- | Check that the result of a computation is not always the same.
notAlwaysSame :: Eq a => Predicate a
notAlwaysSame = somewhereTrue2 (/=)
notAlwaysSame ts = go ts Result { _pass = False, _casesChecked = 0, _failures = [] } where
go (SCTTree a t offs:sibs) res = case (offs, sibs) of
(SCTTree o u _:_, SCTTree s v _:_) -> case (a /= o, a /= s) of
(True, True) -> incCC . incCC $ res { _pass = True }
(True, False) -> incCC . incCC $ res { _pass = True, _failures = (a, t) : (s, v) : _failures res }
(False, True) -> incCC . incCC $ res { _pass = True, _failures = (a, t) : (o, u) : _failures res }
(False, False) -> go sibs . incCC . incCC $ res { _failures = (a, t) : (s, v) : (o, u) : _failures res }
(SCTTree o u _:_, [])
| a /= o -> incCC $ res { _pass = True }
| otherwise -> go (offs++sibs) . incCC $ res { _failures = (a, t) : (o, u) : _failures res }
([], SCTTree s v _:_)
| a /= s -> incCC $ res { _pass = True }
| otherwise -> go (offs++sibs) . incCC $ res { _failures = (a, t) : (s, v) : _failures res }
([], []) -> incCC res
go [] res = res
-- | Check that the result of a unary boolean predicate is always
-- true.
alwaysTrue :: (Either Failure a -> Bool) -> Predicate a
alwaysTrue p xs = go xs Result { _pass = True, _casesChecked = 0, _casesTotal = len, _failures = failures } where
alwaysTrue p ts = go ts Result { _pass = True, _casesChecked = 0, _failures = [] } where
go (SCTTree a t offs:sibs) res
| p a = go (offs++sibs) . incCC $ res
| otherwise = (go sibs res { _failures = (a, t) : _failures res }) { _pass = False, _casesChecked = 1+_casesChecked res }
go [] res = res
go ((y,_):ys) res
| p y = go ys $ incCC res
| otherwise = incCC res { _pass = False }
(len, failures) = findFailures1 p xs
-- | Check that the result of a binary boolean predicate is always
-- true between adjacent pairs of results. In general, it is probably
-- best to only check properties here which are transitive and
-- symmetric, in order to draw conclusions about the entire collection
-- of executions.
-- | Check that the result of a binary boolean predicate is true
-- between all pairs of results. Only properties which are transitive
-- and symmetric should be used here.
--
-- If the predicate fails, /both/ (result,trace) tuples will be added
-- to the failures list.
alwaysTrue2 :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a
alwaysTrue2 _ [_] = Result { _pass = True, _casesChecked = 1, _casesTotal = 1, _failures = [] }
alwaysTrue2 p xs = go xs Result { _pass = True, _casesChecked = 0, _casesTotal = len, _failures = failures } where
go [] = id
go [(y1,_),(y2,_)] = check y1 y2 []
go ((y1,_):(y2,t):ys) = check y1 y2 ((y2,t) : ys)
alwaysTrue2 p ts = go ts Result { _pass = True, _casesChecked = 0, _failures = [] } where
go (SCTTree a t offs:sibs) res = case (offs, sibs) of
(SCTTree o u _:_, SCTTree s v _:_) -> case (p a o, p a s) of
(True, True) -> go (offs++sibs) . incCC . incCC $ res
(True, False) -> (go (offs++sibs) $ res { _failures = (a, t) : (s, v) : _failures res }) { _pass = False, _casesChecked = 2+_casesChecked res }
(False, True) -> (go sibs $ res { _failures = (a, t) : (o, u) : _failures res }) { _pass = False, _casesChecked = 2+_casesChecked res }
(False, False) -> (go sibs $ res { _failures = (a, t) : (s, v) : (o, u) : _failures res }) { _pass = False, _casesChecked = 2+_casesChecked res }
check y1 y2 ys res
| p y1 y2 = go ys $ incCC res
| otherwise = incCC res { _pass = False }
(SCTTree o u _:_, [])
| p a o -> go offs . incCC $ res
| otherwise -> incCC res { _pass = False, _failures = (a, t) : (o, u) : _failures res }
(len, failures) = findFailures2 p xs
([], SCTTree s v _:_)
| p a s -> go sibs . incCC $ res
| otherwise -> incCC res { _pass = False, _failures = (a, t) : (s, v) : _failures res }
([], []) -> incCC res
go [] res = res
-- | Check that the result of a unary boolean predicate is true at
-- least once.
somewhereTrue :: (Either Failure a -> Bool) -> Predicate a
somewhereTrue p xs = go xs Result { _pass = False, _casesChecked = 0, _casesTotal = len, _failures = failures } where
somewhereTrue p ts = go ts Result { _pass = False, _casesChecked = 0, _failures = [] } where
go (SCTTree a t offs:sibs) res
| p a = incCC res { _pass = True }
| otherwise = go (offs++sibs) $ incCC res { _failures = (a, t) : _failures res }
go [] res = res
go ((y,_):ys) res
| p y = incCC res { _pass = True }
| otherwise = go ys $ incCC res
(len, failures) = findFailures1 p xs
-- | Check that the result of a binary boolean predicate is true
-- between at least one adjacent pair of results. In general, it is
-- probably best to only check properties here which are transitive
-- and symmetric, in order to draw conclusions about the entire
-- collection of executions.
--
-- If the predicate fails, /both/ (result,trace) tuples will be added
-- to the failures list.
somewhereTrue2 :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a
somewhereTrue2 _ [x] = Result { _pass = False, _casesChecked = 1, _casesTotal = 1, _failures = [x] }
somewhereTrue2 p xs = go xs Result { _pass = False, _casesChecked = 0, _casesTotal = len, _failures = failures } where
go [] = id
go [(y1,_),(y2,_)] = check y1 y2 []
go ((y1,_):(y2,t):ys) = check y1 y2 ((y2,t) : ys)
check y1 y2 ys res
| p y1 y2 = incCC res { _pass = True }
| otherwise = go ys $ incCC res
(len, failures) = findFailures2 p xs
-- * Internal
@ -356,29 +320,10 @@ doTest name result = do
return $ _pass result
-- | Increment the cases checked
-- | Increment the cases
incCC :: Result a -> Result a
incCC r = r { _casesChecked = _casesChecked r + 1 }
-- | Get the length of the list and find the failing cases in one
-- traversal.
findFailures1 :: (Either Failure a -> Bool) -> [(Either Failure a, Trace)] -> (Int, [(Either Failure a, Trace)])
findFailures1 p xs = findFailures xs 0 [] where
findFailures [] l fs = (l, fs)
findFailures ((z,t):zs) l fs
| p z = findFailures zs (l+1) fs
| otherwise = findFailures zs (l+1) ((z,t):fs)
-- | Get the length of the list and find the failing cases in one
-- traversal.
findFailures2 :: (Either Failure a -> Either Failure a -> Bool) -> [(Either Failure a, Trace)] -> (Int, [(Either Failure a, Trace)])
findFailures2 p xs = findFailures xs 0 [] where
findFailures [] l fs = (l, fs)
findFailures [_] l fs = (l+1, fs)
findFailures ((z1,t1):(z2,t2):zs) l fs
| p z1 z2 = findFailures ((z2,t2):zs) (l+1) fs
| otherwise = findFailures ((z2,t2):zs) (l+1) ((z1,t1):(z2,t2):fs)
-- | Pretty-print a failure
showfail :: Failure -> String
showfail Deadlock = "[deadlock]"

View File

@ -79,7 +79,7 @@ runFixed' fixed runstm sched s idSource ma = do
-- watch out for.
runThreads :: (Functor n, Monad n) => Fixed n r s -> (forall x. s n r x -> CTVarId -> n (Result x, CTVarId))
-> Scheduler g -> g -> Threads n r s -> IdSource -> r (Maybe (Either Failure a)) -> n (g, IdSource, Trace)
runThreads fixed runstm sched origg origthreads idsrc ref = go idsrc [] (-1) origg origthreads where
runThreads fixed runstm sched origg origthreads idsrc ref = go idsrc [] Nothing origg origthreads where
go idSource sofar prior g threads
| isTerminated = return (g, idSource, sofar)
| isDeadlocked = writeRef (wref fixed) ref (Just $ Left Deadlock) >> return (g, idSource, sofar)
@ -92,19 +92,19 @@ runThreads fixed runstm sched origg origthreads idsrc ref = go idsrc [] (-1) ori
Right (threads', idSource', act) ->
let sofar' = (decision, alternatives, act) : sofar
threads'' = if (interruptible <$> M.lookup chosen threads') == Just True then unblockWaitingOn chosen threads' else threads'
in go idSource' sofar' chosen g' threads''
in go idSource' sofar' (Just chosen) g' threads''
Left UncaughtException
| chosen == 0 -> writeRef (wref fixed) ref (Just $ Left UncaughtException) >> return (g, idSource, sofar)
| otherwise ->
let sofar' = (decision, alternatives, Killed) : sofar
threads' = unblockWaitingOn chosen $ kill chosen threads
in go idSource sofar' chosen g' threads'
in go idSource sofar' (Just chosen) g' threads'
Left failure -> writeRef (wref fixed) ref (Just $ Left failure) >> return (g, idSource, sofar)
where
(chosen, g') = if prior == -1 then (0, g) else sched g prior $ head runnable' :| tail runnable'
(chosen, g') = sched g prior $ head runnable' :| tail runnable'
runnable' = M.keys runnable
runnable = M.filter (isNothing . _blocking) threads
thread = M.lookup chosen threads
@ -124,14 +124,14 @@ runThreads fixed runstm sched origg origthreads idsrc ref = go idsrc [] (-1) ori
_ -> thrd
decision
| chosen == prior = Continue
| prior `elem` runnable' = SwitchTo chosen
| otherwise = Start chosen
| Just chosen == prior = Continue
| prior `elem` map Just runnable' = SwitchTo chosen
| otherwise = Start chosen
alternatives
| chosen == prior = map SwitchTo $ filter (/=prior) runnable'
| prior `elem` runnable' = Continue : map SwitchTo (filter (\t -> t /= prior && t /= chosen) runnable')
| otherwise = map Start $ filter (/=chosen) runnable'
| Just chosen == prior = map SwitchTo $ filter (\t -> Just t /= prior) $ runnable'
| prior `elem` map Just runnable' = Continue : map SwitchTo (filter (\t -> Just t /= prior && t /= chosen) runnable')
| otherwise = map Start $ filter (/=chosen) runnable'
--------------------------------------------------------------------------------
-- * Single-step execution

View File

@ -102,15 +102,16 @@ initialIdSource = Id 0 0 0 0
-- * Scheduling & Traces
-- | A @Scheduler@ maintains some internal state, @s@, takes the
-- 'ThreadId' of the last thread scheduled, and the list of runnable
-- threads. It produces a 'ThreadId' to schedule, and a new state.
-- 'ThreadId' of the last thread scheduled, or 'Nothing' if this is
-- the first decision, and the list of runnable threads. It produces a
-- 'ThreadId' to schedule, and a new state.
--
-- Note: In order to prevent computation from hanging, the runtime
-- will assume that a deadlock situation has arisen if the scheduler
-- attempts to (a) schedule a blocked thread, or (b) schedule a
-- nonexistent thread. In either of those cases, the computation will
-- be halted.
type Scheduler s = s -> ThreadId -> NonEmpty ThreadId -> (ThreadId, s)
type Scheduler s = s -> Maybe ThreadId -> NonEmpty ThreadId -> (ThreadId, s)
-- | One of the outputs of the runner is a @Trace@, which is a log of
-- decisions made, alternative decisions, and the action a thread took

View File

@ -34,7 +34,8 @@ randomSchedNP = makeNP randomSched
-- | A round-robin scheduler which, at every step, schedules the
-- thread with the next 'ThreadId'.
roundRobinSched :: Scheduler ()
roundRobinSched _ prior threads
roundRobinSched _ Nothing _ = (0, ())
roundRobinSched _ (Just prior) threads
| prior >= maximum threads' = (minimum threads', ())
| otherwise = (minimum $ filter (>prior) threads', ())
@ -50,6 +51,7 @@ roundRobinSchedNP = makeNP roundRobinSched
-- one.
makeNP :: Scheduler s -> Scheduler s
makeNP sched = newsched where
newsched s prior threads
newsched s (Just prior) threads
| prior `elem` toList threads = (prior, s)
| otherwise = sched s prior threads
| otherwise = sched s (Just prior) threads
newsched s Nothing threads = sched s Nothing threads

View File

@ -1,27 +1,228 @@
{-# LANGUAGE Rank2Types #-}
-- | Systematic testing for concurrent computations.
module Test.DejaFu.SCT
( runSCT
, runSCT'
, runSCTIO
, runSCTIO'
-- * Schedule Bounding
( -- * Schedule Bounding
-- | Schedule bounding is a means of cutting down the search space of
-- schedules, by taking advantage of some intrinsic properties of
-- schedules: such as the number of pre-emptions (pre-emption
-- bounding), or the number of deviations from a deterministic
-- scheduler (delay bounding); and then exploring all schedules
-- within the bound.
, sctBounded
sctBounded
, sctPreBound
, sctDelayBound
, sctBoundedIO
, sctPreBoundIO
, sctDelayBoundIO
-- * Result Trees
, SCTTree(..)
, SCTTreeIO(..)
, sequenceIOTree
-- * Utilities
, preEmpCount
) where
import Test.DejaFu.SCT.Internal
import Test.DejaFu.SCT.Bounding
import Control.Applicative ((<$>), (<*>), pure)
import Control.DeepSeq (NFData(..), force)
import Data.Foldable (Foldable(foldMap))
import Data.Maybe (fromMaybe)
import Data.Traversable (Traversable(traverse), fmapDefault, foldMapDefault)
import Test.DejaFu.Deterministic
import Test.DejaFu.Deterministic.IO (ConcIO, runConcIO)
-- * Result trees
-- | Results are presented in a lazy tree, where each node contains a
-- trace and a result. The children of a node represent those
-- schedules obtainable from it on the next bounding level.
data SCTTree a = SCTTree (Either Failure a) Trace [SCTTree a]
deriving (Eq)
instance Functor SCTTree where
fmap = fmapDefault
instance Foldable SCTTree where
foldMap = foldMapDefault
instance Traversable SCTTree where
traverse f (SCTTree (Left x) t trees) = SCTTree (Left x) <$> pure t <*> traverse (traverse f) trees
traverse f (SCTTree (Right x) t trees) = SCTTree . Right <$> f x <*> pure t <*> traverse (traverse f) trees
instance NFData a => NFData (SCTTree a) where
rnf (SCTTree a t trees) = rnf (a, t, trees)
-- | Results which need IO to compute. Laziness is preserved by
-- wrapping child nodes in an 'IO' list.
data SCTTreeIO a = SCTTreeIO (Either Failure a) Trace (IO [SCTTreeIO a])
instance Functor SCTTreeIO where
fmap f (SCTTreeIO a t iotrees) = SCTTreeIO (fmap f a) t $ fmap (map $ fmap f) iotrees
-- | Perform all of the 'IO' in an 'SCTTreeIO' from left to right. As
-- '>>=' for IO is strict, this will evaluate the entire tree, which
-- may be a lot of work. To counter this, a depth limit can optionally
-- be provided, where children below level @0@ will not be present in
-- the output.
sequenceIOTree :: Maybe Int -> SCTTreeIO a -> IO (SCTTree a)
sequenceIOTree (Just n) (SCTTreeIO a t iotrees)
| n <= 0 = return $ SCTTree a t []
| otherwise = do
trees <- iotrees
SCTTree a t <$> mapM (sequenceIOTree . Just $ n-1) trees
sequenceIOTree Nothing (SCTTreeIO a t iotrees) = do
trees <- iotrees
SCTTree a t <$> mapM (sequenceIOTree Nothing) trees
-- * Pre-emption bounding
-- | An SCT runner using a pre-emption bounding scheduler.
sctPreBound :: (forall t. Conc t a) -> [SCTTree a]
sctPreBound = sctBounded pbSiblings (pbOffspring False)
-- | Variant of 'sctPreBound' for computations which do 'IO'.
sctPreBoundIO :: (forall t. ConcIO t a) -> IO [SCTTreeIO a]
sctPreBoundIO = sctBoundedIO pbSiblings (pbOffspring True)
-- | Return all modifications to this schedule which do not introduce
-- extra pre-emptions.
pbSiblings :: Trace -> [[Decision]]
pbSiblings = siblings . map (\(d,a,_) -> (d,a)) where
siblings ((Start i, alts):ds) = [[a] | a@(Start _) <- alts] ++ [Start i : o | o <- siblings ds, not $ null o]
siblings ((SwitchTo i, alts):ds) = [[a] | a@(SwitchTo _) <- alts] ++ [SwitchTo i : o | o <- siblings ds, not $ null o]
siblings ((d, _):ds) = [d : o | o <- siblings ds, not $ null o]
siblings [] = []
-- | Return all modifications to this schedule which do introduce an
-- extra pre-emption. Only introduce pre-emptions around CVar actions
-- and lifts.
pbOffspring :: Bool -> Trace -> [[Decision]]
pbOffspring lifts ((Continue, alts, ta):ds)
| interesting lifts ta = [[n] | n@(SwitchTo _) <- alts] ++ [Continue : n | n <- pbOffspring lifts ds, not $ null n]
| otherwise = [Continue : n | n <- pbOffspring lifts ds, not $ null n]
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.
sctDelayBound :: (forall t. Conc t a) -> [SCTTree a]
sctDelayBound = sctBounded (const []) (dbOffspring False)
-- | Variant of 'sctDelayBound' for computations which do 'IO'.
sctDelayBoundIO :: (forall t. ConcIO t a) -> IO [SCTTreeIO a]
sctDelayBoundIO = sctBoundedIO (const []) (dbOffspring True)
-- | Return all modifications to the schedule which introduce an extra
-- delay. Only introduce delays around CVar actions and lifts.
dbOffspring :: Bool -> Trace -> [[Decision]]
dbOffspring lifts ((d, alts, ta):ds)
| interesting lifts ta = [[n] | n <- alts] ++ [d : n | n <- dbOffspring lifts ds, not $ null n]
| otherwise = [d : n | n <- dbOffspring lifts ds, not $ null n]
dbOffspring _ [] = []
-- * SCT runners
-- | SCT via schedule bounding. Results are proeduced as a lazy
-- forest, where each level represents one bounding level.
--
-- Schedules are generated by running the computation with a
-- deterministic scheduler with some initial list of decisions, after
-- which non-pre-emptive decisions are made. The generated suffix is
-- then used to generate \"siblings\" (schedule fragments which, when
-- appended to the prefix, form the prefix of a new schedule which
-- does not increase the bound), and \"offspring\" (like siblings, but
-- the bound has been increased by one). It is important that siblings
-- and offspring are unique, and that the same
-- prefix+sibling/offspring cannot arise from two distinct traces, as
-- otherwise the runner may loop.
--
-- For example, the siblings in the pre-emption bounding runner are
-- those schedule fragments which, when appended to the prefix, form
-- the prefix of a new schedule which does not introduce any new
-- pre-emptions; and the offspring do introduce one new pre-emption.
sctBounded :: (Trace -> [[Decision]])
-- ^ Sibling generation function.
-> (Trace -> [[Decision]])
-- ^ Child generation function.
-> (forall t. Conc t a) -> [SCTTree a]
sctBounded siblings offspring c = go [] where
go ds = case res of
Left f -> SCTTree (Left f) trace [] : concatMap go sibs
Right a -> SCTTree (Right a) trace (concatMap go offs) : concatMap go sibs
where
(res, _, trace) = runConc prefixSched ds c
(pref, suff) = let (p, s) = splitAt (length ds) trace in (map (\(a,_,_) -> a) p, s)
sibs = [ pref ++ y | y <- siblings suff]
offs = [ pref ++ y | y <- offspring suff]
-- | Variant of 'sctBounded' for computations which do 'IO'.
sctBoundedIO :: (Trace -> [[Decision]])
-> (Trace -> [[Decision]])
-> (forall t. ConcIO t a) -> IO [SCTTreeIO a]
sctBoundedIO siblings offspring c = go [] where
go ds = do
(res, _, trace) <- runConcIO prefixSched ds c
let (pref, suff) = let (p, s) = splitAt (length ds + 1) trace in (map (\(a,_,_) -> a) p, s)
let sibs = [ pref ++ y | y <- siblings suff]
let offs = [ pref ++ y | y <- offspring suff]
sibs' <- concat <$> mapM go sibs
return $ case res of
Left f -> SCTTreeIO (Left f) trace (return []) : sibs'
Right a -> SCTTreeIO (Right a) trace (concat <$> mapM go offs) : sibs'
-- * Prefix scheduler
-- | Scheduler which uses a list of scheduling decisions to drive the
-- initial decisions.
prefixSched :: Scheduler [Decision]
prefixSched = force $ \s prior threads@(next:|_) -> case s of
-- If we have a decision queued, make it.
(Start t:ds) -> (t, ds)
(Continue:ds) -> (fromMaybe 0 prior, ds)
(SwitchTo t:ds) -> (t, ds)
-- Otherwise just use a non-pre-emptive scheduler.
[] -> case prior of
Just prior' | prior' `elem` toList threads -> (prior', [])
_ -> (next, [])
-- * Utils
-- | Check if a 'ThreadAction' might be an interesting candidate for
-- pre-empting or delaying.
interesting :: Bool -> ThreadAction -> Bool
interesting _ (Put _ _) = True
interesting _ (TryPut _ _ _) = True
interesting _ (Take _ _) = True
interesting _ (TryTake _ _ _) = True
interesting _ (BlockedPut _) = True
interesting _ (Read _) = True
interesting _ (BlockedRead _) = True
interesting _ (BlockedTake _) = True
interesting _ (ReadRef _) = True
interesting _ (ModRef _) = True
interesting _ (STM _) = True
interesting _ BlockedSTM = True
interesting _ (ThrowTo _) = True
interesting _ (SetMasking _ _) = True
interesting _ (ResetMasking _ _ ) = True
interesting l Lift = l
interesting _ _ = False

View File

@ -1,236 +0,0 @@
{-# LANGUAGE Rank2Types #-}
-- Building blocks for SCT runners based on schedule bounding, with
-- implementations of pre-emption bounding and delay bounding.
module Test.DejaFu.SCT.Bounding where
import Control.DeepSeq (NFData(..), force)
import Data.List.Extra
import Test.DejaFu.Deterministic
import Test.DejaFu.Deterministic.IO (ConcIO)
import Test.DejaFu.SCT.Internal
-- * Pre-emption bounding
-- | An SCT runner using a pre-emption bounding scheduler.
sctPreBound :: Int -> (forall t. Conc t a) -> [(Either Failure a, Trace)]
sctPreBound = sctBounded pbSiblings (pbOffspring False)
-- | Variant of 'sctPreBound' for computations which do 'IO'.
sctPreBoundIO :: Int -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]
sctPreBoundIO = sctBoundedIO pbSiblings (pbOffspring True)
-- | Return all modifications to this schedule which do not introduce
-- extra pre-emptions.
pbSiblings :: Trace -> [[Decision]]
pbSiblings = siblings . map (\(d,a,_) -> (d,a)) where
siblings ((Start i, alts):ds) = [[a] | a@(Start _) <- alts] ++ [Start i : o | o <- siblings ds, not $ null o]
siblings ((SwitchTo i, alts):ds) = [[a] | a@(SwitchTo _) <- alts] ++ [SwitchTo i : o | o <- siblings ds, not $ null o]
siblings ((d, _):ds) = [d : o | o <- siblings ds, not $ null o]
siblings [] = []
-- | Return all modifications to this schedule which do introduce an
-- extra pre-emption. Only introduce pre-emptions around CVar actions
-- and lifts.
pbOffspring :: Bool -> Trace -> [[Decision]]
pbOffspring lifts ((Continue, alts, ta):ds)
| interesting lifts ta = [[n] | n@(SwitchTo _) <- alts] ++ [Continue : n | n <- pbOffspring lifts ds, not $ null n]
| otherwise = [Continue : n | n <- pbOffspring lifts ds, not $ null n]
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.
sctDelayBound :: Int -> (forall t. Conc t a) -> [(Either Failure a, Trace)]
sctDelayBound = sctBounded (const []) (dbOffspring False)
-- | Variant of 'sctDelayBound' for computations which do 'IO'.
sctDelayBoundIO :: Int -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]
sctDelayBoundIO = sctBoundedIO (const []) (dbOffspring True)
-- | Return all modifications to the schedule which introduce an extra
-- delay. Only introduce delays around CVar actions and lifts.
dbOffspring :: Bool -> Trace -> [[Decision]]
dbOffspring lifts ((d, alts, ta):ds)
| interesting lifts ta = [[n] | n <- alts] ++ [d : n | n <- dbOffspring lifts ds, not $ null n]
| otherwise = [d : n | n <- dbOffspring lifts ds, not $ null n]
dbOffspring _ [] = []
-- * SCT runners
-- | An SCT runner using schedule bounding. Schedules are explored in
-- a depth-first fashion.
--
-- Schedules are generated by running the computation with a
-- deterministic scheduler with some initial list of decisions, after
-- which non-pre-emptive decisions are made. The generated suffix is
-- then used to generate \"siblings\" (schedule fragments which, when
-- appended to the prefix, form the prefix of a new schedule which
-- does not increase the bound), and \"offspring\" (like siblings, but
-- the bound has been increased by one). It is important that siblings
-- and offspring are unique, and that the same
-- prefix+sibling/offspring cannot arise from two distinct traces, as
-- otherwise the runner may loop.
--
-- For example, the siblings in the pre-emption bounding runner are
-- those schedule fragments which, when appended to the prefix, form
-- the prefix of a new schedule which does not introduce any new
-- pre-emptions; and the offspring do introduce one new pre-emption.
sctBounded :: (Trace -> [[Decision]])
-- ^ Sibling generation function.
-> (Trace -> [[Decision]])
-- ^ Child generation function.
-> Int
-- ^ Bound, anything < 0 will be interpreted as no bound.
-> (forall t. Conc t a) -> [(Either Failure a, Trace)]
sctBounded siblings offspring b = runSCT' prefixSched (initialS, initialG) bTerm (bStep siblings offspring b)
-- | Variant of 'sctBounded' for computations which do 'IO'.
sctBoundedIO :: (Trace -> [[Decision]])
-> (Trace -> [[Decision]])
-> Int
-> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]
sctBoundedIO siblings offspring b = runSCTIO' prefixSched (initialS, initialG) bTerm (bStep siblings offspring b)
-- * State
-- | State for the prefix scheduler.
data Sched = S
{ _decisions :: [Decision]
-- ^ The list of decisions still to make.
, _prefixlen :: Int
-- ^ How long the prefix originally was.
}
instance NFData Sched where
rnf s = rnf (_decisions s, _prefixlen s)
-- | State for the bounded runner.
data State = P
{ _next :: Stream Int [Decision]
-- ^ Schedules to try.
, _halt :: Bool
-- ^ Indicates more schedules couldn't be found, and to halt
-- immediately.
}
-- | Initial scheduler state for the prefix scheduler.
initialS :: Sched
initialS = S { _decisions = [], _prefixlen = 0 }
-- | Initial runner state for the bounded runner.
initialG :: State
initialG = P { _next = Empty 0, _halt = False }
-- * Prefix scheduler
-- | Scheduler which uses a list of scheduling decisions to drive the
-- initial decisions.
prefixSched :: Scheduler Sched
prefixSched = force $ \s prior threads@(next:|_) -> case _decisions s of
-- If we have a decision queued, make it.
(Start t:ds) -> (t, s { _decisions = ds })
(Continue:ds) -> (prior, s { _decisions = ds })
(SwitchTo t:ds) -> (t, s { _decisions = ds })
-- Otherwise just use a non-pre-emptive scheduler.
[] | prior `elem` toList threads -> (prior, s)
| otherwise -> (next, s)
-- * Bounded runner
-- | Termination function: checks for the halt flag.
bTerm :: (a, State) -> Bool
bTerm (_, g) = _halt g
-- | Schedule bounding state step function: computes remaining
-- schedules to try and chooses one.
--
-- This explores schedules in a slightly weird order, it tries to bias
-- towards first exploring schedules with a low, but nonzero, schedule
-- bound. The reason for this is to try to generate simple failing
-- examples quickly, but without getting mired in exploring a lot of
-- zero-bound schedules which might not exhibit a bug.
bStep :: (Trace -> [[Decision]])
-- ^ Sibling generation function.
-> (Trace -> [[Decision]])
-- ^ Offspring generation function.
-> Int
-- ^ Bound.
-> (Sched, State) -> Trace -> (Sched, State)
bStep siblings offspring blim (s, g) t = case _next g of
-- We have schedules remaining, so run the next
Stream (b, x:|xs) rest
| b /= blim && b == 0 -> (s' x, g { _next = (b+1, next) +| (b, this) +| (b, xs) +| rest })
| b /= blim -> (s' x, g { _next = (b, this) +| (b+1, next) +| (b, xs) +| rest })
| otherwise -> (s' x, g { _next = (b, this) +| (b, xs) +| rest })
-- We have no schedules remaining, try to generate some more.
--
-- If there are no more schedules, halt.
Empty b ->
case (this, next) of
-- We still have schedules in the current bound, so add those to
-- the queue (and any schedules from the next bound if we're not at
-- the limit)
(x:xs, _)
| b /= blim && b == 0 -> (s' x, g { _next = (b+1, next) +| (b, xs) +| Empty b })
| b /= blim -> (s' x, g { _next = (b, xs) +| (b+1, next) +| Empty b })
| otherwise -> (s' x, g { _next = (b, xs) +| Empty b })
-- No schedules left in this bound, but if we have some more from
-- the next bound (and we're not at the limit) add those.
([], x:xs)
| b /= blim -> (s' x, g { _next = (b+1, xs) +| Empty (b+1) })
-- No schedules left at all, so halt.
_ -> halt
where
(pref, suff) = splitAtF (\((Start 0,_,_):px) -> (map (\(d,_,_) -> d) px ++)) id (_prefixlen s + 1) t
-- | New scheduler state, with a given list of initial decisions.
s' ds = initialS { _decisions = ds, _prefixlen = length ds }
-- | The halt state
halt = (initialS, g { _halt = True })
-- | All (new, unique) schedules we get from the current one
-- WITHOUT increasing the bound.
this = [ pref y | y <- siblings suff]
-- | All (new, unique) schedules we get from the current one with
-- ONE increase to the bound.
next = [ pref y | y <- offspring suff]
-- * Utils
-- | Check if a 'ThreadAction' might be an interesting candidate for
-- pre-empting or delaying.
interesting :: Bool -> ThreadAction -> Bool
interesting _ (Put _ _) = True
interesting _ (TryPut _ _ _) = True
interesting _ (Take _ _) = True
interesting _ (TryTake _ _ _) = True
interesting _ (BlockedPut _) = True
interesting _ (Read _) = True
interesting _ (BlockedRead _) = True
interesting _ (BlockedTake _) = True
interesting _ (ReadRef _) = True
interesting _ (ModRef _) = True
interesting _ (STM _) = True
interesting _ BlockedSTM = True
interesting _ (ThrowTo _) = True
interesting _ (SetMasking _ _) = True
interesting _ (ResetMasking _ _ ) = True
interesting l Lift = l
interesting _ _ = False

View File

@ -1,68 +0,0 @@
{-# LANGUAGE Rank2Types #-}
-- | A runner for concurrent monads to systematically detect
-- concurrency errors such as data races and deadlocks: internal definitions.
module Test.DejaFu.SCT.Internal where
import Control.Monad.Loops (unfoldrM)
import Data.List (unfoldr)
import Test.DejaFu.Deterministic
import Test.DejaFu.Deterministic.IO (ConcIO, runConcIO)
-- * SCT Runners
-- | Run a concurrent program under a given scheduler a number of
-- times, collecting the results and the trace that gave rise to them.
--
-- The initial state for each run is the final state of the prior run,
-- so it is important that the scheduler actually maintain some
-- internal state, or all the results will be identical.
runSCT :: Scheduler s -- ^ The scheduler
-> s -- ^ The scheduler's initial state
-> Int -- ^ The number of executions to perform
-> (forall t. Conc t a) -- ^ The computation to test
-> [(Either Failure a, Trace)]
runSCT sched s n = runSCT' sched (s, n) term step where
term (_, g) = g == 0
step (s', g) _ = (s', g - 1)
-- | Variant of 'runSCT' for computations which do 'IO'.
runSCTIO :: Scheduler s -> s -> Int -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]
runSCTIO sched s n = runSCTIO' sched (s, n) term step where
term (_, g) = g == 0
step (s', g) _ = (s', g - 1)
-- | Run a concurrent program under a given scheduler, where the SCT
-- runner itself maintains some internal state, and has a function to
-- produce a new scheduler state for each run, and decide termination
-- based on the internal state.
--
-- Note: the state step function takes the state returned by the
-- scheduler, not the initial state!
runSCT' :: Scheduler s -- ^ The scheduler
-> (s, g) -- ^ The scheduler's and runner's initial states
-> ((s, g) -> Bool) -- ^ Termination decider
-> ((s, g) -> Trace -> (s, g)) -- ^ State step function
-> (forall t. Conc t a) -- ^ The computation to test
-> [(Either Failure a, Trace)]
runSCT' sched initial term step c = unfoldr go initial where
go sg@(s, g)
| term sg = Nothing
| otherwise = res `seq` Just ((res, trace), sg')
where
(res, s', trace) = runConc sched s c
sg' = step (s', g) trace
-- | Variant of 'runSCT'' for computations which do 'IO'.
runSCTIO' :: Scheduler s -> (s, g) -> ((s, g) -> Bool) -> ((s, g) -> Trace -> (s, g)) -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]
runSCTIO' sched initial term step c = unfoldrM go initial where
go sg@(s, g)
| term sg = return Nothing
| otherwise = do
(res, s', trace) <- runConcIO sched s c
let sg' = step (s', g) trace
res `seq` return (Just ((res, trace), sg'))

View File

@ -73,8 +73,6 @@ library
, Test.DejaFu.Deterministic.Internal.Common
, Test.DejaFu.Deterministic.Internal.CVar
, Test.DejaFu.Deterministic.Internal.Threading
, Test.DejaFu.SCT.Bounding
, Test.DejaFu.SCT.Internal
, Test.DejaFu.STM.Internal
, Control.State