{-# LANGUAGE DataKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} ----------------------------------------------------------------------------- -- | -- Module : Test.StateMachine.Internal.Parallel -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) -- -- Maintainer : Stevan Andjelkovic -- Stability : provisional -- Portability : non-portable (GHC extensions) -- -- This module contains the building blocks needed to implement the -- 'Test.StateMachine.parallelProperty' helper. -- ----------------------------------------------------------------------------- module Test.StateMachine.Internal.Parallel ( liftGenFork , liftGenFork' , liftShrinkFork , liftSemFork , checkParallelInvariant ) where import Control.Concurrent (threadDelay) import Control.Concurrent.ParallelIO.Local (parallel_, withPool) import Control.Concurrent.STM (STM, atomically) import Control.Concurrent.STM.TChan (TChan, newTChanIO, tryReadTChan, writeTChan) import Control.Monad (foldM) import Control.Monad.State (StateT, evalStateT, execStateT, lift) import Data.Dynamic (Dynamic, fromDynamic, toDyn) import Data.Kind (Type) import Data.List (partition) import qualified Data.Map as M import Data.Maybe (fromMaybe) import Data.Singletons.Decide (SDecide) import Data.Singletons.Prelude (DemoteRep, SingKind, TyFun, fromSing) import Data.Tree (Tree(Node)) import Data.Typeable (Typeable) import System.Random (randomRIO) import Test.QuickCheck (Gen, Property, counterexample, property, (.&&.)) import Test.QuickCheck.Monadic (PropertyM) import Text.PrettyPrint.ANSI.Leijen (Doc, Pretty, pretty, prettyList, text, vsep, (<+>)) import Test.StateMachine.Internal.IxMap (IxMap) import qualified Test.StateMachine.Internal.IxMap as IxM import Test.StateMachine.Internal.Sequential import Test.StateMachine.Internal.Types import Test.StateMachine.Internal.Types.IntRef (showRef) import Test.StateMachine.Internal.Utils import Test.StateMachine.Internal.Utils.BoxDrawer import Test.StateMachine.Types ------------------------------------------------------------------------ -- | Lift a generator of untyped commands with reference placeholders -- into a generator of forks of untyped internal commands. liftGenFork :: Ord ix => SingKind ix => DemoteRep ix ~ ix => IxTraversable cmd => HasResponse cmd => Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Generator to be lifted. -> Gen (Fork [IntRefed cmd]) liftGenFork gen = liftGenFork' (lift gen) () liftGenFork' :: Ord ix => SingKind ix => DemoteRep ix ~ ix => IxTraversable cmd => HasResponse cmd => StateT genState Gen (Untyped cmd (RefPlaceholder ix)) -> genState -> Gen (Fork [IntRefed cmd]) liftGenFork' gen gs = do ((prefix, gs'), ns) <- liftGen' gen gs 0 M.empty left <- fst . fst <$> liftGen' gen gs' 1 ns right <- fst . fst <$> liftGen' gen gs' 2 ns return $ Fork (map (\(IntRefed cmd miref) -> IntRefed (ifmap (fixPid ns) cmd) miref) left) prefix (map (\(IntRefed cmd miref) -> IntRefed (ifmap (fixPid ns) cmd) miref) right) where fixPid ns i iref@(IntRef (Ref ref) _) | ref <= ns M.! fromSing i = IntRef (Ref ref) 0 | otherwise = iref ------------------------------------------------------------------------ -- | Lift a shrinker of internal commands into a shrinker of forks of -- untyped internal commands. liftShrinkFork :: forall cmd . IxFoldable cmd => HasResponse cmd => (forall resp. Shrinker (cmd ConstIntRef resp)) -- ^ Shrinker to be lifted. -> Shrinker (Fork [IntRefed cmd]) liftShrinkFork shrinker f@(Fork l0 p0 r0) = -- Only shrink the branches: [ Fork l' p0 r' | (l', r') <- shrinkPair (liftShrink shrinker) (liftShrink shrinker) (l0, r0) ] ++ -- Only shrink the prefix: shrinkPrefix f where shrinkPrefix :: Fork [IntRefed cmd] -> [Fork [IntRefed cmd]] shrinkPrefix (Fork _ [] _) = [] shrinkPrefix (Fork l (p : ps) r) = [ Fork l' [] r' ] ++ [ Fork l'' (removeCommands p ps) r'' ] ++ [ Fork l''' (p' : ps') r''' | (p', Fork l''' ps' r''') <- shrinkPair (liftShrinker shrinker) shrinkPrefix (p, Fork l ps r) ] where l' = removeManyCommands (p : ps) l r' = removeManyCommands (p : ps) r l'' = removeCommands p l r'' = removeCommands p r removeManyCommands :: [IntRefed cmd] -> [IntRefed cmd] -> [IntRefed cmd] removeManyCommands [] ds = ds removeManyCommands (c : cs) ds = removeManyCommands cs (removeCommands c ds) ------------------------------------------------------------------------ type History cmd = [HistoryEvent (IntRefed cmd)] data HistoryEvent cmd = InvocationEvent cmd Pid | ResponseEvent Dynamic Pid getProcessIdEvent :: HistoryEvent cmd -> Pid getProcessIdEvent (InvocationEvent _ pid) = pid getProcessIdEvent (ResponseEvent _ pid) = pid data Operation cmd = forall resp. (Show (GetResponse_ resp), HasResponse cmd, Typeable resp, Typeable (Response_ ConstIntRef resp)) => Operation (cmd ConstIntRef resp) (Response_ ConstIntRef resp) Pid instance (ShowCmd cmd, IxFunctor cmd) => Pretty (Operation cmd) where pretty (Operation cmd resp _) = text (showCmd $ ifmap (const showRef) cmd) <+> text "-->" <+> text (showResponse_ (response cmd) resp) prettyList = vsep . map pretty takeInvocations :: History cmd -> [HistoryEvent (IntRefed cmd)] takeInvocations = takeWhile $ \h -> case h of InvocationEvent _ _ -> True _ -> False findCorrespondingResp :: Pid -> History cmd -> [(Dynamic, History cmd)] findCorrespondingResp _ [] = [] findCorrespondingResp pid (ResponseEvent resp pid' : es) | pid == pid' = [(resp, es)] findCorrespondingResp pid (e : es) = [ (resp, e : es') | (resp, es') <- findCorrespondingResp pid es ] linearTree :: HasResponse cmd => History cmd -> [Tree (Operation cmd)] linearTree [] = [] linearTree es = [ Node (Operation cmd (dynResp resp) pid) (linearTree es') | InvocationEvent (IntRefed cmd _) pid <- takeInvocations es , (resp, es') <- findCorrespondingResp pid $ filter1 (not . matchInv pid) es ] where dynResp resp = fromMaybe (error "linearTree: impossible.") (fromDynamic resp) filter1 :: (a -> Bool) -> [a] -> [a] filter1 _ [] = [] filter1 p (x : xs) | p x = x : filter1 p xs | otherwise = xs -- Hmm, is this enough? matchInv pid (InvocationEvent _ pid') = pid == pid' matchInv _ _ = False linearise :: forall cmd model . HasResponse cmd => StateMachineModel model cmd -> History cmd -> Property linearise _ [] = property True linearise StateMachineModel {..} xs0 = anyP (step initialModel) . linearTree $ xs0 where step :: model ConstIntRef -> Tree (Operation cmd) -> Property step m (Node (Operation cmd resp _) roses) = postcondition m cmd resp .&&. anyP' (step (transition m cmd resp)) roses where anyP' :: (a -> Property) -> [a] -> Property anyP' _ [] = property True anyP' p xs = anyP p xs ------------------------------------------------------------------------ toForkOfOps :: forall cmd. HasResponse cmd => History cmd -> Fork [Operation cmd] toForkOfOps h = Fork (mkOps l) p' (mkOps r) where (p, h') = partition (\e -> getProcessIdEvent e == 0) h (l, r) = partition (\e -> getProcessIdEvent e == 1) h' p' = mkOps p mkOps :: [HistoryEvent (IntRefed cmd)] -> [Operation cmd] mkOps [] = [] mkOps (InvocationEvent (IntRefed cmd _) _ : ResponseEvent resp pid : es) = Operation cmd (dynResp resp) pid : mkOps es where dynResp = fromMaybe (error "toForkOfOps: impossible.") . fromDynamic mkOps _ = error "mkOps: Impossible." toBoxDrawings :: forall cmd. (IxFunctor cmd, ShowCmd cmd, HasResponse cmd) => History cmd -> Doc toBoxDrawings h = exec evT (fmap out (toForkOfOps h)) where out :: [Operation cmd] -> [String] out [] = [] out (Operation cmd resp _ : os) = showCmd (ifmap (const showRef) cmd) : showResponse_ (response cmd) resp : out os toEventType :: History cmd -> [(EventType, Pid)] toEventType = map $ \e -> case e of InvocationEvent _ pid -> (Open, pid) ResponseEvent _ pid -> (Close, pid) evT :: [(EventType, Pid)] evT = toEventType (filter (\e -> getProcessIdEvent e `elem` [1,2]) h) ------------------------------------------------------------------------ data HistoryKit cmd refs = HistoryKit { getHistoryChannel :: TChan (HistoryEvent (IntRefed cmd)) , getProcessIdHistory :: Pid } mkHistoryKit :: Pid -> IO (HistoryKit cmd refs) mkHistoryKit pid = do chan <- newTChanIO return $ HistoryKit chan pid runMany :: SDecide ix => IxFunctor cmd => HasResponse cmd => HistoryKit cmd ConstIntRef -> (forall resp. cmd refs resp -> IO (Response_ refs resp)) -> [IntRefed cmd] -> StateT (IxMap ix IntRef refs) IO () runMany kit sem = flip foldM () $ \_ cmd'@(IntRefed cmd iref) -> do lift $ atomically $ writeTChan (getHistoryChannel kit) $ InvocationEvent cmd' (getProcessIdHistory kit) resp <- liftSem sem cmd iref lift $ do threadDelay =<< randomRIO (0, 20) atomically $ writeTChan (getHistoryChannel kit) $ ResponseEvent (toDyn resp) (getProcessIdHistory kit) -- | Lift the semantics of a single typed command into a semantics for -- forks of untyped internal commands. The prefix of the fork is -- executed sequentially, while the two suffixes are executed in -- parallel, and the result (or trace) is collected in a so called -- history. liftSemFork :: forall (ix :: Type) (cmd :: Signature ix) (refs :: TyFun ix Type -> Type) . SDecide ix => IxFunctor cmd => HasResponse cmd => (forall resp. cmd refs resp -> IO (Response_ refs resp)) -- ^ Semantics to be lifted. -> Fork [IntRefed cmd] -> IO (History cmd) liftSemFork sem (Fork left prefix right) = do kit <- mkHistoryKit 0 env <- execStateT (runMany kit sem prefix) IxM.empty withPool 2 $ \pool -> parallel_ pool [ evalStateT (runMany (kit { getProcessIdHistory = 1}) sem left) env , evalStateT (runMany (kit { getProcessIdHistory = 2}) sem right) env ] getChanContents $ getHistoryChannel kit where getChanContents :: forall a. TChan a -> IO [a] getChanContents chan = reverse <$> atomically (go []) where go :: [a] -> STM [a] go acc = do mx <- tryReadTChan chan case mx of Just x -> go $ x : acc Nothing -> return acc -- | Check if a history can be linearised. checkParallelInvariant :: (ShowCmd cmd, IxFunctor cmd, HasResponse cmd) => StateMachineModel model cmd -> History cmd -> PropertyM IO () checkParallelInvariant smm hist = liftProperty . counterexample (("Couldn't linearise:\n\n" ++) $ show $ toBoxDrawings hist) $ linearise smm hist