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:   Fri, 16 Nov 2018 01:54:20 +0800
From:   Boqun Feng <boqun.feng@gmail.com>
To:     Alan Stern <stern@rowland.harvard.edu>
Cc:     "Paul E. McKenney" <paulmck@linux.ibm.com>,
        LKMM Maintainers -- Akira Yokosawa <akiyks@gmail.com>,
        Andrea Parri <andrea.parri@amarulasolutions.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>,
        Peter Zijlstra <peterz@infradead.org>,
        Will Deacon <will.deacon@arm.com>,
        Kernel development list <linux-kernel@vger.kernel.org>
Subject: Re: [PATCH 2/3] tools/memory-model: Refactor some RCU relations
Message-ID: <20181115175420.GA3227@tardis>
References: <Pine.LNX.4.44L0.1811151116420.1308-100000@iolanthe.rowland.org>
MIME-Version: 1.0
Content-Type: multipart/signed; micalg=pgp-sha256;
        protocol="application/pgp-signature"; boundary="tKW2IUtsqtDRztdT"
Content-Disposition: inline
In-Reply-To: <Pine.LNX.4.44L0.1811151116420.1308-100000@iolanthe.rowland.org>
User-Agent: Mutt/1.10.1 (2018-07-13)
Sender: linux-kernel-owner@vger.kernel.org
Precedence: bulk


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

Hi Alan,

On Thu, Nov 15, 2018 at 11:19:58AM -0500, Alan Stern wrote:
> In preparation for adding support for SRCU, refactor the definitions
> of rcu-fence, rcu-rscsi, rcu-link, and rb by moving the po and po?
> terms from the first two to the second two.  An rcu-gp relation is
> added; it is equivalent to gp with the po and po? terms removed.
>=20
> This is necessary because for SRCU, we will have to use the loc
> relation to check that the terms at the start and end of each disjunct
> in the definition of rcu-fence refer to the same srcu_struct
> location.  If these terms are hidden behind po and po?, there's no way
> to carry out this check.
>=20
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>=20
> ---
>=20
>=20
>  tools/memory-model/linux-kernel.cat |   25 +++++++++++++++----------
>  1 file changed, 15 insertions(+), 10 deletions(-)
>=20
> Index: usb-4.x/tools/memory-model/linux-kernel.cat
> =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-4.x.orig/tools/memory-model/linux-kernel.cat
> +++ usb-4.x/tools/memory-model/linux-kernel.cat
> @@ -91,32 +91,37 @@ acyclic pb as propagation
>  (*******)
> =20
>  (*
> - * Effect of read-side critical section proceeds from the rcu_read_lock()
> - * onward on the one hand and from the rcu_read_unlock() backwards on the
> + * Effects of read-side critical sections proceed from the rcu_read_unlo=
ck()
> + * backwards on the one hand, and from the rcu_read_lock() forwards on t=
he
>   * other hand.
> + *
> + * In the definition of rcu-fence below, the po term at the left-hand si=
de
> + * of each disjunct and the po? term at the right-hand end have been fac=
tored
> + * out.  They have been moved into the definitions of rcu-link and rb.
>   *)
> -let rcu-rscsi =3D po ; rcu-rscs^-1 ; po?
> +let rcu-gp =3D [Sync-rcu]		(* Compare with gp *)
> +let rcu-rscsi =3D rcu-rscs^-1

Isn't it more straight-forward to use "rcu-rscs^-1" other than
"rcu-rscsi" in the definition of "rcu-fence", is it?

The introduction of "rcu-rscsi" makes sense in the first patch, but with
this refactoring, I think it's better we just don't use it.

Regards,
Boqun

> =20
>  (*
>   * The synchronize_rcu() strong fence is special in that it can order not
>   * one but two non-rf relations, but only in conjunction with an RCU
>   * read-side critical section.
>   *)
> -let rcu-link =3D hb* ; pb* ; prop
> +let rcu-link =3D po? ; hb* ; pb* ; prop ; po
> =20
>  (*
>   * Any sequence containing at least as many grace periods as RCU read-si=
de
>   * critical sections (joined by rcu-link) acts as a generalized strong f=
ence.
>   *)
> -let rec rcu-fence =3D gp |
> -	(gp ; rcu-link ; rcu-rscsi) |
> -	(rcu-rscsi ; rcu-link ; gp) |
> -	(gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) |
> -	(rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; gp) |
> +let rec rcu-fence =3D rcu-gp |
> +	(rcu-gp ; rcu-link ; rcu-rscsi) |
> +	(rcu-rscsi ; rcu-link ; rcu-gp) |
> +	(rcu-gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) |
> +	(rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; rcu-gp) |
>  	(rcu-fence ; rcu-link ; rcu-fence)
> =20
>  (* rb orders instructions just as pb does *)
> -let rb =3D prop ; rcu-fence ; hb* ; pb*
> +let rb =3D prop ; po ; rcu-fence ; po? ; hb* ; pb*
> =20
>  irreflexive rb as rcu
> =20
>=20

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

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

iQEzBAABCAAdFiEEj5IosQTPz8XU1wRHSXnow7UH+rgFAlvtssMACgkQSXnow7UH
+rj0+Af+IDIVrVlyk7c8RrloAC/DfX4vuHEoRyUxxQk5/sWXc0aXrxiNbHpIxc4p
qUSHQgc9YxzrLQtCzrb9WF9QkWbJkOm5JPeQutor4cwxaEzWv5hChO1BaXUoWP1S
nMmbPaB3/5YrZ10b6LbSsXZ0DfckfiXnpmL+geUZHeym6vfoEwkAAk/YqK9BngHq
M0IZy/64AIlIqikqC8IL++Flb/E7zfEVzOZq/Ch0PF8hR0n5uLoeApl3Tqzt6ZAk
ucnqhhmpF/w98eVUe7oWsPYifj/ZEadqzSgZ02qYeJd0F+L0Zvby8ZX4MjVKjLWI
9YJ1UPzEzep43A7Da9iNipfpr/1bRw==
=sjHZ
-----END PGP SIGNATURE-----

--tKW2IUtsqtDRztdT--