quickcheck-state-machine
quickcheck-state-machine copied to clipboard
Generalise to N threads in the parallel property
Currently only two parallel workers are used in the parallel property, some bugs might require more things to happen in parallel...
One idea I have for this is to replace Fork
with the following:
data Fork t a = Fork {
prefix :: a
suffix :: t a
}
Where we would often require t
to be Traversable
. To get back the current behaviour we would use:
data Pair a = Pair a a
instance Traversable Pair where
traverse f (Pair x y) = Pair <$> f x <*> f y
type OldFork a = Fork Pair a
In general we could have Fork (Vec N)
to have N
threads.
I noticed that Erlang uses a list of suffices, i.e. ParallelProg = { prefix: Prog, suffixes : [Prog] }
...
I remember John Hughes quoting a paper that shows that empirically most concurrency bugs can be triggered with two threads.
It can become more important to have more threads when doing fault injection though. For example, Jepsen uses 5 threads.
@stevana, as another generalisation, I think the type of these threads could be extended. For example forking unbound vs bound threads could make a difference at the result, when testing some frameworks. It would be nice if the user had this option. Thoughts?
Nice idea!
(Having a user-land scheduler that we could deterministically control would be great, but that's much more work.)
I've found the quote again:
"Almost all (96%) of the examined concurrency bugs are guaranteed to manifest if certain partial order between 2 threads is enforced."
From the end of the "Parallelism in test cases" section in the paper "Finding Race Conditions in Erlang with QuickCheck and PULSE" which is linked to from the README. This section also talks about performance issues with multiple threads.