[cpp-threads] SC on PPC

[Hans Boehm]

On Tue, 1 May 2007, Alexander Terekhov wrote:

[Raul:?]
> >
> > This depends on how you define acquire, but if it is defined to
> > enforce causality it is insufficient. In particular, it wouldn't
> > support this case:
> >
> > P1: x=1
> > P2: if (x.load_acquire()==1) { y.store_relaxed(1) }
> > P3: if (y.load_acquire()==1) { Assert(x.load_relaxed()==1) }
>
> Well, consider that on Itanium
>
> P1: x.store_relaxed(1)
> P2: if (x.load_acquire()==1) { y.store_relaxed(1) }
> P3: if (y.load_acquire()==1) { Assert(x.load_relaxed()==1) }
>
> may well abort.
>
> I'd define *acquire* no stronger than Itanium and wouldn't impose
> remote write atomicity for release (relax release in this respect).
>
I think (and hope) we're arguing about a bug in the example here.  The
interesting case in my mind is the one in which P1 does at least a
store_release.  The current memory model proposal does not enforce
anything like causality on unordered (relaxed) operations.  An acquire
load has no impact unless it is matched with a release store.  In my
mind, the example as written is almost type incorrect, in some informal
sense.

Hans