Is there any wording in the standard that guarantees that relaxed stores to atomics won't be lifted above the locking of a mutex? If not, is there any wording that explicitly says that it's kosher for the compiler or CPU to do so?
For example, take the following program (which could potentially use acq/rel for foo_has_been_set
and avoid the lock, and/or make foo
itself atomic. It's written this way to illustrate this question.)
std::mutex mu;
int foo = 0; // Guarded by mu
std::atomic<bool> foo_has_been_set{false};
void SetFoo() {
mu.lock();
foo = 1;
foo_has_been_set.store(true, std::memory_order_relaxed);
mu.unlock();
}
void CheckFoo() {
if (foo_has_been_set.load(std::memory_order_relaxed)) {
mu.lock();
assert(foo == 1);
mu.unlock();
}
}
Is it possible for CheckFoo
to crash in the above program if another thread is calling SetFoo
concurrently, or is there some guarantee that the store to foo_has_been_set
can't be lifted above the call to mu.lock
by the compiler and CPU?
This is related to an older question, but it's not 100% clear to me that the answer there applies to this. In particular, the counter-example in that question's answer may apply to two concurrent calls to SetFoo
, but I'm interested in the case where the compiler knows that there is one call to SetFoo
and one call to CheckFoo
. Is that guaranteed to be safe?
I'm looking for specific citations in the standard.
I think I've figured out the particular partial order edges that guarantee the program can't crash. In the answer below I'm referencing version N4659 of the draft standard.
The code involved for the writer thread A and reader thread B is:
We seek a proof that if B3 executes, then A2 happens before B3, as defined in [intro.races]/10. By [intro.races]/10.2, it's sufficient to prove that A2 inter-thread happens before B3.
Because lock and unlock operations on a given mutex happen in a single total order ([thread.mutex.requirements.mutex]/5), we must have either A1 or B2 coming first. The two cases:
Assume that A1 happens before B2. Then by [thread.mutex.class]/1 and [thread.mutex.requirements.mutex]/25, we know that A4 will synchronize with B2. Therefore by [intro.races]/9.1, A4 inter-thread happens before B2. Since B2 is sequenced before B3, by [intro.races]/9.3.1 we know that A4 inter-thread happens before B3. Since A2 is sequenced before A4, by [intro.races]/9.3.2, A2 inter-thread happens before B3.
Assume that B2 happens before A1. Then by the same logic as above, we know that B4 synchronizes with A1. So since A1 is sequenced before A3, by [intro.races]/9.3.1, B4 inter-thread happens before A3. Therefore since B1 is sequenced before B4, by [intro.races]/9.3.2, B1 inter-thread happens before A3. Therefore by [intro.races]/10.2, B1 happens before A3. But then according to [intro.races]/16, B1 must take its value from the pre-A3 state. Therefore the load will return false, and B2 will never run in the first place. In other words, this case can't happen.
So if B3 executes at all (case 1), A2 happens before B3 and the assert will pass. ∎