* [PATCH] CodeSamples/formal/herd: Remove dependency to linux-kernel-hardware.cat
@ 2018-02-19 15:14 Akira Yokosawa
2018-02-19 17:53 ` Paul E. McKenney
2018-02-20 15:29 ` [PATCH v2] CodeSamples/formal/herd: Remove dependency on linux-kernel-hardware.cat Akira Yokosawa
0 siblings, 2 replies; 6+ messages in thread
From: Akira Yokosawa @ 2018-02-19 15:14 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
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.
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
^ permalink raw reply related [flat|nested] 6+ messages in thread
* Re: [PATCH] CodeSamples/formal/herd: Remove dependency to linux-kernel-hardware.cat
2018-02-19 15:14 [PATCH] CodeSamples/formal/herd: Remove dependency to linux-kernel-hardware.cat Akira Yokosawa
@ 2018-02-19 17:53 ` Paul E. McKenney
2018-02-19 22:54 ` Akira Yokosawa
2018-02-20 15:29 ` [PATCH v2] CodeSamples/formal/herd: Remove dependency on linux-kernel-hardware.cat Akira Yokosawa
1 sibling, 1 reply; 6+ messages in thread
From: Paul E. McKenney @ 2018-02-19 17:53 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
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. 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. ;-)
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
>
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [PATCH] CodeSamples/formal/herd: Remove dependency to linux-kernel-hardware.cat
2018-02-19 17:53 ` Paul E. McKenney
@ 2018-02-19 22:54 ` Akira Yokosawa
2018-02-20 0:02 ` Paul E. McKenney
0 siblings, 1 reply; 6+ messages in thread
From: Akira Yokosawa @ 2018-02-19 22:54 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
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.
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 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?
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
>>
>
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [PATCH] CodeSamples/formal/herd: Remove dependency to linux-kernel-hardware.cat
2018-02-19 22:54 ` Akira Yokosawa
@ 2018-02-20 0:02 ` Paul E. McKenney
0 siblings, 0 replies; 6+ messages in thread
From: Paul E. McKenney @ 2018-02-20 0:02 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
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
> >>
> >
>
^ permalink raw reply [flat|nested] 6+ messages in thread
* [PATCH v2] CodeSamples/formal/herd: Remove dependency on linux-kernel-hardware.cat
2018-02-19 15:14 [PATCH] CodeSamples/formal/herd: Remove dependency to linux-kernel-hardware.cat Akira Yokosawa
2018-02-19 17:53 ` Paul E. McKenney
@ 2018-02-20 15:29 ` Akira Yokosawa
2018-02-20 16:33 ` Paul E. McKenney
1 sibling, 1 reply; 6+ messages in thread
From: Akira Yokosawa @ 2018-02-20 15:29 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 8ba8747211c2793fae6d280833190bbe74486198 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 20 Feb 2018 00:09:53 +0900
Subject: [PATCH v2] CodeSamples/formal/herd: Remove dependency on linux-kernel-hardware.cat
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 the provisional
memory-consistency model branch [1] intended to be merged into Linux
mainline.
[1] git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git lkmm
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
Changes in v2:
Rephrase change log to clarify the intention of the change.
--
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
^ permalink raw reply related [flat|nested] 6+ messages in thread
* Re: [PATCH v2] CodeSamples/formal/herd: Remove dependency on linux-kernel-hardware.cat
2018-02-20 15:29 ` [PATCH v2] CodeSamples/formal/herd: Remove dependency on linux-kernel-hardware.cat Akira Yokosawa
@ 2018-02-20 16:33 ` Paul E. McKenney
0 siblings, 0 replies; 6+ messages in thread
From: Paul E. McKenney @ 2018-02-20 16:33 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Wed, Feb 21, 2018 at 12:29:53AM +0900, Akira Yokosawa wrote:
> >From 8ba8747211c2793fae6d280833190bbe74486198 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Tue, 20 Feb 2018 00:09:53 +0900
> Subject: [PATCH v2] CodeSamples/formal/herd: Remove dependency on linux-kernel-hardware.cat
>
> 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 the provisional
> memory-consistency model branch [1] intended to be merged into Linux
> mainline.
>
> [1] git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git lkmm
>
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Applied and pushed, thank you!
Thanx, Paul
> ---
> Changes in v2:
> Rephrase change log to clarify the intention of the change.
> --
> 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
>
>
^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2018-02-20 16:33 UTC | newest]
Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-02-19 15:14 [PATCH] CodeSamples/formal/herd: Remove dependency to linux-kernel-hardware.cat Akira Yokosawa
2018-02-19 17:53 ` Paul E. McKenney
2018-02-19 22:54 ` Akira Yokosawa
2018-02-20 0:02 ` Paul E. McKenney
2018-02-20 15:29 ` [PATCH v2] CodeSamples/formal/herd: Remove dependency on linux-kernel-hardware.cat Akira Yokosawa
2018-02-20 16:33 ` Paul E. McKenney
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.