Coherence Requirements Detailed

ISO/IEC JTC1 SC22 WG21 N3136 = 10-0126 - 2010-08-20

Michael Wong, michaelw@ca.ibm.com

Benjamin Kosnik, bkoz@redhat.com

Mark Batty, mjb220@cl.cam.ac.uk

Introduction

This paper is based on discussions in the Concurrency Working Group in Rapperswil following the presentation of “C++ Concurrency Discussion” by Mark Batty and Peter Sewell. (From wiki.dinkumware.com/twiki/.../ConcurrencyWorkingGroup/cpp-fcd-01.pdf)

Proposed Changes

For the changes below, the new text is put in place with the older text it is replacing represented in strikethrough.

 

1. Modify 1.10p13 as follows:

The visible sequence of side effects on an atomic object M, with respect to a value computation B of M, is a maximal contiguous sub-sequence of side effects in the modification order of M, where the first side effect is visible with respect to B, and for every subsequent side effect, it is not the case that B happens before it.

The value of an atomic object M, as determined by evaluation B, shall be the value stored by some operation in the a visible sequence of M with respect to B. [Note - It can be shown that the visible sequence of side effects of

a value computation is unique given the coherence requirements below.

- end note] Furthermore, if a value computation A of an atomic object M happens before a value computation B of M, and the value computed by A corresponds to the value stored

by side effect X, then the value computed by B shall either equal the value computed by A, or be the value stored by side effect Y, where Y follows X in the modification order of M. [ Note: This effectively disallows compiler reordering of atomic operations to a single object, even if both operations are “relaxed” loads. This effectively makes the “cache coherence” guarantee provided by most hardware available to C++ atomic operations. —end note ] [ Note: The visible sequence depends on the “happens before” relation, which depends on the values observed by loads of atomics, which we are restricting here. The intended reading is that there must exist an association of atomic loads with modifications they observe that, together with suitably chosen modification orders and the “happens before” relation derived as described above, satisfy the resulting constraints as imposed here. —end note ]

 

2. Insert new 1.10p14:

We define the following Coherence Requirements

-Write Write:

    If an operation A that modifies M happens-before an operation B that modifies M then A shall be earlier then B in the modification order of M

 

-Read Read:

If a value computation A of an atomic object M happens before a value

computation B of M, and A takes its value from the side effect X, then

the value computed by B shall either be the value stored by X, or the

value stored by a side effect Y, where Y follows X  in the

modification order of M.

 

-Read Write:

    If a value computation A of an atomic object M happens-before an operation B that modifies M then the value read by A shall be the value of a modification that is earlier in the modification order of M than the value stored by B

 

    -Write Read:

If a side effect X that stores a value to an atomic object M happens-before a value computation B of M then the evaluation B shall return the value stored by X or a value later in the modification order of M

 

3. Insert new 1.10p15:

[ Note: This effectively disallows compiler reordering of atomic operations to a single object, even if both operations are “relaxed” loads. This effectively makes the “cache coherence” guarantee provided by most hardware available to C++ atomic operations. —end note ]

 

 

4. Insert new 1.10p16:

[ Note: The visible sequence depends on the “happens before” relation, which depends on the values observed by loads of atomics, which we are restricting here. The intended reading is that there must exist an association of atomic loads with modifications they observe that, together with suitably chosen modification orders and the “happens before” relation derived as described above, satisfy the resulting constraints as imposed here. —end note ]