mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-11-26 09:20:36 +03:00
Rearrange test hierarchy
This commit is contained in:
parent
92cc44b548
commit
7b527a8793
@ -17,15 +17,17 @@ build-type: Simple
|
||||
cabal-version: >=1.10
|
||||
|
||||
library
|
||||
exposed-modules: Cases
|
||||
, Cases.Async
|
||||
, Cases.SingleThreaded
|
||||
, Cases.MultiThreaded
|
||||
, Cases.Refinement
|
||||
, Cases.Litmus
|
||||
, Cases.Discard
|
||||
, Cases.Regressions
|
||||
, Cases.Properties
|
||||
exposed-modules: Unit
|
||||
, Unit.Properties
|
||||
|
||||
, Integration
|
||||
, Integration.Async
|
||||
, Integration.SingleThreaded
|
||||
, Integration.MultiThreaded
|
||||
, Integration.Refinement
|
||||
, Integration.Litmus
|
||||
, Integration.Discard
|
||||
, Integration.Regressions
|
||||
|
||||
, Examples
|
||||
, Examples.AutoUpdate
|
||||
|
@ -3,16 +3,18 @@ module Main where
|
||||
import qualified Test.Tasty as T
|
||||
import qualified Test.Tasty.QuickCheck as T
|
||||
|
||||
import Cases
|
||||
import Examples
|
||||
import qualified Unit as U
|
||||
import qualified Integration as I
|
||||
import qualified Examples as E
|
||||
|
||||
main :: IO ()
|
||||
main = T.defaultMain $ T.adjustOption reduceQCTests allTests
|
||||
main = T.defaultMain $ T.adjustOption reduceQCTests tests
|
||||
|
||||
allTests :: T.TestTree
|
||||
allTests = T.testGroup "Tests"
|
||||
[ T.testGroup "Cases" testCases
|
||||
, T.testGroup "Examples" testExamples
|
||||
tests :: T.TestTree
|
||||
tests = T.testGroup "Tests"
|
||||
[ T.testGroup "Unit" U.tests
|
||||
, T.testGroup "Integration" I.tests
|
||||
, T.testGroup "Examples" E.tests
|
||||
]
|
||||
|
||||
-- | Reduce the default number of quickcheck runs.
|
||||
|
@ -1,25 +0,0 @@
|
||||
module Cases where
|
||||
|
||||
import qualified Cases.SingleThreaded as S
|
||||
import qualified Cases.MultiThreaded as M
|
||||
import qualified Cases.Refinement as R
|
||||
import qualified Cases.Regressions as G
|
||||
import qualified Cases.Litmus as L
|
||||
import qualified Cases.Async as A
|
||||
import qualified Cases.Discard as D
|
||||
import qualified Cases.Properties as P
|
||||
|
||||
import Common
|
||||
|
||||
-- | Run all the test cases.
|
||||
testCases :: [TestTree]
|
||||
testCases =
|
||||
[ testGroup "Single Threaded" S.tests
|
||||
, testGroup "Multi Threaded" M.tests
|
||||
, testGroup "Refinement" R.tests
|
||||
, testGroup "Litmus" L.tests
|
||||
, testGroup "Async" A.tests
|
||||
, testGroup "Discard" D.tests
|
||||
, testGroup "Properties" P.tests
|
||||
, testGroup "Regressions" G.tests
|
||||
]
|
@ -10,12 +10,12 @@ import qualified Examples.ParMonad as PM
|
||||
import Common
|
||||
|
||||
-- | Run all the example tests.
|
||||
testExamples :: [TestTree]
|
||||
testExamples =
|
||||
[ testGroup "auto-update" A.tests
|
||||
, testGroup "Class Laws" C.tests
|
||||
, testGroup "Dining Philosophers" P.tests
|
||||
, testGroup "Message Logger" L.tests
|
||||
, testGroup "Search Party" S.tests
|
||||
, testGroup "Par Monad (Direct Scheduler)" PM.tests
|
||||
tests :: [TestTree]
|
||||
tests =
|
||||
[ testGroup "AutoUpdate" A.tests
|
||||
, testGroup "ClassLaws" C.tests
|
||||
, testGroup "Logger" L.tests
|
||||
, testGroup "ParMonad" PM.tests
|
||||
, testGroup "Philosophers" P.tests
|
||||
, testGroup "SearchParty" S.tests
|
||||
]
|
||||
|
23
dejafu-tests/lib/Integration.hs
Executable file
23
dejafu-tests/lib/Integration.hs
Executable file
@ -0,0 +1,23 @@
|
||||
module Integration where
|
||||
|
||||
import qualified Integration.SingleThreaded as S
|
||||
import qualified Integration.MultiThreaded as M
|
||||
import qualified Integration.Refinement as R
|
||||
import qualified Integration.Regressions as G
|
||||
import qualified Integration.Litmus as L
|
||||
import qualified Integration.Async as A
|
||||
import qualified Integration.Discard as D
|
||||
|
||||
import Common
|
||||
|
||||
-- | Run all the integration tests.
|
||||
tests :: [TestTree]
|
||||
tests =
|
||||
[ testGroup "Async" A.tests
|
||||
, testGroup "Discard" D.tests
|
||||
, testGroup "Litmus" L.tests
|
||||
, testGroup "MultiThreaded" M.tests
|
||||
, testGroup "Refinement" R.tests
|
||||
, testGroup "Regressions" G.tests
|
||||
, testGroup "SingleThreaded" S.tests
|
||||
]
|
@ -1,7 +1,7 @@
|
||||
{-# LANGUAGE DeriveDataTypeable #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
|
||||
module Cases.Async where
|
||||
module Integration.Async where
|
||||
|
||||
import Control.Concurrent.Classy.Async
|
||||
import Control.Concurrent.Classy.CRef
|
@ -1,4 +1,4 @@
|
||||
module Cases.Discard where
|
||||
module Integration.Discard where
|
||||
|
||||
import Control.Concurrent.Classy
|
||||
import Test.DejaFu (gives')
|
@ -1,6 +1,6 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
module Cases.Litmus where
|
||||
module Integration.Litmus where
|
||||
|
||||
import Control.Monad (replicateM)
|
||||
import Control.Monad.ST (runST)
|
@ -1,4 +1,4 @@
|
||||
module Cases.MultiThreaded where
|
||||
module Integration.MultiThreaded where
|
||||
|
||||
import Control.Exception (ArithException(..))
|
||||
import Control.Monad.IO.Class (liftIO)
|
@ -1,4 +1,4 @@
|
||||
module Cases.Refinement where
|
||||
module Integration.Refinement where
|
||||
|
||||
import Control.Concurrent.Classy.MVar
|
||||
import Control.Monad (void)
|
@ -1,6 +1,6 @@
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
|
||||
module Cases.Regressions where
|
||||
module Integration.Regressions where
|
||||
|
||||
import Test.DejaFu (exceptionsAlways, gives')
|
||||
|
@ -1,6 +1,6 @@
|
||||
{-# LANGUAGE CPP #-}
|
||||
|
||||
module Cases.SingleThreaded where
|
||||
module Integration.SingleThreaded where
|
||||
|
||||
import Control.Exception (ArithException(..), ArrayException(..))
|
||||
import Test.DejaFu (Failure(..), gives, gives', isUncaughtException)
|
11
dejafu-tests/lib/Unit.hs
Normal file
11
dejafu-tests/lib/Unit.hs
Normal file
@ -0,0 +1,11 @@
|
||||
module Unit where
|
||||
|
||||
import qualified Unit.Properties as P
|
||||
|
||||
import Common
|
||||
|
||||
-- | Run all the unit tests.
|
||||
tests :: [TestTree]
|
||||
tests =
|
||||
[ testGroup "Properties" P.tests
|
||||
]
|
@ -1,6 +1,6 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
module Cases.Properties where
|
||||
module Unit.Properties where
|
||||
|
||||
import Control.Monad (zipWithM, liftM2)
|
||||
import qualified Control.Monad.ST as ST
|
||||
@ -27,24 +27,50 @@ import Common
|
||||
|
||||
tests :: [TestTree]
|
||||
tests =
|
||||
[ testGroup "Class Laws"
|
||||
[ testGroup "ClassLaw" classLawProps
|
||||
, testGroup "Common" commonProps
|
||||
, testGroup "Memory" memoryProps
|
||||
, testGroup "SCT" sctProps
|
||||
]
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
classLawProps :: [TestTree]
|
||||
classLawProps = toTestList
|
||||
[ testGroup "Id" (eqord (Proxy :: Proxy D.Id))
|
||||
, testGroup "Failure" (eqord (Proxy :: Proxy D.Failure))
|
||||
]
|
||||
where
|
||||
eqord :: forall a. (Eq a, Ord a, Listable a, Show a) => Proxy a -> [TestTree]
|
||||
eqord _ =
|
||||
[ testProperty "Reflexivity (==)" $ \(x :: a) -> x == x
|
||||
, testProperty "Symmetry (==)" $ \(x :: a) y -> (x == y) == (y == x)
|
||||
, testProperty "Transitivity (==)" $ \(x :: a) y z -> x == y && y == z ==> x == z
|
||||
, testProperty "Reflexivity (<=)" $ \(x :: a) -> x <= x
|
||||
, testProperty "Antisymmetry (<=)" $ \(x :: a) y -> x <= y && y <= x ==> x == y
|
||||
, testProperty "Transitivity (<=)" $ \(x :: a) y z -> x <= y && y <= z ==> x <= z
|
||||
, testProperty "Eq / Ord Consistency" $ \(x :: a) y -> x == y ==> x <= y
|
||||
]
|
||||
|
||||
, testGroup "Common"
|
||||
[ testProperty "simplifyAction a == simplifyLookahead (rewind a)" $
|
||||
\act -> canRewind act ==>
|
||||
D.simplifyAction act == D.simplifyLookahead (rewind' act)
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
, testProperty "isBarrier a ==> synchronises a r" $
|
||||
\a r -> D.isBarrier a ==> D.synchronises a r
|
||||
commonProps :: [TestTree]
|
||||
commonProps = toTestList
|
||||
[ testProperty "simplifyAction a == simplifyLookahead (rewind a)" $
|
||||
\act -> canRewind act ==>
|
||||
D.simplifyAction act == D.simplifyLookahead (rewind' act)
|
||||
|
||||
, testProperty "isCommit a r ==> synchronises a r" $
|
||||
\a r -> D.isCommit a r ==> D.synchronises a r
|
||||
]
|
||||
, testProperty "isBarrier a ==> synchronises a r" $
|
||||
\a r -> D.isBarrier a ==> D.synchronises a r
|
||||
|
||||
, testGroup "Memory"
|
||||
, testProperty "isCommit a r ==> synchronises a r" $
|
||||
\a r -> D.isCommit a r ==> D.synchronises a r
|
||||
]
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
memoryProps :: [TestTree]
|
||||
memoryProps = toTestList
|
||||
[ testProperty "bufferWrite emptyBuffer k c a /= emptyBuffer" $
|
||||
\k a -> crefProp $ \cref -> do
|
||||
wb <- Mem.bufferWrite Mem.emptyBuffer k cref a
|
||||
@ -79,43 +105,34 @@ tests =
|
||||
a' <- Mem.readCRef cref tid1
|
||||
pure (tid1 /= tid2 ==> a' == a1)
|
||||
]
|
||||
|
||||
, testGroup "SCT"
|
||||
[ testProperty "canInterrupt ==> canInterruptL" $
|
||||
\ds tid act ->
|
||||
canRewind act && SCT.canInterrupt ds tid act ==>
|
||||
SCT.canInterruptL ds tid (rewind' act)
|
||||
|
||||
, testProperty "dependent ==> dependent'" $
|
||||
\ds tid1 tid2 ta1 ta2 ->
|
||||
canRewind ta2 && SCT.dependent ds tid1 ta1 tid2 ta2 ==>
|
||||
SCT.dependent' ds tid1 ta1 tid2 (rewind' ta2)
|
||||
|
||||
, testProperty "dependent x y == dependent y x" $
|
||||
\ds tid1 tid2 ta1 ta2 ->
|
||||
SCT.dependent ds tid1 ta1 tid2 ta2 ==
|
||||
SCT.dependent ds tid2 ta2 tid1 ta1
|
||||
|
||||
, testProperty "dependentActions x y == dependentActions y x" $
|
||||
\ds a1 a2 ->
|
||||
SCT.dependentActions ds a1 a2 == SCT.dependentActions ds a2 a1
|
||||
]
|
||||
]
|
||||
where
|
||||
eqord :: forall a. (Eq a, Ord a, Listable a, Show a) => Proxy a -> [TestTree]
|
||||
eqord _ =
|
||||
[ testProperty "Reflexivity (==)" $ \(x :: a) -> x == x
|
||||
, testProperty "Symmetry (==)" $ \(x :: a) y -> (x == y) == (y == x)
|
||||
, testProperty "Transitivity (==)" $ \(x :: a) y z -> x == y && y == z ==> x == z
|
||||
, testProperty "Reflexivity (<=)" $ \(x :: a) -> x <= x
|
||||
, testProperty "Antisymmetry (<=)" $ \(x :: a) y -> x <= y && y <= x ==> x == y
|
||||
, testProperty "Transitivity (<=)" $ \(x :: a) y z -> x <= y && y <= z ==> x <= z
|
||||
, testProperty "Eq / Ord Consistency" $ \(x :: a) y -> x == y ==> x <= y
|
||||
]
|
||||
|
||||
crefProp :: (forall s. D.CRef (ST.STRef s) Int -> ST.ST s Bool) -> D.CRefId -> Bool
|
||||
crefProp prop crid = ST.runST $ makeCRef crid >>= prop
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
sctProps :: [TestTree]
|
||||
sctProps = toTestList
|
||||
[ testProperty "canInterrupt ==> canInterruptL" $
|
||||
\ds tid act ->
|
||||
canRewind act && SCT.canInterrupt ds tid act ==>
|
||||
SCT.canInterruptL ds tid (rewind' act)
|
||||
|
||||
, testProperty "dependent ==> dependent'" $
|
||||
\ds tid1 tid2 ta1 ta2 ->
|
||||
canRewind ta2 && SCT.dependent ds tid1 ta1 tid2 ta2 ==>
|
||||
SCT.dependent' ds tid1 ta1 tid2 (rewind' ta2)
|
||||
|
||||
, testProperty "dependent x y == dependent y x" $
|
||||
\ds tid1 tid2 ta1 ta2 ->
|
||||
SCT.dependent ds tid1 ta1 tid2 ta2 ==
|
||||
SCT.dependent ds tid2 ta2 tid1 ta1
|
||||
|
||||
, testProperty "dependentActions x y == dependentActions y x" $
|
||||
\ds a1 a2 ->
|
||||
SCT.dependentActions ds a1 a2 == SCT.dependentActions ds a2 a1
|
||||
]
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- Utils
|
||||
|
Loading…
Reference in New Issue
Block a user