[cpp-threads] Counter strawman proposal :-)

[Boehm, Hans]

Yes.  And that's essentially the same problem as with my earlier
proposal which essentially used happens-before to define the notion of a
data race.

I would like to see us ensure that:

1) Data-race-free programs (under the "sequential consistency
interpretation" of
a data race, somehow adapted to deal with unordered synchronization
operations)
have sequentially consistent semantics.

2) We avoid prohibiting compiler transformations on ordinary, say
pthread, code
when that's not required to ensure (1).  In particular, it still seems
to me
that if I write r1 = x, where r1 is a local variable, and x is shared,
the
compiler should be able to reload r1 from x after a spill, if there are
no intervening synchronization operations (or operations that might
modify
x).

This sort of reloading is a fairly well studied optimization
(google "rematerialization"), though I'm not sure how important
it is in practice.  Outlawing it seems dubious unless we are
willing to guarantee some sort of atomicity for ordinary loads.
Otherwise it's hard to see how one could take advantage
of the restriction.

I could be talked out of some piece of (2) if we had a consensus
among implementors that it doesn't matter.  Does any of the compiler
writers want to comment?

I think (2) is violated by any approach we've seen so far that doesn't
explicitly leave the semantics of data-race-free programs undefined.
Hence I don't see how to get out of defining the notion.

All of this gets us back to the problem of defining when a program
with unordered synchronization operations is data-race-free, I think.
It looks like that still requires more thought ...


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 Bill Pugh
> Sent: Monday, July 11, 2005 11:57 AM
> To: cpp-threads at decadentplace.org.uk
> Subject: Re: [cpp-threads] Counter strawman proposal :-)
> 
> 
> 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
> >
> 
> 
> -- 
> cpp-threads mailing list
> cpp-threads at decadentplace.org.uk
> http://decadentplace.org.uk/mailman/listinfo/cpp-threads_decad
entplace.org.uk