Support for concurrent model-based testing?

[Aaronontheweb]

Hi there,

I wanted to check if there was any current support for parallel / concurrent model based testing to assert against race conditions and other fun stuff, like what you can do with the Erlang version of Quickcheck. What's possible with FsCheck today in this regard?

[kurtschelfthout]

There is no built-in support for that at the moment. I'm interested to hear what kind of support you would like.

I think it should be straightforward to use what there is now, either the Command or the Experimental.StateMachine to generate in each step, instead of one operation, a list of operations that you then apply concurrently - by starting Threads or Tasks or whatever - and then checking the postcondition as normal. They would have to end up in the same deterministic end state no matter what the interleaving.

I think it's probably best to disable shrinking, as it probably gives weird results with the inherent non-determinism. Not sure how that can be handled in general - I remember there was an MS research project at some point that hooked in to all of Windows and .NET's synchronization points and effectively allowed you to replay any interleaving (and also exhaustively test them). That seems a tad out of scope for FsCheck ;)

[Aaronontheweb]

I remember there was an MS research project at some point that hooked in to all of Windows and .NET's synchronization points and effectively allowed you to replay any interleaving (and also exhaustively test them).

Did you mean http://research.microsoft.com/en-us/projects/chess/? It's a great project by the looks of it but it has major code rot - can't even get the thing to compile on Windows 10 with VS 2015.

I don't think this is out of scope for FsCheck at all! This is one of the killer features of property-based testing.

To get this to work right, the Erlang QuickCheck had to use a randomizing scheduler also: http://quviq.com/documentation/pulse/index.html

Reason why I'm interested in this: I'm one of the authors of Akka.NET and we're looking to use property-based testing to eliminate some race conditions in our networking and clustering systems.

I actually think that with a custom TaskScheduler or Akka.NET Dispatcher it might be possible to do this easily enough.

On paper:

1. When generating a command, be able to specify the number of parallel agents participating in the test, or even better: allow FsCheck to generate the number of parallel agents.
2. Run the test in parallel using a scheduler / actor with the specified degree of parallelism, randomly distributing commands to each agent.
3. Capture the output against the model and see if there's a possible interleaving with each Task that would produce this result. Fail if no, pass if yes. Way to do this would be to use a synchronous task scheduler and run the events in a linear order and see if you can arrive at the same outcome.
4. Repeat for each generated test.

[kurtschelfthout]

Yes, I meant Chess, and yes it's no longer maintained as far as I know. I think it's a pity, it worked really well at the time. I do still think that re-creating that - the Pulse part in Erlang, which captures a trace of how different processes interleave - is not in scope for FsCheck. But I agree that it's super useful.

This paper describes an interesting approach which sounds like what you had in mind, see section 4.3. There are a bunch of constraints though - it "only" tests whether each generated command is atomic, i.e. by testing whether there is a sequential execution that has the same outcome as the parallel one. However, to make this tractable they generate a sequential prefix, and then exactly two sequences for parallel execution, each containing at most 16 operations. To make shrinking deterministic, they just run a particular test a number of times during shrinking so that it only succeeds if it succeeds 10 times in a row :)

Anyway, I agree that is within scope (unlike something like Chess/Pulse...) but it's worth emphasizing that due to the non-determinism and the inherently large state space there are some constraints here.

[Aaronontheweb]

Awesome, thanks for the paper - giving it a read now.

[ivankoster]

@Aaronontheweb I am interested too in something you described above. The last few hours I've been searching for methods to test parallel C# code like Quickcheck can do for some languages, without much luck. I see you've been working on this problem about a year ago. Have you been successful in your ways to test for concurrency issues in your .Net project and if so, would you mind sharing how?

[kurtschelfthout]

Related - came accross https://github.com/Kotlin/kotlinx-lincheck, but haven't studied in much detail.

Does seem like there is still a gap in the .NET space for this.