Validation for programs weaker than lock-free

[bartoszmodelski]

Lots of real-world programs don't have lock-free property and it's often optimal that way. For one, because we mostly have a somewhat fair OS scheduler, and it does not make sense to optimize for the theoretical scenario, where one domain runs indefinitely. But, in absence of concrete bounds for unfairness, dscheck needs to explore all the possible Mazurkiewicz traces to prove properties about programs. In simple words, if thread A spins until thread B does something, dscheck will explore thread's A spinning to infinity.

There's a few things we could do to help here:

• Add depth limit to the search. The easiest thing to do. It's mentioned in the DPOR paper and was used by CDSCheck guys. The problem is that we don't really know how to determine optimal depth. In the CDSCheck paper, they were looking for bugs in existing implementations to show that the algorithm is useful, in our case, obtaining negative results is just as important.
• The papers also mention imposing some fairness conditions on the way DSCheck is scheduling things. I think it's potentially better than depth limit, but still a bit hard to ensure we're actually validating all the required states.
• Letting user place yields. This has the disadvantage, that our atomic's interface will depart from stdlib's, so users have to add indirections (rather than just copy in our atomic in tests with dune rules). But it seems to be the best solution from the perspective of correctness, as it's easy for user to identify cycles in the state space. It also seems quite implementable (although we have to be careful when more than 1 thread is yielding at once).

I don't think that we can reasonably identify the cycles automatically, since we cannot know whether e.g. retries of a spinlock are bounded without reading local state.