[intro.races] p10 How to prove that `B` does not happen before `A` is true when cannot prove that `B` happens before `A` is false?

[xmh0511]

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;
  auto t1 = std::thread([&v](){
     v.store(2, std::memory_order::relaxed); // A
  });
  auto r = v.load(std::memory_order::relaxed); // B
  t1.join();
}

[intro.races] p14 imposes the requirement to limit which values can be possibly read by B, which says:

The value of an atomic object M, as determined by evaluation B, shall be the value stored by some side effect A that modifies M, where B does not happen before A.

This rule limits which values can be possibly read by B. The rules after p14 impose other requirements but they are irrelevant here. Note the emphasized wording, to be the value read by B, the requirement that B does not happen before A should be satisfied. We either directly prove the condition is true or prove the opposition is false. Since we didn't define the concept that X does not happen before Y, we just define how X happens before Y, hence, in order to prove B does not happen before A is true, we need to prove B happens before A is false. The opposition is false can prove !( A happens before B) is true.

However, in this example, according to the definition of "happens before", we cannot prove that B happens before A is false, which means, we cannot prove the condition that B does not happen before A is true. This is, we cannot check the condition in [intro.races] p14 for the above example. Does it mean whether B can read A is underspecified?

Suggested Resolution

When checking [intro.races] p14, how to check the condition "B does not happen before A" is true?

[jensmaurer]

That's exactly the point here: A does not (necessarily) happen before B, thus the value of v read at B is either the value stored by A or the initial value of v (i.e. 0).

I'm not seeing a defect here, and I repeat my earlier statement: This forum is not a tutorial for reading the standard. The memory model descriptions are particularly intricate; please familiarize yourself with partial orders.

[xmh0511]

@jensmaurer The issue may be my misread. If the condition in the list of [intro.races] p10 is not met, then A happens before B is false, so, the negtivation of A happens before B is true.