Received-SPF: pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) client-ip=209.132.180.67;
Date:   Mon, 16 Sep 2019 19:52:54 +0800
From:   Boqun Feng <boqun.feng@gmail.com>
To:     Alan Stern <stern@rowland.harvard.edu>
Cc:     LKMM Maintainers -- Akira Yokosawa <akiyks@gmail.com>,
        Andrea Parri <parri.andrea@gmail.com>,
        Daniel Lustig <dlustig@nvidia.com>,
        David Howells <dhowells@redhat.com>,
        Jade Alglave <j.alglave@ucl.ac.uk>,
        Luc Maranget <luc.maranget@inria.fr>,
        Nicholas Piggin <npiggin@gmail.com>,
        "Paul E. McKenney" <paulmck@linux.ibm.com>,
        Peter Zijlstra <peterz@infradead.org>,
        Will Deacon <will@kernel.org>,
        Kernel development list <linux-kernel@vger.kernel.org>
Subject: Re: Documentation for plain accesses and data races
Message-ID: <20190916115254.GB29216@tardis>
References: <Pine.LNX.4.44L0.1909061405560.1627-100000@iolanthe.rowland.org>
 <20190916051753.GA29216@tardis>
MIME-Version: 1.0
Content-Type: multipart/signed; micalg=pgp-sha256;
        protocol="application/pgp-signature"; boundary="i9LlY+UWpKt15+FH"
Content-Disposition: inline
In-Reply-To: <20190916051753.GA29216@tardis>
User-Agent: Mutt/1.12.1 (2019-06-15)
Sender: linux-kernel-owner@vger.kernel.org
Precedence: bulk


--i9LlY+UWpKt15+FH
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable

On Mon, Sep 16, 2019 at 01:17:53PM +0800, Boqun Feng wrote:
> Hi Alan,
>=20
> I spend some time reading this, really helpful! Thanks.
>=20
> Please see comments below:
>=20
> On Fri, Sep 06, 2019 at 02:11:29PM -0400, Alan Stern wrote:
> [...]
> > If two memory accesses aren't concurrent then one must execute before
> > the other.  Therefore the LKMM decides two accesses aren't concurrent
> > if they can be connected by a sequence of hb, pb, and rb links
> > (together referred to as xb, for "executes before").  However, there
> > are two complicating factors.
> >=20
> > If X is a load and X executes before a store Y, then indeed there is
> > no danger of X and Y being concurrent.  After all, Y can't have any
> > effect on the value obtained by X until the memory subsystem has
> > propagated Y from its own CPU to X's CPU, which won't happen until
> > some time after Y executes and thus after X executes.  But if X is a
> > store, then even if X executes before Y it is still possible that X
> > will propagate to Y's CPU just as Y is executing.  In such a case X
> > could very well interfere somehow with Y, and we would have to
> > consider X and Y to be concurrent.
> >=20
> > Therefore when X is a store, for X and Y to be non-concurrent the LKMM
> > requires not only that X must execute before Y but also that X must
> > propagate to Y's CPU before Y executes.  (Or vice versa, of course, if
> > Y executes before X -- then Y must propagate to X's CPU before X
> > executes if Y is a store.)  This is expressed by the visibility
> > relation (vis), where X ->vis Y is defined to hold if there is an
> > intermediate event Z such that:
> >=20
> > 	X is connected to Z by a possibly empty sequence of
> > 	cumul-fence links followed by an optional rfe link (if none of
> > 	these links are present, X and Z are the same event),
> >=20
>=20
> I wonder whehter we could add an optional ->coe or ->fre between X and
> the possibly empty sequence of cumul-fence, smiliar to the definition
> of ->prop. This makes sense because if we have
>=20
> 	X ->coe X' (and X' in on CPU C)
>=20
> , X must be already propagated to C before X' executed, according to our
> operation model:
>=20
> "... In particular, it must arrange for the store to be co-later than
> (i.e., to overwrite) any other store to the same location which has
> already propagated to CPU C."
>=20
> In other words, we can define ->vis as:
>=20
> 	let vis =3D prop ; ((strong-fence ; [Marked] ; xbstar) | (xbstar & int))
>=20

Hmm.. so the problem with this approach is that the (xbstar & int) part
doesn't satisfy the requirement of visibility... i.e.

	X ->prop Z ->(xbstar & int) Y

may not guarantee when Y executes, X is already propagated to Y's CPU.

Lemme think more on this...

Regards,
Boqun

> , and for this document, reference the "prop" section in
> explanation.txt. This could make the model simple (both for description
> and explanation), and one better thing is that we won't need commit in
> Paul's dev branch:
> =09
> 	c683f2c807d2 "tools/memory-model: Fix data race detection for unordered =
store and load"
>=20
> , and data race rules will look more symmetrical ;-)
>=20
> Thoughts? Or am I missing something subtle here?
>=20
> Regards,
> Boqun
> =09
> > and either:
> >=20
> > 	Z is connected to Y by a strong-fence link followed by a
> > 	possibly empty sequence of xb links,
> >=20
> > or:
> >=20
> > 	Z is on the same CPU as Y and is connected to Y by a possibly
> > 	empty sequence of xb links (again, if the sequence is empty it
> > 	means Z and Y are the same event).
> >=20
> > The motivations behind this definition are straightforward:
> >=20
> > 	cumul-fence memory barriers force stores that are po-before
> > 	the barrier to propagate to other CPUs before stores that are
> > 	po-after the barrier.
> >=20
> > 	An rfe link from an event W to an event R says that R reads
> > 	from W, which certainly means that W must have propagated to
> > 	R's CPU before R executed.
> >=20
> > 	strong-fence memory barriers force stores that are po-before
> > 	the barrier, or that propagate to the barrier's CPU before the
> > 	barrier executes, to propagate to all CPUs before any events
> > 	po-after the barrier can execute.
> >=20
> > To see how this works out in practice, consider our old friend, the MP
> > pattern (with fences and statement labels, but without the conditional
> > test):
> >=20
> > 	int buf =3D 0, flag =3D 0;
> >=20
> > 	P0()
> > 	{
> > 		X: WRITE_ONCE(buf, 1);
> > 		   smp_wmb();
> > 		W: WRITE_ONCE(flag, 1);
> > 	}
> >=20
> > 	P1()
> > 	{
> > 		int r1;
> > 		int r2 =3D 0;
> >=20
> > 		Z: r1 =3D READ_ONCE(flag);
> > 		   smp_rmb();
> > 		Y: r2 =3D READ_ONCE(buf);
> > 	}
> >=20
> > The smp_wmb() memory barrier gives a cumul-fence link from X to W, and
> > assuming r1 =3D 1 at the end, there is an rfe link from W to Z.  This
> > means that the store to buf must propagate from P0 to P1 before Z
> > executes.  Next, Z and Y are on the same CPU and the smp_rmb() fence
> > provides an xb link from Z to Y (i.e., it forces Z to execute before
> > Y).  Therefore we have X ->vis Y: X must propagate to Y's CPU before Y
> > executes.
> >=20
> [...]


--i9LlY+UWpKt15+FH
Content-Type: application/pgp-signature; name="signature.asc"

-----BEGIN PGP SIGNATURE-----

iQEzBAABCAAdFiEEj5IosQTPz8XU1wRHSXnow7UH+rgFAl1/d48ACgkQSXnow7UH
+rj1zQf/fXWjpiHq3iUIeLzjZpvvDpmE2WQp1r3BaswB6uPk8EmMhETCOitfNzLS
9ADJ5iQuMGVyqrMu5BBBubBaxIMwaJ2lWWRj4ZRZC/0RPJ3fiUDSYeenLjufYJc1
bk9rTm6odfDW5XzB6dqfbdaQptor5xK/WqS+lpcHwdhopNLHDp1ToMImBQuVMZIS
MTBqoIUzaw3e2DirwVogqRA/axkawtpzcyc86ejVfEP0w4L7/Fto8UnDgjYqfrm+
NXlYr8iGMaOmOfwQ+x1Q20zCpFt4osFA65sQov/0NkR1ga4HIBLx3igye565Hi33
1UGTzAu7eUwsvCQ2nOnUpvw+ZTLgAw==
=c7aw
-----END PGP SIGNATURE-----

--i9LlY+UWpKt15+FH--