> You get to pretend everything is sequentially consistent if you write proper synchronization. The easiest way to satisfy proper synchronization is an acquire-release model
But acquire/release give, generally,a partial ordering, not a total order like sequential consistency. That's often enough of course.
The data-race-free theorem states that, in the absence of data races, acquire/release is indistinguishable from sequential consistency. Define data races to be UB, as C/C++ do, and you get to the state that acquire/release lets you pretend everything (except atomic operations themselves) is sequentially consistent.
My understanding is that that only applies to programs that use mutex lock/unlock operations (which do have acquire/release semantics), but not to programs that use acq/rel memory operations in general. For example: https://www.hboehm.info/c++mm/sc_proof.html which contains the the SC proof for lock operations that you mention, but also a counterexample for acq/rel atomics.
The original data-race-free models are based on acquire/release semantics that underlie the C++ memory model (https://pages.cs.wisc.edu/~markhill/papers/topds93_drf1.pdf), so the use of acquire/release atomics should provide the same guarantees as mutex lock/unlock.
However, the sequential consistency guarantee doesn't necessarily apply to atomics themselves, and I think the difference between the data-race-free-0 and data-race-free-1 models is whether not they would extend the guarantee to the release-acquire atomic operations.
To clarify, you are saying that there is a model that guarantees DRF-SC even if the atomic operations are not themselves SC? Aside from the fact that I'm not sure such guarantee would be useful or even meaningful, I think you can extend Bohem counterexample to add non-atomic cells (and conditional reads) and show SC violations.
My understanding of the C++ memory model since the early standardization discussions was that DRF-SC is only generally guaranteed[1] if the acquire/release operations themselves were SC and can't be easily recovered otherwise.
I.e.: full SC requires all operations to be SC, DRF-SC requires, in addition of no data races, only the synchronization edges to be SC.
I suspect that's what the drf-1 model in the paper you have linked specifies. But it will take me a bit to digest it and I'll readily admit that I might be wrong (thanks for the paper BTW).
This is at the penumbra of my knowledge of memory ordering, so it's entirely possible that I'm completely incorrect here, especially because confirming correctness requires spending a lot of time making sure that the various papers are all using the same definitions for the various words.
But acquire/release give, generally,a partial ordering, not a total order like sequential consistency. That's often enough of course.