Re: LKMM litmus test for Roman Penyaev's rcu-rr

From: Alan Stern
Date: Wed May 30 2018 - 10:46:50 EST


On Tue, 29 May 2018, Paul E. McKenney wrote:

> On Tue, May 29, 2018 at 04:10:02PM -0500, Linus Torvalds wrote:
> > On Tue, May 29, 2018 at 3:49 PM Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> > wrote:
> >
> > > Putting this into herd would be extremely difficult, if not impossible,
> > > because it involves analyzing code that was not executed.
>
> One (ugly) way to handle it, assuming we are correct about what it
> happening, would be to place ordering on the other side of the "if"
> that is at least as strong as on the first side. Probably some example
> that completely breaks this approach, though...
>
> > Does it?
> >
> > Can't we simplify the whole sequence as basically
> >
> > A
> > if (!B)
> > D
> >
> > for that "not B" case, and just think about that. IOW, let's ignore the
> > whole "not executed" code.
> >
> > If B depends on A like you state, then that already implies that the write
> > in D cannot come before the read of A.
> >
> > You fundamentally cannot do a conditional write before the read that the
> > write condition depends on. So *any* write after a conditional is dependent
> > on the read.
> >
> > So the existence of C - whether it has a barrier or not - is entirely
> > immaterial at run-time.
> >
> > Now, the *compiler* can use the whole existence of that memory barrier in C
> > to determine whether it can re-order the write to D or not, of course, but
> > that's a separate issue, and then the whole "code that isn't executed" is
> > not the issue any more. The compiler obviously sees all code, whether
> > executing or not.
> >
> > Or am I being stupid and missing something entirely? That's possible.
>
> This will take some analysis, both to make sure that I got Roman's
> example correct and to get to the bottom of exactly what LKMM thinks
> can be reordered. I am shifting timezones eastward, so I am not going
> to dig into it today.
>
> But here are a couple of things that take some getting used to:
>
> 1. The "if (r1 == x)" would likely be "if (r1 == &x)" in the Linux
> kernel.
>
> 2. Unless there is something explicit stopping the reordering, the
> herd tool assumes that the compiler can reorder unrelated code
> completely across the entirety of an "if" statement. It might
> well have decided that it could do so in this case, due to the
> fact that the "if" statement isn't doing anything with x (just
> with its address).
>
> But yes, given that r1 comes from the load from *c, it would
> be difficult (at best) to actually apply that optimization in
> this case.
>
> But let's find out what is really happening. Easy to speculate, but
> much harder to speculate correctly. ;-)

What's really happening is that herd doesn't realize the load from *c
must execute before the store to x (as in your 2 above). You can see
this if you add the following to linux-kernel.cat:

let prop2 = ((prop \ id) & int)

and then run the modified litmus test through herd with "-show prop
-doshow prop2 -gv". The output graph has a prop2 link from the store
to x leading back to the load from c, indicating that in this
execution, the store must execute before the load.

Alan