Re: Litmus test for question from Al Viro

[Will Deacon]

On Mon, Oct 05, 2020 at 10:23:51AM -0400, Alan Stern wrote:
> On Mon, Oct 05, 2020 at 10:12:48AM +0100, Will Deacon wrote:
> > On Mon, Oct 05, 2020 at 09:20:03AM +0100, Will Deacon wrote:
> > > On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> > > > Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:
> > > > 
> > > > P1(int *x, int *y)
> > > > {
> > > > 	int r2;
> > > > 
> > > > 	r = READ_ONCE(*y);
> > > 
> > > (r2?)
> > > 
> > > > 	WRITE_ONCE(*x, r2);
> > > > }
> > > > 
> > > > Other than that, this is fine.
> > > 
> > > But yes, module the typo, I agree that this rewrite is much better than the
> > > proposal above. The definition of control dependencies on arm64 (per the Arm
> > > ARM [1]) isn't entirely clear that it provides order if the WRITE is
> > > executed on both paths of the branch, and I believe there are ongoing
> > > efforts to try to tighten that up. I'd rather keep _that_ topic separate
> > > from the "bug in herd" topic to avoid extra confusion.
> > 
> > Ah, now I see that you're changing P1 here, not P0. So I'm now nervous
> > about claiming that this is a bug in herd without input from Jade or Luc,
> > as it does unfortunately tie into the definition of control dependencies
> > and it could be a deliberate choice.
> 
> I think you misunderstood.  The bug in herd7 affects the way it handles 
> P1, not P0.  With
> 
> 	r2 = READ_ONCE(*y);
> 	WRITE_ONCE(*x, r2);
> 
> herd7 generates a data dependency from the read to the write.  With
> 
> 	WRITE_ONCE(*x, READ_ONCE(*y));
> 
> it doesn't generate any dependency, even though the code does exactly 
> the same thing as far as the memory model is concerned.  That's the bug 
> I was referring to.

Thanks, that clears things up. There were lots of mentions of "control
dependency" in the mail thread that threw me, because this bug is clearly
about data dependencies!

> The failure to recognize the dependency in P0 should be considered a 
> combined limitation of the memory model and herd7.  It's not a simple 
> mistake that can be fixed by a small rewrite of herd7; rather it's a 
> deliberate choice we made based on herd7's inherent design.  We 
> explicitly said that control dependencies extend only to the code in the 
> branches of an "if" statement; anything beyond the end of the statement 
> is not considered to be dependent.

Interesting. How does this interact with loops that are conditionally broken
out of, e.g.  a relaxed cmpxchg() loop or an smp_cond_load_relaxed() call
prior to a WRITE_ONCE()?

Will