[cpp-threads] C++ memory model

[Lawrence Crowl]

On 9/8/09, Mark Batty <mbatty at cantab.net> wrote:
> I've been looking at the memory model described in the draft C++
> standard, N2914, trying to understand the model mathematically and
> (ultimately) to provide a basis for C++ metatheory and program or
> compiler verification.
>
> Currently, I've formalized a subset of the model without
> non-sequentially-consistent low-level atomics, and have a
> machine-checked proof that for any race-free execution there exists a
> sequentially consistent execution with the same memory actions (along
> the lines of Theorem 7.1 of Boehm and Adve's PLDI 2008 paper).
>
> In the process of this formalization and proof some parts of the draft
> standard seemed difficult to understand or inconsistent - mostly
> relatively local points.  I've written a note describing the
> formalization and some specific suggestions for local clarifications
> and improvements to the standard.  There's a copy here:
>
>  http://www.cl.cam.ac.uk/~mjb220/cpp/cpp.pdf
>
> I would welcome any comments you have.  Please feel free to forward
> that url to anyone else who might be interested.

Thank you for the effort.  First, I will address some of the issues in
the specification of the standard, using the appendix as the base
document.  Second, I will note some nits in the paper.  I have not tried
to understand the proofs formal parts in detail because I do not have
the time to do so, sadly.

A.1 section 1.10 paragraph 2

| Removing "might be".

Okay with me.

A.2 section 2.20 paragrah 4

| Adding "[Note: Executions that access atomic or locking objects as
| non-atomic objects, through an array of character type, for example,
| will have undefined behaviour - end note]"

As did Clark, I note that mixed non-atomic and atomic accesses were
not intended.  I think I think there is at least evidence that atomics
are not char accessible.  Section 3.9 defines memcpy to be valid only
for trivially copyable types.  Chapter 9 requires a trivially copyable
type to have a trivial copy constructor.  Chapter 29 deletes the copy
constructor.  So, memcpy doesn't work with atomics.  And if memcpy
doesn't work, any other char access doesn't have a reasonable semantics.
The reasoning is weak, admittedly.

Even so, the note is reasonable, though could possibly be justified:

    [Note: Atomic and locking objects are not trivially copyable [3.9],
    so executions that access atomic or locking objects as
    non-atomic objects, through an array of character type, for example,
    will have undefined behaviour - end note]

A.3 section 1.10 paragraph 6

| Adding "length".

Okay with me.

A.4 section 1.10 paragraph 12

| Adding "if one exists, or the intial value of the object otherwise".

Okay with me.

A.5 section 1.10 paragraph 13

I confess that I found the text confusing.  I think it needs shorter
sentences.

A.6 section 1.10 paragraph 14

| Making races over non-atomic actions only.
| Including memory_order_seq_cst operations.

Okay with me.

8.7 section 29.3 paragraph 8

| Deleting the note "The requirements do allow ...".
| Adding "An atomic side effect contained in a substatement of one of
| the selection statements specified in 6.4 must not be moved out of
| the substatement."

I don't think we should delete that note.

The added sentence is okay in direction, but the wording does not
reflect the fact that the standard likes "shall" and the standard
likes to specify whether requirements are on the implementation or
the program.  I would rewrite that statement as:

    The implementation shall not move an atomic side effect contained
    in a substatement of one of the selection statements specified in
    6.4 out of the substatement.

8.7 section 29.3 paragraph 9

| Deleting "Implementations shall not ... out of an unbounded loop."
| Adding "An atomic operation contained in a substatement of one of
| the iteration statements specified in 6.5 must not be moved out of
| the substatement."

The added sentence is okay in direction, but the wording does not
reflect the fact that the standard likes "shall" and the standard
likes to specify whether requirements are on the implementation or
the program.  I would rewrite that statement as:

    The implementation shall not move an atomic side effect contained
    in a substatement of one of the iteration statements specified in
    6.5 out of the substatement.

I can fold the chapter 29 changes into my omnibus atomics paper.
Any objections?


Nits below.

Section 1.  You seem to be using "clause" to mean numbered paragraph.
ISO uses clause to mean chapter.

Section 3.1.  Mixed accessies were not intended.

Section 3.1.  The text "In the standard the value read depends" should
read "In the standard, the value read depends".

Section 4.2.5.  The "parametrized" is a misspelling.

-- 
Lawrence Crowl