mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-11-28 10:49:11 +03:00
Merge branch 'test-concurrently'
This commit is contained in:
Michael Walker
commit
a1ef5a8813
@ -1,34 +1,100 @@
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeSynonymInstances #-}
|
||||
|
||||
-- | This module allows using Deja Fu predicates with HUnit to test
|
||||
-- the behaviour of concurrent systems.
|
||||
module Test.HUnit.DejaFu
|
||||
( -- * Testing
|
||||
( -- * Unit testing
|
||||
|
||||
-- | This is supported by the 'Assertable' and 'Testable'
|
||||
-- instances for 'ConcST' and 'ConcIO'. These instances try all
|
||||
-- executions, reporting as failures the cases which throw an
|
||||
-- 'HUnitFailure' exception.
|
||||
--
|
||||
-- @instance Testable (ConcST t ())@
|
||||
-- @instance Assertable (ConcST t ())@
|
||||
-- @instance Testable (ConcIO ())@
|
||||
-- @instance Assertable (ConcIO ())@
|
||||
--
|
||||
-- These instances use the default memory model and schedule bounds.
|
||||
|
||||
-- * Property testing
|
||||
testAuto
|
||||
, testDejafu
|
||||
, testDejafus
|
||||
|
||||
, testAuto'
|
||||
, testDejafu'
|
||||
, testDejafus'
|
||||
|
||||
-- ** @IO@
|
||||
, testAutoIO
|
||||
, testDejafuIO
|
||||
, testDejafusIO
|
||||
|
||||
-- * Testing under Alternative Memory Models
|
||||
, MemType(..)
|
||||
, testAuto'
|
||||
, testAutoIO'
|
||||
, testDejafu'
|
||||
, testDejafus'
|
||||
, testDejafuIO'
|
||||
, testDejafusIO'
|
||||
|
||||
-- * Re-exports
|
||||
, Bounds(..)
|
||||
, MemType(..)
|
||||
) where
|
||||
|
||||
import Control.Monad.Catch (try)
|
||||
import Data.List (intercalate, intersperse)
|
||||
import Test.DejaFu
|
||||
import Test.DejaFu.Deterministic (ConcST, ConcIO, showFail, showTrace)
|
||||
import Test.DejaFu.Deterministic (ConcST, ConcIO, Trace, ThreadId, ThreadAction, Lookahead, showFail, showTrace)
|
||||
import Test.DejaFu.SCT (sctBound, sctBoundIO)
|
||||
import Test.HUnit (Test(..), assertString)
|
||||
import Test.HUnit (Assertable(..), Test(..), Testable(..), assertString)
|
||||
import Test.HUnit.Lang (HUnitFailure(..))
|
||||
|
||||
-- Can't put the necessary forall in the @Assertable ConcST t@
|
||||
-- instance :(
|
||||
import Unsafe.Coerce (unsafeCoerce)
|
||||
|
||||
#if MIN_VERSION_dejafu(0,3,0)
|
||||
type Trc = Trace ThreadId ThreadAction Lookahead
|
||||
#else
|
||||
type Trc = Trace
|
||||
#endif
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Automated testing
|
||||
-- Unit testing
|
||||
|
||||
instance Testable (ConcST t ()) where
|
||||
test conc = TestCase (assert conc)
|
||||
|
||||
instance Testable (ConcIO ()) where
|
||||
test conc = TestCase (assert conc)
|
||||
|
||||
instance Assertable (ConcST t ()) where
|
||||
assert conc = do
|
||||
let traces = sctBound' conc'
|
||||
assertString . showErr $ assertableP traces
|
||||
|
||||
where
|
||||
conc' :: ConcST t (Either HUnitFailure ())
|
||||
conc' = try conc
|
||||
|
||||
sctBound' :: ConcST t (Either HUnitFailure ()) -> [(Either Failure (Either HUnitFailure ()), Trc)]
|
||||
sctBound' = unsafeCoerce $ sctBound defaultMemType defaultBounds
|
||||
|
||||
instance Assertable (ConcIO ()) where
|
||||
assert conc = do
|
||||
traces <- sctBoundIO defaultMemType defaultBounds (try conc)
|
||||
assertString . showErr $ assertableP traces
|
||||
|
||||
assertableP :: Predicate (Either HUnitFailure ())
|
||||
assertableP = alwaysTrue $ \r -> case r of
|
||||
Right (Left (HUnitFailure _ _)) -> False
|
||||
_ -> True
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Property testing
|
||||
|
||||
-- | Automatically test a computation. In particular, look for
|
||||
-- deadlocks, uncaught exceptions, and multiple return values.
|
||||
@ -68,9 +134,6 @@ autocheckCases =
|
||||
, ("Consistent Result", alwaysSame)
|
||||
]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Manual testing
|
||||
|
||||
-- | Check that a predicate holds.
|
||||
testDejafu :: Show a
|
||||
=> (forall t. ConcST t a)
|
||||
@ -83,7 +146,7 @@ testDejafu :: Show a
|
||||
testDejafu = testDejafu' defaultMemType defaultBounds
|
||||
|
||||
-- | Variant of 'testDejafu' which takes a memory model and
|
||||
-- pre-emption bound.
|
||||
-- schedule bounds.
|
||||
testDejafu' :: Show a
|
||||
=> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
@ -109,8 +172,8 @@ testDejafus :: Show a
|
||||
-> Test
|
||||
testDejafus = testDejafus' defaultMemType defaultBounds
|
||||
|
||||
-- | Variant of 'testDejafus' which takes a memory model and pre-emption
|
||||
-- bound.
|
||||
-- | Variant of 'testDejafus' which takes a memory model and schedule
|
||||
-- bounds.
|
||||
testDejafus' :: Show a
|
||||
=> MemType
|
||||
-- ^ The memory model to use for non-synchronised @CRef@ operations.
|
||||
@ -121,7 +184,7 @@ testDejafus' :: Show a
|
||||
-> [(String, Predicate a)]
|
||||
-- ^ The list of predicates (with names) to check
|
||||
-> Test
|
||||
testDejafus' = test
|
||||
testDejafus' = testst
|
||||
|
||||
-- | Variant of 'testDejafu' for computations which do 'IO'.
|
||||
testDejafuIO :: Show a => ConcIO a -> String -> Predicate a -> Test
|
||||
@ -143,8 +206,8 @@ testDejafusIO' = testio
|
||||
-- HUnit integration
|
||||
|
||||
-- | Produce a HUnit 'Test' from a Deja Fu test.
|
||||
test :: Show a => MemType -> Bounds -> (forall t. ConcST t a) -> [(String, Predicate a)] -> Test
|
||||
test memtype cb conc tests = case map toTest tests of
|
||||
testst :: Show a => MemType -> Bounds -> (forall t. ConcST t a) -> [(String, Predicate a)] -> Test
|
||||
testst memtype cb conc tests = case map toTest tests of
|
||||
[t] -> t
|
||||
ts -> TestList ts
|
||||
|
||||
@ -169,6 +232,9 @@ testio memtype cb concio tests = case map toTest tests of
|
||||
traces <- sctBoundIO memtype cb concio
|
||||
assertString . showErr $ p traces
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Utilities
|
||||
|
||||
-- | Convert a test result into an error message on failure (empty
|
||||
-- string on success).
|
||||
showErr :: Show a => Result a -> String
|
||||
@ -178,7 +244,9 @@ showErr res
|
||||
|
||||
msg = if null (_failureMsg res) then "" else _failureMsg res ++ "\n"
|
||||
|
||||
failures = intersperse "" . map (\(r, t) -> indent $ either showFail show r ++ " " ++ showTrace t) . take 5 $ _failures res
|
||||
failures = intersperse "" . map (indent . showres) . take 5 $ _failures res
|
||||
|
||||
showres (r, t) = either showFail show r ++ " " ++ showTrace t
|
||||
|
||||
rest = if moreThan (_failures res) 5 then "\n\t..." else ""
|
||||
|
||||
|
||||
@ -40,6 +40,7 @@ library
|
||||
-- other-modules:
|
||||
-- other-extensions:
|
||||
build-depends: base >=4.5 && <5
|
||||
, exceptions
|
||||
, dejafu >= 0.2
|
||||
, HUnit
|
||||
-- hs-source-dirs:
|
||||
|
||||
@ -1,39 +1,120 @@
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE DeriveDataTypeable #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE TypeSynonymInstances #-}
|
||||
|
||||
-- | This module allows using Deja Fu predicates with Tasty to test
|
||||
-- the behaviour of concurrent systems.
|
||||
module Test.Tasty.DejaFu
|
||||
( -- * Testing
|
||||
( -- * Unit testing
|
||||
|
||||
-- | This is supported by the 'IsTest' instances for 'ConcST' and
|
||||
-- 'ConcIO'. These instances try all executions, reporting as
|
||||
-- failures the cases which return a 'Just' string.
|
||||
--
|
||||
-- @instance Typeable t => IsTest (ConcST t (Maybe String))@
|
||||
-- @instance IsTest (ConcIO (Maybe String))@
|
||||
-- @instance IsOption Bounds@
|
||||
-- @instance IsOption MemType@
|
||||
|
||||
-- * Property testing
|
||||
testAuto
|
||||
, testDejafu
|
||||
, testDejafus
|
||||
|
||||
, testAuto'
|
||||
, testDejafu'
|
||||
, testDejafus'
|
||||
|
||||
-- ** @IO@
|
||||
, testAutoIO
|
||||
, testDejafuIO
|
||||
, testDejafusIO
|
||||
|
||||
-- * Testing under Alternative Memory Models
|
||||
, MemType(..)
|
||||
, testAuto'
|
||||
, testAutoIO'
|
||||
, testDejafu'
|
||||
, testDejafus'
|
||||
, testDejafuIO'
|
||||
, testDejafusIO'
|
||||
|
||||
-- * Re-exports
|
||||
, Bounds(..)
|
||||
, MemType(..)
|
||||
) where
|
||||
|
||||
import Data.Char (toUpper)
|
||||
import Data.List (intercalate, intersperse)
|
||||
import Data.Proxy (Proxy(..))
|
||||
import Data.Tagged (Tagged(..))
|
||||
import Data.Typeable (Typeable)
|
||||
import Test.DejaFu
|
||||
import Test.DejaFu.Deterministic (ConcST, ConcIO, Trace, ThreadId, ThreadAction, Lookahead, showFail, showTrace)
|
||||
import Test.DejaFu.SCT (sctBound, sctBoundIO)
|
||||
import Test.Tasty (TestName, TestTree, testGroup)
|
||||
import Test.Tasty.Options (OptionDescription(..), IsOption(..), lookupOption)
|
||||
import Test.Tasty.Providers (IsTest(..), singleTest, testPassed, testFailed)
|
||||
|
||||
-- Can't put the necessary forall in the @IsTest ConcST t@
|
||||
-- instance :(
|
||||
import Unsafe.Coerce (unsafeCoerce)
|
||||
|
||||
#if MIN_VERSION_dejafu(0,3,0)
|
||||
type Trc = Trace ThreadId ThreadAction Lookahead
|
||||
#else
|
||||
type Trc = Trace
|
||||
#endif
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Automated testing
|
||||
-- Unit testing
|
||||
|
||||
instance Typeable t => IsTest (ConcST t (Maybe String)) where
|
||||
testOptions = Tagged concOptions
|
||||
|
||||
run options conc callback = do
|
||||
let memtype = lookupOption options :: MemType
|
||||
let bounds = lookupOption options :: Bounds
|
||||
let sctBound' :: ConcST t (Maybe String) -> [(Either Failure (Maybe String), Trc)]
|
||||
sctBound' = unsafeCoerce $ sctBound memtype bounds
|
||||
let traces = sctBound' conc
|
||||
run options (ConcTest traces assertableP) callback
|
||||
|
||||
instance IsTest (ConcIO (Maybe String)) where
|
||||
testOptions = Tagged concOptions
|
||||
|
||||
run options conc callback = do
|
||||
let memtype = lookupOption options
|
||||
let bounds = lookupOption options
|
||||
let traces = sctBoundIO memtype bounds conc
|
||||
run options (ConcIOTest traces assertableP) callback
|
||||
|
||||
concOptions :: [OptionDescription]
|
||||
concOptions =
|
||||
[ Option (Proxy :: Proxy Bounds)
|
||||
, Option (Proxy :: Proxy MemType)
|
||||
]
|
||||
|
||||
assertableP :: Predicate (Maybe String)
|
||||
assertableP = alwaysTrue $ \r -> case r of
|
||||
Right (Just _) -> False
|
||||
_ -> True
|
||||
|
||||
instance IsOption Bounds where
|
||||
defaultValue = defaultBounds
|
||||
parseValue = const Nothing
|
||||
optionName = Tagged "schedule-bounds"
|
||||
optionHelp = Tagged "The schedule bounds to use. This cannot be set on the command line."
|
||||
|
||||
instance IsOption MemType where
|
||||
defaultValue = defaultMemType
|
||||
parseValue str = shortName (map toUpper str) where
|
||||
shortName "SC" = Just SequentialConsistency
|
||||
shortName "TSO" = Just TotalStoreOrder
|
||||
shortName "PSO" = Just PartialStoreOrder
|
||||
shortName _ = Nothing
|
||||
optionName = Tagged "memory-model"
|
||||
optionHelp = Tagged "The memory model to use. This should be one of \"SC\", \"TSO\", or \"PSO\"."
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Property testing
|
||||
|
||||
-- | Automatically test a computation. In particular, look for
|
||||
-- deadlocks, uncaught exceptions, and multiple return values.
|
||||
@ -73,9 +154,6 @@ autocheckCases =
|
||||
, ("Consistent Result", alwaysSame)
|
||||
]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Manual testing
|
||||
|
||||
-- | Check that a predicate holds.
|
||||
testDejafu :: Show a
|
||||
=> (forall t. ConcST t a)
|
||||
@ -126,7 +204,7 @@ testDejafus' :: Show a
|
||||
-> [(TestName, Predicate a)]
|
||||
-- ^ The list of predicates (with names) to check
|
||||
-> TestTree
|
||||
testDejafus' = test
|
||||
testDejafus' = testst
|
||||
|
||||
-- | Variant of 'testDejafu' for computations which do 'IO'.
|
||||
testDejafuIO :: Show a => ConcIO a -> TestName -> Predicate a -> TestTree
|
||||
@ -147,12 +225,6 @@ testDejafusIO' = testio
|
||||
--------------------------------------------------------------------------------
|
||||
-- Tasty integration
|
||||
|
||||
#if MIN_VERSION_dejafu(0,3,0)
|
||||
type Trc = Trace ThreadId ThreadAction Lookahead
|
||||
#else
|
||||
type Trc = Trace
|
||||
#endif
|
||||
|
||||
data ConcTest where
|
||||
ConcTest :: Show a => [(Either Failure a, Trc)] -> Predicate a -> ConcTest
|
||||
deriving Typeable
|
||||
@ -177,8 +249,8 @@ instance IsTest ConcIOTest where
|
||||
return $ if null err then testPassed "" else testFailed err
|
||||
|
||||
-- | Produce a Tasty 'TestTree' from a Deja Fu test.
|
||||
test :: Show a => MemType -> Bounds -> (forall t. ConcST t a) -> [(TestName, Predicate a)] -> TestTree
|
||||
test memtype cb conc tests = case map toTest tests of
|
||||
testst :: Show a => MemType -> Bounds -> (forall t. ConcST t a) -> [(TestName, Predicate a)] -> TestTree
|
||||
testst memtype cb conc tests = case map toTest tests of
|
||||
[t] -> t
|
||||
ts -> testGroup "Deja Fu Tests" ts
|
||||
|
||||
|
||||
@ -41,6 +41,7 @@ library
|
||||
-- other-extensions:
|
||||
build-depends: base >=4.5 && <5
|
||||
, dejafu >= 0.2
|
||||
, tagged
|
||||
, tasty
|
||||
-- hs-source-dirs:
|
||||
default-language: Haskell2010
|
||||
Loading…
Reference in New Issue
Block a user