{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} ----------------------------------------------------------------------------- -- | -- Module : Test.StateMachine.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 helpers for generating, shrinking, and checking -- parallel programs. -- ----------------------------------------------------------------------------- module Test.StateMachine.Parallel ( forAllNParallelCommands , forAllParallelCommands , generateNParallelCommands , generateParallelCommands , shrinkNParallelCommands , shrinkParallelCommands , shrinkAndValidateNParallel , shrinkAndValidateParallel , shrinkCommands' , runNParallelCommands , runParallelCommands , runParallelCommands' , runNParallelCommandsNTimes , runParallelCommandsNTimes , runNParallelCommandsNTimes' , runParallelCommandsNTimes' , executeParallelCommands , linearise , toBoxDrawings , prettyNParallelCommands , prettyParallelCommands , prettyParallelCommandsWithOpts , prettyNParallelCommandsWithOpts , advanceModel , checkCommandNamesParallel , coverCommandNamesParallel , commandNamesParallel ) where import Control.Monad (replicateM, when) import Control.Monad.Catch (MonadMask, mask, onException) import Control.Monad.State.Strict (runStateT) import Data.Bifunctor (bimap) import Data.Foldable (toList) import Data.List (find, partition, permutations) import qualified Data.Map.Strict as Map import Data.Maybe (fromMaybe, mapMaybe) import Data.Monoid import Data.Set (Set) import qualified Data.Set as S import Data.Tree (Tree(Node)) import Prelude import Test.QuickCheck (Gen, Property, Testable, choose, forAllShrinkShow, property, sized) import Test.QuickCheck.Monadic (PropertyM, run) import Text.PrettyPrint.ANSI.Leijen (Doc) import Text.Show.Pretty (ppShow) import UnliftIO (MonadIO, MonadUnliftIO, concurrently, forConcurrently, newTChanIO) import Test.StateMachine.BoxDrawer import Test.StateMachine.ConstructorName import Test.StateMachine.DotDrawing import Test.StateMachine.Logic import Test.StateMachine.Sequential import Test.StateMachine.Types import qualified Test.StateMachine.Types.Rank2 as Rank2 import Test.StateMachine.Utils ------------------------------------------------------------------------ forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (ParallelCommands cmd resp -> prop) -- ^ Predicate. -> Property forAllParallelCommands sm mminSize = forAllShrinkShow (generateParallelCommands sm mminSize) (shrinkParallelCommands sm) ppShow forAllNParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Int -- ^ Number of threads -> (NParallelCommands cmd resp -> prop) -- ^ Predicate. -> Property forAllNParallelCommands sm np = forAllShrinkShow (generateNParallelCommands sm np) (shrinkNParallelCommands sm) ppShow -- | 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 m resp. Rank2.Foldable resp => Show (model Symbolic) => (Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m 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 m 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 m resp. Rank2.Foldable resp => Show (model Symbolic) => (Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m 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 m resp -> model Symbolic -> Commands cmd resp -> Bool parallelSafe StateMachine { precondition, transition, mock } model0 = all (preconditionsHold model0) . 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 m 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 m resp. Rank2.Traversable cmd => Rank2.Foldable resp => StateMachine model cmd m 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 m resp. Rank2.Traversable cmd => Rank2.Foldable resp => StateMachine model cmd m 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 m resp. (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m 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 m resp -> ValidateEnv model -> ValidateEnv model -> Commands cmd resp -> ValidateEnv model combineEnv sm envL envR cmds = ValidateEnv { veModel = advanceModel sm (veModel envL) cmds , veScope = Map.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 m resp. (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m 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') (shrink, cmds) = (False, acc'') where acc'' = do (envPrev, cmdsPrev) <- acc' let envUsed = if firstCall then env else env `withCounterFrom` envPrev (env', cmd') <- shrinkAndValidate sm shrink 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)] ------------------------------------------------------------------------ runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)] runParallelCommands = runParallelCommandsNTimes 10 runParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)] runParallelCommands' = runParallelCommandsNTimes' 10 runNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)] runNParallelCommands = runNParallelCommandsNTimes 10 runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -- ^ How many times to execute the parallel program. -> StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)] runParallelCommandsNTimes n sm cmds = replicateM n $ do (hist, reason1, reason2) <- run (executeParallelCommands sm cmds True) return (hist, logicReason (combineReasons [reason1, reason2]) .&& linearise sm hist) runParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -- ^ How many times to execute the parallel program. -> StateMachine model cmd m resp -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)] runParallelCommandsNTimes' n sm complete cmds = replicateM n $ do (hist, _reason1, _reason2) <- run (executeParallelCommands sm cmds False) let hist' = completeHistory complete hist return (hist', linearise sm hist') runNParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -- ^ How many times to execute the parallel program. -> StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)] runNParallelCommandsNTimes n sm cmds = replicateM n $ do (hist, reason) <- run (executeNParallelCommands sm cmds True) return (hist, logicReason reason .&& linearise sm hist) runNParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -- ^ How many times to execute the parallel program. -> StateMachine model cmd m resp -> (cmd Concrete -> resp Concrete) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)] runNParallelCommandsNTimes' n sm complete cmds = replicateM n $ do (hist, _reason) <- run (executeNParallelCommands sm cmds True) let hist' = completeHistory complete hist return (hist, linearise sm hist') executeParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> Bool -> m (History cmd resp, Reason, Reason) executeParallelCommands sm@StateMachine{ initModel, cleanup } (ParallelCommands prefix suffixes) stopOnError = mask $ \restore -> do hchan <- restore newTChanIO (reason0, (env0, _smodel, _counter, _cmodel)) <- restore (runStateT (executeCommands sm hchan (Pid 0) CheckEverything prefix) (emptyEnvironment, initModel, newCounter, initModel)) `onException` (getChanContents hchan >>= cleanup . mkModel sm . History) if reason0 /= Ok then do hist <- getChanContents hchan cleanup $ mkModel sm $ History hist return (History hist, reason0, reason0) else do (reason1, reason2, _) <- restore (go hchan (Ok, Ok, env0) suffixes) `onException` (getChanContents hchan >>= cleanup . mkModel sm . History) hist <- getChanContents hchan cleanup $ mkModel sm $ History hist return (History hist, reason1, reason2) where go _hchan (res1, res2, env) [] = return (res1, res2, env) go hchan (Ok, Ok, env) (Pair cmds1 cmds2 : pairs) = do ((reason1, (env1, _, _, _)), (reason2, (env2, _, _, _))) <- concurrently -- XXX: Post-conditions not checked, so we can pass in initModel here... -- It would be better if we made executeCommands take a Maybe Environment -- instead of the Check... (runStateT (executeCommands sm hchan (Pid 1) CheckNothing cmds1) (env, initModel, newCounter, initModel)) (runStateT (executeCommands sm hchan (Pid 2) CheckNothing cmds2) (env, initModel, newCounter, initModel)) case (isOK $ combineReasons [reason1, reason2], stopOnError) of (False, True) -> return (reason1, reason2, env1 <> env2) _ -> go hchan ( reason1 , reason2 , env1 <> env2 ) pairs go hchan (Ok, ExceptionThrown e, env) (Pair cmds1 _cmds2 : pairs) = do -- XXX: It's possible that pre-conditions fail at this point, because -- commands may depend on references that never got created in the crashed -- process. For example, consider: -- -- x <- Create -- ------------+---------- -- Write 1 x | Write 2 x -- y <- Create | -- ------------+---------- -- Write 3 x | Write 4 y -- | Read x -- -- If the @Write 1 x@ fails, @y@ will never be created and the -- pre-condition for @Write 4 y@ will fail. This also means that @Read x@ -- will never get executed, and so there could be a bug in @Write@ that -- never gets discovered. Not sure if we can do something better here? -- (reason1, (env1, _, _, _)) <- runStateT (executeCommands sm hchan (Pid 1) CheckPrecondition cmds1) (env, initModel, newCounter, initModel) go hchan ( reason1 , ExceptionThrown e , env1 ) pairs go hchan (ExceptionThrown e, Ok, env) (Pair _cmds1 cmds2 : pairs) = do (reason2, (env2, _, _, _)) <- runStateT (executeCommands sm hchan (Pid 2) CheckPrecondition cmds2) (env, initModel, newCounter, initModel) go hchan ( ExceptionThrown e , reason2 , env2 ) pairs go _hchan out@(ExceptionThrown _, ExceptionThrown _, _env) (_ : _) = return out go _hchan out@(PreconditionFailed {}, ExceptionThrown _, _env) (_ : _) = return out go _hchan out@(ExceptionThrown _, PreconditionFailed {}, _env) (_ : _) = return out go _hchan (res1, res2, _env) (Pair _cmds1 _cmds2 : _pairs) = error ("executeParallelCommands, unexpected result: " ++ show (res1, res2)) logicReason :: Reason -> Logic logicReason Ok = Top logicReason r = Annotate (show r) Bot executeNParallelCommands :: (Rank2.Traversable cmd, Show (cmd Concrete), Rank2.Foldable resp) => Show (resp Concrete) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> Bool -> m (History cmd resp, Reason) executeNParallelCommands sm@StateMachine{ initModel, cleanup } (ParallelCommands prefix suffixes) stopOnError = mask $ \restore -> do hchan <- restore newTChanIO (reason0, (env0, _smodel, _counter, _cmodel)) <- restore (runStateT (executeCommands sm hchan (Pid 0) CheckEverything prefix) (emptyEnvironment, initModel, newCounter, initModel)) `onException` (getChanContents hchan >>= cleanup . mkModel sm . History) if reason0 /= Ok then do hist <- getChanContents hchan cleanup $ mkModel sm $ History hist return (History hist, reason0) else do (errors, _) <- restore (go hchan (Map.empty, env0) suffixes) `onException` (getChanContents hchan >>= cleanup . mkModel sm . History) hist <- getChanContents hchan cleanup $ mkModel sm $ History hist return (History hist, combineReasons $ Map.elems errors) where go _ res [] = return res go hchan (previousErrors, env) (suffix : rest) = do when (isInvalid $ Map.elems previousErrors) $ error ("executeNParallelCommands, unexpected result: " ++ show previousErrors) let noError = Map.null previousErrors check = if noError then CheckNothing else CheckPrecondition res <- forConcurrently (zip [1..] suffix) $ \(i, cmds) -> case Map.lookup i previousErrors of Nothing -> do (reason, (env', _, _, _)) <- runStateT (executeCommands sm hchan (Pid i) check cmds) (env, initModel, newCounter, initModel) return (if isOK reason then Nothing else Just (i, reason), env') Just _ -> return (Nothing, env) let newErrors = Map.fromList $ mapMaybe fst res errors = Map.union previousErrors newErrors newEnv = mconcat $ snd <$> res case (stopOnError, Map.null errors) of (True, False) -> return (errors, newEnv) _ -> go hchan (errors, newEnv) rest combineReasons :: [Reason] -> Reason combineReasons ls = fromMaybe Ok (find (/= Ok) ls) isInvalid :: [Reason] -> Bool isInvalid ls = any isPreconditionFailed ls && all notException ls where notException (ExceptionThrown _) = False notException _ = True isPreconditionFailed :: Reason -> Bool isPreconditionFailed PreconditionFailed {} = True isPreconditionFailed _ = False ------------------------------------------------------------------------ -- | Try to linearise a history of a parallel program execution using a -- sequential model. See the *Linearizability: a correctness condition for -- concurrent objects* paper linked to from the README for more info. linearise :: forall model cmd m resp. (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic linearise StateMachine { transition, postcondition, initModel } = go . unHistory where go :: [(Pid, HistoryEvent cmd resp)] -> Logic go [] = Top go es = exists (interleavings es) (step initModel) step :: model Concrete -> Tree (Operation cmd resp) -> Logic step _model (Node (Crash _cmd _err _pid) _roses) = error "Not implemented yet, see issue #162 for more details." step model (Node (Operation cmd resp _) roses) = postcondition model cmd resp .&& exists' roses (step (transition model cmd resp)) exists' :: Show a => [a] -> (a -> Logic) -> Logic exists' [] _ = Top exists' xs p = exists xs p ------------------------------------------------------------------------ -- | Takes the output of parallel program runs and pretty prints a -- counterexample if any of the runs fail. prettyParallelCommandsWithOpts :: (MonadIO m, Rank2.Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> Maybe GraphOptions -> [(History cmd resp, Logic)] -- ^ Output of 'runParallelCommands'. -> PropertyM m () prettyParallelCommandsWithOpts cmds mGraphOptions = mapM_ (\(h, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l)) where printCounterexample hist' (VFalse ce) = do putStrLn "" print (toBoxDrawings cmds hist') putStrLn "" print (simplify ce) putStrLn "" case mGraphOptions of Nothing -> return () Just gOptions -> createAndPrintDot cmds gOptions hist' printCounterexample _hist _ = error "prettyParallelCommands: impossible, because `boolean l` was False." simplify :: Counterexample -> Counterexample simplify (Fst ce@(AnnotateC _ BotC)) = ce simplify (Snd ce) = simplify ce simplify (ExistsC [] []) = BotC simplify (ExistsC _ [Fst ce]) = ce simplify (ExistsC x (Fst ce : ces)) = ce `EitherC` simplify (ExistsC x ces) simplify (ExistsC _ (Snd ce : _)) = simplify ce simplify _ = error "simplify: impossible,\ \ because of the structure of linearise." prettyParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Rank2.Foldable cmd => ParallelCommands cmd resp -> [(History cmd resp, Logic)] -- ^ Output of 'runNParallelCommands'. -> PropertyM m () prettyParallelCommands cmds = prettyParallelCommandsWithOpts cmds Nothing -- | Takes the output of parallel program runs and pretty prints a -- counterexample if any of the runs fail. prettyNParallelCommandsWithOpts :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Rank2.Foldable cmd => NParallelCommands cmd resp -> Maybe GraphOptions -> [(History cmd resp, Logic)] -- ^ Output of 'runNParallelCommands'. -> PropertyM m () prettyNParallelCommandsWithOpts cmds mGraphOptions = mapM_ (\(h, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l)) where printCounterexample hist' (VFalse ce) = do putStrLn "" print (simplify ce) putStrLn "" case mGraphOptions of Nothing -> return () Just gOptions -> createAndPrintDot cmds gOptions hist' printCounterexample _hist _ = error "prettyNParallelCommands: impossible, because `boolean l` was False." prettyNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Rank2.Foldable cmd => NParallelCommands cmd resp -> [(History cmd resp, Logic)] -- ^ Output of 'runNParallelCommands'. -> PropertyM m () prettyNParallelCommands cmds = prettyNParallelCommandsWithOpts cmds Nothing -- | Draw an ASCII diagram of the history of a parallel program. Useful for -- seeing how a race condition might have occured. toBoxDrawings :: forall cmd resp. Rank2.Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> History cmd resp -> Doc toBoxDrawings (ParallelCommands prefix suffixes) = toBoxDrawings'' allVars where allVars = getAllUsedVars prefix `S.union` foldMap (foldMap getAllUsedVars) suffixes toBoxDrawings'' :: Set Var -> History cmd resp -> Doc toBoxDrawings'' knownVars (History h) = exec evT (fmap (out . snd) <$> Fork l p r) where (p, h') = partition (\e -> fst e == Pid 0) h (l, r) = partition (\e -> fst e == Pid 1) h' out :: HistoryEvent cmd resp -> String out (Invocation cmd vars) | vars `S.isSubsetOf` knownVars = show (S.toList vars) ++ " ← " ++ show cmd | otherwise = show cmd out (Response resp) = show resp out (Exception err) = err toEventType :: History' cmd resp -> [(EventType, Pid)] toEventType = map go where go e = case e of (pid, Invocation _ _) -> (Open, pid) (pid, Response _) -> (Close, pid) (pid, Exception _) -> (Close, pid) evT :: [(EventType, Pid)] evT = toEventType (filter (\e -> fst e `Prelude.elem` map Pid [1, 2]) h) createAndPrintDot :: forall cmd resp t. Foldable t => Rank2.Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommandsF t cmd resp -> GraphOptions -> History cmd resp -> IO () createAndPrintDot (ParallelCommands prefix suffixes) gOptions = toDotGraph allVars where allVars = getAllUsedVars prefix `S.union` foldMap (foldMap getAllUsedVars) suffixes toDotGraph :: Set Var -> History cmd resp -> IO () toDotGraph knownVars (History h) = printDotGraph gOptions $ (fmap out) <$> (Rose (snd <$> prefixMessages) groupByPid) where (prefixMessages, h') = partition (\e -> fst e == Pid 0) h alterF a Nothing = Just [a] alterF a (Just ls) = Just $ a : ls groupByPid = foldr (\(p,e) m -> Map.alter (alterF e) p m) Map.empty h' out :: HistoryEvent cmd resp -> String out (Invocation cmd vars) | vars `S.isSubsetOf` knownVars = show (S.toList vars) ++ " ← " ++ show cmd | otherwise = show cmd out (Response resp) = " → " ++ show resp out (Exception err) = " → " ++ err getAllUsedVars :: Rank2.Foldable cmd => Commands cmd resp -> Set Var getAllUsedVars = S.fromList . foldMap (\(Command cmd _ _) -> getUsedVars cmd) . unCommands -- | Print the percentage of each command used. The prefix check is -- an unfortunate remaining for backwards compatibility. checkCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property checkCommandNamesParallel cmds = checkCommandNames $ toSequential cmds -- | Fail if some commands have not been executed. coverCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property coverCommandNamesParallel cmds = coverCommandNames $ toSequential cmds commandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> [(String, Int)] commandNamesParallel = commandNames . toSequential toSequential :: Foldable t => ParallelCommandsF t cmd resp -> Commands cmd resp toSequential cmds = prefix cmds <> mconcat (concatMap toList (suffixes cmds))