[basic.start.dynamic] p6 "Strongly happens before" vs. "happens before" for atomic object rules

[xmh0511]

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

[basic.start.dynamic] p6 says:

It is implementation-defined whether the dynamic initialization of a non-block inline variable with static storage duration is sequenced before the first statement of main or is deferred. If it is deferred, it strongly happens before any non-initialization odr-use of that variable. It is implementation-defined in which threads and at which points in the program such deferred dynamic initialization occurs.

Consider this example:

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

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

Assuming the dynamic initialization at #1 is deferred, the implementation obeys the rule that the initialization strongly happens before any non-initialization odr-use of that variable.

At best, we can get the conclusion that the side effect to the atomic object strongly happens before #2, that is [intro.races] p18 cannot apply to this case because the rule is in terms of happens-before.

Suggested Resolution

In this document, some evaluations to an object are specified as strongly/simply happens before, and the value computation of an atomic object is in terms of happen before.

[jensmaurer]

First of all, the rule you quoted concerns "inline" variables, but there is no inline variable in your example. Second, the variable "c" is not used at all, thus its initialization may be deferred indefinitely (e.g. until the end of main or so). Third, I thought that "strongly happens before" implied "happens before". If that's not the case in your opinion, we should discuss that.

[xmh0511]

First of all, the rule you quoted concerns "inline" variables, but there is no inline variable in your example.

It's my wrong, I meant p5

It is implementation-defined whether the dynamic initialization of a non-block non-inline variable with static storage duration is sequenced before the first statement of main or is deferred. If it is deferred, it strongly happens before any non-initialization odr-use of any non-inline function or non-inline variable defined in the same translation unit as the variable to be initialized.

Second, the variable "c" is not used at all, thus its initialization may be deferred indefinitely (e.g. until the end of main or so).

The example is intended to be:

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

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

Third, I thought that "strongly happens before" implied "happens before".

This is the key point here. According to the definition, they are not the same, I think.

[ranaanoop]

Related thread: Is the result of the value computation of an atomic object unspecified?

[t3nsor]

Third, I thought that "strongly happens before" implied "happens before".

This is the key point here. According to the definition, they are not the same, I think.

If it's true that "strongly happens before" implies "happens before", then why do you want to weaken the initialization order guarantee from "strongly happens before" to "happens before"?

If it's not true that "strongly happens before" implies "happens before", then can you give an example of two operations X and Y, where X strongly happens before Y, but X doesn't happen before Y?

[xmh0511]

Third, I thought that "strongly happens before" implied "happens before".

This is the key point here. According to the definition, they are not the same, I think.

If it's true that "strongly happens before" implies "happens before", then why do you want to weaken the initialization order guarantee from "strongly happens before" to "happens before"?

If it's not true that "strongly happens before" implies "happens before", then can you give an example of two operations X and Y, where X strongly happens before Y, but X doesn't happen before Y?

Given the condition A, we can infer the result whether it "happens before" or "strongly happens before" according to the rules defined in [intro.races] p10 and [intro.races] p12. However, if I said the evaluation A "strongly happens before" B, you cannot inversely deduce any condition from that result and use that condition to determine whether A "happens before" B or not. It is a simple mathematical question.

[jensmaurer]

So, please walk us through the rules, item by item, why "strongly happens before" does not imply "happens before". It was intended to do so.

[xmh0511]

So, please walk us through the rules, item by item, why "strongly happens before" does not imply "happens before". It was intended to do so.

When the rule directly says A strongly happens before B, we cannot know the reason, in other words, which bullet does it satisfy that is listed in [intro.races] p12?

• A is sequenced before B, or
• A synchronizes with D, and both A and D are sequentially consistent atomic operations ([atomics.order]), or
• there are evaluations B and C such that A is sequenced before B, B simply happens before C, and C is sequenced before D, or
• there is an evaluation B such that A strongly happens before B, and B strongly happens before D.

So, you cannot know whether A happens before B according to the rule defined in [intro.races] p10

• A is sequenced before B, or
• A inter-thread happens before B.

Moreover, strongly happen before is a different concept from happen before because they have different definitions and are literally different.

[frederick-vs-ja]

When the rule directly says A strongly happens before B, we cannot know the reason, in other words, which bullet does it satisfy that is listed in [intro.races] p12?

Whatever the reason is, we can infer that A happens before B.

I don't think it's possible to construct a counterexample. I'd like to see one if I'm wrong.

[xmh0511]

Whatever the reason is, we can infer that A happens before B.

Which provision do you base on? By your logic, Does that mean if A happens before B, the A also strongly happens before B? By your logic, if an identifier is an id-expression, then the identifier is a declarator-id?

When you say A happens before B, A and B should first satisfy the bullet defined for "happens before".

I think, by using mathematical symbols, the issue is simple to embody. P1 -> Q1, P2 -> Q2, where P1 denotes the condition defined in [intro.races] p10 and Q1 means "happens before", as well, Q2 means the condition defined in [intro.races] p12 and Q2 means "strongly happens before", and X∈ P1∩P2, X means these common bullets where [intro.races] p10 and [intro.races] p12 has. Your logic means, given the result Q2, then you can infer X, then you say X can infer Q1.

[jensmaurer]

I'm not following your logic. We need to prove that "A strongly happens before B" implies "A happens before B".

If A is sequenced before B, we satisfy the first bullet of the definition of "A happens before B" and we're good.

If A is not sequenced before B, we need to check whether the three remaining bullets from "A strongly happens before B" imply "A inter-thread happens before B". I believe that is the case (you have to dissolve "inter-thread happens before", of course), but if you find a situation where I'm wrong, please tell me with specificity. Until such time, I can't see a core issue here.

[xmh0511]

If A is not sequenced before B, we need to check whether the three remaining bullets from "A strongly happens before B" imply "A inter-thread happens before B". I believe that is the case (you have to dissolve "inter-thread happens before", of course), but if you find a situation where I'm wrong, please tell me with specificity. Until such time, I can't see a core issue here.

@jensmaurer The issue is basic.start.dynamic#5 says:

If it is deferred, it strongly happens before any non-initialization odr-use of any non-inline function or non-inline variable defined in the same translation unit as the variable to be initialized.

The rule does not clearly specify how it "strongly happens before"? Is it because the sequence before or inter-thread happens before? And you cannot check the three remaining bullets from "A strongly happens before B". Because the rule just didn't say how A "strongly happens before" B. So, consider this case:

int v = 1;
int main(){
  auto r = v;
}

Assuming the initialization of v is deferred, then we unclearly whether the side effect is a visible side effect or not according to intro.races#13, because we cannot check whether the relationship is the "happen before".

[jensmaurer]

You don't need to know whether it's sequenced-before or something else. You can prove (on the abstract level) that "strongly happens before" implies "happens before", so there is no problem. (You can't rely on "sequenced before", though, and that's intentional.)

I would like to remind you that this is not a tutorial forum for reading the standard, but a submission venue for core issues.

[xmh0511]

You don't need to know whether it's sequenced-before or something else. You can prove (on the abstract level) that "strongly happens before" implies "happens before", so there is no problem. (You can't rely on "sequenced before", though, and that's intentional.)

So, you mean A happens before B is equivalent to that A strongly happens before B?

[jensmaurer]

No, I said "A strongly happens before B" implies "A happens before B", i.e. a situation where "A strongly happens before B" is true is also a situation where "A happens before B" is true. The inverse is not true.

[xmh0511]

No, I said "A strongly happens before B" implies "A happens before B", i.e. a situation where "A strongly happens before B" is true is also a situation where "A happens before B" is true. The inverse is not true.

@jensmaurer Since [intro.races] p10 is the definition of happen-before, it should tell the complete story, why don't we augment the list as:

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

• A is sequenced before B, or
• A inter-thread happens before B, or
• A simply happens before B, or
• A strongly happens before B.

This is clearer.

[jensmaurer]

No. Inter-thread happens before is itself a complicated recursive relationship, and there's no point in inlining half of its definition.

[xmh0511]

No. Inter-thread happens before is itself a complicated recursive relationship, and we there's no point in inlining half of its definition.

If the definition of "happens before" does not mention simply happen before and strongly happen before, this implies there is no relationship that can be established between them. The fact is "happens before" does want to cover them.

[jensmaurer]

If the definition of "happens before" does not mention simply happen before and strongly happen before, this implies there is no relationship that can be established between them.

That's plain wrong. Sometimes, you have to look "through" definitions to determine whether one definition implies the other. You can answer the question "is each field also a ring" even if the definition of "field" doesn't mention "ring", but spells out the conditions afresh.