Re: [PATCH] CodeSamples/formal/herd: Remove dependency to linux-kernel-hardware.cat

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

On Tue, Feb 20, 2018 at 07:54:59AM +0900, Akira Yokosawa wrote:
> On 2018/02/20 2:53, Paul E. McKenney wrote:
> > On Tue, Feb 20, 2018 at 12:14:24AM +0900, Akira Yokosawa wrote:
> >> >From 9ef0701c8f161c8582bd6084e5d2706a0ad92d00 Mon Sep 17 00:00:00 2001
> >> From: Akira Yokosawa <akiyks@gmail.com>
> >> Date: Tue, 20 Feb 2018 00:09:53 +0900
> >> Subject: [PATCH] CodeSamples/formal/herd: Remove dependency to linux-kernel-hardware.cat
> >>
> >> linux-kernel-hardware.cat is not present in the branch expected
> >> to be merged in 4.17 window.
> > 
> > Good point, but it might be added at some later date.
> 
> Let me rephrase the change log. How about the following reasoning.
> 
> The target "run-herd7" doesn't depend on linux-kernel-hardware.cat.
> So remove it from the dependency list.
> This change also makes the target compatible with memory-consistency-model
> branch[1] intended to be in Linux 4.17 window at the moment.

What I get for looking at patches too early in the morning!  For some
reason I got the idea that you were removing linux-kernel-hardware.cat
itself.

> NOTE: They say https://github.com/aparri/memory-model.git won't be
> updated any more.
> 
> NOTE: We can add a target to run litmus tests with linux-kernel-hardware.cat
> once it is added in mainline or a prospective branch.
> 
> [1] git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git lkmm

This would be quite good, but let's wait until it gets to mainline.

But yes, please do update the change log as above and I will be happy
to apply the result.

> >                                                       This does raise
> > the question of whether it makes any sense to try to keep up with the
> > Linux-kernel memory model once that model is in mainline.  ;-)
> 
> You mean litmus tests used in perfbook and their explanation?

I mean the models themselves in CodeSamples/formal/herd/memory-model.
Except that yes, this is a symbolic link.  So clearly not a problem
at all.

Never mind!!!  Like I said, too early this morning!  :-/

							Thanx, Paul

>       Thanks, Akira
> 
> > 
> > 							Thanx, Paul
> > 
> >> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> >> ---
> >>  CodeSamples/formal/herd/Makefile | 2 +-
> >>  1 file changed, 1 insertion(+), 1 deletion(-)
> >>
> >> diff --git a/CodeSamples/formal/herd/Makefile b/CodeSamples/formal/herd/Makefile
> >> index 8e0635a..3162659 100644
> >> --- a/CodeSamples/formal/herd/Makefile
> >> +++ b/CodeSamples/formal/herd/Makefile
> >> @@ -31,7 +31,7 @@
> >>
> >>  LKMM_DIR     := memory-model
> >>  LKMM_FILES   := linux-kernel.bell linux-kernel.cat linux-kernel.cfg \
> >> -		linux-kernel.def linux-kernel-hardware.cat lock.cat
> >> +		linux-kernel.def lock.cat
> >>  LKMM_LIST    := $(addprefix $(LKMM_DIR)/,$(LKMM_FILES))
> >>  HERD_DIR     := $(shell pwd)
> >>  HERD7_CMD    := $(shell which herd7)
> >> -- 
> >> 2.7.4
> >>
> > 
>