Details missing around std::sync::atomic and their orderings

[vorner]

The atomic orderings are something that would be really useful to have the exact details documented, as one might want to go as far as to write proofs about what orderings are safe to use, if any at all.

To be more specific, I'm missing these two pieces now:

• SeqCst says it acts like AcqRel with additionally anchoring the operation on a global timeline. However, AcqRel on load is effectively only Acquire (I guess because without store, other threads can't know when that load effectively happened). Does that apply to SeqCst on load as well that operations can be moved after it?
• Is compare_and_swap considered an operation that combines load and store even in case it fails, or is it only a load (and therefore turns AcqRel into Acquire only)?

I'd be happy to update the documentation, but I don't know what guarantees are actually provided.

[RalfJung]

Does that apply to SeqCst on load as well that operations can be moved after it?

A SeqCst on load is like an Acquire that also has a consistent ordering wrt. all other SeqCst operations. It does not, otherwise, have Release semantics.

Also notice that AcqRel does not always mean Acquire and Release! This seems to be a common view, but it is broken by compare_and_swap(..., AcqRel) which, in case of failure is just an Acquire load but not a Release operation -- which answers your second question. I suggested to change the meaning of AcqRel to make that all clearer but couldn't find much agreement.

I have recently updated the docs with #53106, could you check if that helps answering your questions?

[vorner]

Thanks, yes, I think this helps a lot and answers my questions.