[cpp-threads] Counter strawman proposal :-)

[Bill Pugh]

The problem with happens-before consistency is that it does
not, alone, guarantee that correctly synchronized programs have
sequentially consistent semantics.

For example, given:

Initially x = y = 0

Thread 1:
r1 = x
if (r1) y = 1

Thread 2:
r2 = y
if (r2) x = 1

The behavior r1 == r2 == 1 is legal.

I presume that we want to guarantee that correctly synchronized C
programs have sequentially consistent semantics.

     Bill


On Jul 1, 2005, at 9:19 PM, Boehm, Hans wrote:

> After a long pause ...
>
> Peter -
>
> This seems to be much closer to happens-before consistency in Java
> than what we have been discussing.  It no longer invokes undefined
> behavior if there are races, and assumes there is an "accessed value".
> Is that intentional?
>
> With this approach
>
>     r1 = x;
>     if (r1 != (<stuff that doesn't touch r1>, r1) abort();
>
> is guaranteed not to abort.  That means that compilers can
> no longer reload registers that have been spilled with their
> original values, even if they are known not to have been modified.
>
> More comments below ...
>
>
>> -----Original Message-----
>> From:
>> Cpp-threads_decadentplace.org.uk-bounces at decadentplace.org.uk
>> [mailto:Cpp-threads_decadentplace.org.uk-bounces at decadentplace
>> .org.uk] On Behalf Of Peter Dimov
>> Sent: Sunday, June 12, 2005 6:49 AM
>> To: cpp-threads
>> Subject: [cpp-threads] Counter strawman proposal :-)
>>
>>
>> A modification M of a scalar object is _potentially visible_
>> to an attempt A
>> to access the stored value of that object if:
>>
>> - the modification is not _shadowed by_ another modification, and
>> - the modification does not _occur after_ the access.
>>
>> If no modifications are _potentially visible_ at the point
>> where the value
>> is accessed, the behavior is undefined.
>>
>> If two or more modifications that yield distinct values are
>> _potentially
>> visible_, the accessed value is unspecified. Note that the
>> accessed value is
>> not guaranteed to match any of the potentially visible values.
>>
>
> I think we want to just invoke undefined behavior here.
>
>
>>
>>
>> A modification M is _shadowed by_ another modification M2 if:
>>
>> - M2 _occurs after_ M, and
>> - A _occurs after_ M2.
>>
>>
>> An operation O1 _occurs after_ an operation O2 if:
>>
>> - the two operations are done by the same thread and there
>> exists a sequence
>> point between O2 and O1, or
>>
>
> It would be nice if that works without explicitly modeling reads.
> I have to think a bit more about this.
>
>
>>
>> - O1 _synchronizes with_ O2, or
>>
>> - there _exists an ordering constraint between_ O2 and O1.
>>
>
> Why do you separate these?
>
>>
>>
>> There _exists an ordering constraint between_ O1 and O2 when:
>>
>> - a sink-(O1 type) barrier _occurs after_ O1 in its thread, and
>> - a hoist-(O2 type) barrier _occurs before_ O2 in its thread, and
>> - the first barrier precedes the second barrier in the
>> program execution.
>>
>
> This assumes a total ordering on "barriers"?  I thought we wanted
> to accommodate the fact that a release store followed by an acquire  
> load
> have no visibility ordering between them?
>
>>
>> --
>> Peter Dimov
>> http://www.pdimov.com
>>
>>
>> -- 
>> cpp-threads mailing list
>> cpp-threads at decadentplace.org.uk
>> http://decadentplace.org.uk/mailman/listinfo/cpp-threads_decad
>>
> entplace.org.uk
>
> -- 
> cpp-threads mailing list
> cpp-threads at decadentplace.org.uk
> http://decadentplace.org.uk/mailman/listinfo/cpp- 
> threads_decadentplace.org.uk
>