[cpp-threads] Counter strawman proposal :-)

[Boehm, Hans]

Peter -

It might help to pop up a level here for now.  I'm not quite sure what
we're trying to accomplish here.  I think the open issues we have
are:

1) We need a correct model.  I think both of our models actually
currently
have similar problems, in that we don't handle some synchronization-free
race-free code correctly.  I think that can be fixed by requiring
actions
on ordinary variables/members/elements to be essentially sequentially
consistent.  This is what Bill pointed out, and it's the issue that
worries
me the most.  By far.

2) I'm not sure whether we agree that the semantics of programs with
data races (on ordinary variables) should be completely undefined.  This
is
what the strawman proposal says.  And I think your proposal can be
easily
adapted to say so, too.  I still believe we want this, since we would
otherwise
restrict optimizations in ways that are not well motivated and
potentially
significant.

3) My strawman proposal isn't terribly readable, in part because it's
probably
overly abstract.  Your proposal fixed that, perhaps by making it too
specific.
This is a problem if it causes confusion in our group.  Otherwise I
would
ignore it for now, though improvements are certainly welcome at any
time,
and I'm incorporating some of your changes.

4) We have some terminology differences, which might have some
associated
semantic differences.  My proposal is phrased in terms of
acquire/release
operations, not hoist/sink-barriers.  I would personally prefer to stick
with the
acquire/release terminology, since I think it's more widely established.
There may be a more substantive difference here if you consider
something like

(initially everything 0)
Thread1:  lock(l1); x = 17; unlock(l1); lock(l1); y = 1; unlock(l1);
Thread2:  lock(l2); r1 = y; unlock(l2); lock(l2); r2 = x; unlock(l2);

Is r1 = 1 and r2 = 0 possible?  In Java, the answer is yes, since the
two threads operate on distinct locks, and there are thus no
happens-before
relationships between threads.  I think we should allow synchronization
primitives that behave that way.  Otherwise the distributed shared
memory
people will be upset.  (And it looks to me like network and memory
latencies are converging, so DSM systems may get more important.)
And the Java approach has some other performance advantages.

Are these the same problems you're trying to solve?

Hans

> -----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: Wednesday, July 13, 2005 5:30 AM
> To: cpp-threads at decadentplace.org.uk
> Subject: Re: [cpp-threads] Counter strawman proposal :-)
> 
> 
> 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? 
> 
> 
> -- 
> cpp-threads mailing list
> cpp-threads at decadentplace.org.uk 
> http://decadentplace.org.uk/mailman/listinfo/cpp-threads_decad
entplace.org.uk