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

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

[Akira Yokosawa]

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.

        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

[PATCH 1/2] CodeSamples/formal/herd: Add Makefile and utility script

[Akira Yokosawa]

From 4ec89fb990662f555202908eff08ea29ffe87fa8 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 20 Nov 2017 00:09:46 +0900
Subject: [PATCH 1/2] CodeSamples/formal/herd: Add Makefile and utility script

Also add .gitignore for generated files to be ignored.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/formal/herd/.gitignore     |  4 +++
 CodeSamples/formal/herd/Makefile       | 60 ++++++++++++++++++++++++++++++++++
 CodeSamples/formal/herd/litmus2herd.sh | 20 ++++++++++++
 3 files changed, 84 insertions(+)
 create mode 100644 CodeSamples/formal/herd/.gitignore
 create mode 100644 CodeSamples/formal/herd/Makefile
 create mode 100644 CodeSamples/formal/herd/litmus2herd.sh

diff --git a/CodeSamples/formal/herd/.gitignore b/CodeSamples/formal/herd/.gitignore
new file mode 100644
index 0000000..c7ba463
--- /dev/null
+++ b/CodeSamples/formal/herd/.gitignore
@@ -0,0 +1,4 @@
+*.out
+*.herd
+klitmus
+klitmus.tar
diff --git a/CodeSamples/formal/herd/Makefile b/CodeSamples/formal/herd/Makefile
new file mode 100644
index 0000000..9df6e65
--- /dev/null
+++ b/CodeSamples/formal/herd/Makefile
@@ -0,0 +1,60 @@
+# SPDX-License-Identifier: GPL-2.0
+#
+# Default target: Transform litmus tests in ../litmus to herd7 compatible format
+#         (remove 2nd {})
+#
+# run-herd7: Examine transformed litmus tests by herd7 with LKMM
+#
+# cross-klitmus7: Cross-compile transformed litmus tests with klitmus7
+#
+# run-herd7-bench: Run benchmark tests of herd7 itself
+#
+# Note: LKMM model is assumed to reside in a directory next to perfbook's
+#       local repository.
+#
+# Copyright (C) Akira Yokosawa, 2017
+#
+# Authors: Akira Yokosawa <akiyks@gmail.com>
+
+LKMM_DIR     := ../../../../memory-model
+HERD_DIR     := $(shell pwd)
+HERD7_CMD    := $(shell which herd7)
+KLITMUS7_CMD := $(shell which klitmus7)
+LITMUS7_TEST := $(notdir $(wildcard ../litmus/*.litmus))
+LITMUS7_HERD_TEST := $(addsuffix .herd,$(LITMUS7_TEST))
+LITMUS7_HERD_OUT  := $(addsuffix .out,$(LITMUS7_TEST))
+HERD_BENCH        := $(wildcard C-SB+l-*.litmus)
+HERD_BENCH_LONG   := $(wildcard C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-*.litmus)
+HERD_BENCH_SHORT  := $(filter-out $(HERD_BENCH_LONG),$(HERD_BENCH))
+HERD_BENCH_OUT    := $(addsuffix .out,$(HERD_BENCH_SHORT))
+
+.PHONY: all clean litmus2herd run-herd7 run-herd7-bench cross-klitmus
+
+all: litmus2herd
+
+litmus2herd: $(LITMUS7_HERD_TEST)
+
+$(LITMUS7_HERD_TEST): %.herd: ../litmus/%
+	sh ./litmus2herd.sh $< $@
+
+run-herd7: $(LITMUS7_HERD_OUT)
+
+run-herd7-bench: $(HERD_BENCH_OUT)
+
+$(LITMUS7_HERD_OUT): %.out: %.herd
+	cd $(LKMM_DIR); herd7 -conf linux-kernel.cfg $(HERD_DIR)/$< > $(HERD_DIR)/$@
+
+$(HERD_BENCH_OUT): %.out: %
+	cd $(LKMM_DIR); herd7 -conf linux-kernel.cfg $(HERD_DIR)/$< > $(HERD_DIR)/$@
+
+cross-klitmus: klitmus.tar
+
+klitmus.tar: litmus2herd
+	mkdir -p klitmus
+	cd $(LKMM_DIR); klitmus7 -o $(HERD_DIR)/klitmus $(addprefix $(HERD_DIR)/,$(LITMUS7_HERD_TEST))
+	tar cf klitmus.tar ./klitmus
+
+clean:
+	rm -f *.out *.herd
+	rm -rf klitmus
+	rm -f klitmus.tar
diff --git a/CodeSamples/formal/herd/litmus2herd.sh b/CodeSamples/formal/herd/litmus2herd.sh
new file mode 100644
index 0000000..ebcd01b
--- /dev/null
+++ b/CodeSamples/formal/herd/litmus2herd.sh
@@ -0,0 +1,20 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0
+#
+# Remove 2nd {} in litmus tests compatible with litmus7:
+#    {
+#    #include <api.h>
+#    }
+#
+# Borrowed from one of the answers in:
+#   https://unix.stackexchange.comm/questions/213385/
+# Not the selected answer because it read input file twice.
+# But this is easier to follow.
+#
+# Copyright (C) Akira Yokosawa, 2017
+#
+# Authors: Akira Yokosawa <akiyks@gmail.com>
+
+grep -n -A1 -B1 "api.h" $1 | \
+sed -n 's/^\([0-9]\{1,\}\).*/\1d/p' | \
+sed -f - $1 > $2
-- 
2.7.4

[PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus

[Akira Yokosawa]

From 62491d966a645d08ffc6bb0c5bae9f725458cbec Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 23 Nov 2017 12:07:18 +0900
Subject: [PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus

Target "cross-klitmus" does not depend on memory model.
Remove the implicit dependency of "cd $(LKMM_DIR)" from the recipe.

Fixes: ef76630632df ("CodeSamples/formal/herd: Add Makefile and utility script")
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 1abe5c7..b99699b 100644
--- a/CodeSamples/formal/herd/Makefile
+++ b/CodeSamples/formal/herd/Makefile
@@ -73,7 +73,7 @@ cross-klitmus: klitmus.tar

 klitmus.tar: litmus2herd
 	mkdir -p klitmus
-	cd $(LKMM_DIR); klitmus7 -o $(HERD_DIR)/klitmus $(addprefix $(HERD_DIR)/,$(LITMUS7_HERD_TEST))
+	klitmus7 -o klitmus $(LITMUS7_HERD_TEST)
 	tar cf klitmus.tar ./klitmus

 clean:
-- 
2.7.4

Re: [PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus

[Paul E. McKenney]

[-- Attachment #1: Type: text/plain, Size: 1447 bytes --]

On Thu, Nov 23, 2017 at 12:17:57PM +0900, Akira Yokosawa wrote:
> >From 62491d966a645d08ffc6bb0c5bae9f725458cbec Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Thu, 23 Nov 2017 12:07:18 +0900
> Subject: [PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus
> 
> Target "cross-klitmus" does not depend on memory model.
> Remove the implicit dependency of "cd $(LKMM_DIR)" from the recipe.
> 
> Fixes: ef76630632df ("CodeSamples/formal/herd: Add Makefile and utility script")
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>

I applied and pushed both, the first just before the release and the one
below as the first commit after the release.

I also attached the (very crude) scripts that I use to collect herd
performance data, just in case they are useful.

							Thanx, Paul

> ---
>  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 1abe5c7..b99699b 100644
> --- a/CodeSamples/formal/herd/Makefile
> +++ b/CodeSamples/formal/herd/Makefile
> @@ -73,7 +73,7 @@ cross-klitmus: klitmus.tar
> 
>  klitmus.tar: litmus2herd
>  	mkdir -p klitmus
> -	cd $(LKMM_DIR); klitmus7 -o $(HERD_DIR)/klitmus $(addprefix $(HERD_DIR)/,$(LITMUS7_HERD_TEST))
> +	klitmus7 -o klitmus $(LITMUS7_HERD_TEST)
>  	tar cf klitmus.tar ./klitmus
> 
>  clean:
> -- 
> 2.7.4
> 
> 

[-- Attachment #2: absperf.sh --]
[-- Type: application/x-sh, Size: 170 bytes --]

[-- Attachment #3: absperf-reduce.sh --]
[-- Type: application/x-sh, Size: 623 bytes --]

Re: [PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus

[Akira Yokosawa]

On 2017/11/26 10:40:24 -0800, Paul E. McKenney wrote:
> On Thu, Nov 23, 2017 at 12:17:57PM +0900, Akira Yokosawa wrote:
>> >From 62491d966a645d08ffc6bb0c5bae9f725458cbec Mon Sep 17 00:00:00 2001
>> From: Akira Yokosawa <akiyks@gmail.com>
>> Date: Thu, 23 Nov 2017 12:07:18 +0900
>> Subject: [PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus
>>
>> Target "cross-klitmus" does not depend on memory model.
>> Remove the implicit dependency of "cd $(LKMM_DIR)" from the recipe.
>>
>> Fixes: ef76630632df ("CodeSamples/formal/herd: Add Makefile and utility script")
>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> 
> I applied and pushed both, the first just before the release and the one
> below as the first commit after the release.
> 
> I also attached the (very crude) scripts that I use to collect herd
> performance data, just in case they are useful.

Well, I have no idea how to use absperf-reduce.sh.
It's partly because I'm not good at awk, but I can't figure out what kind of
input and arguments the script assumes.

Can you show me an example?

I know absperf.sh runs each litmus test 10 times with timeout of 15 minutes.

I'd be happy to integrate the collection feature into formal/herd/Makefile,
once I know what is expected.

      Thanks, Akira

> 
> 							Thanx, Paul
[...]

Re: [PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus

[Paul E. McKenney]

On Wed, Nov 29, 2017 at 12:24:32AM +0900, Akira Yokosawa wrote:
> On 2017/11/26 10:40:24 -0800, Paul E. McKenney wrote:
> > On Thu, Nov 23, 2017 at 12:17:57PM +0900, Akira Yokosawa wrote:
> >> >From 62491d966a645d08ffc6bb0c5bae9f725458cbec Mon Sep 17 00:00:00 2001
> >> From: Akira Yokosawa <akiyks@gmail.com>
> >> Date: Thu, 23 Nov 2017 12:07:18 +0900
> >> Subject: [PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus
> >>
> >> Target "cross-klitmus" does not depend on memory model.
> >> Remove the implicit dependency of "cd $(LKMM_DIR)" from the recipe.
> >>
> >> Fixes: ef76630632df ("CodeSamples/formal/herd: Add Makefile and utility script")
> >> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> > 
> > I applied and pushed both, the first just before the release and the one
> > below as the first commit after the release.
> > 
> > I also attached the (very crude) scripts that I use to collect herd
> > performance data, just in case they are useful.
> 
> Well, I have no idea how to use absperf-reduce.sh.
> It's partly because I'm not good at awk, but I can't figure out what kind of
> input and arguments the script assumes.

Good point...

> Can you show me an example?
> 
> I know absperf.sh runs each litmus test 10 times with timeout of 15 minutes.
> 
> I'd be happy to integrate the collection feature into formal/herd/Makefile,
> once I know what is expected.

So you run absperf.sh and feed its output into absperf-reduce.sh as
its standard input.

I normally dump the absperf.sh to a file and then run absperf-reduce.sh
on that file.  The output is the litmus-test name followed by the
average, minimum, and maximum runtimes for that litmus test.

One oddity is that both scripts expect the scripts to be in the
directory litmus-tests/absperf -- this is hard-coded into absperf.sh's
for-loop and into the first pattern of absperf-reduce.sh's awk script
(the "/^litmus-tests/ {" line).

So here is how the absperf-reduce.sh script operates, in the likely
event that you would prefer to just rewrite it (which would be fine
by me):

o	Each awk statement block is preceded by a pattern, and
	contains a "{}"-enclosed sequence of statements.  These
	statements are executed only when the pattern matches the
	current line.  The special pattern "END" executes after
	the input has been consumed and processed.

o	The "/^litmus-tests/" matches lines beginning with "litmus-tests".
	These lines are those "echo"ed by absperf.sh.  This check
	relies on the fact that herd7 doesn't output lines beginning
	with "litmus-tests", which is admittedly a very fragile
	approach.

	Upon match, the variable "curtest" is set to the first word
	on the current line (which is the litmus-test pathname)
	and the variable "testrun" is set to zero to say that we
	do not yet have any evidence that the test ran to completion.

o	The "/^Test/" is output by herd7, and indicates that the
	litmus test actually completed.  So we set "testran" to 1.

o	The "/maxresident)k/" matches output from /bin/time.  If
	herd7 ran, the following lines parse the /bin/time output,
	and accumulate the number of runs, the total time, and
	the minimum and maximum time in awk associative arrays.

	(In awk, 'a["efwefew"]++' is a perfectly valid expression,
	and it increments the element of "a" indexed by the string
	"efwefew".  I am pretty sure that most scripting languages
	do this these days, but it was pretty surprising back when
	awk came out with it.)

o	The "END" loops through all elements of the array, with
	the variable "i" taking on each index of that array in
	turn.  The print statement thus prints the litmus test
	name along with its statistics.

I then hand-edited the output to make various tables in email and Table
12.3 in perfbook.

Why awk?  Back when I was starting scripting languages, it was the only
one availalble on UNIX.  This would have been some time in the 1980s.
It is very unlikely to be the best choice for someone starting out
today.  ;-)

							Thanx, Paul

Re: [PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus

[Akira Yokosawa]

On 2017/11/28 16:31:13 -0800, Paul E. McKenney wrote:
> On Wed, Nov 29, 2017 at 12:24:32AM +0900, Akira Yokosawa wrote:
>> On 2017/11/26 10:40:24 -0800, Paul E. McKenney wrote:
>>> On Thu, Nov 23, 2017 at 12:17:57PM +0900, Akira Yokosawa wrote:
>>>> >From 62491d966a645d08ffc6bb0c5bae9f725458cbec Mon Sep 17 00:00:00 2001
>>>> From: Akira Yokosawa <akiyks@gmail.com>
>>>> Date: Thu, 23 Nov 2017 12:07:18 +0900
>>>> Subject: [PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus
>>>>
>>>> Target "cross-klitmus" does not depend on memory model.
>>>> Remove the implicit dependency of "cd $(LKMM_DIR)" from the recipe.
>>>>
>>>> Fixes: ef76630632df ("CodeSamples/formal/herd: Add Makefile and utility script")
>>>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
>>>
>>> I applied and pushed both, the first just before the release and the one
>>> below as the first commit after the release.
>>>
>>> I also attached the (very crude) scripts that I use to collect herd
>>> performance data, just in case they are useful.
>>
>> Well, I have no idea how to use absperf-reduce.sh.
>> It's partly because I'm not good at awk, but I can't figure out what kind of
>> input and arguments the script assumes.
> 
> Good point...
> 
>> Can you show me an example?
>>
>> I know absperf.sh runs each litmus test 10 times with timeout of 15 minutes.
>>
>> I'd be happy to integrate the collection feature into formal/herd/Makefile,
>> once I know what is expected.
> 
> So you run absperf.sh and feed its output into absperf-reduce.sh as
> its standard input.
> 
> I normally dump the absperf.sh to a file and then run absperf-reduce.sh
> on that file.  The output is the litmus-test name followed by the
> average, minimum, and maximum runtimes for that litmus test.
> 
> One oddity is that both scripts expect the scripts to be in the
> directory litmus-tests/absperf -- this is hard-coded into absperf.sh's
> for-loop and into the first pattern of absperf-reduce.sh's awk script
> (the "/^litmus-tests/ {" line).

Ah, this is the key point I could not figure out.
Now I can run the scripts using short litmus tests.

We also need memory model files in the current directory.

So the current scheme in CodeSamples/formal/herd/ of "cd memory-model; herd7 ..."
conflicts with the above assumption.

Let me think what approach is suitable for perfbook's CodeSamples.
This may take a while.

       Thanks, Akira

> 
> So here is how the absperf-reduce.sh script operates, in the likely
> event that you would prefer to just rewrite it (which would be fine
> by me):
> 
> o	Each awk statement block is preceded by a pattern, and
> 	contains a "{}"-enclosed sequence of statements.  These
> 	statements are executed only when the pattern matches the
> 	current line.  The special pattern "END" executes after
> 	the input has been consumed and processed.
> 
> o	The "/^litmus-tests/" matches lines beginning with "litmus-tests".
> 	These lines are those "echo"ed by absperf.sh.  This check
> 	relies on the fact that herd7 doesn't output lines beginning
> 	with "litmus-tests", which is admittedly a very fragile
> 	approach.
> 
> 	Upon match, the variable "curtest" is set to the first word
> 	on the current line (which is the litmus-test pathname)
> 	and the variable "testrun" is set to zero to say that we
> 	do not yet have any evidence that the test ran to completion.
> 
> o	The "/^Test/" is output by herd7, and indicates that the
> 	litmus test actually completed.  So we set "testran" to 1.
> 
> o	The "/maxresident)k/" matches output from /bin/time.  If
> 	herd7 ran, the following lines parse the /bin/time output,
> 	and accumulate the number of runs, the total time, and
> 	the minimum and maximum time in awk associative arrays.
> 
> 	(In awk, 'a["efwefew"]++' is a perfectly valid expression,
> 	and it increments the element of "a" indexed by the string
> 	"efwefew".  I am pretty sure that most scripting languages
> 	do this these days, but it was pretty surprising back when
> 	awk came out with it.)
> 
> o	The "END" loops through all elements of the array, with
> 	the variable "i" taking on each index of that array in
> 	turn.  The print statement thus prints the litmus test
> 	name along with its statistics.
> 
> I then hand-edited the output to make various tables in email and Table
> 12.3 in perfbook.
> 
> Why awk?  Back when I was starting scripting languages, it was the only
> one availalble on UNIX.  This would have been some time in the 1980s.
> It is very unlikely to be the best choice for someone starting out
> today.  ;-)
> 
> 							Thanx, Paul
> 
> 

Re: [PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus

[Paul E. McKenney]

On Thu, Nov 30, 2017 at 12:24:26AM +0900, Akira Yokosawa wrote:
> On 2017/11/28 16:31:13 -0800, Paul E. McKenney wrote:
> > On Wed, Nov 29, 2017 at 12:24:32AM +0900, Akira Yokosawa wrote:
> >> On 2017/11/26 10:40:24 -0800, Paul E. McKenney wrote:
> >>> On Thu, Nov 23, 2017 at 12:17:57PM +0900, Akira Yokosawa wrote:
> >>>> >From 62491d966a645d08ffc6bb0c5bae9f725458cbec Mon Sep 17 00:00:00 2001
> >>>> From: Akira Yokosawa <akiyks@gmail.com>
> >>>> Date: Thu, 23 Nov 2017 12:07:18 +0900
> >>>> Subject: [PATCH] CodeSamples/formal/herd: Remove dependency to memory model in cross-klitmus
> >>>>
> >>>> Target "cross-klitmus" does not depend on memory model.
> >>>> Remove the implicit dependency of "cd $(LKMM_DIR)" from the recipe.
> >>>>
> >>>> Fixes: ef76630632df ("CodeSamples/formal/herd: Add Makefile and utility script")
> >>>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> >>>
> >>> I applied and pushed both, the first just before the release and the one
> >>> below as the first commit after the release.
> >>>
> >>> I also attached the (very crude) scripts that I use to collect herd
> >>> performance data, just in case they are useful.
> >>
> >> Well, I have no idea how to use absperf-reduce.sh.
> >> It's partly because I'm not good at awk, but I can't figure out what kind of
> >> input and arguments the script assumes.
> > 
> > Good point...
> > 
> >> Can you show me an example?
> >>
> >> I know absperf.sh runs each litmus test 10 times with timeout of 15 minutes.
> >>
> >> I'd be happy to integrate the collection feature into formal/herd/Makefile,
> >> once I know what is expected.
> > 
> > So you run absperf.sh and feed its output into absperf-reduce.sh as
> > its standard input.
> > 
> > I normally dump the absperf.sh to a file and then run absperf-reduce.sh
> > on that file.  The output is the litmus-test name followed by the
> > average, minimum, and maximum runtimes for that litmus test.
> > 
> > One oddity is that both scripts expect the scripts to be in the
> > directory litmus-tests/absperf -- this is hard-coded into absperf.sh's
> > for-loop and into the first pattern of absperf-reduce.sh's awk script
> > (the "/^litmus-tests/ {" line).
> 
> Ah, this is the key point I could not figure out.
> Now I can run the scripts using short litmus tests.
> 
> We also need memory model files in the current directory.
> 
> So the current scheme in CodeSamples/formal/herd/ of "cd memory-model; herd7 ..."
> conflicts with the above assumption.

Indeed, and one more reason to rewrite.  ;-)

> Let me think what approach is suitable for perfbook's CodeSamples.
> This may take a while.

Not an emergency as far as I know, especially given that I can continue
using the old scripts.  ;-)

							Thanx, Paul

>        Thanks, Akira
> 
> > 
> > So here is how the absperf-reduce.sh script operates, in the likely
> > event that you would prefer to just rewrite it (which would be fine
> > by me):
> > 
> > o	Each awk statement block is preceded by a pattern, and
> > 	contains a "{}"-enclosed sequence of statements.  These
> > 	statements are executed only when the pattern matches the
> > 	current line.  The special pattern "END" executes after
> > 	the input has been consumed and processed.
> > 
> > o	The "/^litmus-tests/" matches lines beginning with "litmus-tests".
> > 	These lines are those "echo"ed by absperf.sh.  This check
> > 	relies on the fact that herd7 doesn't output lines beginning
> > 	with "litmus-tests", which is admittedly a very fragile
> > 	approach.
> > 
> > 	Upon match, the variable "curtest" is set to the first word
> > 	on the current line (which is the litmus-test pathname)
> > 	and the variable "testrun" is set to zero to say that we
> > 	do not yet have any evidence that the test ran to completion.
> > 
> > o	The "/^Test/" is output by herd7, and indicates that the
> > 	litmus test actually completed.  So we set "testran" to 1.
> > 
> > o	The "/maxresident)k/" matches output from /bin/time.  If
> > 	herd7 ran, the following lines parse the /bin/time output,
> > 	and accumulate the number of runs, the total time, and
> > 	the minimum and maximum time in awk associative arrays.
> > 
> > 	(In awk, 'a["efwefew"]++' is a perfectly valid expression,
> > 	and it increments the element of "a" indexed by the string
> > 	"efwefew".  I am pretty sure that most scripting languages
> > 	do this these days, but it was pretty surprising back when
> > 	awk came out with it.)
> > 
> > o	The "END" loops through all elements of the array, with
> > 	the variable "i" taking on each index of that array in
> > 	turn.  The print statement thus prints the litmus test
> > 	name along with its statistics.
> > 
> > I then hand-edited the output to make various tables in email and Table
> > 12.3 in perfbook.
> > 
> > Why awk?  Back when I was starting scripting languages, it was the only
> > one availalble on UNIX.  This would have been some time in the 1980s.
> > It is very unlikely to be the best choice for someone starting out
> > today.  ;-)
> > 
> > 							Thanx, Paul
> > 
> > 
> 

[PATCH 2/2] CodeSamples/formal/litmus: Fix type of 2:r2 in C-WWC+o+o-*.litmus test

[Akira Yokosawa]

From 180abe9a72d4e3fbe200ce2a032a6c616a70ce03 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 21 Nov 2017 22:26:53 +0900
Subject: [PATCH 2/2] CodeSamples/formal/litmus: Fix type of 2:r2 in C-WWC+o+o-*.litmus test

This change gets rid of warnings in klitmus7 cross-compile:

-------
In file included from include/uapi/linux/stddef.h:1:0,
                 from include/linux/stddef.h:4,
                 from ./include/uapi/linux/posix_types.h:4,
                 from include/uapi/linux/types.h:13,
                 from include/linux/types.h:5,
                 from include/linux/list.h:4,
                 from include/linux/module.h:9,
                 from [...]/CodeSamples/formal/herd/klitmus/litmus012.c:11:
[...]/CodeSamples/formal/herd/klitmus/litmus012.c: In function 'code2':
include/linux/compiler.h:297:14: warning: cast from pointer to integer of different size [-Wpointer-to-int-cast]
   { .__val = (__force typeof(x)) (val) }; \
              ^
[...]/CodeSamples/formal/herd/klitmus/litmus012.c:414:2: note: in expansion of macro 'WRITE_ONCE'
  WRITE_ONCE(*r2, c);
  ^
-------

r2 is declared as "int *r2;", and WRITE_ONCE(*r2, c) will store to an
int variable. r2 should have been "int**" type.

Also revert the variable used in the WRITE_ONCE to "a" as had been
before the changes listed in the "Fixes:" tags below.

Fixes: d78c5805a715 ("advsync: Fix C-WWC+o+o-data-o+o-addr-o litmus tests")
Fixes: f0222eae620f ("advsync: Fix C-WWC+o+o-r+o-addr-o litmus tests")
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus | 9 ++++-----
 CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus      | 9 ++++-----
 2 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus b/CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus
index c0cbee8..cd9df06 100644
--- a/CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus
+++ b/CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus
@@ -3,7 +3,6 @@ C C-WWC+o+o-data-o+o-addr-o
 {
 int a = 0;
 int b = 0;
-int *c = &b;
 int *x = &a;
 int *y = &b;
 }
@@ -25,12 +24,12 @@ P1(int **x, int **y)
 	WRITE_ONCE(*y, r1);
 }

-P2(int **y, int **c)
+P2(int **y, int *a)
 {
-	int *r2;
+	int **r2;

-	r2 = READ_ONCE(*y);
-	WRITE_ONCE(*r2, c);
+	r2 = (int**)READ_ONCE(*y);
+	WRITE_ONCE(*r2, a);
 }

 exists(1:r1=x /\ 2:r2=x /\ x=x)
diff --git a/CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus b/CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus
index 6f0a810..6a65d67 100644
--- a/CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus
+++ b/CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus
@@ -3,7 +3,6 @@ C C-WWC+o+o-r+o-addr-o
 {
 int a = 0;
 int b = 0;
-int *c = &b;
 int *x = &a;
 int *y = &b;
 }
@@ -25,12 +24,12 @@ P1(int **x, int **y)
 	smp_store_release(y, r1);
 }

-P2(int **y, int **c)
+P2(int **y, int *a)
 {
-	int *r2;
+	int **r2;

-	r2 = READ_ONCE(*y);
-	WRITE_ONCE(*r2, c);
+	r2 = (int**)READ_ONCE(*y);
+	WRITE_ONCE(*r2, a);
 }

 exists(1:r1=x /\ 2:r2=x /\ x=x)
-- 
2.7.4

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

[Paul E. McKenney]

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?

							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
> 

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

[Akira Yokosawa]

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?

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
>> 
> 

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

[Paul E. McKenney]

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
> 

[PATCH] CodeSamples/formal/herd: Add existence check of memory model

[Akira Yokosawa]

From 53df3405f334e7cda1d650fefbf5fba416aa4abe Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 22 Nov 2017 20:08:09 +0900
Subject: [PATCH] CodeSamples/formal/herd: Add existence check of memory model

If any of the necessary files is lacking, output a message
to give instructions for preparation of the memory model.

Suggested-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/formal/herd/.gitignore |  1 +
 CodeSamples/formal/herd/Makefile   | 28 +++++++++++++++++++++++++---
 2 files changed, 26 insertions(+), 3 deletions(-)

diff --git a/CodeSamples/formal/herd/.gitignore b/CodeSamples/formal/herd/.gitignore
index c7ba463..e0ad195 100644
--- a/CodeSamples/formal/herd/.gitignore
+++ b/CodeSamples/formal/herd/.gitignore
@@ -2,3 +2,4 @@
 *.herd
 klitmus
 klitmus.tar
+memory-model
diff --git a/CodeSamples/formal/herd/Makefile b/CodeSamples/formal/herd/Makefile
index 9df6e65..1abe5c7 100644
--- a/CodeSamples/formal/herd/Makefile
+++ b/CodeSamples/formal/herd/Makefile
@@ -9,14 +9,24 @@
 #
 # run-herd7-bench: Run benchmark tests of herd7 itself
 #
-# Note: LKMM model is assumed to reside in a directory next to perfbook's
-#       local repository.
+# Note: There need to be a symbolic link "memory-model" under
+#       CodeSamples/formal/herd for herd7 to work.
+#       The memory model is available at the git archive:
+#           https://github.com/aparri/memory-model.git.
+#       Make sure the symbolic link points to the actual directory.
+#       Alternatively, you can copy the files listed in LKMM_FILES to
+#       a subdirectory "memory-model".
+#
+#       klitmus7 doesn't require the memory model.
 #
 # Copyright (C) Akira Yokosawa, 2017
 #
 # Authors: Akira Yokosawa <akiyks@gmail.com>

-LKMM_DIR     := ../../../../memory-model
+LKMM_DIR     := memory-model
+LKMM_FILES   := linux-kernel.bell linux-kernel.cat linux-kernel.cfg \
+		linux-kernel.def linux-kernel-hardware.cat lock.cat
+LKMM_LIST    := $(addprefix $(LKMM_DIR)/,$(LKMM_FILES))
 HERD_DIR     := $(shell pwd)
 HERD7_CMD    := $(shell which herd7)
 KLITMUS7_CMD := $(shell which klitmus7)
@@ -41,6 +51,18 @@ run-herd7: $(LITMUS7_HERD_OUT)

 run-herd7-bench: $(HERD_BENCH_OUT)

+$(LKMM_LIST):
+	@echo "#####################################################"
+	@echo "### Please prepare Linux Kernel Memory Model.     ###"
+	@echo "### You can get it at the git archive:            ###"
+	@echo "###   https://github.com/aparri/memory-model.git  ###"
+	@echo "###                                               ###"
+	@echo "### Refer to comment in Makefile for more info.   ###"
+	@echo "#####################################################"
+	@exit 1
+
+$(LITMUS7_HERD_OUT) $(HERD_BENCH_OUT): $(LKMM_LIST)
+
 $(LITMUS7_HERD_OUT): %.out: %.herd
 	cd $(LKMM_DIR); herd7 -conf linux-kernel.cfg $(HERD_DIR)/$< > $(HERD_DIR)/$@

-- 
2.7.4

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

[Akira Yokosawa]

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

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.

        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