We (@fabbing and I) are reading this, slowly.

"meh, that is not much harder than the current model"

I see the point for Atomic.get_relaxed. Atomic.set_relaxed, on the other hand, is profoundly weird, and there would need to be a better reason than symmetry to add it.

Atomic.set_relaxed breaks coherence of atomic reads

Atomic reads in OCaml satisfy coherence: if another thread writes an atomic and you read it repeatedly, then you will observe only one old->new transition (once you see the new value, further reads will agreee). This is not true of the proposed semantics: if an atomic and nonatomic write race on the same location, then the nonatomic write can choose a higher timestamp then the atomic one without updating the frontier, and atomic readers will then nondeterministically choose between the two, flickering between then arbitrarily many times.

(Underlying hardware is coherent so you might think this saves you from observing such flickering. It does not: see Example 2 in the linked PLDI paper, where this sort of flickering appears due to interactions between compiler and hardware optimisations).

Atomic.set_relaxed breaks the implementation

This assumption from the RFC is false as written:

We assume that the current compilation strategy is enough to realize this memory model, by simply compiling all accesses as we are currently doing.

The OCaml memory model has a property that the proposed semantics preserves, which is that frontiers in threads and locations grow monotonically - information about writes is never forgotten. A consequence of this is that for two atomic writes to the same location, one of them happens before the other, a property that does not hold in most memory models.

This property is not naturally true of hardware models, and OCaml does some work to ensure it. (Roughly, by compiling atomic stores more like atomic exchanges).

The proposed implementation would break this property, as nonatomic writes naively implemented would rewind the frontier of a location, because of weakness of coherence ordering in hardware models. That is, a semantics that is somewhat closer to what the implementation would do is one where Write-NA updates the location's frontier to the minimum of the previous and the thread's frontiers. (This would break the monotonicity and total-ordering-of-atomic-writes properties)

Thanks! It looks like a reasonable next step would be to propose get_relaxed only and forget about set_relaxed for now, at least until we get clear evidence of usefulness/importance of the primitive.

I am planning to close the current PR and open a new one with a revised/simplified proposal, so that we can easily compare the two, disentangle the two discussions, and restart here if we decide to someday.

In #41 I proposed a restricted version that only allows relaxed reads (not relaxed writes) on memory locations. I am closing here as planned -- but feel free to still comment on the full mixed-atomicity model in the present thread if there is something more to be said.

(Thanks @OlivierNicole and @fabbing for the proof-reading / typos!)

Thanks! It looks like a reasonable next step would be to propose get_relaxed only and forget about set_relaxed for now, at least until we get clear evidence of usefulness/importance of the primitive.

Yes, I believe get_relaxed is far more important that set_relaxed.

One use case where I have used the equivalent of set_relaxed is in "initialization". In Kcas, for example, a transaction builds a tree-like data structure, step-by-step, that then needs to be "closed" into a cycle (the cyclic data structure is essential for the lock-free algorithm to update multiple locations atomically). All of this happens before multiple threads can see the data structure. It is entirely safe to close/create the cycle by writing to an atomic location in a relaxed manner. The data structure is then made visible to other threads via a sequentially consistent atomic write (which means that the relaxed write cannot be reordered to happen after the sequentially consistent write).