Re: [PATCH v2] barriers: introduce smp_mb__release_acquire and update documentation

[Boqun Feng]

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]
> 
> > > > We could also include a link to the ppcmem/herd web frontends and your
> > > > lwn.net article. (ppcmem is already linked, but it's not obvious that
> > > > you can run litmus tests in your browser).
> > > 
> > > 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 institution
> > > to another.  For but one example, Susmit Sarkar is now at University
> > > of St. Andrews rather than at Cambridge.
> > > 
> > > 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, actually.
> > > 
> > > Thoughts?
> > 
> > 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?
> > 
> > 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 talking
> > about here do seem to run ok in my browser).
> 
> 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."
> 

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

Attachment: signature.asc
Description: PGP signature