lkml.org 
[lkml]   [2022]   [Jul]   [8]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
Patch in this message
/
Date
From
SubjectRe: [PATCH v2] tools/memory-model: Clarify LKMM's limitations in litmus-tests.txt
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
>

\
 
 \ /
  Last update: 2022-07-08 14:16    [W:0.055 / U:0.448 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site