Reads-from exactly one

[hernanponcedeleon]

According to this (page 149, point 1), the fact that a load reads-from exactly one store is guaranteed by the totality of co and the definition of fr, so we can replace the exactly one (which could be hard for the solver) by an or.

[ThomasHaas]

Note that Sc-per-Loc is enough to make this optimization possible for all memory models (not sure about C11 though). In full generality it may fail though. Unfortunately, this is the case for Refinement without any bias model so this option must be configurable.

[hernanponcedeleon]

Consider the case where a load rf two stores, and without loss of generality we assume a particular co-order between them

Wx1 -rf-> Rx
Wx2 -rf-> Rx
Wx1 -co-> Wx2

This would form a cycle in Rx -rf^{-1}-> Wx1 -co-> Wx2 -rf-> Rx. I think the simpler assumption where this simplification is sound is if the WMM guarantees acyclic(fr U rf). However, to avoid a super specific flag and since most WMM will have Sc-per-Loc, we can enable this optimisation using the ASSUME_LOCAL_CONSISTENCY flag in GlobalSettings.

[ThomasHaas]

Local consistency =/= SC-per-Loc though. Local consistency is even weaker and is basically Sc-per-thread (or Sc-per-thread-per-loc?). I think we should add a second flag for SC-Per-Loc or alternatively a flag Read_Relaxation. You cannot put it into Local consistency as Refinement works fine with local consistency but not with the read relaxation! I think all non-refinement tasks can enable this flag and refinement enables it only if Sc-per-Loc bias is used, otherwise it disables it. We could also make Refinement work with this, by splitting an execution with multiple reads into multiple executions with single reads and refine all of them! This needs some work, but it could actually leverage this optimization in a nice way