Documentation

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

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

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

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

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.

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

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

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

Apply the transition of some commands to a model.

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

Fail if some commands have not been executed.