Copyright | (C) 2017 ATS Advanced Telematic Systems GmbH |
---|---|

License | BSD-style (see the file LICENSE) |

Maintainer | Stevan Andjelkovic <stevan.andjelkovic@here.com> |

Stability | provisional |

Portability | non-portable (GHC extensions) |

Safe Haskell | None |

Language | Haskell2010 |

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

## Synopsis

- forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => CommandNames cmd => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> (ParallelCommands cmd resp -> prop) -> Property
- generateParallelCommands :: forall model cmd m resp. (Foldable resp, Show (model Symbolic)) => CommandNames cmd => StateMachine model cmd m resp -> Gen (ParallelCommands cmd resp)
- shrinkParallelCommands :: forall cmd model m resp. Traversable cmd => Foldable resp => StateMachine model cmd m resp -> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
- shrinkAndValidateParallel :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
- runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)]
- runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)]
- executeParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> m (History cmd resp, Reason)
- linearise :: forall model cmd m resp. (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic
- toBoxDrawings :: forall cmd resp. Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> History cmd resp -> Doc
- prettyParallelCommands :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> [(History cmd resp, Logic)] -> PropertyM m ()
- advanceModel :: StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic

# Documentation

forAllParallelCommands Source #

:: Testable prop | |

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

=> CommandNames cmd | |

=> (Traversable cmd, Foldable resp) | |

=> StateMachine model cmd m resp | |

-> (ParallelCommands cmd resp -> prop) | Predicate. |

-> Property |

generateParallelCommands :: forall model cmd m resp. (Foldable resp, Show (model Symbolic)) => CommandNames cmd => StateMachine model cmd m resp -> 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] ┘

shrinkParallelCommands :: forall cmd model m resp. 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.

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

runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)] Source #

runParallelCommandsNTimes Source #

:: (Show (cmd Concrete), Show (resp Concrete)) | |

=> (Traversable cmd, Foldable resp) | |

=> (MonadCatch 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)] |

executeParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> m (History cmd resp, Reason) Source #

linearise :: forall model cmd m resp. (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 resp. Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> History cmd resp -> Doc Source #

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

prettyParallelCommands Source #

:: (MonadIO m, Foldable cmd) | |

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

=> ParallelCommands cmd resp | |

-> [(History cmd resp, Logic)] | Output of |

-> PropertyM m () |

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

:: 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.