[intro.execution] p8 The meaning of "execution of A shall precede the execution of B" is underspecified #765
Description
Full name of submitter (unless configured in github; will be published with the issue): Jim X
Consider this example:
#include <atomic>
#include <thread>
int main(){
std::atomic<int> v = 0;
std::atomic<bool> flag = false;
std::thread t1([&](){
while(!flag.load(std::memory_order::relaxed)){} // #1
assert(v.exchange(2,std::memory_order::relaxed) == 1); // #2
});
std::thread t2([&](){
if(v.exchange(1,std::memory_order::relaxed) == 0){ // #3
flag.store(true, std::memory_order::relaxed); // #4
}
});
t1.join();
t2.join();
}To prove that the assertion at #2 never fails, we should infer the program in this way, since all operations are relaxed, "happen-before" is useless in the inference of this program(i.e., which is only about visibility), and the behavior in this program is only described by logic.
We can assume that the exchange at #3 reads 1 so that the condition is false, #4 won't be executed, the loop won't exit, the assertion won't be executed, hence the assertion can never fail. Or, in another way, we can assume the assertion could fail and read the value 0, which would mean the condition in if must read 2, the condition is false, #4 won't be executed, the loop cannot exit, so #2 cannot be executed, which contradicts.
In both reasoning chains, however, we need to formally prove why #2 is unreachable if the loop does not exit. I think a possible proof is [intro.execution] p8
Sequenced before is an asymmetric, transitive, pair-wise relation between evaluations executed by a single thread ([intro.multithread]), which induces a partial order among those evaluations. Given any two evaluations A and B, if A is sequenced before B (or, equivalently, B is sequenced after A), then the execution of A shall precede the execution of B.
The condition in the while that returns true is sequenced before #2. The standard does not specify what "the execution of A shall precede the execution of B" means. Does it mean B won't be executed if the evaluation of A is not completed, or something else?
Alternatively, we may specify how an iteration statement affects the control flow to determine whether the subsequent statement is executed.