Search code examples
c++language-lawyeratomic

What can be inferred according to the result of atomic operations?

// Thread 1:
obj.store(1,Release);  // #1

// Thread 2:
obj.store(2, Release);  // #2

//Thread 3:
 obj.load(Acquire);  // #3
 obj.load(Relaxed);  // #4

Assume #3 reads the value 1 and #4 reads the value 2, it can easily infer that:

  1. #1 happens before #3, according to

[intro.races] p9.1

A synchronizes with B

  1. #2 does not happen before #3, according to

[intro.races] p18

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.

  1. #3 happens before #4, according to

[intro.races] p10.1

A is sequenced before B

Conjunct the third condition and [intro.races] p16

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.

We may infer that the side effect at #2 follows #1 in the modification order of obj.

So, could we infer that #1 happens before #2 according to [intro.races] p15

If an operation A that modifies an atomic object M happens before an operation B that modifies M, then A is earlier than B in the modification order of M.

It appears to me that "A is earlier than B in M" is only a necessary condition for "A happens before B", in other words, it seems we cannot infer that #1 happens before #2, right?

Solution

  • Let's look at this sentence again:

    If an operation A that modifies an atomic object M happens before an operation B that modifies M, then A is earlier than B in the modification order of M.

    This sentence takes the form "if X, then Y" where X is "operations A and B both modify an atomic object M, where A happens before B" and Y is "A is earlier than B in the modification order of M".

    However, one cannot logically infer the converse, i.e. "if Y, then X". If A is earlier than B in the modification order of M, one cannot conclude from this rule alone that A happens before B.