cplusplus / CWG

Core Working Group
23 stars 7 forks source link

[intro.races] p18 "or" is ambiguous in its meaning #466

Closed xmh0511 closed 10 months ago

xmh0511 commented 10 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.

Consider this example:

std::atomic<int> v{0};
auto c = [](){v.store(1,std::memory_order::release); return 1;}();
auto c2 = [](){v.store(2,std::memory_order::release); return 2;}();

int main(){
   auto r = v.load(std::memory_order::acquire); // #1
}

It seems that #1 reads the value 2 is intended to be guaranteed by [intro.races] p18. However, or here can have meaning: it's an option, that is, the chosen value can be X or Y. However, the intent is meant to: If there is a side effect following X in the modification order of M, B shall take its value from Y

Suggested Resolution

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, If there is a side effect Y following X in the modification order of M, B shall take its value from Y.

t3nsor commented 10 months ago

[intro.races]/18 applies to each side effect on M that happens before B, thus resulting in a conjunction of constraints:

If X2 follows X1 in the modification order of M, then both constraints are satisfied simultaneously when B takes its value from X2.

There's no ambiguity that I can see here.

tkoeppe commented 10 months ago

See also discussion on https://github.com/cplusplus/draft/pull/6501. I agree that I don't see an ambiguity here.

xmh0511 commented 10 months ago

[intro.races]/18 applies to each side effect on M that happens before B, thus resulting in a conjunction of constraints:

* B takes its value from X1 or from a side effect Y that follows X1, and

* B takes its value from X2 or from a side effect Y that follows X2

If X2 follows X1 in the modification order of M, then both constraints are satisfied simultaneously when B takes its value from X2.

There's no ambiguity that I can see here.

Note that "a". The complete sentence of the rule should be:

If there is 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.

The rule does not convey the meaning: the rule should repeatedly apply until you encounter the last side effect in the modification order of M that satisfies the rule. Instead, it conveys, that if there exists such a side effect, we can take its value. In this example, X1 and X2 both satisfy the rules, why we must take the value from X2?

I think the intended meaning should be worded as:

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

xmh0511 commented 10 months ago

See also discussion on cplusplus/draft#6501. I agree that I don't see an ambiguity here.

In that issue, we only get the conclusion that:

  1. [intro.race]/14 only bounds the set of possible values
  2. [intro.races] p15, [intro.races] p16, [intro.races] p17, and [intro.races] p18 give the further constraints

This issue is about [intro.races] p18, which cannot convey the intended meaning.

t3nsor commented 10 months ago

Note that "a". The complete sentence of the rule should be:

If there is 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.

Well, no, because that's not what the rule is supposed to mean.

I guess, to be extremely clear, the rule should say something like "For each side effect X ..."

But I think everyone else already interpreted it that way.

xmh0511 commented 10 months ago

I guess, to be extremely clear, the rule should say something like "For each side effect X ..."

Honestly, even though we change "a side effect X" to "For each side effect X", the sentence is still hard to read. Why don't we just directly say:

the latest side effect X in the modification order of M that happens before a value computation B ...

t3nsor commented 10 months ago

In general there is no "latest side effect" because "happens before" is not a total order. So in general you can't avoid the need for a conjunction of constraints.

xmh0511 commented 10 months ago

In general there is no "latest side effect" because "happens before" is not a total order. So in general you can't avoid the need for a conjunction of constraints.

I think the proposed sentence means: Given a set of side effects in the modification order that happen before the value computation B, X is the latest one in the modification order in that set. In other words, assuming the modification order is {M0, M1, M2, M3, M4, ... Mn}, each side effect in the modification order that happens before B forms a set, for example, they are {M0, M1, M2, M3}, since in this set, M3 is the latest one in the modification order, X is M3.

t3nsor commented 10 months ago

Well, it sounds like you came up with a more complicated way to say it, then. Is this an improvement?

xmh0511 commented 10 months ago

Well, it sounds like you came up with a more complicated way to say it, then. Is this an improvement?

First, I think the proposed wording can clearly convey what the rule intends to express and avoid the ambiguous. Second, I don't think the proposed wording is more complex than the original wording(from the perspective of understanding). The complete wording is just:

For each side effect X in the modification order of M that happens before a value computation B, evaluation B shall take its value from the latest X(in the modification order) or from a side effect Y that follows such X in the modification order of M.

jensmaurer commented 10 months ago

I'm not seeing an ambiguity, and the proposed text doesn't feel like an improvement to me.

xmh0511 commented 10 months ago

I'm not seeing an ambiguity, and the proposed text doesn't feel like an improvement to me.

@jensmaurer Notice that there are two side effects in the modification that happen before the value computation of the load in this example, so, could you interpret which side effect is X by the current wording?