[cpp-threads] A draft memory model paper

[Herb Sutter]

Peter Dimov wrote:
> Herb Sutter wrote:
> >   http://www.gotw.ca/memmodel/Prism%20-%20draft%200.8.pdf
> 
> There are some interesting parts that might need clarification.

Thanks, Peter, for pointing out two stale examples I didn't keep in sync
as I worked on the rules. I've fixed them in my local working copy.

Re Example 3.2.2: A previous draft of the paper had relied only on
acq/rel semantics and so did allow load-store (but not store-load)
reordering. Hans pointed out that doing that violated my goal of SC
semantics for correctly synchronized programs and that making volatiles
SC solved it, and so the current draft switched to that but I forgot to
update this example.

Re Example 3.2.5: As noted on the cover page, the current draft makes
critical regions asymmetric: The start is a full fence, whereas the end
is only a release. That is, code can move into a critical region from
below but not from above. Whether that's right is something that needs
to be discussed, based on Hans' example reproduced in Example 3.2.5.

> In 3.2.5, if v1 = 1 can be moved after lock(l1), then the example does
contain a race.

I tend to agree it should be treated as a race, but I think one of the
things we need to decide if we want to define "race" to include this
(ab)use of locks. Hans' paper makes an argument that it is probably a
race under pthreads rules.


> The absence of atomic non-interlocked operations is somewhat
disturbing...
> efficient reference counting needs an atomic increment
(fetchadd<raw>(1)).

Yes, I need to add a list of some operations (a_cas and a_swap are
mentioned but not defined, and others are needed). It would be nice to
just follow what C++0x does wherever possible.

Re raw in particular: As you know, I worry about how often even experts
will forget when atomic<> doesn't actually affect ordering and so fall
into SC illusion traps that give correct results most of the time. I
might just be paranoid, though, and this is just a worry and not a set
opinion for me.

Herb