Copyright	(C) 2017 ATS Advanced Telematic Systems GmbH
License	BSD-style (see the file LICENSE)
Maintainer	Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
Stability	provisional
Portability	non-portable (GHC extensions)
Safe Haskell	None
Language	Haskell2010

Test.StateMachine.Parallel

Description

This module contains helpers for generating, shrinking, and checking parallel programs.

Synopsis

forAllNParallelCommands :: forall prop (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type). (Testable prop, Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic), Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Int -> (NParallelCommands cmd resp -> prop) -> Property
forAllNParallelCommandsNTimes :: forall prop (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type). (Testable prop, Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic), Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Int -> Int -> (NParallelCommands cmd resp -> prop) -> Property
forAllParallelCommandsNTimes :: forall prop (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type). (Testable prop, Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic), Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> Int -> (ParallelCommands cmd resp -> prop) -> Property
forAllParallelCommands :: forall prop (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type). (Testable prop, Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic), Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (ParallelCommands cmd resp -> prop) -> Property
generateNParallelCommands :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Int -> Gen (NParallelCommands cmd resp)
generateParallelCommands :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -> Gen (ParallelCommands cmd resp)
shrinkNParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> [NParallelCommands cmd resp]
shrinkParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
shrinkAndValidateNParallel :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> NParallelCommands cmd resp -> [NParallelCommands cmd resp]
shrinkAndValidateParallel :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
shrinkCommands' :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). Commands cmd resp -> [Shrunk (Commands cmd resp)]
runParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic)
runParallelCommands' :: forall cmd resp (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic)
runNParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic)
runNParallelCommands' :: forall cmd resp (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> (cmd Concrete -> resp Concrete) -> NParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic)
prettyNParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), MonadIO m, Foldable cmd) => NParallelCommands cmd resp -> (History cmd resp, model Concrete, Logic) -> PropertyM m ()
prettyParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), MonadIO m, Foldable cmd) => ParallelCommands cmd resp -> (History cmd resp, model Concrete, Logic) -> PropertyM m ()
prettyParallelCommandsWithOpts :: forall (m :: Type -> Type) (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) model. (MonadIO m, Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> Maybe GraphOptions -> (History cmd resp, model Concrete, Logic) -> PropertyM m ()
prettyNParallelCommandsWithOpts :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), MonadIO m, Foldable cmd) => NParallelCommands cmd resp -> Maybe GraphOptions -> (History cmd resp, model Concrete, Logic) -> PropertyM m ()
advanceModel :: forall model (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic
checkCommandNamesParallel :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (t :: Type -> Type). (Foldable t, CommandNames cmd) => ParallelCommandsF t cmd resp -> Property -> Property
coverCommandNamesParallel :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (t :: Type -> Type). (Foldable t, CommandNames cmd) => ParallelCommandsF t cmd resp -> Property -> Property
commandNamesParallel :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (t :: Type -> Type). (Foldable t, CommandNames cmd) => ParallelCommandsF t cmd resp -> [(String, Int)]
linearise :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic
toBoxDrawings :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) ann. (Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> History cmd resp -> Doc ann
executeParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) m model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason, Reason)

Documentation

forAllNParallelCommands Source #

Arguments

:: forall prop (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type). (Testable prop, Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic), Traversable cmd, Foldable resp)
=> StateMachine model cmd m resp
-> Int	Number of threads
-> (NParallelCommands cmd resp -> prop)	Predicate.
-> Property

forAllNParallelCommandsNTimes Source #

Arguments

:: forall prop (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type). (Testable prop, Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic), Traversable cmd, Foldable resp)
=> StateMachine model cmd m resp
-> Int	Number of threads
-> Int
-> (NParallelCommands cmd resp -> prop)	Predicate.
-> Property

forAllParallelCommandsNTimes Source #

Arguments

:: forall prop (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type). (Testable prop, Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic), Traversable cmd, Foldable resp)
=> StateMachine model cmd m resp
-> Maybe Int
-> Int
-> (ParallelCommands cmd resp -> prop)	Predicate.
-> Property

forAllParallelCommands Source #

Arguments

:: forall prop (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type). (Testable prop, Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic), Traversable cmd, Foldable resp)
=> StateMachine model cmd m resp
-> Maybe Int
-> (ParallelCommands cmd resp -> prop)	Predicate.
-> Property

generateNParallelCommands :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Int -> Gen (NParallelCommands cmd resp) Source #

generateParallelCommands :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -> Gen (ParallelCommands cmd resp) Source #

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] ┘

shrinkNParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> [NParallelCommands cmd resp] Source #

Shrink a parallel program in a pre-condition and scope respecting way.

shrinkParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> [ParallelCommands cmd resp] Source #

Shrink a parallel program in a pre-condition and scope respecting way.

shrinkAndValidateNParallel :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> NParallelCommands cmd resp -> [NParallelCommands cmd resp] Source #

shrinkAndValidateParallel :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ParallelCommands cmd resp -> [ParallelCommands cmd resp] Source #

shrinkCommands' :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). Commands cmd resp -> [Shrunk (Commands cmd resp)] Source #

Shrinks Commands in a way that it has strictly less number of commands.

runParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic) Source #

runParallelCommands' :: forall cmd resp (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic) Source #

runNParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic) Source #

runNParallelCommands' :: forall cmd resp (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> (cmd Concrete -> resp Concrete) -> NParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic) Source #

prettyNParallelCommands Source #

Arguments

:: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), MonadIO m, Foldable cmd)
=> NParallelCommands cmd resp
-> (History cmd resp, model Concrete, Logic)	Output of `runNParallelCommands`.
-> PropertyM m ()

prettyParallelCommands Source #

Arguments

:: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), MonadIO m, Foldable cmd)
=> ParallelCommands cmd resp
-> (History cmd resp, model Concrete, Logic)	Output of `runParallelCommands`.
-> PropertyM m ()

prettyParallelCommandsWithOpts Source #

Arguments

:: forall (m :: Type -> Type) (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) model. (MonadIO m, Foldable cmd, Show (cmd Concrete), Show (resp Concrete))
=> ParallelCommands cmd resp
-> Maybe GraphOptions
-> (History cmd resp, model Concrete, Logic)	Output of `runParallelCommands`.
-> PropertyM m ()

Takes the output of parallel program runs and pretty prints a counterexample if any of the runs fail.

prettyNParallelCommandsWithOpts Source #

Arguments

:: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), MonadIO m, Foldable cmd)
=> NParallelCommands cmd resp
-> Maybe GraphOptions
-> (History cmd resp, model Concrete, Logic)	Output of `runNParallelCommands`.
-> PropertyM m ()

Takes the output of parallel program runs and pretty prints a counterexample if any of the runs fail.

advanceModel Source #

Arguments

:: forall model (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). StateMachine model cmd m resp
-> model Symbolic	The model.
-> Commands cmd resp	The commands.
-> model Symbolic

Apply the transition of some commands to a model.

checkCommandNamesParallel :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (t :: Type -> Type). (Foldable t, CommandNames cmd) => ParallelCommandsF t cmd resp -> Property -> Property Source #

Print the percentage of each command used. The prefix check is an unfortunate remaining for backwards compatibility.

coverCommandNamesParallel :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (t :: Type -> Type). (Foldable t, CommandNames cmd) => ParallelCommandsF t cmd resp -> Property -> Property Source #

Fail if some commands have not been executed.

commandNamesParallel :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (t :: Type -> Type). (Foldable t, CommandNames cmd) => ParallelCommandsF t cmd resp -> [(String, Int)] Source #

linearise :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic Source #

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.

toBoxDrawings :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) ann. (Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> History cmd resp -> Doc ann Source #

Draw an ASCII diagram of the history of a parallel program. Useful for seeing how a race condition might have occured.

executeParallelCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) m model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason, Reason) Source #