Re: [PATCH 0/2] Add Makefile in CodeSamples/formal/herd

["Paul E. McKenney" <paulmck@linux.vnet.ibm.com>]

On Wed, Nov 22, 2017 at 10:02:16AM +0900, Akira Yokosawa wrote:
> 
> 
> 
> 2017/11/22 9:12 +0900、Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
> 
> > On Wed, Nov 22, 2017 at 12:34:08AM +0900, Akira Yokosawa wrote:
> >>> From 180abe9a72d4e3fbe200ce2a032a6c616a70ce03 Mon Sep 17 00:00:00 2001
> >> From: Akira Yokosawa <akiyks@gmail.com>
> >> Date: Wed, 22 Nov 2017 00:04:40 +0900
> >> Subject: [PATCH 0/2] Add Makefile in CodeSamples/formal/herd
> >> 
> >> (Resending with To: Paul)
> >> Hi Paul,
> >> 
> >> This is my attempt to add Makefile in CodeSamples/formal/herd.
> >> The recipes here assumes that the memory-model's repository resides
> >> beside the perfbook's repository on your machine.
> >> 
> >> The targets include conversion of litmus7 compatible tests under
> >> litmus/ directory to herd7/klitmus7 compatible ones,
> >> running converted litmus tests by herd7,
> >> running herd7 benchmark tests by herd7,
> >> and preparing directory for klitmus7 cross-compile of converted
> >> tests.
> >> 
> >> Currently, there is no test other than benchmarks under herd/
> >> directory which is not compatible with litmus7. When such tests
> >> are added there, the Makefile can be updated to run and cross-compile
> >> them along with the converted tests.
> >> 
> >> Patch #1 adds the Makefile and a helper script.
> >> 
> >> Patch #2 is a fix of compiler warnings revealed in klitmus7 cross-
> >> compiling.
> >> These C-WWC-o+o-* litmus tests were modified by me in this August.
> >> That looked sufficient for litmus7, but definitions in kernel header
> >> files used in klitmus7 aren't satisfied. The change here is the result
> >> of some try-and-errors. There can be smarter way to describe these tests.
> >> They are not used in the text at the moment, so their fix is not
> >> urgent, I suppose.
> > 
> > I queued these, but let's talk about the memory model.  Currently,
> > it is available in this git archive:
> > 
> >    https://github.com/aparri/memory-model.git
> > 
> > Specifically, these files:
> > 
> >    linux-kernel.bell
> >    linux-kernel.cat
> >    linux-kernel.cfg
> >    linux-kernel.def
> >    linux-kernel-hardware.cat
> >    lock.cat
> > 
> > We hope to get these upstream into the Linux kernel during the next
> > merge window.  So maybe the right thing to do is to require that the
> > user copy the files into the formal/herd directory, and have Makefile
> > give instructions and stop if they are not present.
> > 
> > Thoughts?
> 
> I’m kind of against having those untracked files there.
> The directory where they reside can be specified by
> overriding LKMM_DIR variable in the Makefile by an option to make command.
> So change of the location of memory model won’t be a problem.
> 
> But yes, the check of the existence of the directory can help users. I’ll see what l can do.
> 
> Thoughts?

As long as the directory can be a symbolic link to the actual directory,
that should work fine.

							Thanx, Paul

> Akira 
> (from mobile, might be QP encoded)
> 
> > 
> >                            Thanx, Paul
> > 
> >>        Thanks, Akira
> >> --
> >> Akira Yokosawa (2):
> >>  CodeSamples/formal/herd: Add Makefile and utility script
> >>  CodeSamples/formal/litmus: Fix type of 2:r2 in C-WWC+o+o-*.litmus test
> >> 
> >> CodeSamples/formal/herd/.gitignore                 |  4 ++
> >> CodeSamples/formal/herd/Makefile                   | 60 ++++++++++++++++++++++
> >> CodeSamples/formal/herd/litmus2herd.sh             | 20 ++++++++
> >> .../formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus |  9 ++--
> >> .../formal/litmus/C-WWC+o+o-r+o-addr-o.litmus      |  9 ++--
> >> 5 files changed, 92 insertions(+), 10 deletions(-)
> >> create mode 100644 CodeSamples/formal/herd/.gitignore
> >> create mode 100644 CodeSamples/formal/herd/Makefile
> >> create mode 100644 CodeSamples/formal/herd/litmus2herd.sh
> >> 
> >> -- 
> >> 2.7.4
> >> 
> >> --
> >> To unsubscribe from this list: send the line "unsubscribe perfbook" in
> >> the body of a message to majordomo@vger.kernel.org
> >> More majordomo info at  http://vger.kernel.org/majordomo-info.html
> >> 
> > 
> --
> To unsubscribe from this list: send the line "unsubscribe perfbook" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
>