Test.StateMachine.Parallel

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

Documentation

forAllParallelCommands

Arguments

:: Testable prop

=> (Show (cmd Symbolic), Show (model Symbolic))

=> (Generic1 cmd, GConName1 (Rep1 cmd))

=> (Foldable cmd, Foldable resp)

=> StateMachine model cmd m resp

-> (ParallelCommands cmd -> prop)

Predicate.

-> Property

generateParallelCommands :: forall model cmd m resp. (Foldable resp, Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => StateMachine model cmd m resp -> Gen (ParallelCommands cmd)

shrinkParallelCommands :: forall cmd model m resp. Foldable cmd => Foldable resp => StateMachine model cmd m resp -> ParallelCommands cmd -> [ParallelCommands cmd]

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

validParallelCommands :: forall model cmd m resp. (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> ParallelCommands cmd -> State (model Symbolic, Set Var, Counter) (Maybe (ParallelCommands cmd))

prop_splitCombine :: [[Int]] -> Bool

runParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)]

runParallelCommandsNTimes

Arguments

:: (Traversable cmd, Foldable resp)

=> (MonadCatch m, MonadBaseControl IO m)

=> Int

How many times to execute the parallel program.

-> StateMachine model cmd m resp

-> ParallelCommands cmd

-> PropertyM m [(History cmd resp, Bool)]

executeParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> m (History cmd resp, Reason)

linearise :: forall model cmd m resp. StateMachine model cmd m resp -> History cmd resp -> Bool

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 resp. Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd -> History cmd resp -> Doc

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

prettyParallelCommands

Arguments

:: (MonadIO m, Foldable cmd)

=> (Show (cmd Concrete), Show (resp Concrete))

=> ParallelCommands cmd

-> [(History cmd resp, Bool)]

Output of runParallelCommands.

-> PropertyM m ()

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