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
