Re:Rust Atomics and Locks by Mara Bos
by gpderetta on Wednesday August 14, 2024 @12:00PM
(#41247562)
> as long as all cross-thread interactions follow happens-before, then you can act as if everybody is sequentially-consistent.
I don't think that's the actual guarantee. You can enforce happens-before with just acquire/release, but AFIK that's not enough to recover SC in the general case[1].
As far as I understand, The Data Race Free - Sequentially Consistent memory model (DRF-SC) used by C++11 (and I think Java), says that as long as all operation on atomics are SC and the program is data-race-free, then the whole program can be proven to be sequentially consistent.
[1] but it might in some special cases, for example when all operations are mutex lock and unlock.
I don't think that's the actual guarantee. You can enforce happens-before with just acquire/release, but AFIK that's not enough to recover SC in the general case[1].
As far as I understand, The Data Race Free - Sequentially Consistent memory model (DRF-SC) used by C++11 (and I think Java), says that as long as all operation on atomics are SC and the program is data-race-free, then the whole program can be proven to be sequentially consistent.
[1] but it might in some special cases, for example when all operations are mutex lock and unlock.