Unclear what "prefix" commands are in parallel state machine testing

[ocharles]

The documentation for parallel states

Given the initial model state and set of commands, generates prefix actions to be run sequentially, followed by two branches to be run in parallel.

But it's unclear what "prefix" actions are, and what their connection is to the list of Commands supplied. Could some of the documentation around this be improved?

[jacobstanley]

Yeah that definitely could be worded better. The parallel generator uses the list of Commands to generate three lists of actions to execute. The first is run sequentially to put the system in to a random state, the second two are run in parallel to try and detect commands which are not atomic.

[ocharles]

So all commands are run on all branches - include the sequential run?

[jacobstanley]

Not quite, so let me give a concrete example, say we are testing mutable references and we have 3 commands NewRef, IncRef, ReadRef.

Hedgehog might generate the following set of actions to run:

--- Prefix ---
Var 0 = New Ref
Var 1 = IncRef (Var 0)
--- Branch 1 ---
Var 2 = IncRef (Var 0)
Var 3 = ReadRef (Var 0)
--- Branch 2 ---
Var 4 = IncRef (Var 0)
Var 5 = ReadRef (Var 0)

What this means is that we first execute NewRef, IncRef on the main thread. Now the system is in a certain state, namely we have one reference and it is set to 1. Now we execute branch 1 and branch 2 in parallel. So you can imagine that both threads try to increment Var 0 at the same time, and then they both try to read the value from it.

We record the results that we observed during the actual test run, and then try to see if we can find a sequential ordering which can explain the results which we observed, this is called linearisation.

[jacobstanley]

The whole video is good, but starting at 16:10, this has a pretty good explanation of how parallel testing works:

Thomas Arts - Testing Asynchronous APIs With QuickCheck (video)

[ocharles]

Ok, that much makes sense. I suppose the only part that surprises or confuses me is knowing how much of the [Command] list forms the prefix, and how much forms the suffix. It does seem a little strange to me that a Range controls this, rather than just passing two lists in.

[jacobstanley]

Ah so the [Command] list is just a list of choices, it would be perfectly fine for the prefix and the suffix to contains all or none of the commands in the list of choices passed in.

You can think of parallel as being roughly equivalent to:

parallel :: Range Int -> Range Int -> [Command] -> Gen Parallel
parallel prefixRange branchRange commands =
  Parallel
    <$> Gen.list prefixRange (Gen.choice commands)
    <*> Gen.list branchRange (Gen.choice commands)
    <*> Gen.list branchRange (Gen.choice commands)

The only thing parallel does differently to the above is make sure that we only generate commands which are satisfy the preconditions for the current state.

[ocharles]

I see now that [Command] has actually mislead me as it suggests an ordering, but when I read the code I see element is used which samples random commands out of that list - is that correct? I wonder if a Set or Bag would be better, but then you need a notion of equality which is unfortunate. I think expecting Commands to be executed in a sequence is one source of confusion here.

[jacobstanley]

I see element is used which samples random commands out of that list - is that correct?

Yep, that's exactly right.

A Set would be more appropriate for element and choice also, but as you point out there is the notion of equality which we don't care about, and there is also the matter of syntax.

[jacobstanley]

Perhaps the documentation needs the words "samples random commands out of that list" somewhere in it

[ocharles]

I think so, the whole "state machine testing" section could probably do with a paragraph or two explaining what's going on and pointing to the resources you've given me here and on Twitter/Reddit.