Support exploring more weak memory behaviors

[RalfJung]

Miri can explore some possible behaviors introduced by weak memory, but not all of them. What exactly are our gaps and is it possible to fix them?

Original description

Miri explores a particular interleaving of a concurrent execution, so if a program is buggy only for some executions Miri might miss that bug. Furthermore, Miri will never exhibit "weak" behaviors where the same operation appears to take effect in different order for different threads, which means there is yet another set of executions that Miri will not see and that could be buggy.

It would be great if we could do something about this. However, exploring all interleavings is clearly infeasible. I think one common technique used for such situations in the literature is "(dynamic) partial order reduction", but I am not sure if that technique is applicable to Miri.

[JCTyblaidd]

Useful reading:

CDSChecker - http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf

Optimal DPOR - http://user.it.uu.se/~bengt/Papers/Full/popl14.pdf

CDSChecker is based on the original DPOR paper, this is an improvement of the algorithm, may be worth investigating.

Optimal DPOR with Observers - http://user.it.uu.se/~bengt/Papers/Full/tacas18.pdf

Again another potential improvement to DPOR that may be worth investigating.

[tomtomjhj]

Note: loom implements CDSChecker but it's far from complete. Also, the implementation is quite different from the original one, which IMO makes it difficult to implement the missing features and optimizations.

Recent work on model checking for relaxed memory model:

• RCMC
  • RCMC targets the RC11 memory model which fixes some problems in C11 memory model. RC11 rules out some behaviors permitted in ARM but this is not a problem if the compiler emits fences appropriately (with some performance penalty).
  • Exploiting the properties of RC11, it comes up with a novel and very efficient algorithm that doesn't use DPOR.
• GenMC, source code: It improves RCMC in many ways.
  • It can target memory models other than RC11 as long as they satisfy some conditions. But C11 doesn't satisfy these conditions.
  • For RC11, GenMC is more efficient than RCMC.
  • It takes account of libraries like mutex.
  • The implementation is based on LLVM interpreter (lli) so I believe miri can take a similar approach.

[JCTyblaidd]

For alternative memory models to C11, there are the changes to the memory model in C++20 which we may want to consider, partially based on the RC11 paper: Revising the C++ memory model, Weaken Release Sequences.

[RalfJung]

FWIW Miri now explores some weak memory behaviors and randomly preempts threads, but even running with all possible seeds will still not yield all possible executions -- we only preempt at basic block boundaries, and the weak memory emulation cannot produce all weak memory behaviors. (And making it do that is very hard and probably terribly inefficient.)

[RalfJung]

Given that there cannot be any synchronization operations within a thread, just preempting at basic block boundaries is likely actually covering all possible executions.

But the weak memory emulation is still very incomplete.