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:   Tue, 17 Sep 2019 00:42:46 +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: <20190916164246.GA7098@tardis>
References: <20190916051753.GA29216@tardis>
 <Pine.LNX.4.44L0.1909161119160.1489-100000@iolanthe.rowland.org>
MIME-Version: 1.0
Content-Type: multipart/signed; micalg=pgp-sha256;
        protocol="application/pgp-signature"; boundary="OXfL5xGRrasGEqWY"
Content-Disposition: inline
In-Reply-To: <Pine.LNX.4.44L0.1909161119160.1489-100000@iolanthe.rowland.org>
User-Agent: Mutt/1.12.1 (2019-06-15)
Sender: linux-kernel-owner@vger.kernel.org
Precedence: bulk


--OXfL5xGRrasGEqWY
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable

On Mon, Sep 16, 2019 at 11:22:18AM -0400, Alan Stern wrote:
> On Mon, 16 Sep 2019, Boqun Feng wrote:
>=20
> > > 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
> You have misinterpreted the text.  The operational model says that if X=
=20
> propagates to CPU C before X' executes then X ->coe X'.  It does _not_=20
> say that if X ->coe X' then X propagates to CPU C before X' executes.
>=20

Alright, I got confused. If X ->coe X', we only have "X must execute
before X' propagated to the CPU of X" (otherwise, we will have X' ->coe
X), so we will only know the execution time of X (not the propagation
time) is before the propagation of X' to the CPU of X, and that won't
help build the visiblity, because we know zero about the propagation
time of X to any CPU.

> > In other words, we can define ->vis as:
> >=20
> > 	let vis =3D prop ; ((strong-fence ; [Marked] ; xbstar) | (xbstar & int=
))
> >=20
> > , 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 unordere=
d store and load"
> >=20
> > , and data race rules will look more symmetrical ;-)
> >=20
> > Thoughts? Or am I missing something subtle here?
>=20
> See above.
>=20

Thanks!

Regards,
Boqun

> Alan
>=20

--OXfL5xGRrasGEqWY
Content-Type: application/pgp-signature; name="signature.asc"

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

iQEzBAABCAAdFiEEj5IosQTPz8XU1wRHSXnow7UH+rgFAl1/u4IACgkQSXnow7UH
+riWSwf/Qh5r3G2a6SpaN6aJf2TTnJ6jEVSUgwr+Yqx0F61lcC43s5jkt0ZKtqv9
fbxTEr3DzmtSGZfsmBW1hvdnHs93//L+BGB77jAvB3Lb25WZDtfeUFjHtZessGRw
yOxPmFXS+ftvtfOZKUeTXw9C3586NOAGCyiDyMjfvVUYKZTSnlQl/cMbaE+WWBGl
f5CJYIOcI4q9Mj8YpZyxa/aoYwOhhYVvo/TUZIZSuiczRb91+d/sJiMCrYd0rHoZ
oOR3ZTfOEYlDOC9tXqQCwyKbQfMZJfWELtpZn3uJPzOSskEiA7ZfTo0VfgicriA6
jlxx9ENREq7m0e8RqrMX/H8woULzuA==
=bT+E
-----END PGP SIGNATURE-----

--OXfL5xGRrasGEqWY--