[intro.races] p16 says:
If a value computation A of an atomic object M happens before a value computation B of M, and A takes its value from a side effect X on M, then the value computed by B is either the value stored by X or the value stored by a side effect Y on M, where Y follows X in the modification order of M.
This rule commonly can interpret this example
std::atomic<int> x{0};
// thread 1:
x.store(1); // #1
x.store(2); // #2
// thread 2:
x.load(); // #3
x.load(); // #4
According to [intro.races] p15, #2 follows #1 in the modification order of x, and if #3 reads 1, #4 may be 1 or 2 as per [intro.races] p16. In this case, the emphasized "where" clause imposes the requirement: If B does not read X, it must read some side effect that follows X in the modification order.
However, consider this example:
std::atomic<int> x{0};
// thread 1:
x.store(3); // #1
//thread 2:
x.store(4); // #2
//thread 3:
x.load(); // #3
x.load(); // #4
If #3 read 3 and #4 reads 4, can we infer 4 follows 3 in the modification order as per [intro.races] p16? IIUC, the current wording(i.e. the "where" clause) does not mean it specifies the order for Y, in other words, it does not say something like: if B reads Y, then Y follows X in the modification order.
I wonder if the read-read coherence rule can be used to infer the modification order for the second example.
How does the proposition logic work here such that one can reason backward from the observed behavior to the modification order?
We are not using the logic "backwards"; we're using it directly.
As you say in comments, this rule is an implication of the form "if P then Q", where P is
a value computation A of an atomic object M happens before a value computation B of M, and A takes its value from a side effect X on M
and Q is
the value computed by B is either the value stored by X or the value stored by a side effect Y on M, where Y follows X in the modification order of M.
We take M = x, A = #3, B = #4, and X = #1. Then the antecedent P is certainly true (#3 does happen before #4, by sequencing), so we may conclude that the consequent Q is also true (modus ponens, if you like).
The value computed by B (namely 4) is certainly not the value stored by X (which is 3), so the other branch of the disjunction must be the true one. Thus we now know:
4is the value stored by a side effect Y onx, where Y follows #1 in the modification order ofx.
If you want to be technical here, Y is implicitly bound by an existential quantifier, which they didn't write but which is clearly intended. We could read it more smoothly as "there exists a side effect Y on x such that the value stored by Y is 4, and Y follows #1 in the modification order." Let's abbreviate the subformula "the value stored by Y is 4, and Y follows #1 in the modification order" by R(Y).
So this statement R(Y) must be true of some side effect Y. Now R(#1) is certainly false, since #1 doesn't follow itself and the value stored by #1 is not 4. This leaves only #2. We conclude that R(#2) is true, which tells us two things:
the value stored by #2 is 4 (we already knew this); and
#2 follows #1 in the modification order (as desired).
As a simple example of the logic here, suppose I tell you (truthfully) that "In this room, there is a man who has gray hair and is a famous author." If there is only one man in the room with gray hair, you may validly deduce that he is a famous author.
We are not attempting to use the converse of p16, which would be "if Q then P". That statement is not an axiom of the memory model, and for typical implementations it wouldn't be true. If it were, then given the following code:
std::atomic<int> x;
void t1() {
x.store(3, std::memory_order_relaxed); // #1
x.store(4, std::memory_order_relaxed); // #2
}
void t2() {
x.load(std::memory_order_relaxed); // #3, returns 3
}
void t3() {
x.load(std::memory_order_relaxed); // #4, returns 4
}
we would be able to conclude that #3 happens before #4. But the whole point of the memory model is that without more synchronization, we can't know that. (For that matter, if #3 and #4 both returned 3, the "if Q then P" statement would imply that each happens before the other, which is absurd since happens-before is a partial order.)