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

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
> 

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
>

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

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.

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

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.

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.