Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.18 as permitted sender) client-ip=23.128.96.18;
Message-ID: <fbfc338c-e35e-17c4-b97c-87838dfa4bf2@gmail.com>
Date:   Tue, 1 Feb 2022 10:42:33 +0900
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:91.0) Gecko/20100101
 Thunderbird/91.5.0
Subject: Re: [PATCH] tools/memory-model: Explain syntactic and semantic
 dependencies
Content-Language: en-US
To:     Alan Stern <stern@rowland.harvard.edu>,
        =?UTF-8?Q?Paul_Heidekr=c3=bcger?= <paul.heidekrueger@in.tum.de>
Cc:     Andrea Parri <parri.andrea@gmail.com>,
        Will Deacon <will@kernel.org>,
        Peter Zijlstra <peterz@infradead.org>,
        Boqun Feng <boqun.feng@gmail.com>,
        Nicholas Piggin <npiggin@gmail.com>,
        David Howells <dhowells@redhat.com>,
        Jade Alglave <j.alglave@ucl.ac.uk>,
        Luc Maranget <luc.maranget@inria.fr>,
        "Paul E. McKenney" <paulmck@kernel.org>,
        Daniel Lustig <dlustig@nvidia.com>,
        Joel Fernandes <joel@joelfernandes.org>,
        =?UTF-8?B?QmrDtnJuIFTDtnBlbA==?= <bjorn@kernel.org>,
        linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
        Marco Elver <elver@google.com>,
        Charalampos Mainas <charalampos.mainas@gmail.com>,
        Pramod Bhatotia <pramod.bhatotia@in.tum.de>
References: <20220125172819.3087760-1-paul.heidekrueger@in.tum.de>
 <YfBk265vVo4FL4MJ@rowland.harvard.edu>
 <YfJ7Rr9Kdk4u78lt@Pauls-MacBook-Pro.local>
 <YfLQmgsXp6pg0XIy@rowland.harvard.edu>
 <YfMFQ5IZiGBRw7SH@Pauls-MacBook-Pro.local>
 <YfMKlLInsK0Qr77f@rowland.harvard.edu>
From:   Akira Yokosawa <akiyks@gmail.com>
In-Reply-To: <YfMKlLInsK0Qr77f@rowland.harvard.edu>
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Precedence: bulk

Hi,

On Thu, 27 Jan 2022 16:11:48 -0500,
Alan Stern wrote:
> Paul Heidekr=C3=BCger pointed out that the Linux Kernel Memory Model
> documentation doesn't mention the distinction between syntactic and
> semantic dependencies.  This is an important difference, because the
> compiler can easily break dependencies that are only syntactic, not
> semantic.
>=20
> This patch adds a few paragraphs to the LKMM documentation explaining
> these issues and illustrating how they can matter.
>=20
> Suggested-by: Paul Heidekr=C3=BCger <paul.heidekrueger@in.tum.de>
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>=20
> ---
>=20
>=20
> [as1970]
>=20
>=20
>  tools/memory-model/Documentation/explanation.txt |   47 ++++++++++++++=
+++++++++
>  1 file changed, 47 insertions(+)
>=20
> Index: usb-devel/tools/memory-model/Documentation/explanation.txt
> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
> --- usb-devel.orig/tools/memory-model/Documentation/explanation.txt
> +++ usb-devel/tools/memory-model/Documentation/explanation.txt
> @@ -485,6 +485,53 @@ have R ->po X.  It wouldn't make sense f
>  somehow on a value that doesn't get loaded from shared memory until
>  later in the code!
> =20
> +Here's a trick question: When is a dependency not a dependency?  Answe=
r:
> +When it is purely syntactic rather than semantic.  We say a dependency=

> +between two accesses is purely syntactic if the second access doesn't
> +actually depend on the result of the first.  Here is a trivial example=
:
> +
> +	r1 =3D READ_ONCE(x);
> +	WRITE_ONCE(y, r1 * 0);
> +
> +There appears to be a data dependency from the load of x to the store =
of
> +y, since the value to be stored is computed from the value that was
> +loaded.  But in fact, the value stored does not really depend on
> +anything since it will always be 0.  Thus the data dependency is only
> +syntactic (it appears to exist in the code) but not semantic (the seco=
nd
> +access will always be the same, regardless of the value of the first
> +access).  Given code like this, a compiler could simply eliminate the
> +load from x, which would certainly destroy any dependency.
> +
> +(It's natural to object that no one in their right mind would write co=
de
> +like the above.  However, macro expansions can easily give rise to thi=
s
> +sort of thing, in ways that generally are not apparent to the
> +programmer.)
> +
> +Another mechanism that can give rise to purely syntactic dependencies =
is
> +related to the notion of "undefined behavior".  Certain program behavi=
ors
> +are called "undefined" in the C language specification, which means th=
at
> +when they occur there are no guarantees at all about the outcome.
> +Consider the following example:
> +
> +	int a[1];
> +	int i;
> +
> +	r1 =3D READ_ONCE(i);
> +	r2 =3D READ_ONCE(a[r1]);
> +
> +Access beyond the end or before the beginning of an array is one kind =
of
> +undefined behavior.  Therefore the compiler doesn't have to worry abou=
t
> +what will happen if r1 is nonzero, and it can assume that r1 will alwa=
ys
> +be zero without actually loading anything from i.  (If the assumption
> +turns out to be wrong, the resulting behavior will be undefined anyway=

> +so the compiler doesn't care!)  Thus the load from i can be eliminated=
,
> +breaking the address dependency.
> +
> +The LKMM is unaware that purely syntactic dependencies are different
> +from semantic dependencies and therefore mistakenly predicts that the
> +accesses in the two examples above will be ordered.  This is another
> +example of how the compiler can undermine the memory model.  Be warned=
=2E
> +
> =20
>  THE READS-FROM RELATION: rf, rfi, and rfe
>  -----------------------------------------

FWIW,

Reviewed-by: Akira Yokosawa <akiyks@gmail.com>

        Thanks, Akira