Doc. No.:	WG14/N1768
Date:	2013年10月21日
Related to:	WG21/N3710, N3786, LWG 2265
Reply to:	Hans-J. Boehm	Clark Nelson
Phone:	+1-650-857-3406	+1-503-712-8433
Email:	Hans.Boehm@hp.com	clark.nelson@intel.com

Prohibiting “out of thin air” results in C

We argued in WG21/N3710 that the current attempt prohibit out-of-thin-air results in 7.17.3p13 is both insufficient, in that it leaves it largely impossible to reason about programs with memory_order_relaxed, and seriously harmful, in that it arguably disallows all reasonable implementations of memory_order_relaxed on architectures like ARM and POWER. This proposal attempts to address the latter "seriously harmful" part for C, without addressing the "insufficient" part, possibly along the lines of N3710.

This proposal thus eliminates some amount of complicated standardese that we actually want vendors like ARM and IBM to ignore.

There is no consensus in WG21/SG1 for a more extensive proposal, such as that in N3710, at this time (i.e. in time for C++14).

Proposed wording for 7.17.3

This removes the current badly formulated requirement, and instead promotes the existing note discouraging "out-of-thin-air" results to normative encouragment.

The core problem here is that we do not know (after 10 years of failed attempts, originally in a Java context) how to precisely state this requirement without strengthening it so that it impacts code performance. (See N3710 for details.) Thus it remains of little use to anyone trying to formulate a precise correctness argument. It is roughly analogous to our current statements about progress guarantees, which are also phrased as normative encouragement, in large part because they would be extremely difficult to make precise while remaining implementable.

Proposed wording

Change 7.17.3p13 as follows:

(削除) An atomic store shall only store a value that has been computed from constants and program input values by a finite sequence of program evaluations, such that each evaluation observes the values of variables as computed by the last prior assignment in the sequence.²⁵⁶⁾ The ordering of evaluations in this sequence shall be such that (削除ここまで)

• (削除) If an evaluation B observes a value computed by A in a different thread, then B does not happen before A. (削除ここまで)
• (削除) If an evaluation A is included in the sequence, then all evaluations that assign to the same variable and happen before A are also included. (削除ここまで)

(追記) Recommended practice (追記ここまで)

(追記) Implementations should ensure that no “out-of-thin-air” values are computed that circularly depend on their own computation. (追記ここまで)

Change 7.17.3p14 as follows:

(削除) NOTE 3 The second requirement disallows “out-of-thin-air”, or “speculative” stores of atomics when relaxed atomics are used. Since unordered operations are involved, evaluations may appear in this sequence out of thread order. For example, with x and y initially zero, (削除ここまで)

(削除)

// Thread 1:
r1 = atomic_load_explicit(&y, memory_order_relaxed);
atomic_store_explicit(&x, r1, memory_order_relaxed);
// Thread 2:
r2 = atomic_load_explicit(&x, memory_order_relaxed);
atomic_store_explicit(&y, 42, memory_order_relaxed);

(削除ここまで)

(削除) is allowed to produce r1 == 42 && r2 == 42. The sequence of evaluations justifying this consists of: (削除ここまで)

(削除)

atomic_store_explicit(&y, 42, memory_order_relaxed);
r1 = atomic_load_explicit(&y, memory_order_relaxed);
atomic_store_explicit(&x, r1, memory_order_relaxed);
r2 = atomic_load_explicit(&x, memory_order_relaxed);

(削除ここまで)

(削除) On the other hand, (削除ここまで) (追記) NOTE 3 For example, with x and y initially zero, (追記ここまで)

// Thread 1:
r1 = atomic_load_explicit(&y, memory_order_relaxed);
atomic_store_explicit(&x, r1, memory_order_relaxed);
// Thread 2:
r2 = atomic_load_explicit(&x, memory_order_relaxed);
atomic_store_explicit(&y, r2, memory_order_relaxed);

(削除) is not allowed to (削除ここまで) (追記) should not (追記ここまで) produce r1 == 42 && r2 =(追記) = (追記ここまで) 42, since (追記) the store of 42 to y is only possible if the store to x stores 42, which circularly depends on the store to y storing 42. Note that without this restriction, such an execution is possible. (追記ここまで) (削除) since there is no sequence of evaluations that results in the computation of 42. In the absence of “relaxed” operations and read-modify-write operations with weaker than memory_order_acq_rel ordering, the second requirement has no impact. (削除ここまで)

Change 7.17.3p15 as follows:

(削除) Recommended practice (削除ここまで)

The (削除) requirements do not forbid (削除ここまで) (追記) recommendation similarly disallows (追記ここまで) r1 == 42 && r2 == 42 in the following example, with x and y (追記) again (追記ここまで) initially zero:

// Thread 1:
r1 = atomic_load_explicit(&x, memory_order_relaxed);
if (r1 == 42)
	atomic_store_explicit(&y, (削除) r1 (削除ここまで) (追記) 42 (追記ここまで), memory_order_relaxed);
// Thread 2:
r2 = atomic_load_explicit(&y, memory_order_relaxed);
if (r2 == 42)
	atomic_store_explicit(&x, 42, memory_order_relaxed);

(削除) However, this is not useful behavior, and implementations should not allow it. (削除ここまで)