c++ - Can both conditions be true when each depends on another - Stack Overflow

admin管理员组

文章数量:1023628

I seem to be confused by such two examples. The first example is:

std::atomic<int> x = 1;
//thread 1:
int expected = 1;
if (xpare_exchange_strong(expected,0,relaxed,relaxed) == true){ // #1
    x.store(2,relaxed);  // #2
}
//thread 2:
int expected = 2;
if (xpare_exchange_strong(expected,3,relaxed,relaxed)==true){  // #3
}

In this example, it is impossible that #3 reads the value written by #2 but #1 returns false. I prove that in this way: #2 is invoked only when the condition at #1 is true, so it is impossible that #1 returns false while #3 returns true. I don't know whether there is a formal way to prove that's impossible(for example, from the perspective of the formal wording or modification order).

Consider the second example:

std::atomic<int> x = 2;
std::atomic<int> y = 0;
//thread 1:
if(x.exchange(2,Relaxed) == 1) { // #1
  y.store(1,Relaxed); // #2
}
//thread 2:
if(y.exchange(2,Acquire) == 1){ // #3
    x.store(1,Release); // #4
}

However, applying the above logic to this example seems to not work. In the second example, can both conditions be true? Using the above logic, if #1 returns 1, that means #1 reads #4, and #4 is invoked only if #3 reads #2, and #2 is invoked only if #1 returns 1, so the proof seems to form a cycle. However, from the perspective of memory order, since #4 does not synchronize with #1 and #2 does not synchronize with #3, the condition being true does not impose on how the operations to the other variable are reordered. In other words, when #3 reads #2, #1 and #4 is still unordered, as well as #3 and #2 is also unordered when #1 reads #4.

Is there a formal way to work on both examples?

Updated:

The second example is much like the example in [atomics.order] p9

[Note 7: The recommendation similarly disallows r1 == r2 == 42 in the following example, with x and y again initially zero:
// Thread 1:
r1 = x.load(memory_order::relaxed);
if (r1 == 42) y.store(42, memory_order::relaxed);
// Thread 2:
r2 = y.load(memory_order::relaxed);
if (r2 == 42) x.store(42, memory_order::relaxed);
— end note]

[atomics.order] p8 says:

Implementations should ensure that no “out-of-thin-air” values are computed that circularly depend on their own computation.

However, this wording just uses should, which is not mandatory. So, the second example is still possible that both conditions are true?

How about this one?

std::atomic<int> v = {0};
//thread 1:
if(v.load(acquire) == 1){ // #1
   v.store(2,release);  // #2
}
//thread 2:
if(v.load(relaxed) == 2){ // #3
   v.store(1,relaxed);  // #4
}

I seem to be confused by such two examples. The first example is:

std::atomic<int> x = 1;
//thread 1:
int expected = 1;
if (xpare_exchange_strong(expected,0,relaxed,relaxed) == true){ // #1
    x.store(2,relaxed);  // #2
}
//thread 2:
int expected = 2;
if (xpare_exchange_strong(expected,3,relaxed,relaxed)==true){  // #3
}

In this example, it is impossible that #3 reads the value written by #2 but #1 returns false. I prove that in this way: #2 is invoked only when the condition at #1 is true, so it is impossible that #1 returns false while #3 returns true. I don't know whether there is a formal way to prove that's impossible(for example, from the perspective of the formal wording or modification order).

Consider the second example:

std::atomic<int> x = 2;
std::atomic<int> y = 0;
//thread 1:
if(x.exchange(2,Relaxed) == 1) { // #1
  y.store(1,Relaxed); // #2
}
//thread 2:
if(y.exchange(2,Acquire) == 1){ // #3
    x.store(1,Release); // #4
}

However, applying the above logic to this example seems to not work. In the second example, can both conditions be true? Using the above logic, if #1 returns 1, that means #1 reads #4, and #4 is invoked only if #3 reads #2, and #2 is invoked only if #1 returns 1, so the proof seems to form a cycle. However, from the perspective of memory order, since #4 does not synchronize with #1 and #2 does not synchronize with #3, the condition being true does not impose on how the operations to the other variable are reordered. In other words, when #3 reads #2, #1 and #4 is still unordered, as well as #3 and #2 is also unordered when #1 reads #4.

Is there a formal way to work on both examples?

Updated:

The second example is much like the example in [atomics.order] p9

[Note 7: The recommendation similarly disallows r1 == r2 == 42 in the following example, with x and y again initially zero:
// Thread 1:
r1 = x.load(memory_order::relaxed);
if (r1 == 42) y.store(42, memory_order::relaxed);
// Thread 2:
r2 = y.load(memory_order::relaxed);
if (r2 == 42) x.store(42, memory_order::relaxed);
— end note]

[atomics.order] p8 says:

Implementations should ensure that no “out-of-thin-air” values are computed that circularly depend on their own computation.

However, this wording just uses should, which is not mandatory. So, the second example is still possible that both conditions are true?

How about this one?

std::atomic<int> v = {0};
//thread 1:
if(v.load(acquire) == 1){ // #1
   v.store(2,release);  // #2
}
//thread 2:
if(v.load(relaxed) == 2){ // #3
   v.store(1,relaxed);  // #4
}

• c++
• language-lawyer
• atomic

Share Improve this question Follow edited Nov 22, 2024 at 1:58 xmh0511 asked Nov 19, 2024 at 6:22 xmh0511xmh0511 7,35911 gold badge1111 silver badges4141 bronze badges 21

• 1 This doesn't seem like correct code. First argument is T&, so literal is not accepted. – Marek R Commented Nov 19, 2024 at 10:16
• Another strange thing is: == true (which is obsolete boilerplate), I do not why I can se this so often. – Marek R Commented Nov 19, 2024 at 10:19
• 1 My understanding is that the "should" in the out-of-thin-air rule is simply because the rule itself is not stated in a precise rigorous way - my guess is that the committee struggled with how to do so. So they left it as a "should" so that they can't be accused of trying to bind implementers to an ill-defined rule. But the intent is "you know what we mean by this, please do it". – Nate Eldredge Commented Nov 19, 2024 at 15:02
• 1 @NateEldredge: Indeed, I looked into this in an answer to What formally guarantees that non-atomic variables can't see out-of-thin-air values and create a data race like atomic relaxed theoretically can? - I quoted open-std./jtc1/sc22/wg21/docs/papers/2018/p0668r5.html as We still do not have an acceptable way to make our informal (since C++14) prohibition of out-of-thin-air results precise. They would make it a formal requirement if they could figure out how to state it without disallowing things they don't want to forbid. – Peter Cordes Commented Nov 19, 2024 at 19:52
• 1 @PeterCordes Oh, seems I'm wrong. If the load in t2 reads the store(2), it means store(2) < store(1) in MO(as per [intro.races] p17), as well as if the load in t1 reads the store(1) it means store(1) < store(2) (as per [intro.races] p17 too), so when two conditions is true, the MO should be store(2)<store(1)<store(2), which is invalid, so it's impossible. – xmh0511 Commented Nov 20, 2024 at 8:34

 |  Show 16 more comments

1 Answer 1

Sorted by: Reset to default 0

For the first example, if #3 returns true and #1 returns false, #3 would read #2 while #1 must read #3(Otherwise, #1 reads 0, the comparison would be true and the returned value should be true. #1 happens before #2(by sequence-before) and #1 reads #3, as per [intro.races] p17

If a value computation A of an atomic object M happens before an operation B that modifies M, then A takes its value from a side effect X on M, where X precedes B in the modification order of M.

that is, #3 < #2 in the modification order of x. #3 read #2, per [atomics.order] p10

Atomic read-modify-write operations shall always read the last value (in the modification order) written before the write associated with the read-modify-write operation.

This implies #2 < #3. If the case is true, the modification order of x should be #2 < #3 < #2, which is an invalid total order, so it's impossible.

For the second example, #3 read #2 requires #2 < #3 in MO of y per [atomics.order] p10, as well #1 reads #4 implies #4 < #1 in MO of x. In each store-load, they do not form the synchronization in terms of the specified memory order, so there is no further requirement on #1 must happen before #4 or #3 must happen before #2, so #1 does not happen before #4 and #3 does not happen before #2, according to [intro.races] p14

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

Each store is a possible reading value to the corresponding load.

For the last example, if both conditions were true, that would mean #1 read #4 and #3 read #2, again, [intro.races] p17 rules that #4 < #2 and #2 < #4, both true would make the MO for the single x be #4 < #2 < #4, so that's impossible.

I seem to be confused by such two examples. The first example is:

std::atomic<int> x = 1;
//thread 1:
int expected = 1;
if (xpare_exchange_strong(expected,0,relaxed,relaxed) == true){ // #1
    x.store(2,relaxed);  // #2
}
//thread 2:
int expected = 2;
if (xpare_exchange_strong(expected,3,relaxed,relaxed)==true){  // #3
}

In this example, it is impossible that #3 reads the value written by #2 but #1 returns false. I prove that in this way: #2 is invoked only when the condition at #1 is true, so it is impossible that #1 returns false while #3 returns true. I don't know whether there is a formal way to prove that's impossible(for example, from the perspective of the formal wording or modification order).

Consider the second example:

std::atomic<int> x = 2;
std::atomic<int> y = 0;
//thread 1:
if(x.exchange(2,Relaxed) == 1) { // #1
  y.store(1,Relaxed); // #2
}
//thread 2:
if(y.exchange(2,Acquire) == 1){ // #3
    x.store(1,Release); // #4
}

However, applying the above logic to this example seems to not work. In the second example, can both conditions be true? Using the above logic, if #1 returns 1, that means #1 reads #4, and #4 is invoked only if #3 reads #2, and #2 is invoked only if #1 returns 1, so the proof seems to form a cycle. However, from the perspective of memory order, since #4 does not synchronize with #1 and #2 does not synchronize with #3, the condition being true does not impose on how the operations to the other variable are reordered. In other words, when #3 reads #2, #1 and #4 is still unordered, as well as #3 and #2 is also unordered when #1 reads #4.

Is there a formal way to work on both examples?

Updated:

The second example is much like the example in [atomics.order] p9

[Note 7: The recommendation similarly disallows r1 == r2 == 42 in the following example, with x and y again initially zero:
// Thread 1:
r1 = x.load(memory_order::relaxed);
if (r1 == 42) y.store(42, memory_order::relaxed);
// Thread 2:
r2 = y.load(memory_order::relaxed);
if (r2 == 42) x.store(42, memory_order::relaxed);
— end note]

[atomics.order] p8 says:

Implementations should ensure that no “out-of-thin-air” values are computed that circularly depend on their own computation.

However, this wording just uses should, which is not mandatory. So, the second example is still possible that both conditions are true?

How about this one?

std::atomic<int> v = {0};
//thread 1:
if(v.load(acquire) == 1){ // #1
   v.store(2,release);  // #2
}
//thread 2:
if(v.load(relaxed) == 2){ // #3
   v.store(1,relaxed);  // #4
}

I seem to be confused by such two examples. The first example is:

std::atomic<int> x = 1;
//thread 1:
int expected = 1;
if (xpare_exchange_strong(expected,0,relaxed,relaxed) == true){ // #1
    x.store(2,relaxed);  // #2
}
//thread 2:
int expected = 2;
if (xpare_exchange_strong(expected,3,relaxed,relaxed)==true){  // #3
}

In this example, it is impossible that #3 reads the value written by #2 but #1 returns false. I prove that in this way: #2 is invoked only when the condition at #1 is true, so it is impossible that #1 returns false while #3 returns true. I don't know whether there is a formal way to prove that's impossible(for example, from the perspective of the formal wording or modification order).

Consider the second example:

std::atomic<int> x = 2;
std::atomic<int> y = 0;
//thread 1:
if(x.exchange(2,Relaxed) == 1) { // #1
  y.store(1,Relaxed); // #2
}
//thread 2:
if(y.exchange(2,Acquire) == 1){ // #3
    x.store(1,Release); // #4
}

However, applying the above logic to this example seems to not work. In the second example, can both conditions be true? Using the above logic, if #1 returns 1, that means #1 reads #4, and #4 is invoked only if #3 reads #2, and #2 is invoked only if #1 returns 1, so the proof seems to form a cycle. However, from the perspective of memory order, since #4 does not synchronize with #1 and #2 does not synchronize with #3, the condition being true does not impose on how the operations to the other variable are reordered. In other words, when #3 reads #2, #1 and #4 is still unordered, as well as #3 and #2 is also unordered when #1 reads #4.

Is there a formal way to work on both examples?

Updated:

The second example is much like the example in [atomics.order] p9

[Note 7: The recommendation similarly disallows r1 == r2 == 42 in the following example, with x and y again initially zero:
// Thread 1:
r1 = x.load(memory_order::relaxed);
if (r1 == 42) y.store(42, memory_order::relaxed);
// Thread 2:
r2 = y.load(memory_order::relaxed);
if (r2 == 42) x.store(42, memory_order::relaxed);
— end note]

[atomics.order] p8 says:

Implementations should ensure that no “out-of-thin-air” values are computed that circularly depend on their own computation.

However, this wording just uses should, which is not mandatory. So, the second example is still possible that both conditions are true?

How about this one?

std::atomic<int> v = {0};
//thread 1:
if(v.load(acquire) == 1){ // #1
   v.store(2,release);  // #2
}
//thread 2:
if(v.load(relaxed) == 2){ // #3
   v.store(1,relaxed);  // #4
}

• c++
• language-lawyer
• atomic

Share Improve this question Follow edited Nov 22, 2024 at 1:58 xmh0511 asked Nov 19, 2024 at 6:22 xmh0511xmh0511 7,35911 gold badge1111 silver badges4141 bronze badges 21

• 1 This doesn't seem like correct code. First argument is T&, so literal is not accepted. – Marek R Commented Nov 19, 2024 at 10:16
• Another strange thing is: == true (which is obsolete boilerplate), I do not why I can se this so often. – Marek R Commented Nov 19, 2024 at 10:19
• 1 My understanding is that the "should" in the out-of-thin-air rule is simply because the rule itself is not stated in a precise rigorous way - my guess is that the committee struggled with how to do so. So they left it as a "should" so that they can't be accused of trying to bind implementers to an ill-defined rule. But the intent is "you know what we mean by this, please do it". – Nate Eldredge Commented Nov 19, 2024 at 15:02
• 1 @NateEldredge: Indeed, I looked into this in an answer to What formally guarantees that non-atomic variables can't see out-of-thin-air values and create a data race like atomic relaxed theoretically can? - I quoted open-std./jtc1/sc22/wg21/docs/papers/2018/p0668r5.html as We still do not have an acceptable way to make our informal (since C++14) prohibition of out-of-thin-air results precise. They would make it a formal requirement if they could figure out how to state it without disallowing things they don't want to forbid. – Peter Cordes Commented Nov 19, 2024 at 19:52
• 1 @PeterCordes Oh, seems I'm wrong. If the load in t2 reads the store(2), it means store(2) < store(1) in MO(as per [intro.races] p17), as well as if the load in t1 reads the store(1) it means store(1) < store(2) (as per [intro.races] p17 too), so when two conditions is true, the MO should be store(2)<store(1)<store(2), which is invalid, so it's impossible. – xmh0511 Commented Nov 20, 2024 at 8:34

 |  Show 16 more comments

1 Answer 1

Sorted by: Reset to default 0

For the first example, if #3 returns true and #1 returns false, #3 would read #2 while #1 must read #3(Otherwise, #1 reads 0, the comparison would be true and the returned value should be true. #1 happens before #2(by sequence-before) and #1 reads #3, as per [intro.races] p17

If a value computation A of an atomic object M happens before an operation B that modifies M, then A takes its value from a side effect X on M, where X precedes B in the modification order of M.

that is, #3 < #2 in the modification order of x. #3 read #2, per [atomics.order] p10

Atomic read-modify-write operations shall always read the last value (in the modification order) written before the write associated with the read-modify-write operation.

This implies #2 < #3. If the case is true, the modification order of x should be #2 < #3 < #2, which is an invalid total order, so it's impossible.

For the second example, #3 read #2 requires #2 < #3 in MO of y per [atomics.order] p10, as well #1 reads #4 implies #4 < #1 in MO of x. In each store-load, they do not form the synchronization in terms of the specified memory order, so there is no further requirement on #1 must happen before #4 or #3 must happen before #2, so #1 does not happen before #4 and #3 does not happen before #2, according to [intro.races] p14

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

Each store is a possible reading value to the corresponding load.

For the last example, if both conditions were true, that would mean #1 read #4 and #3 read #2, again, [intro.races] p17 rules that #4 < #2 and #2 < #4, both true would make the MO for the single x be #4 < #2 < #4, so that's impossible.

本文标签： cCan both conditions be true when each depends on anotherStack Overflow