[cpp-threads] Counter strawman proposal :-)

[Peter Dimov]

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?

Yes, matches existing practice and accomodates atomic reads easily.

> With this approach
>
> r1 = x;
> if (r1 != (<stuff that doesn't touch r1>, r1) abort();
>
> is guaranteed not to abort.

I'm not sure that I understand the example... is r1 visible to other 
threads? If it is, the example may abort if there is a race. If not, it 
cannot 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.

If your r1 was supposed to represent a register, then no. In the original 
C++ code:

if( x != (..., x) ) abort();

the two 'x' expressions may yield different values if there is a race, 
regardless of whether there are registers involved in the generated machine 
code.

If you specifically introduce a local variable r1 that is invisible to other 
threads, the compiler no longer can reload it from x, yes. It will have to 
spill it into temporary storage.

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

Perhaps we do. :-)

>> - O1 _synchronizes with_ O2, or
>>
>> - there _exists an ordering constraint between_ O2 and O1.
>
> Why do you separate these?

This is a sketch. "synchronizes with" is supposed to cover pthread_create, 
pthread_join and mutex locks. But the specification isn't quite right this 
way, so in its final form these would probably need to be described under 
"ordering constraints", too.

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

I'll have to think about this question a bit. Depending on how the above is 
interpreted, it does seem that it either imposes a total ordering, or too 
little ordering. In:

T1: store.rel( x, 1 );
T2: if( load.acq( x ) == 1 ) assert( load.acq( x ) == 1 );

the second load is not guaranteed to see 1, because the sink-* barrier does 
not occur after itself.

Very tricky.