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

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

[Paul Heidekrüger]

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@ethstick13.dse.in.tum.de/T/#u
Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
Cc: Marco Elver <elver@google.com>
Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
Cc: Martin Fink <martin.fink@in.tum.de>
---
 .../Documentation/litmus-tests.txt            | 29 ++++++++++++-------
 1 file changed, 19 insertions(+), 10 deletions(-)

diff --git a/tools/memory-model/Documentation/litmus-tests.txt b/tools/memory-model/Documentation/litmus-tests.txt
index 8a9d5d2787f9..623059eff84e 100644
--- a/tools/memory-model/Documentation/litmus-tests.txt
+++ b/tools/memory-model/Documentation/litmus-tests.txt
@@ -946,22 +946,31 @@ 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 overstate the amount of reordering
+	done by architectures and compilers, leading it to missing some
+	pretty obvious orderings.  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.)
+	There is no dependency from the WRITE_ONCE() to the READ_ONCE(),
+	and as a result, LKMM does not assume ordering.  However, the
+	smp_mb() in the if branch will prevent architectures from
+	reordering the WRITE_ONCE() ahead of the READ_ONCE() but only if r1
+	is 0.  This, by definition, is not a control dependency, yet
+	ordering is guaranteed in some cases, depending on the READ_ONCE(),
+	which LKMM doesn't recognize.
+
+	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, because a value of 0 triggers undefined behavior
+	elsewhere, 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.
-- 
2.35.1

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

[Alan Stern]

On Mon, Jun 13, 2022 at 12:27:44PM +0000, Paul Heidekrüger 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@ethstick13.dse.in.tum.de/T/#u
> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
> Cc: Marco Elver <elver@google.com>
> Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
> Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
> Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
> Cc: Martin Fink <martin.fink@in.tum.de>
> ---
>  .../Documentation/litmus-tests.txt            | 29 ++++++++++++-------
>  1 file changed, 19 insertions(+), 10 deletions(-)
> 
> diff --git a/tools/memory-model/Documentation/litmus-tests.txt b/tools/memory-model/Documentation/litmus-tests.txt
> index 8a9d5d2787f9..623059eff84e 100644
> --- a/tools/memory-model/Documentation/litmus-tests.txt
> +++ b/tools/memory-model/Documentation/litmus-tests.txt
> @@ -946,22 +946,31 @@ 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 overstate the amount of reordering
> +	done by architectures and compilers, leading it to missing some
> +	pretty obvious orderings.  A simple example is:

I don't like the word "overstate" here.  How about instead:

	LKMM will sometimes overestimate the amount of reordering
	CPUs and compilers can carry out, leading it to miss some
	pretty obvious cases of ordering.

>  
>  		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.)
> +	There is no dependency from the WRITE_ONCE() to the READ_ONCE(),

You mean "from the READ_ONCE() to the WRITE_ONCE()".

> +	and as a result, LKMM does not assume ordering.  However, the

... does not claim that the load is ordered before the store.

> +	smp_mb() in the if branch will prevent architectures from
> +	reordering the WRITE_ONCE() ahead of the READ_ONCE() but only if r1

Architectures don't do reordering; CPUs do.  In any case this sentence 
is wrong; the presence of the "if" statement is what prevents the 
reordering.  CPUs will never reorder a store before a conditional 
branch, even if the store gets executed on both branches of the 
conditional.

By contrast, the smp_mb() in one of the branches prevents _compilers_ 
from moving the store before the conditional.

> +	is 0.  This, by definition, is not a control dependency, yet
> +	ordering is guaranteed in some cases, depending on the READ_ONCE(),
> +	which LKMM doesn't recognize.

Say instead:

	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, because a value of 0 triggers undefined behavior

"because a value of 0 triggers undefined behavior" implies that 
undefined behavior will always occur.  Instead say:

	For instance, suppose that a 0 value in r1 would trigger
	undefined behavior later on.  Then a clever compiler...

> +	elsewhere, 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.

Alan

>  
>  2.	Multiple access sizes for a single variable are not supported,
>  	and neither are misaligned or partially overlapping accesses.
> -- 
> 2.35.1
> 

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

[Paul Heidekrüger]

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@ethstick13.dse.in.tum.de/T/#u
Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
Cc: Marco Elver <elver@google.com>
Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
Cc: Martin Fink <martin.fink@in.tum.de>
---

v2:
- Incorporate Alan Stern's feedback.
- Add suggested text by Alan Stern to clearly state how the branch and the
  smp_mb() affect ordering.
- Add "Co-developed-by: Alan Stern <stern@rowland.harvard.edu>" based on the
  above.

 .../Documentation/litmus-tests.txt            | 37 ++++++++++++++-----
 1 file changed, 27 insertions(+), 10 deletions(-)

diff --git a/tools/memory-model/Documentation/litmus-tests.txt b/tools/memory-model/Documentation/litmus-tests.txt
index 8a9d5d2787f9..cc355999815c 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.
-- 
2.35.1

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

[Marco Elver]

On Tue, 14 Jun 2022 at 17:49, Paul Heidekrüger
<paul.heidekrueger@in.tum.de> 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@ethstick13.dse.in.tum.de/T/#u
> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
> Co-developed-by: Alan Stern <stern@rowland.harvard.edu>

Reviewed-by: Marco Elver <elver@google.com>

However with the Co-developed-by, this is missing Alan's SOB.

> Cc: Marco Elver <elver@google.com>
> Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
> Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
> Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
> Cc: Martin Fink <martin.fink@in.tum.de>
> ---
>
> v2:
> - Incorporate Alan Stern's feedback.
> - Add suggested text by Alan Stern to clearly state how the branch and the
>   smp_mb() affect ordering.
> - Add "Co-developed-by: Alan Stern <stern@rowland.harvard.edu>" based on the
>   above.
>
>  .../Documentation/litmus-tests.txt            | 37 ++++++++++++++-----
>  1 file changed, 27 insertions(+), 10 deletions(-)
>
> diff --git a/tools/memory-model/Documentation/litmus-tests.txt b/tools/memory-model/Documentation/litmus-tests.txt
> index 8a9d5d2787f9..cc355999815c 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.
> --
> 2.35.1
>

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

[Joel Fernandes]

On Tue, Jun 14, 2022 at 03:48:11PM +0000, Paul Heidekrüger 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@ethstick13.dse.in.tum.de/T/#u
> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
> Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> Cc: Marco Elver <elver@google.com>
> Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
> Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
> Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
> Cc: Martin Fink <martin.fink@in.tum.de>
> ---

Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>

thanks,

 - Joel


> v2:
> - Incorporate Alan Stern's feedback.
> - Add suggested text by Alan Stern to clearly state how the branch and the
>   smp_mb() affect ordering.
> - Add "Co-developed-by: Alan Stern <stern@rowland.harvard.edu>" based on the
>   above.
> 
>  .../Documentation/litmus-tests.txt            | 37 ++++++++++++++-----
>  1 file changed, 27 insertions(+), 10 deletions(-)
> 
> diff --git a/tools/memory-model/Documentation/litmus-tests.txt b/tools/memory-model/Documentation/litmus-tests.txt
> index 8a9d5d2787f9..cc355999815c 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.
> -- 
> 2.35.1
> 

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

[Alan Stern]

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@in.tum.de> 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@ethstick13.dse.in.tum.de/T/#u
> > Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
> > Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> 
> Reviewed-by: Marco Elver <elver@google.com>
> 
> However with the Co-developed-by, this is missing Alan's SOB.

For the record:

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>

(Note that according to Documentation/process/submitting-patches.rst, 
the submitting author's SOB is supposed to come last.)

Alan

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

[Paul E. McKenney]

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@in.tum.de> 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@ethstick13.dse.in.tum.de/T/#u
> > > Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
> > > Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> > 
> > Reviewed-by: Marco Elver <elver@google.com>
> > 
> > However with the Co-developed-by, this is missing Alan's SOB.
> 
> For the record:
> 
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> 
> (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

------------------------------------------------------------------------

commit 3c7753e959706f39e1ee183ef8dcde3b4cfbb4c7
Author: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
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@ethstick13.dse.in.tum.de/T/#u
    Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
    Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
    Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
    Reviewed-by: Marco Elver <elver@google.com>
    Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
    Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
    Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
    Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
    Cc: Martin Fink <martin.fink@in.tum.de>
    Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

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.

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

[Paul Heidekrüger]

> On 8. Jul 2022, at 20:47, Paul E. McKenney <paulmck@kernel.org> 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@in.tum.de> 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@ethstick13.dse.in.tum.de/T/#u
>>>> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
>>>> Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
>>> 
>>> Reviewed-by: Marco Elver <elver@google.com>
>>> 
>>> However with the Co-developed-by, this is missing Alan's SOB.
>> 
>> For the record:
>> 
>> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>> 
>> (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!

Thanks everyone!

Paul

> ------------------------------------------------------------------------
> 
> commit 3c7753e959706f39e1ee183ef8dcde3b4cfbb4c7
> Author: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
> 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@ethstick13.dse.in.tum.de/T/#u
> Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
> Reviewed-by: Marco Elver <elver@google.com>
> Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
> Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
> Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
> Cc: Martin Fink <martin.fink@in.tum.de>
> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> 
> 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.

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@kernel.org> 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@in.tum.de> 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@ethstick13.dse.in.tum.de/T/#u
> >>>> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
> >>>> Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> >>> 
> >>> Reviewed-by: Marco Elver <elver@google.com>
> >>> 
> >>> However with the Co-developed-by, this is missing Alan's SOB.
> >> 
> >> For the record:
> >> 
> >> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> >> 
> >> (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@in.tum.de>
> > 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@ethstick13.dse.in.tum.de/T/#u
> > Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
> > Reviewed-by: Marco Elver <elver@google.com>
> > Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> > Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
> > Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
> > Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
> > Cc: Martin Fink <martin.fink@in.tum.de>
> > Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > 
> > 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.

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

[Paul Heidekrüger]

Paul E. McKenney <paulmck@kernel.org> wrote:

> 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@kernel.org> 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@in.tum.de> 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@ethstick13.dse.in.tum.de/T/#u
>>>>>> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
>>>>>> Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
>>>>> 
>>>>> Reviewed-by: Marco Elver <elver@google.com>
>>>>> 
>>>>> However with the Co-developed-by, this is missing Alan's SOB.
>>>> 
>>>> For the record:
>>>> 
>>>> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>>>> 
>>>> (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!!! ;-)

Thanks! Hopefully many more to come :-)

> 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!

Awesome!

Many thanks,
Paul

> 							Thanx, Paul
> 
>> Thanks everyone!
>> 
>> Paul
>> 
>>> ------------------------------------------------------------------------
>>> 
>>> commit 3c7753e959706f39e1ee183ef8dcde3b4cfbb4c7
>>> Author: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
>>> 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@ethstick13.dse.in.tum.de/T/#u
>>> Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
>>> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>>> Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
>>> Reviewed-by: Marco Elver <elver@google.com>
>>> Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
>>> Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
>>> Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
>>> Cc: Soham Chakraborty <s.s.chakraborty@tudelft.nl>
>>> Cc: Martin Fink <martin.fink@in.tum.de>
>>> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
>>> 
>>> 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.