Re: [PATCH v2] tools/memory-model: Clarify LKMM's limitations in litmus-tests.txt

[Paul E. McKenney]

On Mon, Jul 11, 2022 at 05:14:55PM +0200, Paul Heidekrüger wrote:
> > On 8. Jul 2022, at 20:47, Paul E. McKenney <paulmck@xxxxxxxxxx> wrote:
> > 
> > On Fri, Jul 08, 2022 at 10:45:06AM -0400, Alan Stern wrote:
> >> On Fri, Jul 08, 2022 at 01:44:06PM +0200, Marco Elver wrote:
> >>> On Tue, 14 Jun 2022 at 17:49, Paul Heidekrüger
> >>> <paul.heidekrueger@xxxxxxxxx> wrote:
> >>>> As discussed, clarify LKMM not recognizing certain kinds of orderings.
> >>>> In particular, highlight the fact that LKMM might deliberately make
> >>>> weaker guarantees than compilers and architectures.
> >>>> 
> >>>> Link: https://lore.kernel.org/all/YpoW1deb%2FQeeszO1@xxxxxxxxxxxxxxxxxxxxxxxx/T/#u
> >>>> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@xxxxxxxxx>
> >>>> Co-developed-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> >>> 
> >>> Reviewed-by: Marco Elver <elver@xxxxxxxxxx>
> >>> 
> >>> However with the Co-developed-by, this is missing Alan's SOB.
> >> 
> >> For the record:
> >> 
> >> Signed-off-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> >> 
> >> (Note that according to Documentation/process/submitting-patches.rst, 
> >> the submitting author's SOB is supposed to come last.)
> > 
> > And this is what I ended up with. Please provide additional feedback
> > as needed, and in the meantime, thank you all!
> > 
> > 							Thanx, Paul
> 
> Looks great - my first commit in the Linux kernel!

Congratulations!!!  ;-)

My commits for the upcoming merge window, which is probably 2-3 weeks
from now, are already set.  So this is targeted at the merge window
after that, which is likely to be in late September or early October.

So it is well on its way!

							Thanx, Paul

> Thanks everyone!
> 
> Paul
> 
> > ------------------------------------------------------------------------
> > 
> > commit 3c7753e959706f39e1ee183ef8dcde3b4cfbb4c7
> > Author: Paul Heidekrüger <paul.heidekrueger@xxxxxxxxx>
> > Date: Tue Jun 14 15:48:11 2022 +0000
> > 
> > tools/memory-model: Clarify LKMM's limitations in litmus-tests.txt
> > 
> > As discussed, clarify LKMM not recognizing certain kinds of orderings.
> > In particular, highlight the fact that LKMM might deliberately make
> > weaker guarantees than compilers and architectures.
> > 
> > Link: https://lore.kernel.org/all/YpoW1deb%2FQeeszO1@xxxxxxxxxxxxxxxxxxxxxxxx/T/#u
> > Co-developed-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> > Signed-off-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> > Signed-off-by: Paul Heidekrüger <paul.heidekrueger@xxxxxxxxx>
> > Reviewed-by: Marco Elver <elver@xxxxxxxxxx>
> > Reviewed-by: Joel Fernandes (Google) <joel@xxxxxxxxxxxxxxxxx>
> > Cc: Charalampos Mainas <charalampos.mainas@xxxxxxxxx>
> > Cc: Pramod Bhatotia <pramod.bhatotia@xxxxxxxxx>
> > Cc: Soham Chakraborty <s.s.chakraborty@xxxxxxxxxx>
> > Cc: Martin Fink <martin.fink@xxxxxxxxx>
> > Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxx>
> > 
> > diff --git a/tools/memory-model/Documentation/litmus-tests.txt b/tools/memory-model/Documentation/litmus-tests.txt
> > index 8a9d5d2787f9e..cc355999815cb 100644
> > --- a/tools/memory-model/Documentation/litmus-tests.txt
> > +++ b/tools/memory-model/Documentation/litmus-tests.txt
> > @@ -946,22 +946,39 @@ Limitations of the Linux-kernel memory model (LKMM) include:
> > 	carrying a dependency, then the compiler can break that dependency
> > 	by substituting a constant of that value.
> > 
> > -	Conversely, LKMM sometimes doesn't recognize that a particular
> > -	optimization is not allowed, and as a result, thinks that a
> > -	dependency is not present (because the optimization would break it).
> > -	The memory model misses some pretty obvious control dependencies
> > -	because of this limitation. A simple example is:
> > +	Conversely, LKMM will sometimes overestimate the amount of
> > +	reordering compilers and CPUs can carry out, leading it to miss
> > +	some pretty obvious cases of ordering. A simple example is:
> > 
> > 		r1 = READ_ONCE(x);
> > 		if (r1 == 0)
> > 			smp_mb();
> > 		WRITE_ONCE(y, 1);
> > 
> > -	There is a control dependency from the READ_ONCE to the WRITE_ONCE,
> > -	even when r1 is nonzero, but LKMM doesn't realize this and thinks
> > -	that the write may execute before the read if r1 != 0. (Yes, that
> > -	doesn't make sense if you think about it, but the memory model's
> > -	intelligence is limited.)
> > +	The WRITE_ONCE() does not depend on the READ_ONCE(), and as a
> > +	result, LKMM does not claim ordering. However, even though no
> > +	dependency is present, the WRITE_ONCE() will not be executed before
> > +	the READ_ONCE(). There are two reasons for this:
> > +
> > + The presence of the smp_mb() in one of the branches
> > + prevents the compiler from moving the WRITE_ONCE()
> > + up before the "if" statement, since the compiler has
> > + to assume that r1 will sometimes be 0 (but see the
> > + comment below);
> > +
> > + CPUs do not execute stores before po-earlier conditional
> > + branches, even in cases where the store occurs after the
> > + two arms of the branch have recombined.
> > +
> > +	It is clear that it is not dangerous in the slightest for LKMM to
> > +	make weaker guarantees than architectures. In fact, it is
> > +	desirable, as it gives compilers room for making optimizations. 
> > +	For instance, suppose that a 0 value in r1 would trigger undefined
> > +	behavior elsewhere. Then a clever compiler might deduce that r1
> > +	can never be 0 in the if condition. As a result, said clever
> > +	compiler might deem it safe to optimize away the smp_mb(),
> > +	eliminating the branch and any ordering an architecture would
> > +	guarantee otherwise.
> > 
> > 2.	Multiple access sizes for a single variable are not supported,
> > 	and neither are misaligned or partially overlapping accesses.