[cpp-threads] C++ memory model (N.M. Maclaren)

[Mark Batty]

Firstly, thank you for looking over the document and giving me feedback on it.

> My first comment is that I hope that you will put this on the Web.

I don't know where people look for documents like this besides this
list, did you have somewhere particular in mind?


> There is a similar problem to do with updates performed via calls to the
> inherited C and other non-C++ libraries.  Nowhere in the C standard (or
> POSIX, for that matter) is this issue addressed; we had a vigorous
> debate in Fortran on the matter.  This is NOT just a theoretical point
> as, for example, the Intel memory consistency model does not require
> full-size SSE accesses to be atomic, so a vectorised library function
> interacts in unspecified ways with all 'simple' accesses.
>
> While I personally agree with your solution, which has similarities to
> the one that Fortran has adopted, it has the consequence of preventing a
> lot of reasonable constructions.  For example, such objects could not be
> accessed by any of the functions in <cstring>, nor could they be
> transferred in I/O.  It's a knotty problem.

This is useful to me, I have not considered the interaction of C
libraries with the memory model or any specific architecture dependant
implementation details yet.


> 3.4 specifies this by introducing the concept of an initial value,
> which is a bigger change than it might appear.

This is an important point, in light of what you have highlighted, the
model as I have formalized it with an initial state does not
necessarily correspond to the description in the standard, although as
you point out, the standard does not properly define 'indeterminate
value' either. I will have to give this some careful thought.


> [...] the actions must be countable [...] is this solely to make the Axiom of Choice hold?

Yes, at the moment but it might be important for proving a progress
property as well.


I will be posting a new version of the document soon with a more
comprehensive section on atomic operations and control flow.

Thanks again,
Mark