There is a debate at #12713 about whether CSE for atomic loads is correct. I think that this debate should be resolved before we consider the present PR. I am closing for now, and we can reopen any time we want.

Further examples from @polytypic over at #12713 suggest the following example where CSE is clearly (?) invalid:

  let x0 = Atomic.get x in
  let y0 = Atomic.get y in
  let x1 = Atomic.get x in

Merging the two reads of x is wrong, because the read of y0 could have observed a write on x that happens after the read of x0. In operational terms, the read of y0 updated our frontier, so the read of x1 happens in a different state. Atomic loads mutate the frontier state.

I wonder why this was not done back when Multicore was merged. Was it a blind spot, we didn't think of which compiler optimisations should be disabled? Did we say we would disable CSE and forget to do it? Are there other bugs of this category looking around?

Earlier, atomic loads were translated to an external call to caml_atomic_load. The external calls are not optimised by the compiler and hence, the SC semantics for atomics was preserved. Later ocaml-multicore/ocaml-multicore#251 lowered it through the compiler. In this PR, we didn't take care of the interaction with the compiler optimisations. This was an oversight.

Atomic.set is compiled to an atomic exchange, which is translated to an external call

Hence, the compiler should not optimise atomic stores.

It would be useful to do an audit of all the optimisations that we perform on loads of mutable locations. The easiest would be to disable any optimisations of atomic loads. For example, we have disabled the reordering of atomic loads in the scheduling pass in #12248.

It would be useful to do an audit of all the optimisations that we perform on loads of mutable locations.

@lthls Is there a list of optimisations that we perform on loads of mutable locations? If such a list doesn't exist (very likely), how would we go about gathering it? I assume this would also be needed for flambda.

No, there isn't such a list. For Flambda we decided to give some sensible semantics to the internal IR, and as a result we can check our optimisations against that (although we never published the semantics properly, hopefully we will correct that with Flambda 2).
One thing that makes these discussions particularly tricky is that what is considered as a mutable location can change during compilation. For example, CSE of mutable loads across a mutable write are forbidden in the backend, but if the right conditions are met the middle-end might be able to do the CSE because at that point the loads are not mutable yet. (Example: let x0 = fst x in y := 1; let x1 = fst x).

My intuition though is that for multicore-related issues we should only look at what happens from Mach and forward. Everything before that is too high-level (for instance, evaluation order is not finalised until the translation to Mach).
That still leaves a decent number of files to look at, but I believe they're relatively easy to sort into optional optimisation passes and required, non-optimising passes. From memory I would say that the optimisation passes are Deadcode, Split, and CSE. Although it's likely that a few optimisations are hidden in the translation passes (Selection, Linearize, Emit`).

Since this change is disabling a problematic optimisation, and we are moving to 5.1.1 as the reference version for 5.1, I think it is better to cherry-pick it to 5.1.