Idea: a hostile thread scheduler to look for bugs

[johnynek]

a friend described: https://microsoft.github.io/coyote/

as "property based testing meets jepsen". It occurred to me that it would be cool to have an ContextShift, or ExecutionContext, or whatever, that uses randomization to try to see if properties are ever violated.

So, you would write some law about some IO code, then run it many times with this scheduler that isn't going for throughput, but is instead trying to trigger all the different orderings your code could have.

That could be really interesting for helping people find bugs in their async code.

[SystemFw]

I often dream of something along these lines, but specialised to the Java Memory Model (in between a model checker and a simulator)

[djspiewak]

I've thought about stuff like this. :-) There are several different ways it can be done. Coop provides one answer (you can actually layer ThreadT on top of IO and get pure concurrency with controllable yielding). Another answer is TestContext.

There are two problems to solve here:

• The combinatorial explosive space of interleavings. Property testing is infinitely more useful than it might otherwise be due to the fact that generators can usually be designed to preferentially explore the useful part of the domain. It's very difficult to define what this is when you're talking about fiber scheduling, and even more difficult when discussing fiber scheduling with more than one carrier thread.
• How do you print the errors? This is a bigger problem than it seems, because you need to be able to achieve two things: communicate very clearly to the user what happened, and provide them with the ability to easily repeat that outcome. I don't exactly know how to concisely represent interleaving, even with tracing and other tools at my disposal.

I really really like the idea, but there's some research to be done to get to a working solution. :-)

[johnynek]

It would be interesting to have a TestContext that is deterministic based on some seed. Then make a Gen[TestContext] and finally just have normal properties you are checking.

When you find a failing case, you use scalacheck's ability to print the seed to rerun the test.

[djspiewak]

Working in terms of seeds seems logical, but again how do you communicate what went wrong? Being able to trace through the exact combination of things that exhibited the race is really important. Minimization is an important and related element here.