[cpp-threads] A draft memory model paper

[Peter Dimov]

Herb Sutter wrote:
> 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.

How do you expect a compiler that follows this memory model to translate:

extern interlocked int x;

void f()
{
    x = 1;
}

and:

extern interlocked int y;
extern void h();

void g()
{
    if( y ) h();
}

into x86 assembly? (let's assume separate compilation for illustration 
purposes, no whole program optimization.)

> 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.

3.2.3 says that y = 53 can move into either critical section; under the 
lock-fence rules, it can only be moved into the upper one, although this 
doesn't affect the outcome.

3.2.4 however is invalidated by the lock-fence model; x = 1 and y = 1 cannot 
be moved into the critical section.