[PATCH 0/8] Improve conversion of litmus test snippet

[PATCH 0/8] Improve conversion of litmus test snippet

[Akira Yokosawa]

Hi Paul,

In snippets of litmus tests you added recently uses "locations"
directive. It was not covered by reorder_ltms.pl.
This series enhances reorder_ltms.pl to add an option to
the meta command "\end[snippet]".

Now you can put C-RCU-remove.litmus and
C-RomanPenyanev-list-rcu-rr.litmus under CodeSamples/.

Patch #1 is the enhancement of reorder_ltms.pl.
Patch #2 adds C-RCU-remove.litmus in CodeSamples/formal/herd.
Note that I modified the choice of characters given to
the "commandchars=" option to avoid collision with characters
used in snippets.
Patch #3 adds recipe in Makefile to run the added tests by
"make run-herd7".
Patch #4 replaces the inline snippet code with converted one.
Patch #5 adds another RCU litmus test in CodeSamples/formal/herd.
Patch #6 imports snippet converted from above.
Patch #7 converts existing PPC IRIW litmus tests to new scheme
It also reduces the width of the snippets to fit in 2c column
width.
Patch #8 is a trivial typo fix.

I'm afraid commit logs in this series is not descriptive
enough, but hopefully the intention of the changes are evident.

        Thanks, Akira
-- 
Akira Yokosawa (8):
  reorder_ltms.pl: Add 'locationslabel=' option to \end[snippet]
  CodeSamples/formal: Add C-RCU-remove.litmus
  CodeSamples/formal/herd: Add recipe for native .litmus tests
  formal/axiomatic: Import snippet from C-RCU-remove.litmus
  CodeSamples/formal: Add C-RomanPenyanev-list-rcu-rr.litmus
  formal/axiomatic: Import snippet from
    C-RomanPenyanev-list-rcu-rr.litmus
  formal/axiomatic: Convert snippets of IRIW tests to new scheme
  formal/axiomatic: Fill in missing ')'

 CodeSamples/formal/herd/C-RCU-remove.litmus        |  27 +++
 .../formal/herd/C-RomanPenyaev-list-rcu-rr.litmus  |  47 +++++
 CodeSamples/formal/herd/Makefile                   |  21 ++-
 formal/axiomatic.tex                               | 201 +++++++--------------
 utilities/reorder_ltms.pl                          |  15 ++
 5 files changed, 164 insertions(+), 147 deletions(-)
 create mode 100644 CodeSamples/formal/herd/C-RCU-remove.litmus
 create mode 100644 CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus

-- 
2.7.4

[PATCH 1/8] reorder_ltms.pl: Add 'locationslabel=' option to \end[snippet]

[Akira Yokosawa]

From 3a6f1d8ea52b05c8b790e27bc7a9bf73cbda2555 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 31 Oct 2018 07:38:43 +0900
Subject: [PATCH 1/8] reorder_ltms.pl: Add 'locationslabel=' option to \end[snippet]

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 utilities/reorder_ltms.pl | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/utilities/reorder_ltms.pl b/utilities/reorder_ltms.pl
index d4770d0..9999c29 100755
--- a/utilities/reorder_ltms.pl
+++ b/utilities/reorder_ltms.pl
@@ -47,6 +47,7 @@ my $end_command;
 my $lnlbl_command;
 my $lnlbl_on_exists = "";
 my $lnlbl_on_filter = "";
+my $lnlbl_on_locations = "";
 my $status = 0;	# 0: just started, 1: first_line read; 2: begin line output,
 		# 3: end line read
 
@@ -58,6 +59,9 @@ while($line = <>) {
 	} elsif ($line =~ /filter/) {
 	    chomp $line;
 	    print $line . $lnlbl_on_filter . "\n";
+	} elsif ($line =~ /locations/) {
+	    chomp $line;
+	    print $line . $lnlbl_on_locations . "\n";
 	} else {
 	    print $line;
 	}
@@ -87,6 +91,9 @@ while($line = <>) {
 	    if ($line =~ /filterlabel=([^\],]+)/) {
 		$lnlbl_on_filter = "//\\lnlbl\{$1\}";
 	    }
+	    if ($line =~ /locationslabel=([^\],]+)/) {
+		$lnlbl_on_locations = "//\\lnlbl\{$1\}";
+	    }
 	    $status = 3;
 	    next;
 	} else {
@@ -95,6 +102,11 @@ while($line = <>) {
 		s/\\lnlbl\[([^\]]*)\]/\\lnlbl\{$1\}/ ;
 		$line = $_ ;
 	    }
+	    if ($line =~ /\(\*\s*\\lnlbl\{[^\}]*\}\s*\*\)/) {
+		$_ = $line ;
+		s/\(\*\s*(\\lnlbl\{[^\}]*\})\s*\*\)/\/\/$1/ ;
+		$line = $_ ;
+	    }
 	    print $line ;
 	}
     } elsif ($status == 3) {
@@ -104,6 +116,9 @@ while($line = <>) {
 	} elsif ($line =~ /filter/) {
 	    chomp $line;
 	    print $line . $lnlbl_on_filter . "\n";
+	} elsif ($line =~ /locations/) {
+	    chomp $line;
+	    print $line . $lnlbl_on_locations . "\n";
 	} else {
 	    print $line ;
 	}
-- 
2.7.4

[PATCH 2/8] CodeSamples/formal: Add C-RCU-remove.litmus

[Akira Yokosawa]

From aafc555fe798bcf3c65d0092ca5c8b2d4f6880d3 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 31 Oct 2018 07:40:45 +0900
Subject: [PATCH 2/8] CodeSamples/formal: Add C-RCU-remove.litmus

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/formal/herd/C-RCU-remove.litmus | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 CodeSamples/formal/herd/C-RCU-remove.litmus

diff --git a/CodeSamples/formal/herd/C-RCU-remove.litmus b/CodeSamples/formal/herd/C-RCU-remove.litmus
new file mode 100644
index 0000000..0dc806e
--- /dev/null
+++ b/CodeSamples/formal/herd/C-RCU-remove.litmus
@@ -0,0 +1,27 @@
+C C-RCU-remove
+//\begin[snippet][labelbase=ln:formal:C-RCU-remove:whole,commandchars=\\\@\$]
+
+{
+	int *z=1; (* \lnlbl[tail:2] *)
+	int *y=2; (* \lnlbl[tail:1] *)
+	int *x=y; (* \lnlbl[head] *)
+}
+
+P0(int *x, int *y, int *z)		//\lnlbl[P0start]
+{
+	rcu_assign_pointer(*x, z);	//\lnlbl[assignnewtail]
+	synchronize_rcu();		//\lnlbl[sync]
+	WRITE_ONCE(*y, 0);		//\lnlbl[free]
+}					//\lnlbl[P0end]
+
+P1(int *x, int *y, int *z)		//\lnlbl[P1start]
+{
+	rcu_read_lock();		//\lnlbl[rl]
+	r1 = rcu_dereference(*x);	//\lnlbl[rderef]
+	r2 = READ_ONCE(*r1);		//\lnlbl[read]
+	rcu_read_unlock();		//\lnlbl[rul]
+}					//\lnlbl[P1end]
+
+//\end[snippet][locationslabel=locations_,existslabel=exists_]
+locations [0:r1; 1:r1; x; y; z]
+exists (1:r2=0)
-- 
2.7.4

[PATCH 3/8] CodeSamples/formal/herd: Add recipe for native .litmus tests

[Akira Yokosawa]

From 64a22b4d12c77d2a6332b39b82425276125d5f7d Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 31 Oct 2018 07:41:39 +0900
Subject: [PATCH 3/8] CodeSamples/formal/herd: Add recipe for native .litmus tests

Also update info on where the kernel memory model resides.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/formal/herd/Makefile | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

diff --git a/CodeSamples/formal/herd/Makefile b/CodeSamples/formal/herd/Makefile
index 3162659..05a8e6d 100644
--- a/CodeSamples/formal/herd/Makefile
+++ b/CodeSamples/formal/herd/Makefile
@@ -17,15 +17,16 @@
 #
 # 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.
+#       The memory model is available at tools/memory-model in
+#       the source tree of Linux kernel v4.17 (or later).
+#
 #       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
+# Copyright (C) Akira Yokosawa, 2017, 2018
 #
 # Authors: Akira Yokosawa <akiyks@gmail.com>
 
@@ -39,12 +40,15 @@ 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))
+HERD7_LITMUS   := $(wildcard *.litmus)
 TIMEOUT = 15m
 ITER    = 10
 ABSPERF_TEST   := $(wildcard C-SB+l-*.litmus)
 ABSPERF_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)
 ABSPERF_SHORT  := $(filter-out $(ABSPERF_LONG),$(ABSPERF_TEST))
 ABSPERF_OUT    = absperf.out absperf-all.out
+HERD7_TEST     := $(filter-out $(ABSPERF_TEST),$(HERD7_LITMUS))
+HERD7_OUT      := $(HERD7_TEST:%.litmus=%.out)
 
 .PHONY: all clean litmus2herd run-herd7 run-absperf run-absperf-all cross-klitmus
 .PHONY: help
@@ -56,25 +60,28 @@ litmus2herd: $(LITMUS7_HERD_TEST)
 $(LITMUS7_HERD_TEST): %.herd: ../litmus/%
 	sh ./litmus2herd.sh $< $@
 
-run-herd7: $(LITMUS7_HERD_OUT)
+run-herd7: $(LITMUS7_HERD_OUT) $(HERD7_OUT)
 run-absperf: absperf.out
 run-absperf-all: absperf-all.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 "### It is available at tools/memory-model in      ###"
+	@echo "### the source of Linux kernel v4.17 (or later).  ###"
 	@echo "###                                               ###"
 	@echo "### Refer to comment in Makefile for more info.   ###"
 	@echo "#####################################################"
 	@exit 1
 
-$(LITMUS7_HERD_OUT) $(ABSPERF_OUT): $(LKMM_LIST)
+$(LITMUS7_HERD_OUT) $(ABSPERF_OUT) $(HERD7_OUT): $(LKMM_LIST)
 
 $(LITMUS7_HERD_OUT): %.out: %.herd
 	cd $(LKMM_DIR); herd7 -conf linux-kernel.cfg $(HERD_DIR)/$< > $(HERD_DIR)/$@
 
+$(HERD7_OUT): %.out: %.litmus
+	cd $(LKMM_DIR); herd7 -conf linux-kernel.cfg $(HERD_DIR)/$< > $(HERD_DIR)/$@
+
 absperf.out: ABSPERF_LIST = $(ABSPERF_SHORT)
 absperf.out: $(ABSPERF_SHORT)
 absperf-all.out: ABSPERF_LIST = $(ABSPERF_TEST)
-- 
2.7.4

[PATCH 4/8] formal/axiomatic: Import snippet from C-RCU-remove.litmus

[Akira Yokosawa]

From f7553e5f74241123c3f2a850a870b892176056cf Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 31 Oct 2018 07:55:15 +0900
Subject: [PATCH 4/8] formal/axiomatic: Import snippet from C-RCU-remove.litmus

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/axiomatic.tex | 36 ++++--------------------------------
 1 file changed, 4 insertions(+), 32 deletions(-)

diff --git a/formal/axiomatic.tex b/formal/axiomatic.tex
index 41af129..8706635 100644
--- a/formal/axiomatic.tex
+++ b/formal/axiomatic.tex
@@ -235,40 +235,12 @@ And in this case, the \co{herd} tool's output features the string
 \label{sec:formal:Axiomatic Approaches and RCU}
 
 \begin{listing}[tb]
-\begin{linelabel}[ln:formal:Canonical RCU Removal Litmus Test]
-\begin{VerbatimL}[commandchars=\\\[\]]
-C C-RCU-remove
-
-{
-	int *z=1;\lnlbl[tail:2]
-	int *y=2;\lnlbl[tail:1]
-	int *x=y;\lnlbl[head]
-}
-
-P0(int *x, int *y, int *z)\lnlbl[P0start]
-{
-	rcu_assign_pointer(*x, z);\lnlbl[assignnewtail]
-	synchronize_rcu();\lnlbl[sync]
-	WRITE_ONCE(*y, 0);\lnlbl[free]
-}\lnlbl[P0end]
-
-P1(int *x, int *y, int *z)\lnlbl[P1start]
-{
-	rcu_read_lock();\lnlbl[rl]
-	r1 = rcu_dereference(*x);\lnlbl[rderef]
-	r2 = READ_ONCE(*r1);\lnlbl[read]
-	rcu_read_unlock();\lnlbl[rul]
-}\lnlbl[P1end]
-
-locations [0:r1; 1:r1; x; y; z]\lnlbl[locations]
-exists (1:r2=0)\lnlbl[exists]
-\end{VerbatimL}
-\end{linelabel}
+\input{CodeSamples/formal/herd/C-RCU-remove@whole.fcv}
 \caption{Canonical RCU Removal Litmus Test}
 \label{lst:formal:Canonical RCU Removal Litmus Test}
 \end{listing}
 
-\begin{lineref}[ln:formal:Canonical RCU Removal Litmus Test]
+\begin{lineref}[ln:formal:C-RCU-remove:whole]
 Axiomatic approaches can also analyze litmus tests involving RCU.
 To that end,
 Listing~\ref{lst:formal:Canonical RCU Removal Litmus Test}
@@ -289,9 +261,9 @@ executes within an RCU read-side critical section
 picking up the list head (line~\lnref{rderef}) and then
 loading the next element (line~\lnref{read}).
 The next element should be non-zero, that is, not yet freed
-(line~\lnref{exists}).
+(line~\lnref{exists_}).
 Several other variables are output for debugging purposes
-(line~\lnref{locations}).
+(line~\lnref{locations_}).
 
 The output of the \co{herd} tool when running this litmus test features
 \co{Never}, indicating that \co{P0()} never accesses a freed element,
-- 
2.7.4

[PATCH 5/8] CodeSamples/formal: Add C-RomanPenyanev-list-rcu-rr.litmus

[Akira Yokosawa]

From 37a1a26897a72e8cac8c5c1cc6e0982d76effd52 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 31 Oct 2018 08:34:35 +0900
Subject: [PATCH 5/8] CodeSamples/formal: Add C-RomanPenyanev-list-rcu-rr.litmus

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 .../formal/herd/C-RomanPenyaev-list-rcu-rr.litmus  | 47 ++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus

diff --git a/CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus b/CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus
new file mode 100644
index 0000000..bf88ee4
--- /dev/null
+++ b/CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus
@@ -0,0 +1,47 @@
+C C-RomanPenyaev-list-rcu-rr
+//\begin[snippet][labelbase=ln:formal:C-RomanPenyaev-list-rcu-rr:whole,commandchars=\%\@\$]
+
+{
+	int *z=1;			(* \lnlbl[listtail] *)
+	int *y=z;
+	int *x=y;
+	int *w=x;
+	int *v=w;			(* \lnlbl[listhead] *)
+	int *c=w;			(* \lnlbl[rrcache] *)
+}
+
+P0(int *c, int *v)			//\lnlbl[P0start]
+{
+	rcu_read_lock();		//\lnlbl[rl1]
+	r1 = READ_ONCE(*c);		//\lnlbl[rdcache]
+	if (r1 == 0) {			//\lnlbl[rdckcache]
+		r1 = READ_ONCE(*v);	//\lnlbl[rdinitcache]
+	}
+	r2 = rcu_dereference(*r1);	//\lnlbl[rdnext]
+	smp_store_release(c, r2);	//\lnlbl[rdupdcache]
+	rcu_read_unlock();		//\lnlbl[rul1]
+	rcu_read_lock();		//\lnlbl[rl2]
+	r3 = READ_ONCE(*c);
+	if (r3 == 0) {
+		r3 = READ_ONCE(*v);
+	}
+	r4 = rcu_dereference(*r3);
+	smp_store_release(c, r4);
+	rcu_read_unlock();		//\lnlbl[rul2]
+}					//\lnlbl[P0end]
+
+P1(int *c, int *v, int *w, int *x, int *y)//\lnlbl[P1start]
+{
+	rcu_assign_pointer(*w, y);	//\lnlbl[updremove]
+	synchronize_rcu();		//\lnlbl[updsync1]
+	r1 = READ_ONCE(*c);		//\lnlbl[updrdcache]
+	if (r1 == x) {			//\lnlbl[updckcache]
+		WRITE_ONCE(*c, 0);	//\lnlbl[updinitcache]
+		synchronize_rcu();	//\lnlbl[updsync2]
+	}
+	smp_store_release(x, 0);	//\lnlbl[updfree]
+}					//\lnlbl[P1end]
+
+//\end[snippet][locationslabel=locations_,existslabel=exists_]
+locations [0:r1; 1:r1; 1:r3; c; v; w; x; y]
+exists (0:r1=0 \/ 0:r2=0 \/ 0:r3=0 \/ 0:r4=0)
-- 
2.7.4

[PATCH 6/8] formal/axiomatic: Import snippet from C-RomanPenyanev-list-rcu-rr.litmus

[Akira Yokosawa]

From ec371f214cc26b5d3be12e2c8947964ac1b7be35 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 31 Oct 2018 08:35:19 +0900
Subject: [PATCH 6/8] formal/axiomatic: Import snippet from C-RomanPenyanev-list-rcu-rr.litmus

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/axiomatic.tex | 62 ++++++----------------------------------------------
 1 file changed, 7 insertions(+), 55 deletions(-)

diff --git a/formal/axiomatic.tex b/formal/axiomatic.tex
index 8706635..797b8f2 100644
--- a/formal/axiomatic.tex
+++ b/formal/axiomatic.tex
@@ -274,60 +274,12 @@ the \co{herd} output.
 \end{lineref}
 
 \begin{listing}[tb]
-\begin{linelabel}[ln:formal:Complex RCU Litmus Test]
-\begin{VerbatimL}[commandchars=\\\[\]]
-C C-RomanPenyaev-list-rcu-rr
-
-{
-	int *z=1;\lnlbl[listtail]
-	int *y=z;
-	int *x=y;
-	int *w=x;
-	int *v=w;\lnlbl[listhead]
-	int *c=w;\lnlbl[rrcache]
-}
-
-P0(int *c, int *v)\lnlbl[P0start]
-{
-	rcu_read_lock();\lnlbl[rl1]
-	r1 = READ_ONCE(*c);\lnlbl[rdcache]
-	if (r1 == 0) {\lnlbl[rdckcache]
-		r1 = READ_ONCE(*v);\lnlbl[rdinitcache]
-	}
-	r2 = rcu_dereference(*r1);\lnlbl[rdnext]
-	smp_store_release(c, r2);\lnlbl[rdupdcache]
-	rcu_read_unlock();\lnlbl[rul1]
-	rcu_read_lock();\lnlbl[rl2]
-	r3 = READ_ONCE(*c);
-	if (r3 == 0) {
-		r3 = READ_ONCE(*v);
-	}
-	r4 = rcu_dereference(*r3);
-	smp_store_release(c, r4);
-	rcu_read_unlock();\lnlbl[rul2]
-}\lnlbl[P0end]
-
-P1(int *c, int *v, int *w, int *x, int *y)\lnlbl[P1start]
-{
-	rcu_assign_pointer(*w, y);\lnlbl[updremove]
-	synchronize_rcu();\lnlbl[updsync1]
-	r1 = READ_ONCE(*c);\lnlbl[updrdcache]
-	if (r1 == x) {\lnlbl[updckcache]
-		WRITE_ONCE(*c, 0);\lnlbl[updinitcache]
-		synchronize_rcu();\lnlbl[updsync2]
-	}
-	smp_store_release(x, 0);\lnlbl[updfree]
-}\lnlbl[P1end]
-
-locations [0:r1; 1:r1; 1:r3; c; v; w; x; y]\lnlbl[locations]
-exists (0:r1=0 \/ 0:r2=0 \/ 0:r3=0 \/ 0:r4=0)\lnlbl[exists]
-\end{VerbatimL}
-\end{linelabel}
+\input{CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr@whole.fcv}
 \caption{Complex RCU Litmus Test}
 \label{lst:formal:Complex RCU Litmus Test}
 \end{listing}
 
-\begin{lineref}[ln:formal:Complex RCU Litmus Test]
+\begin{lineref}[ln:formal:C-RomanPenyaev-list-rcu-rr:whole]
 A litmus test for a more complex example proposed by
 Roman Penyaev~\cite{RomanPenyaev2018rrRCU} is shown in
 Figure~\ref{lst:formal:Complex RCU Litmus Test}.
@@ -374,7 +326,7 @@ registers \co{r3} and \co{r4} instead of \co{r1} and \co{r2}.
 As with
 Listing~\ref{lst:formal:Canonical RCU Removal Litmus Test},
 this litmus test stores zero to emulate \co{free()}, so
-line~\lnref{exists} checks for any of these four registers being
+line~\lnref{exists_} checks for any of these four registers being
 \co{NULL}, also known as zero.
 
 Because \co{P0()} leaks an RCU-protected pointer from its first
@@ -400,26 +352,26 @@ in the \co{herd} output.
 \end{lineref}
 
 \QuickQuiz{}
-	\begin{lineref}[ln:formal:Complex RCU Litmus Test]
+	\begin{lineref}[ln:formal:C-RomanPenyaev-list-rcu-rr:whole]
 	In Listing~\ref{lst:formal:Complex RCU Litmus Test},
 	why not have just one call to \co{synchronize_rcu()}
 	immediately before line~\lnref{updfree}?
 	\end{lineref}
 \QuickQuizAnswer{
-	\begin{lineref}[ln:formal:Complex RCU Litmus Test]
+	\begin{lineref}[ln:formal:C-RomanPenyaev-list-rcu-rr:whole]
 	Because this results in \co{P0()} accessing a freed element.
 	But don't take my word for this, try it out in \co{herd}!
 	\end{lineref}
 } \QuickQuizEnd
 
 \QuickQuiz{}
-	\begin{lineref}[ln:formal:Complex RCU Litmus Test]
+	\begin{lineref}[ln:formal:C-RomanPenyaev-list-rcu-rr:whole]
 	Also in Listing~\ref{lst:formal:Complex RCU Litmus Test},
 	can't line~\lnref{updfree} be \co{WRITE_ONCE} instead
 	of \co{smp_store_release(}?
 	\end{lineref}
 \QuickQuizAnswer{
-	\begin{lineref}[ln:formal:Complex RCU Litmus Test]
+	\begin{lineref}[ln:formal:C-RomanPenyaev-list-rcu-rr:whole]
 	That is an excellent question.
 	As of late 2018, the answer is ``no one knows''.
 	Much depends on the semantics of ARMv8's conditional-move
-- 
2.7.4

[PATCH 7/8] formal/axiomatic: Convert snippets of IRIW tests to new scheme

[Akira Yokosawa]

From a5c69acf48225773c83a5fab84e7aaaa0fae3664 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 31 Oct 2018 19:59:22 +0900
Subject: [PATCH 7/8] formal/axiomatic: Convert snippets of IRIW tests to new scheme

Also by reducing width of header comment, use "listing" env
instead of "listing*" env.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/axiomatic.tex | 101 +++++++++++++++++++++++++--------------------------
 1 file changed, 49 insertions(+), 52 deletions(-)

diff --git a/formal/axiomatic.tex b/formal/axiomatic.tex
index 797b8f2..a5f610d 100644
--- a/formal/axiomatic.tex
+++ b/formal/axiomatic.tex
@@ -7,32 +7,30 @@
 \epigraph{Theory helps us to bear our ignorance of facts.}
 	{\emph{George Santayana}}
 
-\begin{listing*}[tb]
-{ \scriptsize
-\begin{verbbox}
- 1 PPC IRIW.litmus
- 2 ""
- 3 (* Traditional IRIW. *)
- 4 {
- 5 0:r1=1; 0:r2=x;
- 6 1:r1=1;         1:r4=y;
- 7         2:r2=x; 2:r4=y;
- 8         3:r2=x; 3:r4=y;
- 9 }
-10 P0           | P1           | P2           | P3           ;
-11 stw r1,0(r2) | stw r1,0(r4) | lwz r3,0(r2) | lwz r3,0(r4) ;
-12              |              | sync         | sync         ;
-13              |              | lwz r5,0(r4) | lwz r5,0(r2) ;
-14 
-15 exists
-16 (2:r3=1 /\ 2:r5=0 /\ 3:r3=1 /\ 3:r5=0)
-\end{verbbox}
+\begin{listing}[tb]
+\begin{linelabel}[ln:formal:IRIW Litmus Test]
+\begin{VerbatimL}[commandchars=\%\@\$]
+PPC IRIW.litmus
+""
+(* Traditional IRIW. *)
+{
+0:r1=1; 0:r2=x;
+1:r1=1;         1:r4=y;
+        2:r2=x; 2:r4=y;
+        3:r2=x; 3:r4=y;
 }
-\centering
-\theverbbox
+P0           | P1           | P2           | P3           ;
+stw r1,0(r2) | stw r1,0(r4) | lwz r3,0(r2) | lwz r3,0(r4) ;
+             |              | sync         | sync         ;
+             |              | lwz r5,0(r4) | lwz r5,0(r2) ;
+
+exists
+(2:r3=1 /\ 2:r5=0 /\ 3:r3=1 /\ 3:r5=0)
+\end{VerbatimL}
+\end{linelabel}
 \caption{IRIW Litmus Test}
 \label{lst:formal:IRIW Litmus Test}
-\end{listing*}
+\end{listing}
 
 Although the PPCMEM tool can solve the famous ``independent reads of
 independent writes'' (IRIW) litmus test shown in
@@ -75,38 +73,37 @@ The resulting tool, called ``herd'',  conveniently takes as input the
 same litmus tests as PPCMEM, including the IRIW litmus test shown in
 Listing~\ref{lst:formal:IRIW Litmus Test}.
 
-\begin{listing*}[tb]
-{ \scriptsize
-\begin{verbbox}
- 1 PPC IRIW5.litmus
- 2 ""
- 3 (* Traditional IRIW, but with five stores instead of just one. *)
- 4 {
- 5 0:r1=1; 0:r2=x;
- 6 1:r1=1;         1:r4=y;
- 7         2:r2=x; 2:r4=y;
- 8         3:r2=x; 3:r4=y;
- 9 }
-10 P0           | P1           | P2           | P3           ;
-11 stw r1,0(r2) | stw r1,0(r4) | lwz r3,0(r2) | lwz r3,0(r4) ;
-12 addi r1,r1,1 | addi r1,r1,1 | sync         | sync         ;
-13 stw r1,0(r2) | stw r1,0(r4) | lwz r5,0(r4) | lwz r5,0(r2) ;
-14 addi r1,r1,1 | addi r1,r1,1 |              |              ;
-15 stw r1,0(r2) | stw r1,0(r4) |              |              ;
-16 addi r1,r1,1 | addi r1,r1,1 |              |              ;
-17 stw r1,0(r2) | stw r1,0(r4) |              |              ;
-18 addi r1,r1,1 | addi r1,r1,1 |              |              ;
-19 stw r1,0(r2) | stw r1,0(r4) |              |              ;
-20 
-21 exists
-22 (2:r3=1 /\ 2:r5=0 /\ 3:r3=1 /\ 3:r5=0)
-\end{verbbox}
+\begin{listing}[tb]
+\begin{linelabel}[ln:formal:Expanded IRIW Litmus Test]
+\begin{VerbatimL}[commandchars=\%\@\$]
+PPC IRIW5.litmus
+""
+(* Traditional IRIW, but with five stores instead of *)
+(* just one.                                         *)
+{
+0:r1=1; 0:r2=x;
+1:r1=1;         1:r4=y;
+        2:r2=x; 2:r4=y;
+        3:r2=x; 3:r4=y;
 }
-\centering
-\theverbbox
+P0           | P1           | P2           | P3           ;
+stw r1,0(r2) | stw r1,0(r4) | lwz r3,0(r2) | lwz r3,0(r4) ;
+addi r1,r1,1 | addi r1,r1,1 | sync         | sync         ;
+stw r1,0(r2) | stw r1,0(r4) | lwz r5,0(r4) | lwz r5,0(r2) ;
+addi r1,r1,1 | addi r1,r1,1 |              |              ;
+stw r1,0(r2) | stw r1,0(r4) |              |              ;
+addi r1,r1,1 | addi r1,r1,1 |              |              ;
+stw r1,0(r2) | stw r1,0(r4) |              |              ;
+addi r1,r1,1 | addi r1,r1,1 |              |              ;
+stw r1,0(r2) | stw r1,0(r4) |              |              ;
+
+exists
+(2:r3=1 /\ 2:r5=0 /\ 3:r3=1 /\ 3:r5=0)
+\end{VerbatimL}
+\end{linelabel}
 \caption{Expanded IRIW Litmus Test}
 \label{lst:formal:Expanded IRIW Litmus Test}
-\end{listing*}
+\end{listing}
 
 However, where PPCMEM requires 14 CPU hours to solve IRIW, herd does so
 in 17 milliseconds, which represents a speedup of more than six orders
-- 
2.7.4

[PATCH 8/8] formal/axiomatic: Fill in missing ')'

[Akira Yokosawa]

From 134f743e70db33fdbd1f822dd0b3b4548aedc95a Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 31 Oct 2018 20:15:23 +0900
Subject: [PATCH 8/8] formal/axiomatic: Fill in missing ')'

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/axiomatic.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/axiomatic.tex b/formal/axiomatic.tex
index a5f610d..992eb97 100644
--- a/formal/axiomatic.tex
+++ b/formal/axiomatic.tex
@@ -365,7 +365,7 @@ in the \co{herd} output.
 	\begin{lineref}[ln:formal:C-RomanPenyaev-list-rcu-rr:whole]
 	Also in Listing~\ref{lst:formal:Complex RCU Litmus Test},
 	can't line~\lnref{updfree} be \co{WRITE_ONCE} instead
-	of \co{smp_store_release(}?
+	of \co{smp_store_release()}?
 	\end{lineref}
 \QuickQuizAnswer{
 	\begin{lineref}[ln:formal:C-RomanPenyaev-list-rcu-rr:whole]
-- 
2.7.4

Re: [PATCH 0/8] Improve conversion of litmus test snippet

[Paul E. McKenney]

On Thu, Nov 01, 2018 at 12:08:02AM +0900, Akira Yokosawa wrote:
> Hi Paul,
> 
> In snippets of litmus tests you added recently uses "locations"
> directive. It was not covered by reorder_ltms.pl.
> This series enhances reorder_ltms.pl to add an option to
> the meta command "\end[snippet]".
> 
> Now you can put C-RCU-remove.litmus and
> C-RomanPenyanev-list-rcu-rr.litmus under CodeSamples/.
> 
> Patch #1 is the enhancement of reorder_ltms.pl.
> Patch #2 adds C-RCU-remove.litmus in CodeSamples/formal/herd.
> Note that I modified the choice of characters given to
> the "commandchars=" option to avoid collision with characters
> used in snippets.
> Patch #3 adds recipe in Makefile to run the added tests by
> "make run-herd7".
> Patch #4 replaces the inline snippet code with converted one.
> Patch #5 adds another RCU litmus test in CodeSamples/formal/herd.
> Patch #6 imports snippet converted from above.
> Patch #7 converts existing PPC IRIW litmus tests to new scheme
> It also reduces the width of the snippets to fit in 2c column
> width.
> Patch #8 is a trivial typo fix.
> 
> I'm afraid commit logs in this series is not descriptive
> enough, but hopefully the intention of the changes are evident.

They should do.  I queued these and pushed them, thank you!

						Thanx, Paul

>         Thanks, Akira
> -- 
> Akira Yokosawa (8):
>   reorder_ltms.pl: Add 'locationslabel=' option to \end[snippet]
>   CodeSamples/formal: Add C-RCU-remove.litmus
>   CodeSamples/formal/herd: Add recipe for native .litmus tests
>   formal/axiomatic: Import snippet from C-RCU-remove.litmus
>   CodeSamples/formal: Add C-RomanPenyanev-list-rcu-rr.litmus
>   formal/axiomatic: Import snippet from
>     C-RomanPenyanev-list-rcu-rr.litmus
>   formal/axiomatic: Convert snippets of IRIW tests to new scheme
>   formal/axiomatic: Fill in missing ')'
> 
>  CodeSamples/formal/herd/C-RCU-remove.litmus        |  27 +++
>  .../formal/herd/C-RomanPenyaev-list-rcu-rr.litmus  |  47 +++++
>  CodeSamples/formal/herd/Makefile                   |  21 ++-
>  formal/axiomatic.tex                               | 201 +++++++--------------
>  utilities/reorder_ltms.pl                          |  15 ++
>  5 files changed, 164 insertions(+), 147 deletions(-)
>  create mode 100644 CodeSamples/formal/herd/C-RCU-remove.litmus
>  create mode 100644 CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus
> 
> -- 
> 2.7.4
>