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 su

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). [1] so aside the lock/unlock special case.