From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1753196AbbJTOVK (ORCPT ); Tue, 20 Oct 2015 10:21:10 -0400 Received: from mail-pa0-f47.google.com ([209.85.220.47]:34415 "EHLO mail-pa0-f47.google.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1752229AbbJTOVI (ORCPT ); Tue, 20 Oct 2015 10:21:08 -0400 Date: Tue, 20 Oct 2015 22:20:40 +0800 From: Boqun Feng To: "Paul E. McKenney" Cc: Will Deacon , Peter Zijlstra , Michael Ellerman , linux-arch@vger.kernel.org, linux-kernel@vger.kernel.org, Anton Blanchard , Benjamin Herrenschmidt , Paul Mackerras , linuxppc-dev@lists.ozlabs.org Subject: Re: [PATCH v2] barriers: introduce smp_mb__release_acquire and update documentation Message-ID: <20151020142040.GD17714@fixme-laptop.cn.ibm.com> References: <20151007132317.GK16065@arm.com> <20151007152501.GI3910@linux.vnet.ibm.com> <1444276236.9940.5.camel@ellerman.id.au> <20151008111638.GL3816@twins.programming.kicks-ass.net> <20151008125937.GH16807@arm.com> <20151008221716.GF3910@linux.vnet.ibm.com> <20151009095129.GF26278@arm.com> <20151009174327.GV3910@linux.vnet.ibm.com> <20151009183328.GV26278@arm.com> <20151012233048.GK3910@linux.vnet.ibm.com> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="hoZxPH4CaxYzWscb" Content-Disposition: inline In-Reply-To: <20151012233048.GK3910@linux.vnet.ibm.com> User-Agent: Mutt/1.5.24 (2015-08-30) Sender: linux-kernel-owner@vger.kernel.org List-ID: X-Mailing-List: linux-kernel@vger.kernel.org --hoZxPH4CaxYzWscb Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-Transfer-Encoding: quoted-printable On Mon, Oct 12, 2015 at 04:30:48PM -0700, Paul E. McKenney wrote: > On Fri, Oct 09, 2015 at 07:33:28PM +0100, Will Deacon wrote: > > On Fri, Oct 09, 2015 at 10:43:27AM -0700, Paul E. McKenney wrote: > > > On Fri, Oct 09, 2015 at 10:51:29AM +0100, Will Deacon wrote: [snip] >=20 > > > > We could also include a link to the ppcmem/herd web frontends and y= our > > > > lwn.net article. (ppcmem is already linked, but it's not obvious th= at > > > > you can run litmus tests in your browser). > > >=20 > > > I bet that the URLs for the web frontends are not stable long term. > > > Don't get me wrong, PPCMEM/ARMMEM has been there for me for a goodly > > > number of years, but professors do occasionally move from one institu= tion > > > to another. For but one example, Susmit Sarkar is now at University > > > of St. Andrews rather than at Cambridge. > > >=20 > > > So to make this work, we probably need to be thinking in terms of > > > asking the researchers for permission to include their ocaml code in = the > > > Linux-kernel source tree. I would be strongly in favor of this, actu= ally. > > >=20 > > > Thoughts? > >=20 > > I'm extremely hesitant to import a bunch of dubiously licensed, academic > > ocaml code into the kernel. Even if we did, who would maintain it? > >=20 > > A better solution might be to host a mirror of the code on kernel.org, > > along with a web front-end for people to play with (the tests we're tal= king > > about here do seem to run ok in my browser). >=20 > I am not too worried about how this happens, but we should avoid > constraining the work of our academic partners. The reason I was thinking > in terms of in the kernel was to avoid version-synchronization issues. > "Wait, this is Linux kernel v4.17, which means that you need to use > version 8.3.5.1 of the tooling... And with these four patches as well." >=20 Maybe including only the models' code(arm.cat, ppc.cat, etc.) into kernel rather than the whole code base could also solve the version-synchronization in some degree, and avoid maintaining the whole tool code? I'm assuming modifying the verifier's code other than the models' code will unlikely change the result of a litmus test. Regards, Boqun --hoZxPH4CaxYzWscb Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQEcBAABCAAGBQJWJk20AAoJEEl56MO1B/q4ZhgIAIJNKrEF8I4MaF7LblwtWQzy ZUULOT+HNdB8QIEjg2jg0eimdW4BjsI+ISr0330Hu6x2gSjmgPVUaSz0xniAXpCC pfytWZFIxQC8KX5i5AceCKpmaaBEVWjMR8zjc20VXffNCyI7Jnt/UlMy+vPIgh8m qN4G4GToiNQAltlNKJs0tikoAz75uS0WKpgzvQrc5kGUa03HYcXG9w0jGpfs7lEN W38loU2QFBqMlWJU/XKSTF0JeJqtLxMc/4YOZlcMUCWy/6nEM1BhO+jqbKkWgCYl gWn57Z+Vv6uHWcL1ojbOm6/9KJ3DQwa7aZTzUy10xBlsa3uY9jIkJ/0CtDH+o9Y= =aig7 -----END PGP SIGNATURE----- --hoZxPH4CaxYzWscb--