mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-24 05:55:18 +03:00
Provide utilities for writing SCT test cases
This commit is contained in:
parent
232c1a852f
commit
886da7195e
103
Control/Monad/Conc/SCT/Tests.hs
Normal file
103
Control/Monad/Conc/SCT/Tests.hs
Normal file
@ -0,0 +1,103 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
-- | Useful functions for writing SCT test cases for @Conc@
|
||||
-- computations.
|
||||
module Control.Monad.Conc.SCT.Tests
|
||||
( -- * Test cases
|
||||
Result(..)
|
||||
, runTest
|
||||
, runTestIO
|
||||
-- * Predicates
|
||||
, Predicate
|
||||
, deadlocksNever
|
||||
, deadlocksAlways
|
||||
, alwaysSame
|
||||
-- * Utilities
|
||||
, pAnd
|
||||
, pNot
|
||||
, toPredicate
|
||||
, takeWhile'
|
||||
) where
|
||||
|
||||
import Control.Applicative ((<$>))
|
||||
import Control.Monad.Conc.Fixed
|
||||
import Control.Monad.Conc.SCT.PreBound
|
||||
import Data.Maybe (isJust, isNothing)
|
||||
|
||||
import qualified Control.Monad.Conc.Fixed.IO as CIO
|
||||
|
||||
-- * 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!.
|
||||
data Result = Result
|
||||
{ _pass :: Bool
|
||||
-- ^ Whether the test passed or not.
|
||||
, _casesChecked :: Int
|
||||
-- ^ The number of cases checked.
|
||||
, _casesTotal :: Int
|
||||
-- ^ The total number of cases.
|
||||
}
|
||||
|
||||
-- | Run a test using the pre-emption bounding scheduler, with a bound
|
||||
-- of 2.
|
||||
runTest :: Predicate a -> (forall t. Conc t a) -> Result
|
||||
runTest predicate conc = predicate . map fst $ sctPreBound 2 conc
|
||||
|
||||
-- | Variant of 'runTest' using 'IO'. See usual caveats about 'IO'.
|
||||
runTestIO :: Predicate a -> (forall t. CIO.Conc t a) -> IO Result
|
||||
runTestIO predicate conc = predicate . map fst <$> sctPreBoundIO 2 conc
|
||||
|
||||
-- * Predicates
|
||||
|
||||
-- | A @Predicate@ is a function which collapses a list of results
|
||||
-- into a 'Result'.
|
||||
type Predicate a = [Maybe a] -> Result
|
||||
|
||||
-- | Check that a computation never deadlocks.
|
||||
deadlocksNever :: Predicate a
|
||||
deadlocksNever = toPredicate isJust
|
||||
|
||||
-- | Check that a computation always deadlocks.
|
||||
deadlocksAlways :: Predicate a
|
||||
deadlocksAlways = toPredicate isNothing
|
||||
|
||||
-- | Check that the result of a computation is always the same. In
|
||||
-- particular this means either: (a) it always deadlocks, or (b) the
|
||||
-- result is always 'Just' @x@, for some fixed @x@.
|
||||
alwaysSame :: Eq a => Predicate a
|
||||
alwaysSame [] = Result { _pass = True, _casesChecked = 0, _casesTotal = 0 }
|
||||
alwaysSame (x:xs) = go xs Result { _pass = True, _casesChecked = 1, _casesTotal = length xs } where
|
||||
go [] s = s
|
||||
go (y:ys) res
|
||||
| y == x = go ys $ res { _casesChecked = _casesChecked res + 1 }
|
||||
| otherwise = res { _pass = False, _casesChecked = _casesChecked res + 1 }
|
||||
|
||||
-- * Utils
|
||||
|
||||
-- | 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
|
||||
|
||||
-- | Invert the result of a predicate.
|
||||
pNot :: Predicate a -> Predicate a
|
||||
pNot p xs = r { _pass = not $ _pass r } where
|
||||
r = p xs
|
||||
|
||||
-- | Convert a boolean function to a 'Result'-producing predicate.
|
||||
toPredicate :: (Maybe a -> Bool) -> [Maybe a] -> Result
|
||||
toPredicate f xs = Result { _pass = pass, _casesChecked = cases, _casesTotal = length xs } where
|
||||
(_, pass, cases) = takeWhile' f xs
|
||||
|
||||
-- | Variant of 'takeWhile' that also includes a count of results
|
||||
-- returned and whether it traversed the entire list.
|
||||
takeWhile' :: (a -> Bool) -> [a] -> ([a], Bool, Int)
|
||||
takeWhile' f = go [] 0 where
|
||||
go ts n [] = (reverse ts, True, n)
|
||||
go ts n (x:xs)
|
||||
| f x = go (x:ts) (n + 1) xs
|
||||
| otherwise = (reverse ts, False, n)
|
@ -51,6 +51,7 @@ library
|
||||
, Control.Monad.Conc.Fixed.IO
|
||||
, Control.Monad.Conc.Fixed.Schedulers
|
||||
, Control.Monad.Conc.SCT
|
||||
, Control.Monad.Conc.SCT.Tests
|
||||
other-modules: Control.Monad.Conc.Fixed.Internal
|
||||
, Control.Monad.Conc.SCT.Internal
|
||||
, Control.Monad.Conc.SCT.PreBound
|
||||
|
@ -1,8 +1,8 @@
|
||||
module Main (main) where
|
||||
|
||||
import Control.Monad (when)
|
||||
import Control.Monad.Conc.SCT.Tests (Result(..))
|
||||
import Tests.Cases
|
||||
import Tests.Utils
|
||||
import System.Exit (exitFailure, exitSuccess)
|
||||
|
||||
main :: IO ()
|
||||
@ -11,8 +11,8 @@ main = do
|
||||
if and results then exitSuccess else exitFailure
|
||||
|
||||
runTest :: Bool -> Test -> IO Bool
|
||||
runTest verbose (Test {name = name, result = result}) =
|
||||
case result of
|
||||
Pass -> when verbose (putStrLn $ "\27[32m[pass]\27[0m " ++ name) >> return True
|
||||
Fail str -> putStrLn ("\27[31m[fail]\27[0m " ++ name ++ ": " ++ str) >> return False
|
||||
Error str -> putStrLn ("\27[35m[error]\27[0m " ++ name ++ ": " ++ str) >> return False
|
||||
runTest verbose (Test {name = name, result = result}) = do
|
||||
if _pass result
|
||||
then when verbose (putStrLn $ "\27[32m[pass]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")")
|
||||
else putStrLn ("\27[31m[fail]\27[0m " ++ name ++ " (checked: " ++ show (_casesChecked result) ++ ")")
|
||||
return $ _pass result
|
||||
|
@ -4,21 +4,23 @@ module Tests.Cases where
|
||||
import Control.Monad (replicateM)
|
||||
import Control.Monad.Conc.Class
|
||||
import Control.Monad.Conc.CVar
|
||||
import Tests.Utils
|
||||
import Control.Monad.Conc.SCT.Tests
|
||||
|
||||
data Test = Test { name :: String, result :: Result }
|
||||
|
||||
-- | List of all tests
|
||||
testCases :: [Test]
|
||||
testCases =
|
||||
[ Test "Simple 2-Deadlock" $ testNot "No deadlocks found!" $ testDeadlockFree 1 simple2Deadlock
|
||||
, Test "2 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 2
|
||||
, Test "3 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 3
|
||||
, Test "4 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 4
|
||||
, Test "25 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 25
|
||||
, Test "100 Philosophers" $ testNot "No deadlocks found!" $ testDeadlockFree 2 $ philosophers 100
|
||||
, Test "Threshold Value" $ testNot "All values equal!" $ testAlwaysSame 1 thresholdValue
|
||||
, Test "Forgotten Unlock" $ testDeadlocks 1 forgottenUnlock
|
||||
, Test "Simple 2-Race" $ testNot "All values equal!" $ testAlwaysSame 1 simple2Race
|
||||
, Test "Racey Stack" $ testNot "All values equal!" $ testAlwaysSame 1 raceyStack
|
||||
[ Test "Simple 2-Deadlock" $ runTest (pNot deadlocksNever) simple2Deadlock
|
||||
, Test "2 Philosophers" $ runTest (pNot deadlocksNever) $ philosophers 2
|
||||
, Test "3 Philosophers" $ runTest (pNot deadlocksNever) $ philosophers 3
|
||||
, Test "4 Philosophers" $ runTest (pNot deadlocksNever) $ philosophers 4
|
||||
, Test "25 Philosophers" $ runTest (pNot deadlocksNever) $ philosophers 25
|
||||
, Test "100 Philosophers" $ runTest (pNot deadlocksNever) $ philosophers 100
|
||||
, Test "Threshold Value" $ runTest (pNot alwaysSame) thresholdValue
|
||||
, Test "Forgotten Unlock" $ runTest deadlocksAlways forgottenUnlock
|
||||
, Test "Simple 2-Race" $ runTest (pNot alwaysSame) simple2Race
|
||||
, Test "Racey Stack" $ runTest (pNot alwaysSame) raceyStack
|
||||
]
|
||||
|
||||
-- | Should deadlock on a minority of schedules.
|
||||
|
@ -1,45 +0,0 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
module Tests.Utils where
|
||||
|
||||
import Control.Monad.Conc.Fixed (Conc)
|
||||
import Control.Monad.Conc.SCT (sctPreBound)
|
||||
import Data.List (group, sort)
|
||||
import Data.Maybe (isJust, isNothing)
|
||||
|
||||
-- Couldn't get Cabal's detailed tests to work, hence this approach.
|
||||
data Test = Test { name :: String, result :: Result }
|
||||
data Result = Pass | Fail String | Error String
|
||||
|
||||
-- | Test that a predicate holds over the results of a concurrent
|
||||
-- computation.
|
||||
testPred :: ([Maybe a] -> Result) -> Int -> (forall t. Conc t a) -> Result
|
||||
testPred predicate num conc = predicate . map fst $ sctPreBound num conc
|
||||
|
||||
-- | Test that a concurrent computation is free of deadlocks.
|
||||
testDeadlockFree :: Int -> (forall t. Conc t a) -> Result
|
||||
testDeadlockFree = testPred predicate where
|
||||
predicate xs = case filter isNothing xs of
|
||||
[] -> Pass
|
||||
ds -> Fail $ "Found " ++ show (length ds) ++ "/" ++ show (length xs) ++ " deadlocking schedules."
|
||||
|
||||
-- | Test that a concurrent computation always deadlocks.
|
||||
testDeadlocks :: Int -> (forall t. Conc t a) -> Result
|
||||
testDeadlocks = testPred predicate where
|
||||
predicate xs = case filter isJust xs of
|
||||
[] -> Pass
|
||||
ds -> Fail $ "Found " ++ show (length ds) ++ "/" ++ show (length xs) ++ " productive schedules."
|
||||
|
||||
-- | Test that a concurrent computation always returns the same
|
||||
-- result.
|
||||
testAlwaysSame :: (Eq a, Ord a) => Int -> (forall t. Conc t a) -> Result
|
||||
testAlwaysSame = testPred predicate where
|
||||
predicate xs = case group $ sort xs of
|
||||
[] -> Pass
|
||||
[[_]] -> Pass
|
||||
gs -> Fail $ "Found " ++ show (length gs) ++ " distinct results."
|
||||
|
||||
-- | Invert the result of a test.
|
||||
testNot :: String -> Result -> Result
|
||||
testNot err Pass = Fail err
|
||||
testNot _ (Fail _) = Pass
|
||||
testNot _ err = err
|
Loading…
Reference in New Issue
Block a user