Re: XDP socket rings, and LKMM litmus tests

[Alan Stern]

On Tue, Mar 02, 2021 at 03:50:19PM -0800, Paul E. McKenney wrote:
> On Tue, Mar 02, 2021 at 04:14:46PM -0500, Alan Stern wrote:

> > This result is wrong, apparently because of a bug in herd7.  There 
> > should be control dependencies from each of the two loads in P0 to each 
> > of the two stores, but herd7 doesn't detect them.
> > 
> > Maybe Luc can find some time to check whether this really is a bug and 
> > if it is, fix it.
> 
> I agree that herd7's control dependency tracking could be improved.
> 
> But sadly, it is currently doing exactly what I asked Luc to make it do,
> which is to confine the control dependency to its "if" statement.  But as
> usual I wasn't thinking globally enough.  And I am not exactly sure what
> to ask for.  Here a store to a local was control-dependency ordered after
> a read, and so that should propagate to a read from that local variable.
> Maybe treat local variables as if they were registers, so that from
> herd7's viewpoint the READ_ONCE()s are able to head control-dependency
> chains in multiple "if" statements?
> 
> Thoughts?

Local variables absolutely should be treated just like CPU registers, if 
possible.  In fact, the compiler has the option of keeping local 
variables stored in registers.

(Of course, things may get complicated if anyone writes a litmus test 
that uses a pointer to a local variable,  Especially if the pointer 
could hold the address of a local variable in one execution and a 
shared variable in another!  Or if the pointer is itself a shared 
variable and is dereferenced in another thread!)

But even if local variables are treated as non-shared storage locations, 
we should still handle this correctly.  Part of the problem seems to lie 
in the definition of the to-r dependency relation; the relevant portion 
is:

	(dep ; [Marked] ; rfi)

Here dep is the control dependency from the READ_ONCE to the 
local-variable store, and the rfi refers to the following load of the 
local variable.  The problem is that the store to the local variable 
doesn't go in the Marked class, because it is notated as a plain C 
assignment.  (And likewise for the following load.)

Should we change the model to make loads from and stores to local 
variables always count as Marked?

What should have happened if the local variable were instead a shared 
variable which the other thread didn't access at all?  It seems like a 
weak point of the memory model that it treats these two things 
differently.

Alan