[cpp-threads] Counter strawman proposal :-)

[Peter Dimov]

Peter Dimov wrote:
> Boehm, Hans wrote:

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

I have a rough sketch for this now.

The three basic ordered cases are as follows:

1. op-load-store

T1: store
T2: load, ..., op

where T2.load sees the stored value of T1.store and load and op are ordered. 
It follows that store and op are ordered.

Load and op are ordered if either of the following is true:

a. There is a hoist-(op type) barrier associated with the load,
b. There is a sink-load barrier associated with op,
c. There is a sink-load+hoist-(op type) bidirectional barrier between load 
and op.

2. load-store-op

T1: op, ..., store
T2: load

as above, follows that op and load are ordered.

3. op-load-store-op

T1: op1, ..., store
T2: load, ..., op2

as above, op1 and op2 are ordered.

(This model doesn't address the causality loop problem. I'm not sure that it 
falls in the "correctly synchronized" category.)

Based on the above, the formal relation can be specified as:

P < Q if either of the following is true:

1. P and Q occur in the same thread of execution, there exists a sequence 
point between them and either:

1a. P has an associated hoist-Qtype ordering constraint, or
1b. Q has an associated sink-Ptype ordering constaint.

2. P and Q occur in different threads of execution, P is a store, Q is a 
load from the same object, and during the program execution Q has seen the 
value stored by P.

3. There exists R such that P < R and R < Q.

Do you see any holes in that?