The key point in your example is the claim that Flambda may optimize

let new_val = x :: old_val in
if r.contents == old_val
then (r.contents <- new_val; true)
else false

into

if r.contents == old_val
then
  (let new_val = x :: old_val in
  r.contents <- new_val; true)
else false

This is counter-intuitive, as in my intuition they are not equivalent (the allocation may result in OCaml callbacks running that can change the result of the r.contents == old_val test). If I understand @gadmm correctly, the point is that Flambda assumes a more pessimistic model, where callbacks may fire not only at allocation points, but basically at any point, including right before and after computing the test of an if construct (so moving the allocation from before to after does not change the places that could callback).

Here again (as in #9998) the proposed solution is the use of [@inline never] to restrict the compiler reasoning. In this case, what we are working around is the fact that Flambda does does not model the fact that callbacks may only fire at certain synchronization point. I understand the need and it sounds desirable to have this PR as a protection, but it still a bit unfortunate. What would better alternatives be?

• We could just have compare_and_set and fetch_and_add be compiler primitives that Flambda would treat atomically.
• Flambda could use a less pessimistic model where only certain program constructs may run callbacks, not any program point. (But I suppose there are sensible reasons why the current behavior was chosen?)
• There could be a way to localy "opt out" of the pessimistic be model to ask Flambda to be fine-grained only in some specific blocks. This would be ideal here, a more precise and meaningful annotation than [@inline never] (and wouldn't prevent inlining), and a more generic solution than adding more and more primitives as the need arises.

Yes, this is my understanding.

What would better alternatives be?

• We could just have compare_and_set and fetch_and_add be compiler primitives that Flambda would treat atomically.

The problem is more general, see for instance https://github.com/search?p=1&q=org%3Ajanestreet+%28%2A+BEGIN+ATOMIC+%2A%29&type=Code or b84f7ee#diff-3281003824dbd4299b844117c245dab1aff4aa02452d0c534fd096d388105ad8R53-R66

• Flambda could use a less pessimistic model where only certain program constructs may run callbacks, not any program point. (But I suppose there are sensible reasons why the current behavior was chosen?)

I do not think we need to ask as much, which sounds like would invalidate many transformations (most of the times code will be atomic only accidentally).

• There could be a way to localy "opt out" of the pessimistic be model to ask Flambda to be fine-grained only in some specific blocks. This would be ideal here, a more precise and meaningful annotation than [@inline never] (and wouldn't prevent inlining), and a more generic solution than adding more and more primitives as the need arises.

As a heavy user of reasoning on polling locations (re. prototypes of safe resource management), this is something I am looking forward to. Discussing the details of such an annotation would heavily depend on details of the work on adding new polling locations for multicore, which is why I tried to make it out of scope of the current PR. But you are right that this PR is a very good example of why such an annotation is desired, for the reasons you give.

Merged in trunk and in 4.12 (955a4b4).

Thanks!