From 3cad91f4e92c17f308225875f5a4e87b15368b30 Mon Sep 17 00:00:00 2001 From: Javier Sagredo Date: Tue, 8 Oct 2024 14:55:53 +0200 Subject: [PATCH] QSM --- io-sim/io-sim.cabal | 46 ++ io-sim/qsm-test/BasicTest/Correct.hs | 54 ++ io-sim/qsm-test/BasicTest/InternalFork.hs | 59 ++ .../qsm-test/BasicTest/InternalForkAtomic.hs | 59 ++ io-sim/qsm-test/BasicTest/NoIncr.hs | 49 ++ io-sim/qsm-test/BasicTest/Racy.hs | 53 ++ io-sim/qsm-test/BasicTest/Template.hs | 68 ++ io-sim/qsm-test/Main.hs | 52 ++ io-sim/qsm/Test/StateMachine/IOSim.hs | 15 + io-sim/qsm/Test/StateMachine/IOSim/Execute.hs | 740 ++++++++++++++++++ .../qsm/Test/StateMachine/IOSim/Generate.hs | 580 ++++++++++++++ io-sim/qsm/Test/StateMachine/IOSim/Types.hs | 23 + 12 files changed, 1798 insertions(+) create mode 100644 io-sim/qsm-test/BasicTest/Correct.hs create mode 100644 io-sim/qsm-test/BasicTest/InternalFork.hs create mode 100644 io-sim/qsm-test/BasicTest/InternalForkAtomic.hs create mode 100644 io-sim/qsm-test/BasicTest/NoIncr.hs create mode 100644 io-sim/qsm-test/BasicTest/Racy.hs create mode 100644 io-sim/qsm-test/BasicTest/Template.hs create mode 100644 io-sim/qsm-test/Main.hs create mode 100644 io-sim/qsm/Test/StateMachine/IOSim.hs create mode 100644 io-sim/qsm/Test/StateMachine/IOSim/Execute.hs create mode 100644 io-sim/qsm/Test/StateMachine/IOSim/Generate.hs create mode 100644 io-sim/qsm/Test/StateMachine/IOSim/Types.hs diff --git a/io-sim/io-sim.cabal b/io-sim/io-sim.cabal index c0b442b0..63d48451 100644 --- a/io-sim/io-sim.cabal +++ b/io-sim/io-sim.cabal @@ -97,6 +97,27 @@ library if flag(asserts) ghc-options: -fno-ignore-asserts +library qsm + import: warnings + hs-source-dirs: qsm + exposed-modules: Test.StateMachine.IOSim.Execute + Test.StateMachine.IOSim.Generate + Test.StateMachine.IOSim.Types + Test.StateMachine.IOSim + + reexported-modules: Test.StateMachine.Types.Rank2 + + build-depends: base, + io-sim, + QuickCheck, + mtl, + containers, + pretty-show, + io-classes, + quickcheck-state-machine:no-vendored-treediff, + default-extensions: ImportQualifiedPost + default-language: Haskell2010 + test-suite test import: test-warnings type: exitcode-stdio-1.0 @@ -144,3 +165,28 @@ benchmark bench -Wpartial-fields -Widentities -Wredundant-constraints + +test-suite qsm-test + import: test-warnings + type: exitcode-stdio-1.0 + hs-source-dirs: qsm-test + main-is: Main.hs + + other-modules: BasicTest.Template + BasicTest.Correct + BasicTest.NoIncr + BasicTest.Racy + BasicTest.InternalFork + BasicTest.InternalForkAtomic + Exception.Deadlocks + Exception.TryPutMVar + Exception.WithMVar + + default-language: Haskell2010 + default-extensions: ImportQualifiedPost + build-depends: base, + io-sim:qsm, + io-classes, + QuickCheck, + tasty, + tasty-quickcheck diff --git a/io-sim/qsm-test/BasicTest/Correct.hs b/io-sim/qsm-test/BasicTest/Correct.hs new file mode 100644 index 00000000..aae234e4 --- /dev/null +++ b/io-sim/qsm-test/BasicTest/Correct.hs @@ -0,0 +1,54 @@ +-- | + +module BasicTest.Correct where + +import BasicTest.Template +import Control.Concurrent.Class.MonadSTM +import Test.QuickCheck +import Test.StateMachine.IOSim + +{------------------------------------------------------------------------------- + SUT +-------------------------------------------------------------------------------} + +newtype AtomicCounter m = AtomicCounter (TVar m Int) + +newSUT :: MonadLabelledSTM m => m (AtomicCounter m) +newSUT = do + ref <- atomically $ do + tv <- newTVar 0 + labelTVar tv "TheCounter" + pure tv + return (AtomicCounter ref) + +incr :: MonadSTM m => AtomicCounter m -> m () +incr (AtomicCounter ref) = + atomically $ do + i <- readTVar ref + writeTVar ref (i + 1) + +get :: MonadSTM m => AtomicCounter m -> m Int +get (AtomicCounter ref) = readTVarIO ref + +semantics :: MonadSTM m => AtomicCounter m -> Cmd Concrete -> m (Resp Concrete) +semantics sut Incr = do + incr sut *> pure Void +semantics sut Get = do + GetR <$> get sut + +transition :: Model r -> Cmd r -> Resp r -> Model r +transition (Model m) Incr _ = Model (m + 1) +transition m Get _ = m + +sm :: StateMachine Model Cmd AtomicCounter Resp +sm = StateMachine initModel transition precondition postcondition Nothing + generator shrinker newSUT semantics mock + +prop_sequential :: Property +prop_sequential = forAllCommands sm Nothing $ runSequential sm + +prop_sequential' :: Property +prop_sequential' = forAllCommands sm Nothing $ runSequentialPOR sm + +prop_parallel :: Property +prop_parallel = forAllParallelCommands sm Nothing $ runParallel sm diff --git a/io-sim/qsm-test/BasicTest/InternalFork.hs b/io-sim/qsm-test/BasicTest/InternalFork.hs new file mode 100644 index 00000000..31bca72c --- /dev/null +++ b/io-sim/qsm-test/BasicTest/InternalFork.hs @@ -0,0 +1,59 @@ +-- | + +module BasicTest.InternalFork where + +import BasicTest.Template +import Control.Concurrent.Class.MonadSTM +import Control.Monad.Class.MonadAsync +import Test.QuickCheck +import Test.StateMachine.IOSim + +{------------------------------------------------------------------------------- + SUT +-------------------------------------------------------------------------------} + +newtype AtomicCounter m = AtomicCounter (TVar m Int) + +newSUT :: MonadLabelledSTM m => m (AtomicCounter m) +newSUT = do + ref <- atomically $ do + tv <- newTVar 0 + labelTVar tv "TheCounter" + pure tv + return (AtomicCounter ref) + +incr :: MonadAsync m => AtomicCounter m -> m () +incr (AtomicCounter ref) = do + t1 <- async f + t2 <- async f + wait t1 >> wait t2 + where f = do + i <- readTVarIO ref + atomically $ writeTVar ref (i + 1) + +get :: (MonadSTM m) => AtomicCounter m -> m Int +get (AtomicCounter ref) = readTVarIO ref + +semantics :: MonadAsync m => AtomicCounter m -> Cmd Concrete -> m (Resp Concrete) +semantics sut Incr = do + incr sut *> pure Void +semantics sut Get = do + GetR <$> get sut + +transition :: Model r -> Cmd r -> Resp r -> Model r +-- each increment will increment by 2 +transition (Model m) Incr _ = Model (m + 2) +transition m Get _ = m + +sm :: StateMachine Model Cmd AtomicCounter Resp +sm = StateMachine initModel transition precondition postcondition Nothing + generator shrinker newSUT semantics mock + +prop_sequential :: Property +prop_sequential = forAllCommands sm Nothing $ runSequential sm + +prop_sequential' :: Property +prop_sequential' = forAllCommands sm Nothing $ runSequentialPOR sm + +prop_parallel :: Property +prop_parallel = forAllParallelCommands sm Nothing $ runParallel sm diff --git a/io-sim/qsm-test/BasicTest/InternalForkAtomic.hs b/io-sim/qsm-test/BasicTest/InternalForkAtomic.hs new file mode 100644 index 00000000..29be5768 --- /dev/null +++ b/io-sim/qsm-test/BasicTest/InternalForkAtomic.hs @@ -0,0 +1,59 @@ +-- | + +module BasicTest.InternalForkAtomic where + +import BasicTest.Template +import Control.Concurrent.Class.MonadSTM +import Control.Monad.Class.MonadAsync +import Test.QuickCheck +import Test.StateMachine.IOSim + +{------------------------------------------------------------------------------- + SUT +-------------------------------------------------------------------------------} + +newtype AtomicCounter m = AtomicCounter (TVar m Int) + +newSUT :: MonadLabelledSTM m => m (AtomicCounter m) +newSUT = do + ref <- atomically $ do + tv <- newTVar 0 + labelTVar tv "TheCounter" + pure tv + return (AtomicCounter ref) + +incr :: MonadAsync m => AtomicCounter m -> m () +incr (AtomicCounter ref) = do + t1 <- async f + t2 <- async f + wait t1 >> wait t2 + where f = atomically $ do + i <- readTVar ref + writeTVar ref (i + 1) + +get :: (MonadSTM m) => AtomicCounter m -> m Int +get (AtomicCounter ref) = readTVarIO ref + +semantics :: MonadAsync m => AtomicCounter m -> Cmd Concrete -> m (Resp Concrete) +semantics sut Incr = do + incr sut *> pure Void +semantics sut Get = do + GetR <$> get sut + +transition :: Model r -> Cmd r -> Resp r -> Model r +-- each increment will increment by 2 +transition (Model m) Incr _ = Model (m + 2) +transition m Get _ = m + +sm :: StateMachine Model Cmd AtomicCounter Resp +sm = StateMachine initModel transition precondition postcondition Nothing + generator shrinker newSUT semantics mock + +prop_sequential :: Property +prop_sequential = forAllCommands sm Nothing $ runSequential sm + +prop_sequential' :: Property +prop_sequential' = forAllCommands sm Nothing $ runSequentialPOR sm + +prop_parallel :: Property +prop_parallel = forAllParallelCommands sm Nothing $ runParallel sm diff --git a/io-sim/qsm-test/BasicTest/NoIncr.hs b/io-sim/qsm-test/BasicTest/NoIncr.hs new file mode 100644 index 00000000..f3b92521 --- /dev/null +++ b/io-sim/qsm-test/BasicTest/NoIncr.hs @@ -0,0 +1,49 @@ +-- | + +module BasicTest.NoIncr where + +import BasicTest.Template +import Control.Concurrent.Class.MonadSTM +import Test.QuickCheck +import Test.StateMachine.IOSim + +{------------------------------------------------------------------------------- + SUT +-------------------------------------------------------------------------------} + +newtype AtomicCounter m = AtomicCounter (TVar m Int) + +newSUT :: MonadLabelledSTM m => m (AtomicCounter m) +newSUT = do + ref <- atomically $ do + tv <- newTVar 0 + labelTVar tv "TheCounter" + pure tv + return (AtomicCounter ref) + +incr :: MonadSTM m => AtomicCounter m -> m () +incr (AtomicCounter ref) = + atomically $ do + i <- readTVar ref + -- Deliberate bug, no increment + writeTVar ref i + +get :: MonadSTM m => AtomicCounter m -> m Int +get (AtomicCounter ref) = readTVarIO ref + +semantics :: MonadSTM m => AtomicCounter m -> Cmd Concrete -> m (Resp Concrete) +semantics sut Incr = do + incr sut *> pure Void +semantics sut Get = do + GetR <$> get sut + +transition :: Model r -> Cmd r -> Resp r -> Model r +transition (Model m) Incr _ = Model (m + 1) +transition m Get _ = m + +sm :: StateMachine Model Cmd AtomicCounter Resp +sm = StateMachine initModel transition precondition postcondition Nothing + generator shrinker newSUT semantics mock + +prop_sequential :: Property +prop_sequential = forAllCommands sm Nothing $ runSequential sm diff --git a/io-sim/qsm-test/BasicTest/Racy.hs b/io-sim/qsm-test/BasicTest/Racy.hs new file mode 100644 index 00000000..bc7a0dc3 --- /dev/null +++ b/io-sim/qsm-test/BasicTest/Racy.hs @@ -0,0 +1,53 @@ +-- | + +module BasicTest.Racy where + +import BasicTest.Template +import Control.Concurrent.Class.MonadSTM +import Test.QuickCheck +import Test.StateMachine.IOSim + +{------------------------------------------------------------------------------- + SUT +-------------------------------------------------------------------------------} + +newtype AtomicCounter m = AtomicCounter (TVar m Int) + +newSUT :: MonadLabelledSTM m => m (AtomicCounter m) +newSUT = do + ref <- atomically $ do + tv <- newTVar 0 + labelTVar tv "TheCounter" + pure tv + return (AtomicCounter ref) + +incr :: MonadSTM m => AtomicCounter m -> m () +incr (AtomicCounter ref) = do + i <- readTVarIO ref + atomically $ writeTVar ref (i + 1) + +get :: MonadSTM m => AtomicCounter m -> m Int +get (AtomicCounter ref) = readTVarIO ref + +semantics :: MonadSTM m => AtomicCounter m -> Cmd Concrete -> m (Resp Concrete) +semantics sut Incr = do + incr sut *> pure Void +semantics sut Get = do + GetR <$> get sut + +transition :: Model r -> Cmd r -> Resp r -> Model r +transition (Model m) Incr _ = Model (m + 1) +transition m Get _ = m + +sm :: StateMachine Model Cmd AtomicCounter Resp +sm = StateMachine initModel transition precondition postcondition Nothing + generator shrinker newSUT semantics mock + +prop_sequential :: Property +prop_sequential = forAllCommands sm Nothing $ runSequential sm + +prop_sequential' :: Property +prop_sequential' = forAllCommands sm Nothing $ runSequentialPOR sm + +prop_parallel :: Property +prop_parallel = forAllParallelCommands sm Nothing $ runParallel sm diff --git a/io-sim/qsm-test/BasicTest/Template.hs b/io-sim/qsm-test/BasicTest/Template.hs new file mode 100644 index 00000000..992d03ee --- /dev/null +++ b/io-sim/qsm-test/BasicTest/Template.hs @@ -0,0 +1,68 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE StandaloneKindSignatures #-} + +-- | + +module BasicTest.Template where + +import Data.Kind +import GHC.Generics +import Test.QuickCheck +import Test.StateMachine.IOSim +import Test.StateMachine.Types.Rank2 qualified as Rank2 + +{------------------------------------------------------------------------------- + Cmd and response +-------------------------------------------------------------------------------} + +type Cmd :: (Type -> Type) -> Type +data Cmd r = Incr | Get + deriving (Eq, Show, Generic, Generic1, Read) + +deriving instance Rank2.Functor Cmd +deriving instance Rank2.Traversable Cmd +deriving instance Rank2.Foldable Cmd + +type Resp :: (Type -> Type) -> Type +data Resp r = Void | GetR Int + deriving (Eq, Show, Generic, Generic1, Read) + +deriving instance Rank2.Functor Resp +deriving instance Rank2.Traversable Resp +deriving instance Rank2.Foldable Resp + +{------------------------------------------------------------------------------- + Model +--------------------------------------------------------------------------------} + +type Model :: (Type -> Type) -> Type +data Model r = Model + { value :: Int } + deriving (Show) + +initModel :: Model r +initModel = Model 0 + +precondition :: model Symbolic -> cmd Symbolic -> Logic +precondition _ _ = Top + +postcondition :: Model Concrete -> Cmd Concrete -> Resp Concrete -> Logic +postcondition (Model m) Get (GetR m') = m .== m' +postcondition _ _ _ = Top + +invariant :: Maybe (model Concrete -> Logic) +invariant = Nothing + +generator :: model Symbolic -> Maybe (Gen (Cmd Symbolic)) +generator _ = Just $ oneof [pure Incr, pure Get] + +shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic] +shrinker _ _ = [] + +mock :: Model Symbolic -> Cmd Symbolic -> GenSym (Resp Symbolic) +mock _ Incr = pure Void +mock (Model m) Get = pure (GetR m) diff --git a/io-sim/qsm-test/Main.hs b/io-sim/qsm-test/Main.hs new file mode 100644 index 00000000..6242f743 --- /dev/null +++ b/io-sim/qsm-test/Main.hs @@ -0,0 +1,52 @@ +module Main where + +import BasicTest.Correct qualified +import BasicTest.InternalFork qualified +import BasicTest.InternalForkAtomic qualified +import BasicTest.NoIncr qualified +import BasicTest.Racy qualified +import Exception.Deadlocks qualified +import Exception.TryPutMVar qualified +import Exception.WithMVar qualified +import Test.Tasty +import Test.Tasty.QuickCheck + +main :: IO () +main = defaultMain $ + testGroup "QSM" [ + testGroup "Sequential" [ + -- Fully correct implementation + testProperty "Correct" BasicTest.Correct.prop_sequential + -- Buggy implementation, doesn't increment. The error is found in sequential testing + , testProperty "NoIncr" $ expectFailure BasicTest.NoIncr.prop_sequential + -- Racy implementation, sequential testing passes + , testProperty "Racy" BasicTest.Racy.prop_sequential + , testProperty "Internal" BasicTest.InternalFork.prop_sequential + , testProperty "Internal'" BasicTest.InternalForkAtomic.prop_sequential + ] + , testGroup "SequentialPOR" [ + testProperty "Internal" $ expectFailure BasicTest.InternalFork.prop_sequential' + -- TODO this is still too slow because it will replay all possible reorderings from the past + -- @exploreRaces@ should be called at an appropriate point in time? + -- , testProperty "Internal'" $ BasicTest.InternalForkAtomic.prop_sequential' + ] + , testGroup "Parallel" [ + -- Fully correct implementation + testProperty "Correct" BasicTest.Correct.prop_parallel + -- Racy implementation, parallel test case fails + , testProperty "Racy" $ expectFailure BasicTest.Racy.prop_parallel + ] + , testGroup "Exceptions" [ + testGroup "DoublePut" [ + testProperty "Sequential" Exception.Deadlocks.prop_sequential + , testProperty "SequentialPOR" $ expectFailure Exception.Deadlocks.prop_sequential' + -- , testProperty "Parallel" Exception.Deadlocks.prop_parallel + ] + , testGroup "TryPutMVar" [ + testProperty "Parallel" $ expectFailure Exception.TryPutMVar.prop_parallel' + ] + , testGroup "WithMVar" [ + testProperty "Parallel" Exception.WithMVar.prop_parallel' + ] + ] + ] diff --git a/io-sim/qsm/Test/StateMachine/IOSim.hs b/io-sim/qsm/Test/StateMachine/IOSim.hs new file mode 100644 index 00000000..5372e284 --- /dev/null +++ b/io-sim/qsm/Test/StateMachine/IOSim.hs @@ -0,0 +1,15 @@ +-- | + +module Test.StateMachine.IOSim + ( module Test.StateMachine.IOSim.Execute + , module Test.StateMachine.IOSim.Generate + , module Test.StateMachine.IOSim.Types + , module Test.StateMachine.Types + , module Test.StateMachine.Logic + ) where + +import Test.StateMachine.IOSim.Execute +import Test.StateMachine.IOSim.Generate +import Test.StateMachine.IOSim.Types (StateMachine (StateMachine)) +import Test.StateMachine.Logic +import Test.StateMachine.Types hiding (StateMachine (..)) diff --git a/io-sim/qsm/Test/StateMachine/IOSim/Execute.hs b/io-sim/qsm/Test/StateMachine/IOSim/Execute.hs new file mode 100644 index 00000000..4f3cca00 --- /dev/null +++ b/io-sim/qsm/Test/StateMachine/IOSim/Execute.hs @@ -0,0 +1,740 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} + +module Test.StateMachine.IOSim.Execute + ( -- * Executing + runSequential + , runParallel + , runParallelException + , runSequentialPOR + , runSequentialPORException + ) where + +import Control.Concurrent.Class.MonadSTM hiding (check) +import Control.Monad.Class.MonadAsync +import Control.Monad.Class.MonadTest +import Control.Monad.Class.MonadThrow +import Control.Monad.IOSim +import Data.Bifunctor +import Data.Dynamic (Dynamic, toDyn) +import Data.Either +import Data.Foldable (foldl') +import Data.Function ((&)) +import Data.Maybe +import Test.QuickCheck +import Test.StateMachine.IOSim.Types +import Test.StateMachine.Logic +import Test.StateMachine.Types hiding (StateMachine (..)) +import Test.StateMachine.Types.Rank2 qualified as Rank2 +import Text.Show.Pretty hiding (reify) + +{------------------------------------------------------------------------------- + Runner helpers +-------------------------------------------------------------------------------} + +-- | Run an IOSim action +runIOSim :: + (Show (resp Concrete)) => + (forall s. IOSim s (resp Concrete)) -> + ( SimTrace (resp Concrete) + , -- \^ Trace for printing + resp Concrete + , -- \^ Response + Property + -- \^ False if there was an exception thrown + ) +runIOSim act = + let trace = runSimTrace act + e msg err = + ( trace + , undefined + , counterexample (ppTrace trace) $ + counterexample (msg <> show err) $ + property False + ) + in case traceResult False trace of + Left (FailureException err) -> e "Exception thrown: " err + Left err -> e "Internal IOSim error: " err + Right v -> (trace, v, property True) + +-- | Run an IOSimPOR action and check the property for each possible interleaving +runIOSimPOR :: + (Show a) => + -- | Test to run + (forall s. IOSim s a) -> + ( SimTrace a -> + -- \^ Trace + Bool -> + -- \^ Was there a previous successful trace? + a -> + -- \^ traceResult + Property + ) -> + Property +runIOSimPOR act prop = + exploreSimTrace id (exploreRaces >> act) $ \(isJust -> pt) trace -> + let e msg err = + counterexample (ppTrace trace) $ + counterexample (msg <> show err) $ + property False + in case traceResult False trace of + Left (FailureException err) -> + e + ( ( if pt + then ("Race condition found! " <>) + else id + ) + "Exception thrown: " + ) + err + Left (FailureDeadlock err) -> + e + ( ( if pt + then ("Race condition found! " <>) + else id + ) + "Deadlock found: " + ) + err + Left err -> + e + ( ( if pt + then ("Race condition found! " <>) + else id + ) + "Internal IOSim error: " + ) + err + Right v -> prop trace pt v + +-- | Run an IOSimPOR action and check the property for each possible interleaving +runIOSimPORAcceptExceptions :: + (Show a) => + -- | Test to run + (forall s. IOSim s a) -> + ( SimTrace a -> + -- \^ Trace + Bool -> + -- \^ Was there a previous successful trace? + Either SomeException a -> + -- \^ traceResult + Property + ) -> + Property +runIOSimPORAcceptExceptions act prop = + exploreSimTrace id (exploreRaces >> act) $ \(isJust -> pt) trace -> + let e msg err = + counterexample (ppTrace trace) $ + counterexample (msg <> show err) $ + property False + in case traceResult False trace of + Left (FailureDeadlock err) -> + e + ( ( if pt + then ("Race condition found! " <>) + else id + ) + "Deadlock found: " + ) + err + Right v -> prop trace pt (Right v) + Left (FailureException err) -> prop trace pt (Left err) + Left err -> + e + ( ( if pt + then ("Race condition found! " <>) + else id + ) + "Internal IOSim error: " + ) + err + +{------------------------------------------------------------------------------- + Running functions +-------------------------------------------------------------------------------} + +{- | Run a sequence of commands sequentially + +Checks for: + + * precondition + + * exceptions + + * postcondition + + * invariant + + * mock semantics match +-} +runSequential :: + forall cmd resp sut model. + (Show (cmd Concrete), Show (resp Concrete)) => + (Rank2.Traversable cmd, Rank2.Foldable resp) => + StateMachine model cmd sut resp -> + Commands cmd resp -> + Property +runSequential sm@StateMachine{..} (Commands scmds) = + foldl' act (property True, [], emptyEnvironment, initModel, newCounter, initModel) scmds + & (\(p, _, _, _, _, _) -> p) + where + act (prevProp, prevCmds, env, smodel, counter, cmodel) (Command scmd _ vars) = + let + -- Precondition + pPre = prec sm smodel scmd + + -- Simulate + ccmd = fromRight (error "runSequential: impossible") (reify env scmd) + prevCmds' = prevCmds ++ [ccmd] + (trace, cresp, prop) = runIOSim $ do + sut <- initSut + sequence_ $ map (\c -> semantics sut c) prevCmds + semantics sut ccmd + + -- Postcondition and invariant + pPost = post sm cmodel ccmd cresp False trace + pInv = inv sm cmodel False trace + + -- Mock + (pMock, cvars) = mockCheck ccmd cresp vars + (sresp, counter') = runGenSym (mock smodel scmd) counter + in + ( prevProp .&&. pPre .&&. prop .&&. pMock .&&. pPost .&&. pInv + , prevCmds' + , insertConcretes vars cvars env + , transition smodel scmd sresp + , counter' + , transition cmodel ccmd cresp + ) + +{- | Run a sequence of commands sequentially, additionally checking for races. + +Checks for: + + * precondition + + * exceptions + + * postcondition + + * invariant + + * mock semantics match + +For all possible races found, the postcondition and invariant must hold. +-} +runSequentialPOR :: + forall cmd resp sut model. + (Show (cmd Concrete), Show (resp Concrete)) => + (Rank2.Traversable cmd, Rank2.Foldable resp) => + StateMachine model cmd sut resp -> + Commands cmd resp -> + Property +runSequentialPOR sm@StateMachine{..} (Commands scmds) = + foldl' act (property True, [], emptyEnvironment, initModel, newCounter, initModel) scmds + & (\(p, _, _, _, _, _) -> p) + where + act (prevProp, prevCmds, env, smodel, counter, cmodel) (Command scmd _ vars) = + let + -- Precondition + pPre = prec sm smodel scmd + + -- Simulation + ccmd = fromRight (error "runSequential: impossible") (reify env scmd) + prevCmds' = prevCmds ++ [ccmd] + simAction = do + sut <- initSut + sequence_ $ map (\c -> semantics sut c) prevCmds + semantics sut ccmd + -- Parallel property (for all interleavings) + porProp = runIOSimPOR simAction $ \trace pt cresp' -> + let + (pMock, _) = mockCheck ccmd cresp' vars + pPost = post sm cmodel ccmd cresp' pt trace + pInv = inv sm cmodel pt trace + in + prevProp .&&. pPre .&&. pMock .&&. pPost .&&. pInv + + -- Advance model + (_, cresp, _) = runIOSim simAction + (_, cvars) = mockCheck ccmd cresp vars + (sresp, counter') = runGenSym (mock smodel scmd) counter + in + ( prevProp .&&. porProp + , prevCmds' + , insertConcretes vars cvars env + , transition smodel scmd sresp + , counter' + , transition cmodel ccmd cresp + ) + +runSequentialPORException :: + forall cmd resp sut model. + (Show (cmd Concrete), Show (resp Concrete)) => + (Rank2.Traversable cmd, Rank2.Foldable resp) => + StateMachine model cmd sut resp -> + Commands cmd resp -> + Property +runSequentialPORException sm@StateMachine{..} (Commands scmds) = + foldl' act (property True, [], emptyEnvironment, initModel, newCounter, initModel) scmds + & (\(p, _, _, _, _, _) -> p) + where + act (prevProp, prevCmds, env, smodel, counter, cmodel) (Command scmd _ vars) = + let + -- Precondition + pPre = prec sm smodel scmd + + -- Simulation + ccmd = fromRight (error "runSequential: impossible") (reify env scmd) + prevCmds' = prevCmds ++ [ccmd] + simAction = do + sut <- initSut + sequence_ $ map (\c -> semantics sut c) prevCmds + t1 <- async $ semantics sut ccmd + canceller <- async (cancel t1) + wait canceller + wait t1 + -- Parallel property (for all interleavings) + porProp = runIOSimPORAcceptExceptions simAction $ \trace pt -> \case + Right cresp' -> + let + (pMock, _) = mockCheck ccmd cresp' vars + pPost = post sm cmodel ccmd cresp' pt trace + pInv = inv sm cmodel pt trace + in + prevProp .&&. pPre .&&. pMock .&&. pPost .&&. pInv + Left _ -> property True + + -- Advance model + (_, cresp, _) = runIOSim simAction + (_, cvars) = mockCheck ccmd cresp vars + (sresp, counter') = runGenSym (mock smodel scmd) counter + in + ( prevProp .&&. porProp + , prevCmds' + , insertConcretes vars cvars env + , transition smodel scmd sresp + , counter' + , transition cmodel ccmd cresp + ) + +{------------------------------------------------------------------------------- + Parallel +-------------------------------------------------------------------------------} + +data OnePairF f a = One a | PP (f a) + +-- | Run a ParallelCommands +runParallel :: + forall cmd resp sut model. + (Show (cmd Concrete), Show (resp Concrete)) => + (Rank2.Traversable cmd, Rank2.Foldable resp) => + StateMachine model cmd sut resp -> + ParallelCommands cmd resp -> + Property +runParallel sm@StateMachine{..} (ParallelCommands pref suff) = + foldl' act (property True, [], emptyEnvironment, initModel, newCounter, initModel) (One pref : map PP suff) + & (\(p, _, _, _, _, _) -> p) + where + act st (One (Commands scmds)) = foldl' runSequential' st scmds + act (prevProp, prevCmds, env, _smodel, _counter, cmodel) (PP (Pair (Commands p1) (Commands p2))) = + let + -- Reify commands and create environments + -- + -- The only way to do this is to run the actions in two separate IOSim + -- simulations, accumulating the environment and commands. + -- + -- Due to the iterative nature of this test, we can be confident this will + -- not fail if previous steps did not fail. + reifyCmd (acc, env') (Command scmd _ vars) = + let ccmd = fromRight (error "runSequential: impossible") (reify env' scmd) + simAction' = do + sut <- initSut + sequence_ $ map (semantics sut) (prevCmds ++ map fst acc) + semantics sut ccmd + (_, cresp, _) = runIOSim simAction' + (_, cvars) = mockCheck ccmd cresp vars + in (acc ++ [(ccmd, cresp)], insertConcretes vars cvars env') + + (p1', env1) = foldl' reifyCmd ([], env) p1 + (p2', env2) = foldl' reifyCmd ([], env) p2 + + -- The IOSimPOR parallel action + simAction = do + -- We create a TQueue to which we will send command + response pairs + tq <- atomically $ do + tq <- newTQueue + labelTQueue tq "CONTROL" + pure tq + sut <- initSut + -- Run the sequential prefix + sequence_ $ map (\c -> semantics sut c) prevCmds + + let racingAction = + async + . sequence_ + . map + ( \ccmd -> do + cresp <- semantics sut ccmd + atomically $ writeTQueue tq (ccmd, cresp) + ) + . map fst + -- Run both actions in a race, and wait for both + t1 <- racingAction p1' + t2 <- racingAction p2' + + wait t1 + wait t2 + + -- Get all command + response pairs + atomically $ drainTQueue tq + + -- The simulation + porProp = runIOSimPOR simAction $ \trace _ cmds -> + let events = traceEvents trace + events' = [first reverse $ splitAt n events | n <- [0 .. length events]] + -- A real interleaving is one in which the thread that sent + -- the message to the TQueue has done some work since it was + -- scheduled, i.e. the TQueue writing action was not + -- artificially delayed + fakeInterleaving = + [ not $ hasDoneWork id2 before + | (before, (_, id2, _, EventTxCommitted w _ _) : _) <- events' + , Just "CONTROL" `elem` map l_label w -- has written to the CONTROL TQueue + ] + in counterexample (ppTrace trace) $ + -- If this was a fake interleaving just make it pass + property (or fakeInterleaving) + .||. ( fst $ + foldl' + ( \(prop, model) (cmd, resp) -> + let model' = transition model cmd resp + prop' = case logic (postcondition model cmd resp) of + VFalse ce -> counterexample ("Poscondition impossible! " <> show ce) $ property False + _ -> property True + in (prop .&&. prop', model') + ) + (property True, cmodel) + cmds + ) + in + ( prevProp .&&. porProp + , prevCmds ++ map fst p1' ++ map fst p2' + , env1 <> env2 + , undefined + , undefined + , foldl (\x (y, z) -> transition x y z) cmodel $ p1' ++ p2' + ) + + -- This is almost the same as @runSequential@ but it accumulates the concrete + -- commands. + runSequential' (prevProp, prevCmds, env, smodel, counter, cmodel) (Command scmd _ vars) = + let + -- Precondition + pPre = prec sm smodel scmd + + -- Simulate + ccmd = fromRight (error "runSequential: impossible") (reify env scmd) + prevCmds' = prevCmds ++ [ccmd] + simAction = do + sut <- initSut + sequence_ $ map (\c -> semantics sut c) prevCmds + semantics sut ccmd + (trace, cresp, prop) = runIOSim simAction + + -- Postcondition + pPost = post sm cmodel ccmd cresp False trace + pInv = inv sm cmodel False trace + + -- Mock + (pMock, cvars) = mockCheck ccmd cresp vars + (sresp, counter') = runGenSym (mock smodel scmd) counter + in + ( prevProp .&&. pPre .&&. prop .&&. pPost .&&. pInv .&&. pMock + , prevCmds' + , insertConcretes vars cvars env + , transition smodel scmd sresp + , counter' + , transition cmodel ccmd cresp + ) + +-- | Run a ParallelCommands +runParallelException :: + forall cmd resp sut model. + (Show (cmd Concrete), Show (resp Concrete)) => + (Rank2.Traversable cmd, Rank2.Foldable resp) => + StateMachine model cmd sut resp -> + ParallelCommands cmd resp -> + Property +runParallelException sm@StateMachine{..} (ParallelCommands pref suff) = + foldl' act (property True, [], emptyEnvironment, initModel, newCounter, initModel) (One pref : map PP suff) + & (\(p, _, _, _, _, _) -> p) + where + act st (One (Commands scmds)) = foldl' runSequential' st scmds + act (prevProp, prevCmds, env, _smodel, _counter, cmodel) (PP (Pair (Commands p1) (Commands p2))) = + let + -- Reify commands and create environments + -- + -- The only way to do this is to run the actions in two separate IOSim + -- simulations, accumulating the environment and commands. + -- + -- Due to the iterative nature of this test, we can be confident this will + -- not fail if previous steps did not fail. + reifyCmd (acc, env') (Command scmd _ vars) = + let ccmd = fromRight (error "runSequential: impossible") (reify env' scmd) + simAction' = do + sut <- initSut + sequence_ $ map (semantics sut) (prevCmds ++ map fst acc) + semantics sut ccmd + (_, cresp, _) = runIOSim simAction' + (_, cvars) = mockCheck ccmd cresp vars + in (acc ++ [(ccmd, cresp)], insertConcretes vars cvars env') + + (p1', env1) = foldl' reifyCmd ([], env) p1 + (p2', env2) = foldl' reifyCmd ([], env) p2 + + -- The IOSimPOR parallel action + simAction = do + -- We create a TQueue to which we will send command + response pairs + tq <- atomically $ do + tq <- newTQueue + labelTQueue tq "CONTROL" + pure tq + sut <- initSut + -- Run the sequential prefix + sequence_ $ map (\c -> semantics sut c) prevCmds + + let racingAction = + async + . sequence_ + . map + ( \ccmd -> do + cresp <- semantics sut ccmd + atomically $ writeTQueue tq (ccmd, cresp) + ) + . map fst + -- Run both actions in a race, and wait for both + t1 <- racingAction p1' + t2 <- racingAction p2' + t3 <- async (cancel t1) + wait t3 + wait t2 + wait t1 + + -- Get all command + response pairs + atomically $ drainTQueue tq + + -- The simulation + porProp = runIOSimPORAcceptExceptions simAction $ \trace _ -> \case + Left {} -> property True + Right cmds -> + let events = traceEvents trace + events' = [first reverse $ splitAt n events | n <- [0 .. length events]] + -- A real interleaving is one in which the thread that sent + -- the message to the TQueue has done some work since it was + -- scheduled, i.e. the TQueue writing action was not + -- artificially delayed + fakeInterleaving = + [ not $ hasDoneWork id2 before + | (before, (_, id2, _, EventTxCommitted w _ _) : _) <- events' + , Just "CONTROL" `elem` map l_label w -- has written to the CONTROL TQueue + ] + in counterexample (ppTrace trace) $ + -- If this was a fake interleaving just make it pass + property (or fakeInterleaving) + .||. ( fst $ + foldl' + ( \(prop, model) (cmd, resp) -> + let model' = transition model cmd resp + prop' = case logic (postcondition model cmd resp) of + VFalse ce -> counterexample ("Poscondition impossible! " <> show ce) $ property False + _ -> property True + in (prop .&&. prop', model') + ) + (property True, cmodel) + cmds + ) + in + ( prevProp .&&. porProp + , prevCmds ++ map fst p1' ++ map fst p2' + , env1 <> env2 + , undefined + , undefined + , foldl (\x (y, z) -> transition x y z) cmodel $ p1' ++ p2' + ) + + -- This is almost the same as @runSequential@ but it accumulates the concrete + -- commands. + runSequential' (prevProp, prevCmds, env, smodel, counter, cmodel) (Command scmd _ vars) = + let + -- Precondition + pPre = prec sm smodel scmd + + -- Simulate + ccmd = fromRight (error "runSequential: impossible") (reify env scmd) + prevCmds' = prevCmds ++ [ccmd] + simAction = do + sut <- initSut + sequence_ $ map (\c -> semantics sut c) prevCmds + semantics sut ccmd + (trace, cresp, prop) = runIOSim simAction + + -- Postcondition + pPost = post sm cmodel ccmd cresp False trace + pInv = inv sm cmodel False trace + + -- Mock + (pMock, cvars) = mockCheck ccmd cresp vars + (sresp, counter') = runGenSym (mock smodel scmd) counter + in + ( prevProp .&&. pPre .&&. prop .&&. pPost .&&. pInv .&&. pMock + , prevCmds' + , insertConcretes vars cvars env + , transition smodel scmd sresp + , counter' + , transition cmodel ccmd cresp + ) + +hasDoneWork :: (Eq p) => p -> [(a, p, c, SimEventType)] -> Bool +hasDoneWork idX evs = + go False evs + where + go acc [] = acc + go acc ((_, idY, _, ev) : next) + | idX /= idY = acc + | otherwise = + go + ( acc || case ev of + EventThrow{} -> True + EventThrowTo{} -> True + EventThreadForked{} -> True + EventTxCommitted{} -> True + EventTxAborted{} -> True + EventTxBlocked{} -> True + EventThreadDelay{} -> True + _ -> False + ) + next + +drainTQueue :: (MonadSTM m) => TQueue m a -> STM m [a] +drainTQueue tc = do + msg <- tryReadTQueue tc + case msg of + Nothing -> pure [] + Just v -> (v :) <$> drainTQueue tc + +{------------------------------------------------------------------------------- + Helpers +-------------------------------------------------------------------------------} + +-- | Check the precondition +prec :: + StateMachine model cmd sut resp -> + model Symbolic -> + cmd Symbolic -> + Property +prec StateMachine{precondition} smodel scmd = + let e ce = counterexample ("Precondition failed: " <> show ce) $ property False + in case logic (precondition smodel scmd) of + VFalse ce -> e ce + _otherwise -> property True + +-- | Check the postcondition +post :: + (Show a) => + StateMachine model cmd sut resp -> + model Concrete -> + cmd Concrete -> + resp Concrete -> + Bool -> + SimTrace a -> + Property +post StateMachine{postcondition} cmodel ccmd cresp wasRace trace = + case logic (postcondition cmodel ccmd cresp) of + VFalse ce -> + counterexample (ppTrace trace) + $ counterexample + ( (if wasRace then ("Race found! " <>) else id) + "Postcondition failed: " + <> show ce + ) + $ property False + _otherwise -> property True + +-- | Check the invariant +inv :: + (Show a) => + StateMachine model cmd sut resp -> + model Concrete -> + Bool -> + SimTrace a -> + Property +inv StateMachine{invariant} cmodel wasRace trace = + case logic (fromMaybe (const Top) invariant cmodel) of + VFalse ce -> + counterexample (ppTrace trace) + $ counterexample + ( (if wasRace then ("Race found! " <>) else id) + "Invariant broken: " + <> show ce + ) + $ property False + _otherwise -> property True + +mockCheck :: + ( Foldable t + , Rank2.Foldable resp + , Show (cmd Concrete) + , Show (t a) + , Show (resp Concrete) + ) => + cmd Concrete -> + resp Concrete -> + t a -> + (Property, [Dynamic]) +mockCheck ccmd cresp vars = + let cvars = Rank2.foldMap (\(Concrete x) -> [toDyn x]) cresp + in if length vars /= length cvars + then + let err = mockSemanticsMismatchError (ppShow ccmd) (ppShow vars) (ppShow cresp) (ppShow cvars) + in (counterexample ("Mock semantics mismatch: " <> err) $ property False, cvars) + else (property True, cvars) + +mockSemanticsMismatchError :: String -> String -> String -> String -> String +mockSemanticsMismatchError cmd svars cresp cvars = + unlines + [ "" + , "Mismatch between `mock` and `semantics`." + , "" + , "The definition of `mock` for the command:" + , "" + , " " + , cmd + , "" + , "returns the following references:" + , "" + , " " + , svars + , "" + , "while the response from `semantics`:" + , "" + , " " + , cresp + , "" + , "returns the following references:" + , "" + , " " + , cvars + , "" + , "Continuing to execute commands at this point could result in scope" + , "errors, because we might have commands that use references (returned" + , "by `mock`) that are not available (returned by `semantics`)." + , "" + ] diff --git a/io-sim/qsm/Test/StateMachine/IOSim/Generate.hs b/io-sim/qsm/Test/StateMachine/IOSim/Generate.hs new file mode 100644 index 00000000..553a9940 --- /dev/null +++ b/io-sim/qsm/Test/StateMachine/IOSim/Generate.hs @@ -0,0 +1,580 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} + +-- | + +module Test.StateMachine.IOSim.Generate + ( forAllCommands + , forAllParallelCommands + , forAllNParallelCommands + ) where + +import Control.Monad.State +import Data.Bifunctor +import Data.List qualified as L +import Data.Map (Map) +import Data.Map.Strict qualified as M +import Data.Maybe +import Test.QuickCheck +import Test.StateMachine.IOSim.Types (StateMachine (..)) +import Test.StateMachine.Logic +import Test.StateMachine.Types hiding (StateMachine (..)) +import Test.StateMachine.Types.Rank2 qualified as Rank2 +import Test.StateMachine.Utils +import Text.Show.Pretty hiding (reify) + +forAllCommands :: Testable prop + => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) + => (Rank2.Traversable cmd, Rank2.Foldable resp) + => StateMachine model cmd sut resp + -> Maybe Int -- ^ Minimum number of commands. + -> (Commands cmd resp -> prop) -- ^ Predicate. + -> Property +forAllCommands sm mminSize = + forAllShrinkShow (generateCommands sm mminSize) (shrinkCommands sm) ppShow + +deadlockError :: (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) + => model Symbolic -> [Command cmd resp] -> String -> b +deadlockError model generated counterexamples = error $ concat + [ "\n" + , "A deadlock occured while generating commands.\n" + , "No pre-condition holds in the following model:\n\n" + , " " ++ ppShow model + , "\n\nThe following commands have been generated so far:\n\n" + , " " ++ ppShow generated + , "\n\n" + , "Example commands generated whose pre-condition doesn't hold:\n\n" + , " " ++ counterexamples + , "\n" + ] + +generateCommands :: (Rank2.Foldable resp, Show (model Symbolic)) + => (Show (cmd Symbolic), Show (resp Symbolic)) + => StateMachine model cmd sut resp + -> Maybe Int -- ^ Minimum number of commands. + -> Gen (Commands cmd resp) +generateCommands sm@StateMachine {..} mminSize = + evalStateT (generateCommandsState sm newCounter mminSize) initModel + +generateCommandsState :: forall model cmd sut resp. Rank2.Foldable resp + => (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) + => StateMachine model cmd sut resp + -> Counter + -> Maybe Int -- ^ Minimum number of commands. + -> StateT (model Symbolic) Gen (Commands cmd resp) +generateCommandsState StateMachine {..} counter0 mminSize = do + let minSize = fromMaybe 0 mminSize + size0 <- lift (sized (\k -> choose (minSize, k + minSize))) + go size0 counter0 [] + where + go :: Int -> Counter -> [Command cmd resp] + -> StateT (model Symbolic) Gen (Commands cmd resp) + go 0 _ cmds = return (Commands (reverse cmds)) + go size counter cmds = do + model <- get + case generator model of + Nothing -> return (Commands (reverse cmds)) + Just gen -> do + enext <- lift $ gen `suchThatEither` (boolean . precondition model) + case enext of + Left ces -> deadlockError model (reverse cmds) (ppShow ces) + Right next -> do + let (resp, counter') = runGenSym (mock model next) counter + put (transition model next resp) + go (size - 1) counter' (Command next resp (getUsedVars resp) : cmds) + +getUsedVars :: Rank2.Foldable f => f Symbolic -> [Var] +getUsedVars = Rank2.foldMap (\(Symbolic v) -> [v]) + +-- | Shrink commands in a pre-condition and scope respecting way. +shrinkCommands :: forall model cmd sut resp. (Rank2.Traversable cmd, Rank2.Foldable resp) + => StateMachine model cmd sut resp -> Commands cmd resp + -> [Commands cmd resp] +shrinkCommands sm@StateMachine {..} = + concatMap go . shrinkListS' . unCommands + where + go :: Shrunk [Command cmd resp] -> [Commands cmd resp] + go (Shrunk shrunk cmds) = map snd $ + shrinkAndValidate sm + (if shrunk then DontShrink else MustShrink) + (initValidateEnv initModel) + (Commands cmds) + +-- | Environment required during 'shrinkAndValidate' +data ValidateEnv model = ValidateEnv { + -- | The model we're starting validation from + veModel :: model Symbolic + + -- | Reference renumbering + -- + -- When a command + -- + -- > Command .. [Var i, ..] + -- + -- is changed during validation to + -- + -- > Command .. [Var j, ..] + -- + -- then any subsequent uses of @Var i@ should be replaced by @Var j@. This + -- is recorded in 'veScope'. When we /remove/ the first command + -- altogether (during shrinking), then @Var i@ won't appear in the + -- 'veScope' and shrank candidates that contain commands referring to @Var + -- i@ should be considered as invalid. + , veScope :: Map Var Var + + -- | Counter (for generating new references) + , veCounter :: Counter + } + +initValidateEnv :: model Symbolic -> ValidateEnv model +initValidateEnv initModel = ValidateEnv { + veModel = initModel + , veScope = M.empty + , veCounter = newCounter + } + +data ShouldShrink = MustShrink | DontShrink + +-- | Validate list of commands, optionally shrinking one of the commands +-- +-- The input to this function is a list of commands ('Commands'), for example +-- +-- > [A, B, C, D, E, F, G, H] +-- +-- The /result/ is a /list/ of 'Commands', i.e. a list of lists. The +-- outermost list is used for all the shrinking possibilities. For example, +-- let's assume we haven't shrunk something yet, and therefore need to shrink +-- one of the commands. Let's further assume that only commands B and E can be +-- shrunk, to B1, B2 and E1, E2, E3 respectively. Then the result will look +-- something like +-- +-- > [ -- outermost list recording all the shrink possibilities +-- > [A', B1', C', D', E' , F', G', H'] -- B shrunk to B1 +-- > , [A', B2', C', D', E' , F', G', H'] -- B shrunk to B2 +-- > , [A', B' , C', D', E1', F', G', H'] -- E shrunk to E1 +-- > , [A', B' , C', D', E2', F', G', H'] -- E shrunk to E2 +-- > , [A', B' , C', D', E3', F', G', H'] -- E shrunk to E3 +-- > ] +-- +-- where one of the commands has been shrunk and all commands have been +-- validated and renumbered (references updated). So, in this example, the +-- result will contain at most 5 lists; it may contain fewer, since some of +-- these lists may not be valid. +-- +-- If we _did_ already shrink something, then no commands will be shrunk, and +-- the resulting list will either be empty (if the list of commands was invalid) +-- or contain a /single/ element with the validated and renumbered commands. +shrinkAndValidate :: forall model cmd sut resp. (Rank2.Traversable cmd, Rank2.Foldable resp) + => StateMachine model cmd sut resp + -> ShouldShrink + -> ValidateEnv model + -> Commands cmd resp + -> [(ValidateEnv model, Commands cmd resp)] +shrinkAndValidate StateMachine {..} = + \env shouldShrink cmds -> map (second Commands) $ go env shouldShrink (unCommands cmds) + where + go :: ShouldShrink -> ValidateEnv model -> [Command cmd resp] -> [(ValidateEnv model, [Command cmd resp])] + go MustShrink _ [] = [] -- we failed to shrink anything + go DontShrink env [] = [(env, [])] -- successful termination + go shouldShrink (ValidateEnv model scope counter) (Command cmd' _resp vars' : cmds) = + case Rank2.traverse (remapVars scope) cmd' of + Just remapped -> + -- shrink at most one command + let candidates :: [(ShouldShrink, cmd Symbolic)] + candidates = + case shouldShrink of + DontShrink -> [(DontShrink, remapped)] + MustShrink -> map (DontShrink,) (shrinker model remapped) + ++ [(MustShrink, remapped)] + in flip concatMap candidates $ \(shouldShrink', cmd) -> + if boolean (precondition model cmd) + then let (resp, counter') = runGenSym (mock model cmd) counter + vars = getUsedVars resp + env' = ValidateEnv { + veModel = transition model cmd resp + , veScope = M.fromList (zip vars' vars) `M.union` scope + , veCounter = counter' + } + in map (second (Command cmd resp vars:)) $ go shouldShrink' env' cmds + else [] + Nothing -> + [] + + remapVars :: Map Var Var -> Symbolic a -> Maybe (Symbolic a) + remapVars scope (Symbolic v) = Symbolic <$> M.lookup v scope + + +------------------------------------------------------------------------ + +forAllParallelCommands :: Testable prop + => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) + => (Rank2.Traversable cmd, Rank2.Foldable resp) + => StateMachine model cmd sut resp + -> Maybe Int + -> (ParallelCommands cmd resp -> prop) -- ^ Predicate. + -> Property +forAllParallelCommands sm mminSize prop = + forAllShrinkShow (generateParallelCommands sm mminSize) (shrinkParallelCommands sm) ppShow prop + +forAllNParallelCommands :: Testable prop + => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) + => (Rank2.Traversable cmd, Rank2.Foldable resp) + => StateMachine model cmd sut resp + -> Int -- ^ Number of threads + -> (NParallelCommands cmd resp -> prop) -- ^ Predicate. + -> Property +forAllNParallelCommands sm np prop = + forAllShrinkShow (generateNParallelCommands sm np) (shrinkNParallelCommands sm) ppShow prop + +-- | Generate parallel commands. +-- +-- Parallel commands are generated as follows. We begin by generating +-- sequential commands and then splitting this list in two at some index. The +-- first half will be used as the prefix. +-- +-- The second half will be used to build suffixes. For example, starting from +-- the following sequential commands: +-- +-- > [A, B, C, D, E, F, G, H, I] +-- +-- We split it in two, giving us the prefix and the rest: +-- +-- > prefix: [A, B] +-- > rest: [C, D, E, F, G, H, I] +-- +-- We advance the model with the prefix. +-- +-- __Make a suffix__: we take commands from @rest@ as long as these are +-- parallel safe (see 'parallelSafe'). This means that the pre-conditions +-- (using the \'advanced\' model) of each of those commands will hold no +-- matter in which order they are executed. +-- +-- Say this is true for @[C, D, E]@, but not anymore for @F@, maybe because +-- @F@ depends on one of @[C, D, E]@. Then we divide this \'chunk\' in two by +-- splitting it in the middle, obtaining @[C]@ and @[D, E]@. These two halves +-- of the chunk (stored as a 'Pair') will later be executed in parallel. +-- Together they form one suffix. +-- +-- Then the model is advanced using the whole chunk @[C, D, E]@. Think of it +-- as a barrier after executing the two halves of the chunk in parallel. Then +-- this process of building a chunk/suffix repeats itself, starting from +-- __Make a suffix__ using the \'advanced\' model. +-- +-- In the end we might end up with something like this: +-- +-- > ┌─ [C] ──┐ ┌ [F, G] ┐ +-- > [A, B] ─┤ ├──┤ │ +-- > └ [D, E] ┘ └ [H, I] ┘ +-- +generateParallelCommands :: forall model cmd sut resp. Rank2.Foldable resp + => Show (model Symbolic) + => (Show (cmd Symbolic), Show (resp Symbolic)) + => StateMachine model cmd sut resp + -> Maybe Int + -> Gen (ParallelCommands cmd resp) +generateParallelCommands sm@StateMachine { initModel } mminSize = do + Commands cmds <- generateCommands sm mminSize + prefixLength <- sized (\k -> choose (0, k `div` 3)) + let (prefix, rest) = bimap Commands Commands (splitAt prefixLength cmds) + return (ParallelCommands prefix + (makeSuffixes (advanceModel sm initModel prefix) rest)) + where + makeSuffixes :: model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)] + makeSuffixes model0 = go model0 [] . unCommands + where + go _ acc [] = reverse acc + go model acc cmds = go (advanceModel sm model (Commands safe)) + (Pair (Commands safe1) (Commands safe2) : acc) + rest + where + (safe, rest) = spanSafe sm model [] cmds + (safe1, safe2) = splitAt (length safe `div` 2) safe + +-- Split the list of commands in two such that the first half is a +-- list of commands for which the preconditions of all commands hold +-- for permutation of the list, i.e. it is parallel safe. The other +-- half is the remainder of the input list. +spanSafe :: Rank2.Foldable resp + => StateMachine model cmd sut resp + -> model Symbolic -> [Command cmd resp] -> [Command cmd resp] + -> ([Command cmd resp], [Command cmd resp]) +spanSafe _ _ safe [] = (reverse safe, []) +spanSafe sm model safe (cmd : cmds) + | length safe <= 5 + , parallelSafe sm model (Commands (cmd : safe)) + = spanSafe sm model (cmd : safe) cmds + | otherwise + = (reverse safe, cmd : cmds) + +-- Generate Parallel commands. The length of each suffix, indicates how many thread can +-- concurrently execute the commands safely. +generateNParallelCommands :: forall model cmd sut resp. Rank2.Foldable resp + => Show (model Symbolic) + => (Show (cmd Symbolic), Show (resp Symbolic)) + => StateMachine model cmd sut resp + -> Int + -> Gen (NParallelCommands cmd resp) +generateNParallelCommands sm@StateMachine { initModel } np = + if np <= 0 then error "number of threads must be positive" else do + Commands cmds <- generateCommands sm Nothing + prefixLength <- sized (\k -> choose (0, k `div` 3)) + let (prefix, rest) = bimap Commands Commands (splitAt prefixLength cmds) + return (ParallelCommands prefix + (makeSuffixes (advanceModel sm initModel prefix) rest)) + where + makeSuffixes :: model Symbolic -> Commands cmd resp -> [[Commands cmd resp]] + makeSuffixes model0 = go model0 [] . unCommands + where + go :: model Symbolic + -> [[Commands cmd resp]] + -> [Command cmd resp] + -> [[Commands cmd resp]] + go _ acc [] = reverse acc + go model acc cmds = go (advanceModel sm model (Commands safe)) + (safes : acc) + rest + where + (safe, rest) = spanSafe sm model [] cmds + safes = Commands <$> chunksOf np (length safe `div` np) safe + + -- Split the list in n sublists, whose concat is the initial list. + -- We try to keep the length of each sublist len. + -- + -- It is important that we miss no elements here or else executeCommands may fail, because + -- of missing references. It is also important that the final list has the correct length + -- n, or else there will be different number of threads than the user specified. + chunksOf :: Int -> Int -> [a] -> [[a]] + chunksOf 1 _ xs = [xs] + chunksOf n len xs = as : chunksOf (n-1) len bs + where (as, bs) = splitAt len xs + + +-- | A list of commands is parallel safe if the pre-conditions for all commands +-- hold in all permutations of the list. +parallelSafe :: Rank2.Foldable resp + => StateMachine model cmd sut resp -> model Symbolic + -> Commands cmd resp -> Bool +parallelSafe StateMachine { precondition, transition, mock } model0 + = all (preconditionsHold model0) + . L.permutations + . unCommands + where + preconditionsHold _ [] = True + preconditionsHold model (Command cmd resp vars : cmds) = + boolean (precondition model cmd) && + preconditionsHold (transition model cmd resp) cmds && + -- This makes sure that in all permutations the length of variables created is the same. + -- By doing so, we try to avoid MockSemanticsMismatch errors. + -- More https://github.com/advancedtelematic/quickcheck-state-machine/pull/348 + length vars == length (getUsedVars $ fst $ runGenSym (mock model cmd) newCounter) + +-- | Apply the transition of some commands to a model. +advanceModel :: StateMachine model cmd sut resp + -> model Symbolic -- ^ The model. + -> Commands cmd resp -- ^ The commands. + -> model Symbolic +advanceModel StateMachine { transition } model0 = + go model0 . unCommands + where + go model [] = model + go model (Command cmd resp _vars : cmds) = + go (transition model cmd resp) cmds + +------------------------------------------------------------------------ + +-- | Shrink a parallel program in a pre-condition and scope respecting +-- way. +shrinkParallelCommands + :: forall cmd model sut resp. Rank2.Traversable cmd + => Rank2.Foldable resp + => StateMachine model cmd sut resp + -> (ParallelCommands cmd resp -> [ParallelCommands cmd resp]) +shrinkParallelCommands sm (ParallelCommands prefix suffixes) + = concatMap go + [ Shrunk s (ParallelCommands prefix' (map toPair suffixes')) + | Shrunk s (prefix', suffixes') <- shrinkPairS shrinkCommands' shrinkSuffixes + (prefix, map fromPair suffixes) + ] + ++ + shrinkMoveSuffixToPrefix + where + go :: Shrunk (ParallelCommands cmd resp) -> [ParallelCommands cmd resp] + go (Shrunk shrunk cmds) = + shrinkAndValidateParallel sm + (if shrunk then DontShrink else MustShrink) + cmds + + shrinkSuffixes :: [(Commands cmd resp, Commands cmd resp)] + -> [Shrunk [(Commands cmd resp, Commands cmd resp)]] + shrinkSuffixes = shrinkListS (shrinkPairS' shrinkCommands') + + -- Moving a command from a suffix to the prefix preserves validity + shrinkMoveSuffixToPrefix :: [ParallelCommands cmd resp] + shrinkMoveSuffixToPrefix = case suffixes of + [] -> [] + (suffix : suffixes') -> + [ ParallelCommands (prefix <> Commands [prefix']) + (fmap Commands (toPair suffix') : suffixes') + | (prefix', suffix') <- pickOneReturnRest2 (unCommands (proj1 suffix), + unCommands (proj2 suffix)) + ] + +-- | Shrink a parallel program in a pre-condition and scope respecting +-- way. +shrinkNParallelCommands + :: forall cmd model sut resp. Rank2.Traversable cmd + => Rank2.Foldable resp + => StateMachine model cmd sut resp + -> (NParallelCommands cmd resp -> [NParallelCommands cmd resp]) +shrinkNParallelCommands sm (ParallelCommands prefix suffixes) + = concatMap go + [ Shrunk s (ParallelCommands prefix' suffixes') + | Shrunk s (prefix', suffixes') <- shrinkPairS shrinkCommands' shrinkSuffixes + (prefix, suffixes) + ] + ++ + shrinkMoveSuffixToPrefix + where + go :: Shrunk (NParallelCommands cmd resp) -> [NParallelCommands cmd resp] + go (Shrunk shrunk cmds) = + shrinkAndValidateNParallel sm + (if shrunk then DontShrink else MustShrink) + cmds + + shrinkSuffixes :: [[Commands cmd resp]] + -> [Shrunk [[Commands cmd resp]]] + shrinkSuffixes = shrinkListS (shrinkListS'' shrinkCommands') + + -- Moving a command from a suffix to the prefix preserves validity + shrinkMoveSuffixToPrefix :: [NParallelCommands cmd resp] + shrinkMoveSuffixToPrefix = case suffixes of + [] -> [] + (suffix : suffixes') -> + [ ParallelCommands (prefix <> Commands [prefix']) + (fmap Commands suffix' : suffixes') + | (prefix', suffix') <- pickOneReturnRestL (unCommands <$> suffix) + ] + +-- | Shrinks Commands in a way that it has strictly less number of commands. +shrinkCommands' :: Commands cmd resp -> [Shrunk (Commands cmd resp)] +shrinkCommands' = map (fmap Commands) . shrinkListS' . unCommands + +shrinkAndValidateParallel :: forall model cmd sut resp. (Rank2.Traversable cmd, Rank2.Foldable resp) + => StateMachine model cmd sut resp + -> ShouldShrink + -> ParallelCommands cmd resp + -> [ParallelCommands cmd resp] +shrinkAndValidateParallel sm@StateMachine { initModel } = \shouldShrink (ParallelCommands prefix suffixes) -> + let env = initValidateEnv initModel + curryGo shouldShrink' (env', prefix') = go prefix' env' shouldShrink' suffixes in + case shouldShrink of + DontShrink -> concatMap (curryGo DontShrink) (shrinkAndValidate sm DontShrink env prefix) + MustShrink -> concatMap (curryGo DontShrink) (shrinkAndValidate sm MustShrink env prefix) + ++ concatMap (curryGo MustShrink) (shrinkAndValidate sm DontShrink env prefix) + where + go :: Commands cmd resp -- validated prefix + -> ValidateEnv model -- environment after the prefix + -> ShouldShrink -- should we /still/ shrink something? + -> [Pair (Commands cmd resp)] -- suffixes to validate + -> [ParallelCommands cmd resp] + go prefix' = go' [] + where + go' :: [Pair (Commands cmd resp)] -- accumulated validated suffixes (in reverse order) + -> ValidateEnv model -- environment after the validated suffixes + -> ShouldShrink -- should we /still/ shrink something? + -> [Pair (Commands cmd resp)] -- suffixes to validate + -> [ParallelCommands cmd resp] + go' _ _ MustShrink [] = [] -- Failed to shrink something + go' acc _ DontShrink [] = [ParallelCommands prefix' (reverse acc)] + go' acc env shouldShrink (Pair l r : suffixes) = do + ((shrinkL, shrinkR), shrinkRest) <- shrinkOpts + (envL, l') <- shrinkAndValidate sm shrinkL env l + (envR, r') <- shrinkAndValidate sm shrinkR (env `withCounterFrom` envL) r + go' (Pair l' r' : acc) (combineEnv sm envL envR r') shrinkRest suffixes + where + + shrinkOpts :: [((ShouldShrink, ShouldShrink), ShouldShrink)] + shrinkOpts = + case shouldShrink of + DontShrink -> [ ((DontShrink, DontShrink), DontShrink) ] + MustShrink -> [ ((MustShrink, DontShrink), DontShrink) + , ((DontShrink, MustShrink), DontShrink) + , ((DontShrink, DontShrink), MustShrink) ] + +combineEnv :: StateMachine model cmd sut resp + -> ValidateEnv model + -> ValidateEnv model + -> Commands cmd resp + -> ValidateEnv model +combineEnv sm envL envR cmds = ValidateEnv { + veModel = advanceModel sm (veModel envL) cmds + , veScope = M.union (veScope envL) (veScope envR) + , veCounter = veCounter envR + } + +withCounterFrom :: ValidateEnv model -> ValidateEnv model -> ValidateEnv model +withCounterFrom e e' = e { veCounter = veCounter e' } + +shrinkAndValidateNParallel :: forall model cmd sut resp. (Rank2.Traversable cmd, Rank2.Foldable resp) + => StateMachine model cmd sut resp + -> ShouldShrink + -> NParallelCommands cmd resp + -> [NParallelCommands cmd resp] +shrinkAndValidateNParallel sm = \shouldShrink (ParallelCommands prefix suffixes) -> + let env = initValidateEnv $ initModel sm + curryGo shouldShrink' (env', prefix') = go prefix' env' shouldShrink' suffixes in + case shouldShrink of + DontShrink -> concatMap (curryGo DontShrink) (shrinkAndValidate sm DontShrink env prefix) + MustShrink -> concatMap (curryGo DontShrink) (shrinkAndValidate sm MustShrink env prefix) + ++ concatMap (curryGo MustShrink) (shrinkAndValidate sm DontShrink env prefix) + where + + go :: Commands cmd resp -- validated prefix + -> ValidateEnv model -- environment after the prefix + -> ShouldShrink -- should we /still/ shrink something? + -> [[Commands cmd resp]] -- suffixes to validate + -> [NParallelCommands cmd resp] + go prefix' = go' [] + where + go' :: [[Commands cmd resp]] -- accumulated validated suffixes (in reverse order) + -> ValidateEnv model -- environment after the validated suffixes + -> ShouldShrink -- should we /still/ shrink something? + -> [[Commands cmd resp]] -- suffixes to validate + -> [NParallelCommands cmd resp] + go' _ _ MustShrink [] = [] -- Failed to shrink something + go' acc _ DontShrink [] = [ParallelCommands prefix' (reverse acc)] + go' acc env shouldShrink (suffix : suffixes) = do + (suffixWithShrinks, shrinkRest) <- shrinkOpts suffix + (envFinal, suffix') <- snd $ foldl f (True, [(env,[])]) suffixWithShrinks + go' (reverse suffix' : acc) envFinal shrinkRest suffixes + where + + f :: (Bool, [(ValidateEnv model, [Commands cmd resp])]) + -> (ShouldShrink, Commands cmd resp) + -> (Bool, [(ValidateEnv model, [Commands cmd resp])]) + f (firstCall, acc') (toShrink, cmds) = (False, acc'') + where + acc'' = do + (envPrev, cmdsPrev) <- acc' + let envUsed = if firstCall then env else env `withCounterFrom` envPrev + (env', cmd') <- shrinkAndValidate sm toShrink envUsed cmds + let env'' = if firstCall then env' else + combineEnv sm envPrev env' cmd' + return (env'', cmd' : cmdsPrev) + + shrinkOpts :: [a] -> [([(ShouldShrink, a)], ShouldShrink)] + shrinkOpts ls = + let len = length ls + dontShrink = replicate len DontShrink + shrinks = if len == 0 + then error "Invariant violation! A suffix should never be an empty list" + else flip map [1..len] $ \n -> + replicate (n - 1) DontShrink ++ [MustShrink] ++ replicate (len - n) DontShrink + in case shouldShrink of + DontShrink -> [(zip dontShrink ls, DontShrink)] + MustShrink -> fmap (\shrinkLs -> (zip shrinkLs ls, DontShrink)) shrinks + ++ [(zip dontShrink ls, MustShrink)] diff --git a/io-sim/qsm/Test/StateMachine/IOSim/Types.hs b/io-sim/qsm/Test/StateMachine/IOSim/Types.hs new file mode 100644 index 00000000..ec01982a --- /dev/null +++ b/io-sim/qsm/Test/StateMachine/IOSim/Types.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE RankNTypes #-} +-- | + +module Test.StateMachine.IOSim.Types (StateMachine (..)) where + +import Control.Monad.IOSim +import Data.Functor.Classes +import Test.QuickCheck +import Test.StateMachine.Logic +import Test.StateMachine.Types hiding (StateMachine (..)) + +data StateMachine model cmd sut resp = StateMachine + { initModel :: forall r. model r + , transition :: forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r + , precondition :: model Symbolic -> cmd Symbolic -> Logic + , postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic + , invariant :: Maybe (model Concrete -> Logic) + , generator :: model Symbolic -> Maybe (Gen (cmd Symbolic)) + , shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic] + , initSut :: forall s. IOSim s (sut (IOSim s)) + , semantics :: forall s. sut (IOSim s) -> cmd Concrete -> IOSim s (resp Concrete) + , mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) + }