barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2024-12-18 19:11:37 +03:00
Code Issues Projects Releases Wiki Activity

Refactor code and update docs to make more not-me friendly

Browse Source
This commit is contained in:
Michael Walker 2015-02-01 01:21:42 +00:00
parent fbc262c361
commit 00ad122b65
16 changed files with 430 additions and 552 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Control/Concurrent/CVar/Strict.hs
View File

@ -1,6 +1,6 @@
-- | Strict alternatives to the functions in
-- Control.Monad.Conc.CVar. Specifically, values are evaluated to
-- normal form befire being put into a @CVar@.
-- normal form before being put into a @CVar@.
module Control.Concurrent.CVar.Strict
( -- *@CVar@s
CVar

9
Control/Monad/Conc/Class.hs
View File

@ -1,7 +1,7 @@
{-# LANGUAGE TypeFamilies #-}
-- | This module captures the interface of @Conc@ monads in a
-- typeclass.
-- | This module captures in a typeclass the interface of concurrency
-- monads.
module Control.Monad.Conc.Class where
import Control.Concurrent (forkIO)
@ -9,8 +9,9 @@ import Control.Concurrent.MVar (MVar, readMVar, newEmptyMVar, putMVar, tryPutMVa
import Control.Monad (unless, void)
-- | @MonadConc@ is like a combination of 'ParFuture' and 'ParIVar'
-- from the abstract-par package. It captures the interface of @Conc@
-- monads in terms of how they can operate on shared state.
-- from the abstract-par package. It captures the interface of
-- concurrency monads in terms of how they can operate on shared
-- state.
--
-- There are a few notable differences: firstly, @Par@ imposes
-- 'NFData' constraints on everything, as it achieves its speed-up by

26
Data/List/Extra.hs
View File

@ -10,29 +10,6 @@ import Data.List (groupBy)
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)
-- | Get the longest common prefix of a bunch of lists.
commonPrefix :: Eq a => [[a]] -> [a]
commonPrefix [] = []
commonPrefix ls = foldl1 commonPrefix2 ls where
commonPrefix2 [] _ = []
commonPrefix2 _ [] = []
commonPrefix2 (x:xs) (y:ys)
| x == y = x : commonPrefix2 xs ys
| otherwise = []
-- | Get the longest common suffix of a bunch of lists.
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
@ -54,7 +31,8 @@ groupByIsh f = merge Nothing . merge Nothing . merge Nothing . groupBy f where
merge (Just (xs, ys)) zs = xs : ys : zs
-- * Non-empty lists
-- | This gets exposed to users of the library, so it has a bunch of
-- 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
-- it more friendly to further use.

287
Test/DejaFu.hs
View File

@ -1,17 +1,71 @@
{-# LANGUAGE Rank2Types #-}
-- | Useful functions for writing SCT test cases for @Conc@
-- computations.
-- | Deterministic testing for concurrent computations.
--
-- As an example, consider this program, which has two locks and a
-- shared variable. Two threads are spawned, which claim the locks,
-- update the shared variable, and release the locks. The main thread
-- waits for them both to terminate, and returns the final result.
--
-- > bad :: MonadConc m => m Int
-- > bad = do
-- > a <- newEmptyCVar
-- > b <- newEmptyCVar
-- >
-- > c <- newCVar 0
-- >
-- > j1 <- spawn $ lock a >> lock b >> modifyCVar_ c (return . succ) >> unlock b >> unlock a
-- > j2 <- spawn $ lock b >> lock a >> modifyCVar_ c (return . pred) >> unlock a >> unlock b
-- >
-- > takeCVar j1
-- > takeCVar j2
-- >
-- > takeCVar c
--
-- The correct result is 0, as it starts out as 0 and is incremented
-- and decremented by threads 1 and 2, respectively. However, note the
-- order of acquisition of the locks in the two threads. If thread 2
-- pre-empts thread 1 between the acquisition of the locks (or if
-- thread 1 pre-empts thread 2), a deadlock situation will arise, as
-- thread 1 will have lock @a@ and be waiting on @b@, and thread 2
-- will have @b@ and be waiting on @a@.
--
-- Here is what @dejafu@ has to say about it:
--
-- > > autocheck bad
-- > [fail] Never Deadlocks (checked: 4)
-- > [deadlock] S0---------S1-P2--S1-
-- > [deadlock] S0---------S2-P1--S2-
-- > [fail] Consistent Result (checked: 3)
-- > [deadlock] S0---------S1-P2--S1-
-- > 0 S0---------S1--------S2--------S0-----
-- > [deadlock] S0---------S2-P1--S2-
-- > False
--
-- It identifies the deadlock, and also the possible results the
-- computation can produce, and displays a simplified trace leading to
-- each failing outcome. It also returns @False@ as there are test
-- failures. The automatic testing functionality is good enough if you
-- only want to check your computation is deterministic, but if you
-- have more specific requirements (or have some expected and
-- tolerated level of nondeterminism), you can write tests yourself
-- using the @dejafu*@ functions.
--
-- __Warning:__ If your computation under test does @IO@, the @IO@
-- will be executed lots of times! Be sure that it is deterministic
-- enough not to invalidate your test results.
module Test.DejaFu
( doTests
, doTests'
, autocheck
( autocheck
, dejafu
, dejafus
, autocheckIO
, dejafuIO
, dejafusIO
-- * Test cases
, Result(..)
, runTest
, runTestIO
, runTest'
, runTestIO
, runTestIO'
-- * Predicates
, Predicate
@ -19,109 +73,66 @@ module Test.DejaFu
, deadlocksAlways
, deadlocksSometimes
, alwaysSame
, notAlwaysSame
, alwaysTrue
, alwaysTrue2
, somewhereTrue
, somewhereTrue2
-- * Utilities
, pAnd
, pNot
, rForgetful
) where
import Control.Applicative ((<$>))
import Control.Arrow (first)
import Control.DeepSeq (NFData(..))
import Control.Monad (when, void)
import Data.Function (on)
import Data.List (foldl')
import Control.Monad (when)
import Data.List (nubBy)
import Data.List.Extra
import Data.Maybe (mapMaybe, isJust, isNothing)
import Data.Maybe (isJust, isNothing)
import Test.DejaFu.Deterministic
import Test.DejaFu.SCT.Internal
import Test.DejaFu.SCT.Bounding
import Test.DejaFu.Deterministic.Internal
import Test.DejaFu.Deterministic.IO (ConcIO)
import Test.DejaFu.SCT
import Test.DejaFu.Shrink
import qualified Test.DejaFu.Deterministic.IO as CIO
-- | Run a test and print the result to stdout, return 'True' if it
-- passes.
dejafu :: (Eq a, Show a)
=> (forall t. Conc t a)
-- ^ The computation to test
-> (String, Predicate a)
-- ^ The test case, as a (name, predicate) pair.
-> IO Bool
dejafu conc test = dejafus conc [test]
-- * Test suites
-- | Variant of 'dejafu' for computations which do 'IO'.
dejafuIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> (String, Predicate a) -> IO Bool
dejafuIO concio test = dejafusIO concio [test]
-- | Run a collection of tests (with a pb of 2), printing results to
-- stdout, and returning 'True' iff all tests pass.
doTests :: Show a
=> Bool
-- ^ Whether to print test passes.
-> [(String, Result a)]
-- ^ The test cases
-> IO Bool
doTests = doTests' show
-- | Run a collection of tests, returning 'True' if all pass.
dejafus :: (Eq a, Show a) => (forall t. Conc t a) -> [(String, Predicate a)] -> IO Bool
dejafus conc tests = do
results <- mapM (\(name, test) -> doTest name $ runTest test conc) tests
return $ and results
-- | Variant of 'doTests' which takes a result printing function.
doTests' :: (a -> String) -> Bool -> [(String, Result a)] -> IO Bool
doTests' showf verbose tests = do
results <- mapM (doTest showf verbose) tests
-- | Variant of 'dejafus' for computations which do 'IO'.
dejafusIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> [(String, Predicate a)] -> IO Bool
dejafusIO concio tests = do
results <- mapM (\(name, test) -> doTest name =<< runTestIO test concio) tests
return $ and results
-- | Automatically test a computation. In particular, look for
-- deadlocks and multiple return values.
autocheck :: (Eq a, Show a) => (forall t. Conc t a) -> IO Bool
autocheck t = doTests True cases where
cases = [ ("Never Deadlocks", runTest deadlocksNever t)
, ("Consistent Result", runTest alwaysSame t)
autocheck conc = dejafus conc cases where
cases = [ ("Never Deadlocks", deadlocksNever)
, ("Consistent Result", alwaysSame)
]
-- | Automatically test an 'IO' computation. In particular, look for
-- deadlocks and multiple return values. See usual caveats about 'IO'.
autocheckIO :: (Eq a, Show a) => (forall t. CIO.Conc t a) -> IO Bool
autocheckIO t = do
dead <- runTestIO deadlocksNever t
same <- runTestIO alwaysSame t
doTests True [ ("Never Deadlocks", dead)
, ("Consistent Result", same)
]
-- | Run a test and print to stdout
doTest :: (a -> String) -> Bool -> (String, Result a) -> IO Bool
doTest showf verbose (name, result) = do
if _pass result
then
-- If verbose, display a pass message.
when verbose $
putStrLn $ "\27[32m[pass]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")"
else do
-- Display a failure message, and the first 5 (simplified) failed traces
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 (moreThan (_failures result) 5) $
putStrLn "\t..."
return $ _pass result
-- | Simplify a collection of traces, by attempting to factor out
-- common prefixes and suffixes.
simplify :: [SCTTrace] -> [(SCTTrace, SCTTrace, SCTTrace)]
simplify [t] = [([], t, [])]
simplify ts = map (\t -> (pref, drop plen $ take (length t - slen) t, suff)) ts where
pref = commonPrefix ts
plen = length pref
suff = commonSuffix ts
slen = length suff
-- | Pretty-print a simplified trace
showtrc :: (SCTTrace, SCTTrace, SCTTrace) -> String
showtrc (p, t, s) = case (p, s) of
([], []) -> hilight ++ showtrc' t ++ reset
([], _) -> hilight ++ showtrc' t ++ reset ++ s'
(_, []) -> p' ++ hilight ++ showtrc' t ++ reset
(_, _) -> p' ++ hilight ++ showtrc' t ++ reset ++ s'
where
showtrc' = showTrace . map (\(d,as,_) -> (d,as))
hilight = "\27[33m"
reset = "\27[0m"
p' = (if length p > 50 then ("..." ++) . reverse . take 50 . reverse else id) $ showtrc' p
s' = (if length s > 50 then (++ "...") . take 50 else id) $ showtrc' s
-- | Variant of 'autocheck' for computations which do 'IO'.
autocheckIO :: (Eq a, Show a) => (forall t. ConcIO t a) -> IO Bool
autocheckIO concio = dejafusIO concio cases where
cases = [ ("Never Deadlocks", deadlocksNever)
, ("Consistent Result", alwaysSame)
]
-- * Test cases
@ -136,7 +147,7 @@ data Result a = Result
-- ^ The number of cases checked.
, _casesTotal :: Int
-- ^ The total number of cases.
, _failures :: [(Maybe a, SCTTrace)]
, _failures :: [(Maybe a, Trace)]
-- ^ The failed cases, if any.
} deriving (Show, Eq)
@ -146,45 +157,45 @@ instance NFData a => NFData (Result a) where
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, and attempt to shrink any failing traces.
-- | Run a predicate over all executions with two or fewer
-- pre-emptions, and attempt to shrink any failing traces. A
-- pre-emption is a context switch where the old thread was still
-- runnable.
--
-- In the resultant traces, a pre-emption is displayed as \"Px\",
-- where @x@ is the ID of the thread being switched to, whereas a
-- regular context switch is displayed as \"Sx\" (for \"start\").
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 :: Eq a => Predicate a -> (forall t. CIO.Conc t a) -> IO (Result a)
-- | Variant of 'runTest' for computations which do 'IO'.
runTestIO :: Eq a => Predicate a -> (forall t. ConcIO t a) -> IO (Result a)
runTestIO = runTestIO' 2
-- | Run a test using the pre-emption bounding scheduler, and attempt
-- to shrink any failing traces.
-- | 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 = 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' :: Eq a => Int -> Predicate a -> (forall t. CIO.Conc t a) -> IO (Result a)
-- | 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 = (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) . groupByIsh ((==) `on` fst) where
simplest' Nothing r = Just r
simplest' r@(Just (_, trc)) s@(_, trc')
| simplest [trc, trc'] == Just trc = r
| otherwise = Just s
-- | Strip out duplicates
uniques :: Eq a => [(Maybe a, Trace)] -> [(Maybe a, Trace)]
uniques = map head . groupByIsh (==)
-- * Predicates
-- | A @Predicate@ is a function which collapses a list of results
-- into a 'Result'.
type Predicate a = [(Maybe a, SCTTrace)] -> Result a
type Predicate a = [(Maybe a, Trace)] -> Result a
-- | Check that a computation never deadlocks.
deadlocksNever :: Predicate a
@ -204,8 +215,12 @@ deadlocksSometimes = somewhereTrue isNothing
alwaysSame :: Eq a => Predicate a
alwaysSame = alwaysTrue2 (==)
-- | Check that the result of a computation is not always the same.
notAlwaysSame :: Eq a => Predicate a
notAlwaysSame = somewhereTrue2 (/=)
-- | Check that the result of a unary boolean predicate is always
-- true. An empty list of results counts as 'True'.
-- true.
alwaysTrue :: (Maybe a -> Bool) -> Predicate a
alwaysTrue p xs = go xs Result { _pass = True, _casesChecked = 0, _casesTotal = len, _failures = failures } where
go [] res = res
@ -216,10 +231,12 @@ alwaysTrue p xs = go xs Result { _pass = True, _casesChecked = 0, _casesTotal =
(len, failures) = findFailures1 p xs
-- | Check that the result of a binary boolean predicate is always
-- true between adjacent pairs of results. An empty list of results
-- counts as 'True'.
-- 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.
--
-- If the predicate fails, *both* (result,trace) tuples will be added
-- If the predicate fails, /both/ (result,trace) tuples will be added
-- to the failures list.
alwaysTrue2 :: (Maybe a -> Maybe a -> Bool) -> Predicate a
alwaysTrue2 _ [_] = Result { _pass = True, _casesChecked = 1, _casesTotal = 1, _failures = [] }
@ -235,7 +252,7 @@ alwaysTrue2 p xs = go xs Result { _pass = True, _casesChecked = 0, _casesTotal
(len, failures) = findFailures2 p xs
-- | Check that the result of a unary boolean predicate is true at
-- least once. An empty list of results counts as 'False'.
-- least once.
somewhereTrue :: (Maybe a -> Bool) -> Predicate a
somewhereTrue p xs = go xs Result { _pass = False, _casesChecked = 0, _casesTotal = len, _failures = failures } where
go [] res = res
@ -246,10 +263,12 @@ somewhereTrue p xs = go xs Result { _pass = False, _casesChecked = 0, _casesTota
(len, failures) = findFailures1 p xs
-- | Check that the result of a binary boolean predicate is true
-- between at least one adjacent pair of results. An empty list of
-- results counts as 'False'.
-- 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
-- If the predicate fails, /both/ (result,trace) tuples will be added
-- to the failures list.
somewhereTrue2 :: (Maybe a -> Maybe a -> Bool) -> Predicate a
somewhereTrue2 _ [x] = Result { _pass = False, _casesChecked = 1, _casesTotal = 1, _failures = [x] }
@ -264,23 +283,35 @@ somewhereTrue2 p xs = go xs Result { _pass = False, _casesChecked = 0, _casesTo
(len, failures) = findFailures2 p xs
-- * Utils
-- * Internal
-- | Compose two predicates sequentially.
pAnd :: Predicate a -> Predicate a -> Predicate a
pAnd p q xs = if _pass r1 then r2 else r1 where
r1 = p xs
r2 = q xs
-- | Run a test and print to stdout
doTest :: (Eq a, Show a) => String -> Result a -> IO Bool
doTest name result = do
if _pass result
then
-- Display a pass message.
putStrLn $ "\27[32m[pass]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")"
else do
-- Display a failure message, and the first 5 (simplified) failed traces
putStrLn ("\27[31m[fail]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")")
let failures = nubBy reseq $ _failures result
mapM_ (\(r, t) -> putStrLn $ "\t" ++ maybe "[deadlock]" show r ++ " " ++ showTrace t) $ take 5 failures
when (moreThan failures 5) $
putStrLn "\t..."
-- | Invert the result of a predicate.
pNot :: Predicate a -> Predicate a
pNot p xs = r { _pass = not $ _pass r } where
r = p xs
return $ _pass result
-- | Throw away the failures information in a Result (useful for
-- storing them in a list).
rForgetful :: Result a -> Result ()
rForgetful = void
where
reseq (res, trc) (res', trc') = res == res' && trc `eq` trc'
-- Two traces are "equal" if their decisions differ ONLY in
-- non-preemptive context switches. This helps filter out some
-- false positives.
eq [] [] = True
eq _ [] = False
eq [] _ = False
eq ((Start _,_,_):as) ((Start _,_,_):bs) = as `eq` bs
eq ((a,_,_):as) ((b,_,_):bs) = a == b && as `eq` bs
-- | Increment the cases checked
incCC :: Result a -> Result a
@ -288,7 +319,7 @@ incCC r = r { _casesChecked = _casesChecked r + 1 }
-- | Get the length of the list and find the failing cases in one
-- traversal.
findFailures1 :: (Maybe a -> Bool) -> [(Maybe a, SCTTrace)] -> (Int, [(Maybe a, SCTTrace)])
findFailures1 :: (Maybe a -> Bool) -> [(Maybe a, Trace)] -> (Int, [(Maybe a, Trace)])
findFailures1 p xs = findFailures xs 0 [] where
findFailures [] l fs = (l, fs)
findFailures ((z,t):zs) l fs
@ -297,7 +328,7 @@ findFailures1 p xs = findFailures xs 0 [] where
-- | Get the length of the list and find the failing cases in one
-- traversal.
findFailures2 :: (Maybe a -> Maybe a -> Bool) -> [(Maybe a, SCTTrace)] -> (Int, [(Maybe a, SCTTrace)])
findFailures2 :: (Maybe a -> Maybe a -> Bool) -> [(Maybe a, Trace)] -> (Int, [(Maybe a, Trace)])
findFailures2 p xs = findFailures xs 0 [] where
findFailures [] l fs = (l, fs)
findFailures [_] l fs = (l+1, fs)

40
Test/DejaFu/Deterministic.hs
View File

@ -2,14 +2,16 @@
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
-- | Concurrent monads with a fixed scheduler.
-- | Deterministic traced execution of concurrent computations which
-- don't do @IO@.
--
-- This works by executing the computation on a single thread, calling
-- out to the supplied scheduler after each step to determine which
-- thread runs next.
module Test.DejaFu.Deterministic
( -- * The Conc Monad
( -- * The @Conc@ Monad
Conc
, Trace
, ThreadAction(..)
, runConc
, runConc'
, fork
, spawn
@ -22,8 +24,14 @@ module Test.DejaFu.Deterministic
, takeCVar
, tryTakeCVar
-- * Schedulers
, module Test.DejaFu.Deterministic.Schedulers
-- * Execution traces
, Trace
, Decision
, ThreadAction
, showTrace
-- * Scheduling
, module Test.DejaFu.Deterministic.Schedule
) where
import Control.Applicative (Applicative(..), (<$>))
@ -31,14 +39,14 @@ import Control.Monad.Cont (cont, runCont)
import Control.Monad.ST (ST, runST)
import Data.STRef (STRef, newSTRef, readSTRef, writeSTRef)
import Test.DejaFu.Deterministic.Internal
import Test.DejaFu.Deterministic.Schedulers
import Test.DejaFu.Deterministic.Schedule
import qualified Control.Monad.Conc.Class as C
-- | The @Conc@ monad itself. This uses the same
-- universally-quantified indexing state trick as used by 'ST' and
-- 'STRef's to prevent mutable references from leaking out of the
-- monad. See 'runConc' for an example of what this means.
-- monad.
newtype Conc t a = C { unC :: M (ST t) (STRef t) a } deriving (Functor, Applicative, Monad)
instance C.MonadConc (Conc t) where
@ -107,20 +115,16 @@ tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar
-- | Run a concurrent computation with a given 'Scheduler' and initial
-- state, returning a 'Just' if it terminates, and 'Nothing' if a
-- deadlock is detected.
-- deadlock is detected. Also returned is the final state of the
-- scheduler, and an execution trace.
--
-- Note how the @t@ in 'Conc' is universally quantified, what this
-- means in practice is that you can't do something like this:
--
-- > runConc (\s _ (x:_) -> (x, s)) () $ new >>= return
-- > runConc (\s _ (x:_) -> (x, s)) () newEmptyCVar
--
-- So 'CVar's cannot leak out of the 'Conc' computation. If this is
-- making your head hurt, check out the \"How @runST@ works\" section
-- of <https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html>
runConc :: Scheduler s -> s -> (forall t. Conc t a) -> Maybe a
runConc sched s ma = let (a,_,_) = runConc' sched s ma in a
-- | Variant of 'runConc' which returns the final state of the
-- scheduler and an execution trace.
runConc' :: Scheduler s -> s -> (forall t. Conc t a) -> (Maybe a, s, Trace)
runConc' sched s ma = runST $ runFixed' fixed sched s ma
runConc :: Scheduler s -> s -> (forall t. Conc t a) -> (Maybe a, s, Trace)
runConc sched s ma = runST $ runFixed fixed sched s ma

93
Test/DejaFu/Deterministic/IO.hs
View File

@ -2,21 +2,19 @@
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
-- | Concurrent monads with a fixed scheduler which can do IO.
-- | Deterministic traced execution of concurrent computations which
-- may do @IO@.
--
-- Caution! Blocking on the action of another thread in 'liftIO'
-- __Caution!__ Blocking on the action of another thread in 'liftIO'
-- cannot be detected! So if you perform some potentially blocking
-- action in a 'liftIO' the entire collection of threads may deadlock!
-- You should therefore keep 'IO' blocks small, and only perform
-- You should therefore keep @IO@ blocks small, and only perform
-- blocking operations with the supplied primitives, insofar as
-- possible.
module Test.DejaFu.Deterministic.IO
( -- * The Conc Monad
Conc
, Trace
, ThreadAction(..)
, runConc
, runConc'
( -- * The @ConcIO@ Monad
ConcIO
, runConcIO
, liftIO
, fork
, spawn
@ -30,30 +28,33 @@ module Test.DejaFu.Deterministic.IO
, takeCVar
, tryTakeCVar
-- * Schedulers
, module Test.DejaFu.Deterministic.Schedulers
-- * Execution traces
, Trace
, Decision
, ThreadAction
, showTrace
-- * Scheduling
, module Test.DejaFu.Deterministic.Schedule
) where
import Control.Applicative (Applicative(..), (<$>))
import Control.Monad.Cont (cont, runCont)
import Data.IORef (IORef, newIORef, readIORef, writeIORef)
import Test.DejaFu.Deterministic.Internal
import Test.DejaFu.Deterministic.Schedulers
import Test.DejaFu.Deterministic.Schedule
import qualified Control.Monad.Conc.Class as C
import qualified Control.Monad.IO.Class as IO
-- | The @Conc@ monad itself. This uses the same
-- universally-quantified indexing state trick as used by 'ST' and
-- 'STRef's to prevent mutable references from leaking out of the
-- monad. See 'runConc' for an example of what this means.
newtype Conc t a = C { unC :: M IO IORef a } deriving (Functor, Applicative, Monad)
-- | The 'IO' variant of Test.DejaFu.Deterministic's @Conc@ monad.
newtype ConcIO t a = C { unC :: M IO IORef a } deriving (Functor, Applicative, Monad)
instance IO.MonadIO (Conc t) where
instance IO.MonadIO (ConcIO t) where
liftIO = liftIO
instance C.MonadConc (Conc t) where
type CVar (Conc t) = CVar t
instance C.MonadConc (ConcIO t) where
type CVar (ConcIO t) = CVar t
fork = fork
newEmptyCVar = newEmptyCVar
@ -63,8 +64,7 @@ instance C.MonadConc (Conc t) where
takeCVar = takeCVar
tryTakeCVar = tryTakeCVar
-- This is horrible, but it makes the types work
fixed :: Fixed Conc IO IORef t
fixed :: Fixed ConcIO IO IORef t
fixed = F
{ newRef = newIORef
, readRef = readIORef
@ -73,72 +73,55 @@ fixed = F
, getCont = unC
}
-- | The concurrent variable type used with the 'Conc' monad. One
-- notable difference between these and 'MVar's is that 'MVar's are
-- single-wakeup, and wake up in a FIFO order. Writing to a @CVar@
-- wakes up all threads blocked on reading it, and it is up to the
-- scheduler which one runs next. Taking from a @CVar@ behaves
-- analogously.
-- | The concurrent variable type used with the 'ConcIO' monad. These
-- behave the same as @Conc@'s @CVar@s
newtype CVar t a = V { unV :: R IORef a } deriving Eq
-- | Lift an 'IO' action into the 'Conc' monad.
liftIO :: IO a -> Conc t a
-- | Lift an 'IO' action into the 'ConcIO' monad.
liftIO :: IO a -> ConcIO t a
liftIO ma = C $ cont lifted where
lifted c = ALift $ c <$> ma
-- | Run the provided computation concurrently, returning the result.
spawn :: Conc t a -> Conc t (CVar t a)
spawn :: ConcIO t a -> ConcIO t (CVar t a)
spawn = C.spawn
-- | Block on a 'CVar' until it is full, then read from it (without
-- emptying).
readCVar :: CVar t a -> Conc t a
readCVar :: CVar t a -> ConcIO t a
readCVar cvar = C $ cont $ AGet $ unV cvar
-- | Run the provided computation concurrently.
fork :: Conc t () -> Conc t ()
fork :: ConcIO t () -> ConcIO t ()
fork (C ma) = C $ cont $ \c -> AFork (runCont ma $ const AStop) $ c ()
-- | Create a new empty 'CVar'.
newEmptyCVar :: Conc t (CVar t a)
newEmptyCVar :: ConcIO t (CVar t a)
newEmptyCVar = C $ cont lifted where
lifted c = ANew $ c <$> newEmptyCVar'
newEmptyCVar' = V <$> newIORef (Nothing, [])
-- | Block on a 'CVar' until it is empty, then write to it.
putCVar :: CVar t a -> a -> Conc t ()
putCVar :: CVar t a -> a -> ConcIO t ()
putCVar cvar a = C $ cont $ \c -> APut (unV cvar) a $ c ()
-- | Put a value into a 'CVar' if there isn't one, without blocking.
tryPutCVar :: CVar t a -> a -> Conc t Bool
tryPutCVar :: CVar t a -> a -> ConcIO t Bool
tryPutCVar cvar a = C $ cont $ ATryPut (unV cvar) a
-- | Block on a 'CVar' until it is full, then read from it (with
-- emptying).
takeCVar :: CVar t a -> Conc t a
takeCVar :: CVar t a -> ConcIO t a
takeCVar cvar = C $ cont $ ATake $ unV cvar
-- | Read a value from a 'CVar' if there is one, without blocking.
tryTakeCVar :: CVar t a -> Conc t (Maybe a)
tryTakeCVar :: CVar t a -> ConcIO t (Maybe a)
tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar
-- | Run a concurrent computation with a given 'Scheduler' and initial
-- state, returning 'Just' if it terminates, and 'Nothing' if a
-- deadlock is detected.
--
-- Note how the @t@ in 'Conc' is universally quantified, what this
-- means in practice is that you can't do something like this:
--
-- > runConc (\s _ (x:_) -> (x, s)) () newEmptyCVar
--
-- So 'CVar's cannot leak out of the 'Conc' computation. If this is
-- making your head hurt, check out the \"How @runST@ works\" section
-- of <https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html>
runConc :: Scheduler s -> s -> (forall t. Conc t a) -> IO (Maybe a)
runConc sched s ma = (\(a,_,_) -> a) <$> runConc' sched s ma
-- | Variant of 'runConc' which returns the final state of the
-- scheduler and an execution trace.
runConc' :: Scheduler s -> s -> (forall t. Conc t a) -> IO (Maybe a, s, Trace)
-- deadlock is detected. Also returned is the final state of the
-- scheduler, and an execution trace.
runConcIO :: Scheduler s -> s -> (forall t. ConcIO t a) -> IO (Maybe a, s, Trace)
-- Note: Don't eta-reduce, the forall t messes up type inference.
runConc' sched s ma = runFixed' fixed sched s ma
runConcIO sched s ma = runFixed fixed sched s ma

73
Test/DejaFu/Deterministic/Internal.hs
View File

@ -6,7 +6,7 @@
module Test.DejaFu.Deterministic.Internal where
import Control.DeepSeq (NFData(..))
import Control.Monad (liftM, mapAndUnzipM)
import Control.Monad (mapAndUnzipM)
import Control.Monad.Cont (Cont, runCont)
import Data.List.Extra
import Data.Map (Map)
@ -57,23 +57,53 @@ data Action n r =
-- | Every live thread has a unique identitifer. These are implemented
-- as integers, but you shouldn't assume they are necessarily
-- contiguous.
-- contiguous, or globally unique (although it is the case that no two
-- threads alive at the same time will have the same identifier).
type ThreadId = Int
-- | 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.
--
-- Note: In order to prevent computation from hanging, the 'Conc'
-- 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.
-- 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)
-- | One of the outputs of the runner is a @Trace@, which is just a
-- log of threads and actions they have taken.
type Trace = [(ThreadId, ThreadAction)]
-- | 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
-- in its step.
type Trace = [(Decision, [Decision], ThreadAction)]
-- | Pretty-print a trace.
showTrace :: Trace -> String
showTrace = trace "" 0 where
trace prefix num ((Start tid,_,_):ds) = thread prefix num ++ trace ("S" ++ show tid) 1 ds
trace prefix num ((SwitchTo tid,_,_):ds) = thread prefix num ++ trace ("P" ++ show tid) 1 ds
trace prefix num ((Continue,_,_):ds) = trace prefix (num + 1) ds
trace prefix num [] = thread prefix num
thread prefix num = prefix ++ replicate num '-'
-- | Scheduling decisions are based on the state of the running
-- program, and so we can capture some of that state in recording what
-- specific decision we made.
data Decision =
Start ThreadId
-- ^ Start a new thread, because the last was blocked (or it's the
-- start of computation).
| Continue
-- ^ Continue running the last thread for another step.
| SwitchTo ThreadId
-- ^ Pre-empt the running thread, and switch to another.
deriving (Eq, Show)
instance NFData Decision where
rnf (Start tid) = rnf tid
rnf (SwitchTo tid) = rnf tid
rnf Continue = ()
-- | All the actions that a thread can perform.
data ThreadAction =
@ -121,16 +151,11 @@ instance NFData ThreadAction where
-- | Run a concurrent computation with a given 'Scheduler' and initial
-- state, returning a 'Just' if it terminates, and 'Nothing' if a
-- deadlock is detected.
-- deadlock is detected. Also returned is the final state of the
-- scheduler, and an execution trace.
runFixed :: (Monad (c t), Monad n) => Fixed c n r t
-> Scheduler s -> s -> c t a -> n (Maybe a)
runFixed fixed sched s ma = liftM (\(a,_,_) -> a) $ runFixed' fixed sched s ma
-- | Variant of 'runFixed' which returns the final state of the
-- scheduler and an execution trace.
runFixed' :: (Monad (c t), Monad n) => Fixed c n r t
-> Scheduler s -> s -> c t a -> n (Maybe a, s, Trace)
runFixed' fixed sched s ma = do
runFixed fixed sched s ma = do
ref <- newRef fixed Nothing
let c = getCont fixed $ ma >>= liftN fixed . writeRef fixed ref . Just
@ -167,7 +192,7 @@ runThreads fixed sofar prior sched s threads ref
| isBlocked = writeRef fixed ref Nothing >> return (s, sofar)
| otherwise = do
(threads', act) <- stepThread (fst $ fromJust thread) fixed chosen threads
let sofar' = (chosen, act) : sofar
let sofar' = (decision, alternatives, act) : sofar
runThreads fixed sofar' chosen sched s' threads' ref
where
@ -180,6 +205,16 @@ runThreads fixed sofar prior sched s threads ref
isTerminated = 0 `notElem` M.keys threads
isDeadlocked = M.null runnable
decision
| chosen == prior = Continue
| prior `elem` 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'
-- | Run a single thread one step, by dispatching on the type of
-- 'Action'.
stepThread :: (Monad (c t), Monad n)

7
Test/DejaFu/Deterministic/Schedulers.hs → Test/DejaFu/Deterministic/Schedule.hs
View File

@ -1,7 +1,6 @@
-- | Schedulers for the fixed @Conc@ monads.
module Test.DejaFu.Deterministic.Schedulers
( -- * Types
Scheduler
-- | Deterministic scheduling for concurrent computations.
module Test.DejaFu.Deterministic.Schedule
( Scheduler
, ThreadId
, NonEmpty(..)
-- * Pre-emptive

65
Test/DejaFu/SCT.hs
View File

@ -1,51 +1,10 @@
-- | A runner for concurrent monads to systematically detect
-- concurrency errors such as data races and deadlocks.
--
-- As an example, consider this program, which has two locks and a
-- shared variable. Two threads are spawned, which claim the locks,
-- update the shared variable, and release the locks. The main thread
-- waits for them both to terminate, and returns the final result.
--
-- > bad :: MonadConc m => m Int
-- > bad = do
-- > a <- newEmptyCVar
-- > b <- newEmptyCVar
-- >
-- > c <- newCVar 0
-- >
-- > j1 <- spawn $ lock a >> lock b >> modifyCVar_ c (return . succ) >> unlock b >> unlock a
-- > j2 <- spawn $ lock b >> lock a >> modifyCVar_ c (return . pred) >> unlock a >> unlock b
-- >
-- > takeCVar j1
-- > takeCVar j2
-- >
-- > takeCVar c
--
-- The correct result is 0, as it starts out as 0 and is incremented
-- and decremented by threads 1 and 2, respectively. However, note the
-- order of acquisition of the locks in the two threads. If thread 2
-- pre-empts thread 1 between the acquisition of the locks (or if
-- thread 1 pre-empts thread 2), a deadlock situation will arise, as
-- thread 1 will have lock @a@ and be waiting on @b@, and thread 2
-- will have @b@ and be waiting on @a@.
-- | Systematic testing for concurrent computations.
module Test.DejaFu.SCT
( -- * Types
SCTScheduler
, SchedTrace
, SCTTrace
, Decision(..)
-- * SCT Runners
, runSCT
, runSCTIO
( runSCT
, runSCT'
, runSCTIO
, runSCTIO'
-- * Random Schedulers
, sctRandom
, sctRandomNP
-- * Schedule Bounding
-- | Schedule bounding is a means of cutting down the search space of
-- schedules, by taking advantage of some intrinsic properties of
@ -54,29 +13,15 @@ module Test.DejaFu.SCT
-- scheduler (delay bounding); and then exploring all schedules
-- within the bound.
, sctBounded
, sctBoundedIO
, sctPreBound
, sctPreBoundIO
, sctDelayBound
, sctBoundedIO
, sctPreBoundIO
, sctDelayBoundIO
-- * Utilities
, makeSCT
, preEmpCount
, showTrace
) where
import System.Random (RandomGen)
import Test.DejaFu.Deterministic
import Test.DejaFu.SCT.Internal
import Test.DejaFu.SCT.Bounding
-- * Random Schedulers
-- | A simple pre-emptive random scheduler.
sctRandom :: RandomGen g => SCTScheduler g
sctRandom = makeSCT randomSched
-- | A random scheduler with no pre-emption.
sctRandomNP :: RandomGen g => SCTScheduler g
sctRandomNP = makeSCT randomSchedNP

72
Test/DejaFu/SCT/Bounding.hs
View File

@ -7,24 +7,23 @@ module Test.DejaFu.SCT.Bounding where
import Control.DeepSeq (NFData(..), force)
import Data.List.Extra
import Test.DejaFu.Deterministic
import Test.DejaFu.Deterministic.Internal
import Test.DejaFu.Deterministic.IO (ConcIO)
import Test.DejaFu.SCT.Internal
import qualified Test.DejaFu.Deterministic.IO as CIO
-- * Pre-emption bounding
-- | An SCT runner using a pre-emption bounding scheduler. Schedules
-- are explored systematically, in a depth-first fashion.
sctPreBound :: Int -> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
-- | An SCT runner using a pre-emption bounding scheduler.
sctPreBound :: Int -> (forall t. Conc t a) -> [(Maybe a, Trace)]
sctPreBound = sctBounded pbSiblings (pbOffspring False)
-- | Variant of 'sctPreBound' using 'IO'. See usual caveats about IO.
sctPreBoundIO :: Int -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
-- | Variant of 'sctPreBound' for computations which do 'IO'.
sctPreBoundIO :: Int -> (forall t. ConcIO t a) -> IO [(Maybe a, Trace)]
sctPreBoundIO = sctBoundedIO pbSiblings (pbOffspring True)
-- | Return all modifications to this schedule which do not introduce
-- extra pre-emptions.
pbSiblings :: SCTTrace -> [[Decision]]
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]
@ -34,7 +33,7 @@ pbSiblings = siblings . map (\(d,a,_) -> (d,a)) where
-- | Return all modifications to this schedule which do introduce an
-- extra pre-emption. Only introduce pre-emptions around CVar actions
-- and lifts.
pbOffspring :: Bool -> SCTTrace -> [[Decision]]
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]
@ -50,19 +49,17 @@ preEmpCount [] = 0
-- * Delay bounding
-- | An SCT runner using a delay-bounding scheduler. Schedules are
-- explored systematically, in a depth-first fashion.
sctDelayBound :: Int -> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
-- | An SCT runner using a delay-bounding scheduler.
sctDelayBound :: Int -> (forall t. Conc t a) -> [(Maybe a, Trace)]
sctDelayBound = sctBounded (const []) (dbOffspring False)
-- | Variant of 'sctDelayBound' using 'IO'. See usual caveats about
-- IO.
sctDelayBoundIO :: Int -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
-- | Variant of 'sctDelayBound' for computations which do 'IO'.
sctDelayBoundIO :: Int -> (forall t. ConcIO t a) -> IO [(Maybe 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 -> SCTTrace -> [[Decision]]
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]
@ -71,21 +68,38 @@ dbOffspring _ [] = []
-- * SCT runners
-- | An SCT runner using schedule bounding.
sctBounded :: (SCTTrace -> [[Decision]])
-- | 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.
-> (SCTTrace -> [[Decision]])
-> (Trace -> [[Decision]])
-- ^ Child generation function.
-> Int
-- ^ Bound, anything < 0 will be interpreted as no bound.
-> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
-> (forall t. Conc t a) -> [(Maybe a, Trace)]
sctBounded siblings offspring b = runSCT' prefixSched (initialS, initialG) bTerm (bStep siblings offspring b)
-- | Variant of 'sctBounded' using 'IO'.
sctBoundedIO :: (SCTTrace -> [[Decision]])
-> (SCTTrace -> [[Decision]])
-- | Variant of 'sctBounded' for computations which do 'IO'.
sctBoundedIO :: (Trace -> [[Decision]])
-> (Trace -> [[Decision]])
-> Int
-> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
-> (forall t. ConcIO t a) -> IO [(Maybe a, Trace)]
sctBoundedIO siblings offspring b = runSCTIO' prefixSched (initialS, initialG) bTerm (bStep siblings offspring b)
-- * State
@ -122,8 +136,8 @@ initialG = P { _next = Empty 0, _halt = False }
-- | Scheduler which uses a list of scheduling decisions to drive the
-- initial decisions.
prefixSched :: SCTScheduler Sched
prefixSched = force . makeSCT $ \s prior threads@(next:|_) -> case _decisions s of
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 })
@ -147,13 +161,13 @@ bTerm (_, g) = _halt g
-- a higher bound before all the ones with a lower bound. Testing with
-- a very concurrent problem (finding a deadlock in 100 dining
-- philosophers) has revealed this may work better in practice.
bStep :: (SCTTrace -> [[Decision]])
bStep :: (Trace -> [[Decision]])
-- ^ Sibling generation function.
-> (SCTTrace -> [[Decision]])
-> (Trace -> [[Decision]])
-- ^ Offspring generation function.
-> Int
-- ^ Bound.
-> (Sched, State) -> SCTTrace -> (Sched, State)
-> (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

126
Test/DejaFu/SCT/Internal.hs
View File

@ -4,71 +4,30 @@
-- concurrency errors such as data races and deadlocks: internal definitions.
module Test.DejaFu.SCT.Internal where
import Control.DeepSeq (NFData(..))
import Control.Monad.Loops (unfoldrM)
import Data.List (unfoldr)
import Test.DejaFu.Deterministic
import qualified Test.DejaFu.Deterministic.IO as CIO
-- * Types
-- | An @SCTScheduler@ is like a regular 'Scheduler', except it builds
-- a trace of scheduling decisions made.
--
-- If implementing your own scheduler, note that the 'SchedTrace' is
-- built in reverse, as this is more efficient than appending to the
-- list every time, also note that the scheduler is not called before
-- starting the first thread, as there is only one possible decision.
type SCTScheduler s = Scheduler (s, SchedTrace)
-- | A @SchedTrace@ is just a list of all the decisions that were made,
-- with the alternative decisions that could have been made at each
-- step.
type SchedTrace = [(Decision, [Decision])]
-- | An @SCTTrace@ is a combined 'SchedTrace' and 'Trace'.
type SCTTrace = [(Decision, [Decision], ThreadAction)]
-- | Scheduling decisions are based on the state of the running
-- program, and so we can capture some of that state in recording what
-- specific decision we made.
data Decision =
Start ThreadId
-- ^ Start a new thread, because the last was blocked (or it's the
-- start of computation).
| Continue
-- ^ Continue running the last thread for another step.
| SwitchTo ThreadId
-- ^ Pre-empt the running thread, and switch to another.
deriving (Eq, Show)
instance NFData Decision where
rnf (Start tid) = rnf tid
rnf (SwitchTo tid) = rnf tid
rnf Continue = ()
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 scheduling that gave rise to
-- them.
-- times, collecting the results and the trace that gave rise to them.
--
-- The initial state for each run is the final state of the last run,
-- 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 :: SCTScheduler s -> s -> Int -> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
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
-> [(Maybe a, Trace)]
runSCT sched s n = runSCT' sched (s, n) term step where
term (_, g) = g == 0
step (s', g) _ = (s', g - 1)
-- | A varant of 'runSCT' for concurrent programs that do 'IO'.
--
-- Warning! The IO will be executed lots of times, in lots of
-- interleavings! Be very confident that nothing in a 'liftIO' can
-- block on the action of another thread, or you risk deadlocking this
-- function!
runSCTIO :: SCTScheduler s -> s -> Int -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
-- | Variant of 'runSCT' for computations which do 'IO'.
runSCTIO :: Scheduler s -> s -> Int -> (forall t. ConcIO t a) -> IO [(Maybe a, Trace)]
runSCTIO sched s n = runSCTIO' sched (s, n) term step where
term (_, g) = g == 0
step (s', g) _ = (s', g - 1)
@ -80,79 +39,30 @@ runSCTIO sched s n = runSCTIO' sched (s, n) term step where
--
-- Note: the state step function takes the state returned by the
-- scheduler, not the initial state!
runSCT' :: SCTScheduler s -- ^ The scheduler
runSCT' :: Scheduler s -- ^ The scheduler
-> (s, g) -- ^ The scheduler's and runner's initial states
-> ((s, g) -> Bool) -- ^ Termination decider
-> ((s, g) -> SCTTrace -> (s, g)) -- ^ State step function
-> (forall t. Conc t a) -- ^ Conc program
-> [(Maybe a, SCTTrace)]
-> ((s, g) -> Trace -> (s, g)) -- ^ State step function
-> (forall t. Conc t a) -- ^ The computation to test
-> [(Maybe 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', strace), ttrace) = runConc' sched (s, initialTrace) c
trace = scttrace (reverse strace) ttrace
(res, s', trace) = runConc sched s c
sg' = step (s', g) trace
-- | A variant of runSCT' for concurrent programs that do IO.
--
-- Warning! The IO will be executed lots of times, in lots of
-- interleavings! Be very confident that nothing in a 'liftIO' can
-- block on the action of another thread, or you risk deadlocking this
-- function!
runSCTIO' :: SCTScheduler s -> (s, g) -> ((s, g) -> Bool) -> ((s, g) -> SCTTrace -> (s, g)) -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
-- | 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 [(Maybe a, Trace)]
runSCTIO' sched initial term step c = unfoldrM go initial where
go sg@(s, g)
| term sg = return Nothing
| otherwise = do
(res, (s', strace), ttrace) <- CIO.runConc' sched (s, initialTrace) c
(res, s', trace) <- runConcIO sched s c
let trace = scttrace (reverse strace) ttrace
let sg' = step (s', g) trace
res `seq` return (Just ((res, trace), sg'))
-- * Schedulers and Traces
-- | Convert a 'Scheduler' to an 'SCTScheduler' by recording the
-- trace.
makeSCT :: Scheduler s -> SCTScheduler s
makeSCT sched (s, trace) prior threads = (tid, (s', (decision, alters) : trace)) where
(tid, s') = sched s prior threads
decision
| tid == prior = Continue
| prior `elem` threads' = SwitchTo tid
| otherwise = Start tid
alters
| tid == prior = map SwitchTo $ filter (/=prior) threads'
| prior `elem` threads' = Continue : map SwitchTo (filter (\t -> t /= prior && t /= tid) threads')
| otherwise = map Start $ filter (/=tid) threads'
threads' = toList threads
-- | Pretty-print a scheduler trace.
showTrace :: SchedTrace -> String
showTrace = trace "" 0 . map fst where
trace prefix num (Start tid:ds) = thread prefix num ++ trace ("S" ++ show tid) 1 ds
trace prefix num (SwitchTo tid:ds) = thread prefix num ++ trace ("P" ++ show tid) 1 ds
trace prefix num (Continue:ds) = trace prefix (num + 1) ds
trace prefix num [] = thread prefix num
thread prefix num = prefix ++ replicate num '-'
-- * Utils (Internal)
-- | Zip a list of 'SchedTrace's and a 'Trace' together into an
-- 'SCTTrace'.
scttrace :: SchedTrace -> Trace -> SCTTrace
scttrace = zipWith $ \(d, alts) (_, act) -> (d, alts, act)
-- | The initial trace of a @Conc@ computation.
initialTrace :: SchedTrace
initialTrace = [(Start 0, [])]

95
Test/DejaFu/Shrink.hs
View File

@ -3,11 +3,8 @@
-- | Functions for attempting to find maximally simple traces
-- producing a given result.
module Test.DejaFu.Shrink
( -- * Trace shrinking
shrink
, shrink'
( shrink
, shrinkIO
, shrinkIO'
-- * Utilities
-- | If you wanted to implement your own shrinking logic, these are
@ -21,35 +18,25 @@ module Test.DejaFu.Shrink
import Control.Applicative ((<$>))
import Data.Function (on)
import Data.List (sortBy, isPrefixOf)
import Data.List.Extra
import Data.List (sortBy, isPrefixOf, nubBy)
import Data.Maybe (fromJust, listToMaybe)
import Data.Ord (comparing)
import Test.DejaFu.Deterministic
import Test.DejaFu.Deterministic.Internal
import Test.DejaFu.Deterministic.IO (ConcIO)
import Test.DejaFu.SCT.Bounding
import Test.DejaFu.SCT.Internal
import qualified Test.DejaFu.Deterministic.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
shrink :: Eq a => (Maybe a, Trace) -> (forall t. Conc t a) -> Trace
shrink (result, 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
ts -> fromJust . simplest $ map (uncurry shrink') ts
where
-- Get all candidate trace prefixes which start with the given
@ -63,7 +50,7 @@ shrink' p trace t = shrink'' [] trace where
-- 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
let tries = filter (/=trace) $ try (==result) pref t
in case simplest tries of
-- No further candidates available.
Nothing -> []
@ -75,22 +62,20 @@ shrink' p trace t = shrink'' [] trace where
-- 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
-- | Variant of 'shrink' for computations which do 'IO'.
shrinkIO :: Eq a => (Maybe a, Trace) -> (forall t. ConcIO t a) -> IO Trace
shrinkIO (result, 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
ts -> fromJust . simplest <$> mapM (uncurry shrink') ts
where
step (pref, tid) = do
tries <- tryIO p pref t
tries <- tryIO (==result) pref t
return $
case simplest tries of
Nothing -> []
@ -103,34 +88,35 @@ shrinkIO' p trace t = shrink'' [] trace where
-- 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 :: Trace -> [([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 all traces with a given trace prefix, which introduce no more
-- than one new pre-emption, and return those which satisfy the
-- predicate.
try :: (Maybe a -> Bool) -> [Decision] -> (forall t. Conc t a) -> [Trace]
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]
-- | Variant of 'try' for computations which do 'IO'.
tryIO :: (Maybe a -> Bool) -> [Decision] -> (forall t. ConcIO t a) -> IO [Trace]
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
-- | Given a list of 'Trace's which follow on from a given prefix,
-- determine if the removed pre-emption is /essential/. That is, every
-- 'Trace' starts with the prefix followed immediately by a
-- pre-emption to the given thread.
essential :: ([Decision], ThreadId) -> [Trace] -> Bool
essential (ds, tid) = all ((pref `isPrefixOf`) . map (\(d,_,_) -> d)) where
pref = ds ++ [SwitchTo tid]
-- | Return the simplest 'SCTTrace' from a collection. Roughly, the
-- | Return the simplest 'Trace' 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
simplest :: [Trace] -> Maybe Trace
simplest = listToMaybe . nubBy (lexico `on` map (\(d,_,_) -> d)) . restrict contextSwitch . restrict preEmpCount where
-- Favour schedules with fewer context switches if they have the
-- same number of pre-emptions.
@ -148,24 +134,21 @@ simplest = listToMaybe . nubishBy (lexico `on` unSCT) . restrict contextSwitch .
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
restrict f xs =
let f' = f . map (\(d,_,_) -> d)
in case sortBy (comparing $ f') xs of
[] -> []
ys -> let best = f' $ head ys in filter ((==best) . f') 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 :: [Decision] -> (forall t. Conc t a) -> [(Maybe a, Trace)]
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)]
-- | Variant of 'sctPreBoundOffset' for computations which do 'IO'.
sctPreBoundOffsetIO :: [Decision] -> (forall t. ConcIO t a) -> IO [(Maybe a, Trace)]
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

2
dejafu.cabal
View File

@ -53,7 +53,7 @@ library
, Test.DejaFu
, Test.DejaFu.Deterministic
, Test.DejaFu.Deterministic.IO
, Test.DejaFu.Deterministic.Schedulers
, Test.DejaFu.Deterministic.Schedule
, Test.DejaFu.SCT
, Test.DejaFu.Shrink

25
tests/Tests.hs
View File

@ -1,10 +1,29 @@
module Main (main) where
import Test.DejaFu (doTests')
import Tests.Cases
import Test.DejaFu
import System.Exit (exitFailure, exitSuccess)
import qualified Tests.Cases as C
import qualified Tests.Logger as L
andM :: (Functor m, Monad m) => [m Bool] -> m Bool
andM = fmap and . sequence
runTests :: IO Bool
runTests =
andM [dejafu C.simple2Deadlock ("Simple 2-Deadlock", deadlocksSometimes)
,dejafu (C.philosophers 2) ("2 Philosophers", deadlocksSometimes)
,dejafu (C.philosophers 3) ("3 Philosophers", deadlocksSometimes)
,dejafu (C.philosophers 4) ("4 Philosophers", deadlocksSometimes)
,dejafu C.thresholdValue ("Threshold Value", notAlwaysSame)
,dejafu C.forgottenUnlock ("Forgotten Unlock", deadlocksAlways)
,dejafu C.simple2Race ("Simple 2-Race", notAlwaysSame)
,dejafu C.raceyStack ("Racey Stack", notAlwaysSame)
,dejafus L.badLogger [("Logger (Valid)", L.validResult)
,("Logger (Good)", L.isGood)
,("Logger (Bad", L.isBad)]]
main :: IO ()
main = do
success <- doTests' id True testCases
success <- runTests
if success then exitSuccess else exitFailure

20
tests/Tests/Cases.hs
View File

@ -1,29 +1,9 @@
-- | Tests sourced from <https://github.com/sctbenchmarks>.
module Tests.Cases where
import Control.Applicative ((<$>))
import Control.Monad (replicateM)
import Control.Concurrent.CVar
import Control.Monad.Conc.Class
import Test.DejaFu
import qualified Tests.Logger as L
-- | List of all tests
testCases :: [(String, Result String)]
testCases =
[ ("Simple 2-Deadlock" , show <$> runTest deadlocksSometimes simple2Deadlock)
, ("2 Philosophers" , show <$> runTest deadlocksSometimes (philosophers 2))
, ("3 Philosophers" , show <$> runTest deadlocksSometimes (philosophers 3))
, ("4 Philosophers" , show <$> runTest deadlocksSometimes (philosophers 4))
, ("Threshold Value" , show <$> runTest (pNot alwaysSame) thresholdValue)
, ("Forgotten Unlock" , show <$> runTest deadlocksAlways forgottenUnlock)
, ("Simple 2-Race" , show <$> runTest (pNot alwaysSame) simple2Race)
, ("Racey Stack" , show <$> runTest (pNot alwaysSame) raceyStack)
, ("Logger (LA)" , show <$> L.testLA)
, ("Logger (LP)" , show <$> L.testLP)
, ("Logger (LE)" , show <$> L.testLE)
]
-- | Should deadlock on a minority of schedules.
simple2Deadlock :: MonadConc m => m Int

40
tests/Tests/Logger.hs
View File

@ -1,12 +1,8 @@
-- Modification (to introduce bug) of an example in Parallel and
-- Concurrent Programming in Haskell, chapter 7.
module Tests.Logger
( Logger
, initLogger
, logMessage
, logStop
, bad
, testLA, testLP, testLE
( badLogger
, validResult, isGood, isBad
) where
import Control.Concurrent.CVar
@ -48,8 +44,8 @@ logStop (Logger cmd log) = do
readCVar log
-- | Race condition! Can you see where?
bad :: MonadConc m => m [String]
bad = do
badLogger :: MonadConc m => m [String]
badLogger = do
l <- initLogger
logMessage l "Hello"
logMessage l "World"
@ -60,21 +56,21 @@ bad = do
-- | Test that the result is always in the set of allowed values, and
-- doesn't deadlock.
testLA :: Result [String]
testLA = runTest (alwaysTrue listContents) bad where
listContents (Just strs) = strs `elem` [ ["Hello", "World", "Foo", "Bar", "Baz"]
, ["Hello", "World", "Foo", "Bar"]
]
listContents Nothing = False
validResult :: Predicate [String]
validResult = alwaysTrue check where
check (Just strs) = strs `elem` [ ["Hello", "World", "Foo", "Bar", "Baz"]
, ["Hello", "World", "Foo", "Bar"]
]
check Nothing = False
-- | Test that the "proper" result occurs at least once.
testLP :: Result [String]
testLP = runTest (somewhereTrue loggedAll) bad where
loggedAll (Just a) = length a == 5
loggedAll Nothing = False
isGood :: Predicate [String]
isGood = somewhereTrue check where
check (Just a) = length a == 5
check Nothing = False
-- | Test that the erroneous result occurs at least once.
testLE :: Result [String]
testLE = runTest (somewhereTrue loggedAlmostAll) bad where
loggedAlmostAll (Just a) = length a == 4
loggedAlmostAll Nothing = False
isBad :: Predicate [String]
isBad = somewhereTrue check where
check (Just a) = length a == 4
check Nothing = False