From 29b1f285462725bef7b17a948648d0233c04f8ef Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Mon, 30 Oct 2017 20:07:25 +0000 Subject: [PATCH] Add some property tests Goes some way to solving #142, but it would be nice to have some for the memory stuff. --- .weeder.yaml | 6 + dejafu-tests/Cases.hs | 2 + dejafu-tests/Cases/Properties.hs | 192 +++++++++++++++++++++++++++++++ dejafu-tests/Common.hs | 11 +- dejafu-tests/dejafu-tests.cabal | 2 + 5 files changed, 212 insertions(+), 1 deletion(-) create mode 100644 dejafu-tests/Cases/Properties.hs diff --git a/.weeder.yaml b/.weeder.yaml index b519b6d..016502e 100644 --- a/.weeder.yaml +++ b/.weeder.yaml @@ -57,6 +57,11 @@ - stmTests - subconcurrencyTests - threadingTests + - module: + - name: Cases.Properties + - identifier: + - canRewind + - rewind' - module: - name: Cases.Refinement - identifier: @@ -76,6 +81,7 @@ - identifier: - BT - failing + - hunitTest - module: - name: Examples.AutoUpdate - identifier: diff --git a/dejafu-tests/Cases.hs b/dejafu-tests/Cases.hs index 2ae6b86..30b882d 100755 --- a/dejafu-tests/Cases.hs +++ b/dejafu-tests/Cases.hs @@ -7,6 +7,7 @@ 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 @@ -19,5 +20,6 @@ testCases = , testGroup "Litmus" L.tests , testGroup "Async" A.tests , testGroup "Discard" D.tests + , testGroup "Properties" P.tests , testGroup "Regressions" G.tests ] diff --git a/dejafu-tests/Cases/Properties.hs b/dejafu-tests/Cases/Properties.hs new file mode 100644 index 0000000..b69420a --- /dev/null +++ b/dejafu-tests/Cases/Properties.hs @@ -0,0 +1,192 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Cases.Properties where + +import qualified Control.Exception as E +import Data.Map (Map, fromList) +import Data.Maybe (fromJust, isJust) +import Data.Proxy (Proxy(..)) +import Test.DejaFu.Common (ThreadAction, Lookahead) +import qualified Test.DejaFu.Common as D +import qualified Test.DejaFu.SCT.Internal as SCT +import Test.Framework (Test) +import Test.LeanCheck (Listable(..), (\/), (><), (==>), cons0, cons1, cons2, cons3, mapT) + +import Common + +tests :: [Test] +tests = + [ testGroup "Class Laws" + [ testGroup "ThreadId" (eqord (Proxy :: Proxy D.ThreadId)) + , testGroup "CRefId" (eqord (Proxy :: Proxy D.CRefId)) + , testGroup "MVarId" (eqord (Proxy :: Proxy D.MVarId)) + , testGroup "TVarId" (eqord (Proxy :: Proxy D.TVarId)) + , testGroup "Failure" (eqord (Proxy :: Proxy D.Failure)) + ] + + , testGroup "Common" + [ leancheck "simplifyAction a == simplifyLookahead (rewind a)" $ + \act -> canRewind act ==> + D.simplifyAction act == D.simplifyLookahead (rewind' act) + + , leancheck "isBarrier a ==> synchronises a r" $ + \a r -> D.isBarrier a ==> D.synchronises a r + + , leancheck "isCommit a r ==> synchronises a r" $ + \a r -> D.isCommit a r ==> D.synchronises a r + ] + + , testGroup "SCT" + [ leancheck "canInterrupt ==> canInterruptL" $ + \ds tid act -> + canRewind act && SCT.canInterrupt ds tid act ==> + SCT.canInterruptL ds tid (rewind' act) + + , leancheck "dependent ==> dependent'" $ + \mem ds tid1 tid2 ta1 ta2 -> + canRewind ta2 && SCT.dependent mem ds tid1 ta1 tid2 ta2 ==> + SCT.dependent' mem ds tid1 ta1 tid2 (rewind' ta2) + + , leancheck "dependent x y == dependent y x" $ + \mem ds tid1 tid2 ta1 ta2 -> + SCT.dependent mem ds tid1 ta1 tid2 ta2 == + SCT.dependent mem ds tid2 ta2 tid1 ta1 + + , leancheck "dependentActions x y == dependentActions y x" $ + \mem ds a1 a2 -> + SCT.dependentActions mem ds a1 a2 == SCT.dependentActions mem ds a2 a1 + ] + ] + where + eqord :: forall a. (Eq a, Ord a, Listable a, Show a) => Proxy a -> [Test] + eqord _ = + [ leancheck "Reflexivity (==)" $ \(x :: a) -> x == x + , leancheck "Symmetry (==)" $ \(x :: a) y -> (x == y) == (y == x) + , leancheck "Transitivity (==)" $ \(x :: a) y z -> x == y && y == z ==> x == z + , leancheck "Reflexivity (<=)" $ \(x :: a) -> x <= x + , leancheck "Antisymmetry (<=)" $ \(x :: a) y -> x <= y && y <= x ==> x == y + , leancheck "Transitivity (<=)" $ \(x :: a) y z -> x <= y && y <= z ==> x <= z + , leancheck "Eq / Ord Consistency" $ \(x :: a) y -> x == y ==> x <= y + ] + +------------------------------------------------------------------------------- +-- Utils + +canRewind :: ThreadAction -> Bool +canRewind = isJust . D.rewind + +rewind' :: ThreadAction -> Lookahead +rewind' = fromJust . D.rewind + +------------------------------------------------------------------------------- +-- Arbitrary instances + +instance Listable D.ThreadId where + tiers = mapT (D.ThreadId Nothing) tiers + +instance Listable D.CRefId where + tiers = mapT (D.CRefId Nothing) tiers + +instance Listable D.MVarId where + tiers = mapT (D.MVarId Nothing) tiers + +instance Listable D.TVarId where + tiers = mapT (D.TVarId Nothing) tiers + +instance Listable D.ThreadAction where + tiers = + cons1 D.Fork + \/ cons0 D.MyThreadId + \/ cons1 D.GetNumCapabilities + \/ cons1 D.SetNumCapabilities + \/ cons0 D.Yield + \/ cons1 D.ThreadDelay + \/ cons1 D.NewMVar + \/ cons2 D.PutMVar + \/ cons1 D.BlockedPutMVar + \/ cons3 D.TryPutMVar + \/ cons1 D.ReadMVar + \/ cons2 D.TryReadMVar + \/ cons1 D.BlockedReadMVar + \/ cons2 D.TakeMVar + \/ cons1 D.BlockedTakeMVar + \/ cons3 D.TryTakeMVar + \/ cons1 D.NewCRef + \/ cons1 D.ReadCRef + \/ cons1 D.ReadCRefCas + \/ cons1 D.ModCRef + \/ cons1 D.ModCRefCas + \/ cons1 D.WriteCRef + \/ cons2 D.CasCRef + \/ cons2 D.CommitCRef + \/ cons2 D.STM + \/ cons1 D.BlockedSTM + \/ cons0 D.Catching + \/ cons0 D.PopCatching + \/ cons0 D.Throw + \/ cons1 D.ThrowTo + \/ cons1 D.BlockedThrowTo + \/ cons0 D.Killed + \/ cons2 D.SetMasking + \/ cons2 D.ResetMasking + \/ cons0 D.LiftIO + \/ cons0 D.Return + \/ cons0 D.Stop + \/ cons0 D.Subconcurrency + \/ cons0 D.StopSubconcurrency + +instance Listable D.TAction where + tiers = + cons1 D.TNew + \/ cons1 D.TRead + \/ cons1 D.TWrite + \/ cons0 D.TRetry + \/ cons2 D.TOrElse + \/ cons0 D.TThrow + \/ cons2 D.TCatch + \/ cons0 D.TStop + +instance Listable E.MaskingState where + list = + [ E.Unmasked + , E.MaskedInterruptible + , E.MaskedUninterruptible + ] + +instance Listable D.ActionType where + tiers = + cons1 D.UnsynchronisedRead + \/ cons1 D.UnsynchronisedWrite + \/ cons0 D.UnsynchronisedOther + \/ cons1 D.PartiallySynchronisedCommit + \/ cons1 D.PartiallySynchronisedWrite + \/ cons1 D.PartiallySynchronisedModify + \/ cons1 D.SynchronisedModify + \/ cons1 D.SynchronisedRead + \/ cons1 D.SynchronisedWrite + \/ cons0 D.SynchronisedOther + +instance Listable D.MemType where + list = + [ D.SequentialConsistency + , D.TotalStoreOrder + , D.PartialStoreOrder + ] + +instance Listable SCT.DepState where + tiers = mapT (uncurry SCT.DepState) (tiers >< tiers) + +instance (Ord k, Listable k, Listable v) => Listable (Map k v) where + tiers = mapT fromList tiers + +instance Listable D.Failure where + list = + [ D.InternalError + , D.Abort + , D.Deadlock + , D.STMDeadlock + , D.IllegalSubconcurrency + ] ++ map D.UncaughtException -- have a few different exception types + [ E.toException E.Overflow + , E.toException E.ThreadKilled + , E.toException E.NonTermination + ] diff --git a/dejafu-tests/Common.hs b/dejafu-tests/Common.hs index 80829b0..ba32ced 100644 --- a/dejafu-tests/Common.hs +++ b/dejafu-tests/Common.hs @@ -18,6 +18,7 @@ import qualified Test.Framework as TF import Test.Framework.Providers.HUnit (hUnitTestToTests) import qualified Test.HUnit as TH import Test.HUnit.DejaFu (Bounds, defaultBounds, defaultMemType, uniformly, randomly, swarmy, systematically, testDejafu, testDejafuWay) +import qualified Test.LeanCheck as LeanCheck ------------------------------------------------------------------------------- -- Tests @@ -53,7 +54,7 @@ testGroup :: IsTest t => String -> t -> TF.Test testGroup name = TF.testGroup name . toTestList djfu :: Show a => String -> Predicate a -> (forall t. ConcST t a) -> TF.Test -djfu name p c = head . toTestList $ testDejafu c name p +djfu name p c = hunitTest $ testDejafu c name p djfuT :: Show a => String -> Predicate a -> (forall t. ConcST t a) -> [TF.Test] djfuT name p c = toTestList $ T name c p @@ -61,6 +62,14 @@ djfuT name p c = toTestList $ T name c p alwaysFailsWith :: (Failure -> Bool) -> Predicate a alwaysFailsWith p = alwaysTrue (either p (const False)) +leancheck :: LeanCheck.Testable a => String -> a -> TF.Test +leancheck name = hunitTest . TH.TestLabel name . lcheck . LeanCheck.counterExamples 2500 where + lcheck = TH.TestCase . TH.assertString . unlines . map showf + showf xs = "Failed for " ++ unwords xs + +hunitTest :: TH.Test -> TF.Test +hunitTest = head . toTestList + ------------------------------------------------------------------------------- -- Exceptions diff --git a/dejafu-tests/dejafu-tests.cabal b/dejafu-tests/dejafu-tests.cabal index 6be95d7..edacb43 100644 --- a/dejafu-tests/dejafu-tests.cabal +++ b/dejafu-tests/dejafu-tests.cabal @@ -27,6 +27,7 @@ executable dejafu-tests , Cases.Litmus , Cases.Discard , Cases.Regressions + , Cases.Properties , Examples , Examples.AutoUpdate @@ -49,6 +50,7 @@ executable dejafu-tests , exceptions , HUnit , hunit-dejafu + , leancheck , QuickCheck , random , test-framework