3 ms·

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

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 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.

jcranmer 3y ago
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 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.
- gpderetta 3y ago
  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.
  - jcranmer 3y ago
    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.
deleted 3y ago
[deleted]

jcranmer 3y ago

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 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.

gpderetta 3y ago
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.
- jcranmer 3y ago
  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.

deleted 3y ago

[deleted]