cplusplus / CWG

Core Working Group
23 stars 7 forks source link

[intro.races] p18 should have a similar wording to that of [intro.races] p13 to avoid the intervening side effect #468

Closed xmh0511 closed 8 months ago

xmh0511 commented 8 months ago

Full name of submitter (unless configured in github; will be published with the issue): Jim X

[intro.races] p18 says:

If a side effect X on an atomic object M happens before a value computation B of M, then the evaluation B shall take its value from X or from a side effect Y that follows X in the modification order of M.

Just consider this example:

int main(){
  std::atomic<int> m{0};
  m.store(1, std::memory_order::release);  // #1 
  m.store(2, std::memory_order::release); // #2
  m.load(std::memory_order::acquire);  // #3
}

#1 is sequenced before #2 and #2 is sequenced before #3 according to [intro.execution] p9. Since sequenced before is transitive as per [intro.execution] p8, #1 is also sequenced before #3. Then, according to [intro.races] p10:

An evaluation A happens before an evaluation B (or, equivalently, B happens after A) if:

  • A is sequenced before B, or

Because #1 is sequenced before #3, #1 happens before #3. Similarly, #2 happens before #3. So, there are two side effects in the modification of atomic object m that happen before the value computation by #3. In this example, [intro.races] p18 cannot clearly which side effect is that X, #1 or #2? They both satisfy the rule.

If, in this example, assume the object m were a non-atomic scalar object, then [intro.races] p13 would clearly specify the result for this case, which says:

A visible side effect A on a scalar object or bit-field M with respect to a value computation B of M satisfies the conditions:

  • A happens before B and
  • there is no other side effect X to M such that A happens before X and X happens before B.

The value of a non-atomic scalar object or bit-field M, as determined by evaluation B, shall be the value stored by the visible side effect A.

The second bullet prevents us from considering #1 a visible side effect here if m is a non-atomic object. As well, [intro.races] p18 should have similar wording to make the intervening/previous side effect not to be considered as the side effect X.

Suggested Resolution

If a side effect X on an atomic object M happens before a value computation B of M and there is no other side effect D to M such that X happens before D and D happens before B, then the evaluation B shall take its value from X or from a side effect Y that follows X in the modification order of M.

jensmaurer commented 8 months ago

[intro.races] p18 must be applied to both stores in your example, and must hold for both stores. Thus:

  m.store(1, std::memory_order::release);  // X1
  m.store(2, std::memory_order::release); // X2; might be Y1
  m.load(std::memory_order::acquire);  // B

Reminder on the rule:

If a side effect X on an atomic object M happens before a value computation B of M , then the evaluation B takes its value from X or from a side effect Y that follows X in the modification order of M.

If you instantiate this rule for X1, then it's unspecified whether B observes X1 or X2. If you instantiate this rule for X2, then it's clear that B observes X2.

Both together can only be true if B observes X2.

I can't see a core issue here; the wording says what it should say.

xmh0511 commented 8 months ago

@jensmaurer

If you instantiate this rule for X1, then it's unspecified whether B observes X1 or X2. If you instantiate this rule for X2, then it's clear that B observes X2.

No rule says that the observation of B must be specified. Consider introducing the third store

  m.store(1, std::memory_order::release);  // X1
  m.store(2, std::memory_order::release); // X2; 
  m.store(3, std::memory_order::release); // X3;
  m.load(std::memory_order::acquire);  // B

How do you think the current wording can impose the requirement that what B observe should make all three must be true?

jensmaurer commented 8 months ago

There's a single B; you instantiate the rule once for each X_n, among them:

"If a side effect X3 on an atomic object M happens before a value computation B of M , then the evaluation B takes its value from X3 or from a side effect Y that follows X in the modification order of M."

Since X3 is sequenced before B and thus happens before B and there is no other side effect Y that follows X3 (or is your claim that there might be one?), B must observe X3.

xmh0511 commented 8 months ago

Since X3 is sequenced before B and thus happens before B and there is no other side effect Y that follows X3 (or is your claim that there might be one?), B must observe X3.

Do you agree that X1, X2, and X3 all happen before the value computation B? When B reads X1, Is the rule violated? When B reads X2, Is the rule violated? When B reads X3, Is the rule violated? Notice the "a" in a side effect happens before B in .... The rule just requires two conditions:

  1. The side effect happens before B, and
  2. It is in the modification order.

Why only does B read X3 won't violate that rule? According to the current wording, why is X1 not the side effect? Why is X2 not the side effect?

xmh0511 commented 8 months ago

I see our divergence here. You mean, the current wording intends to mean that the value observed by the value computation B should also make the rule be satisfied when applying to all other side effects that happen before B.

My opinion of this rule is, that the rule actually can be understood as the rule is true when applying for every single side effect that happens before B, and does not intend to mean we need to associate the result with other results of applying the rule to other side effects. In other words, separately consider that rule instead of considering the rule repeatedly for each side effect and conjunct the results to determine the common result that can make them all be true.