[PATCH 0/4] Update snippets of litmus tests

[PATCH 0/4] Update snippets of litmus tests

[Akira Yokosawa]

From f07d05ca837a57e07f7a87bcbac2bf034905adab Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Fri, 30 Nov 2018 06:55:25 +0900
Subject: [PATCH 0/4] Update snippets of litmus tests

Hi Paul,

RCU litmus tests recently added in "formal" did not compile
by klitmus7. Patch #1 is my attempt to manage them klitmus7
ready.

Patch #2 add recipe for klitmus7-ready tests. Such tests need
to be manually added in a list.

In preparing Patch #3, I looked up your "litmus" repository
and found that comments on "exists" clause are actually allowed
in the form of "(* ... *)".  Patch #3 updates labels embedded
in litmus tests. Patch #4 updates styleguide accordingly.

        Thanks, Akira
--
Akira Yokosawa (4):
  formal: Make RCU litmus tests klitmus7 ready
  CodeSamples/formal/herd: Add recipe for klitmus7-ready tests
  Use '(* ... *)' style comments in epilogue of litmus tests
  styleguide: Loosen restriction on comment in litmus test

 CodeSamples/formal/herd/C-RCU-remove.litmus        | 18 +++++---
 .../formal/herd/C-RomanPenyaev-list-rcu-rr.litmus  | 28 ++++++++----
 .../formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus      |  4 +-
 CodeSamples/formal/herd/Makefile                   |  6 ++-
 appendix/styleguide/styleguide.tex                 | 25 ++++-------
 utilities/reorder_ltms.pl                          | 50 ++++++----------------
 6 files changed, 57 insertions(+), 74 deletions(-)

-- 
2.7.4

[PATCH 1/4] formal: Make RCU litmus tests klitmus7 ready

[Akira Yokosawa]

From cd34622c4250a6884b8b79c0f6a9b40eca4403a7 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 29 Nov 2018 20:39:43 +0900
Subject: [PATCH 1/4] formal: Make RCU litmus tests klitmus7 ready

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/formal/herd/C-RCU-remove.litmus        | 14 ++++++++-----
 .../formal/herd/C-RomanPenyaev-list-rcu-rr.litmus  | 24 ++++++++++++++++------
 2 files changed, 27 insertions(+), 11 deletions(-)

diff --git a/CodeSamples/formal/herd/C-RCU-remove.litmus b/CodeSamples/formal/herd/C-RCU-remove.litmus
index 0dc806e..6084f12 100644
--- a/CodeSamples/formal/herd/C-RCU-remove.litmus
+++ b/CodeSamples/formal/herd/C-RCU-remove.litmus
@@ -2,20 +2,24 @@ 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 z=1; (* \lnlbl[tail:2] *)
+	int y=2; (* \lnlbl[tail:1] *)
 	int *x=y; (* \lnlbl[head] *)
+	int * 1:r1; (* \fcvexclude *)
 }
 
-P0(int *x, int *y, int *z)		//\lnlbl[P0start]
+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]
+P1(int **x, int *y, int *z)		//\lnlbl[P1start]
 {
+	int *r1;
+	int r2;
+
 	rcu_read_lock();		//\lnlbl[rl]
 	r1 = rcu_dereference(*x);	//\lnlbl[rderef]
 	r2 = READ_ONCE(*r1);		//\lnlbl[read]
@@ -23,5 +27,5 @@ P1(int *x, int *y, int *z)		//\lnlbl[P1start]
 }					//\lnlbl[P1end]
 
 //\end[snippet][locationslabel=locations_,existslabel=exists_]
-locations [0:r1; 1:r1; x; y; z]
+locations [1:r1; x; y; z]
 exists (1:r2=0)
diff --git a/CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus b/CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus
index bf88ee4..f0080c1 100644
--- a/CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus
+++ b/CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus
@@ -8,16 +8,26 @@ C C-RomanPenyaev-list-rcu-rr
 	int *w=x;
 	int *v=w;			(* \lnlbl[listhead] *)
 	int *c=w;			(* \lnlbl[rrcache] *)
+	int * 0:r1;			(* \fcvexclude *)
+	int * 0:r2;			(* \fcvexclude *)
+	int * 0:r3;			(* \fcvexclude *)
+	int * 0:r4;			(* \fcvexclude *)
+	int * 1:r1;			(* \fcvexclude *)
 }
 
-P0(int *c, int *v)			//\lnlbl[P0start]
+P0(int **c, int **v)			//\lnlbl[P0start]
 {
+	int *r1;
+	int *r2;
+	int *r3;
+	int *r4;
+
 	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]
+	r2 = rcu_dereference(*(int **)r1);//\lnlbl[rdnext]
 	smp_store_release(c, r2);	//\lnlbl[rdupdcache]
 	rcu_read_unlock();		//\lnlbl[rul1]
 	rcu_read_lock();		//\lnlbl[rl2]
@@ -25,17 +35,19 @@ P0(int *c, int *v)			//\lnlbl[P0start]
 	if (r3 == 0) {
 		r3 = READ_ONCE(*v);
 	}
-	r4 = rcu_dereference(*r3);
+	r4 = rcu_dereference(*(int **)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]
+P1(int **c, int **v, int **w, int **x, int **y)//\lnlbl[P1start]
 {
+	int *r1;
+
 	rcu_assign_pointer(*w, y);	//\lnlbl[updremove]
 	synchronize_rcu();		//\lnlbl[updsync1]
 	r1 = READ_ONCE(*c);		//\lnlbl[updrdcache]
-	if (r1 == x) {			//\lnlbl[updckcache]
+	if ((int **)r1 == x) {		//\lnlbl[updckcache]
 		WRITE_ONCE(*c, 0);	//\lnlbl[updinitcache]
 		synchronize_rcu();	//\lnlbl[updsync2]
 	}
@@ -43,5 +55,5 @@ P1(int *c, int *v, int *w, int *x, int *y)//\lnlbl[P1start]
 }					//\lnlbl[P1end]
 
 //\end[snippet][locationslabel=locations_,existslabel=exists_]
-locations [0:r1; 1:r1; 1:r3; c; v; w; x; y]
+locations [1:r1; c; v; w; x; y]
 exists (0:r1=0 \/ 0:r2=0 \/ 0:r3=0 \/ 0:r4=0)
-- 
2.7.4

[PATCH 2/4] CodeSamples/formal/herd: Add recipe for klitmus7-ready tests

[Akira Yokosawa]

From 0d7dfde21ffe55289ade8c84385a3abbd3c7502b Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 29 Nov 2018 20:55:43 +0900
Subject: [PATCH 2/4] CodeSamples/formal/herd: Add recipe for klitmus7-ready tests

List such tests in KLITMUS_READY.

Those tests converted from ../litmus are klitmus7 ready from the
beginning.

Add "-rcu yes" option to klitmus7 to cover RCU tests.

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

diff --git a/CodeSamples/formal/herd/Makefile b/CodeSamples/formal/herd/Makefile
index 05a8e6d..e23148e 100644
--- a/CodeSamples/formal/herd/Makefile
+++ b/CodeSamples/formal/herd/Makefile
@@ -49,6 +49,8 @@ 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)
+KLITMUS_READY = C-RCU-remove C-RomanPenyaev-list-rcu-rr
+KLITMUS_TEST   := $(addsuffix .litmus,$(KLITMUS_READY))
 
 .PHONY: all clean litmus2herd run-herd7 run-absperf run-absperf-all cross-klitmus
 .PHONY: help
@@ -98,9 +100,9 @@ $(ABSPERF_OUT):
 
 cross-klitmus: klitmus.tar
 
-klitmus.tar: litmus2herd
+klitmus.tar: litmus2herd $(KLITMUS_TEST)
 	mkdir -p klitmus
-	klitmus7 -o klitmus $(LITMUS7_HERD_TEST)
+	klitmus7 -rcu yes -o klitmus $(LITMUS7_HERD_TEST) $(KLITMUS_TEST)
 	tar cf klitmus.tar ./klitmus
 
 help:
-- 
2.7.4

[PATCH 3/4] Use '(* ... *)' style comments in epilogue of litmus tests

[Akira Yokosawa]

From 71caf0c6be60746b61fa0b5384fd1485536fbcc5 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 29 Nov 2018 21:36:43 +0900
Subject: [PATCH 3/4] Use '(* ... *)' style comments in epilogue of litmus tests

It turned out that comments of this style are allowed in the
epilogue part of litmus tests.

Move labels in options to \end[snippet] meta commands to
comments on their respective lines.

Remove code supporting the options to the meta command in
reorder_ltms.pl.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/formal/herd/C-RCU-remove.litmus        |  6 +--
 .../formal/herd/C-RomanPenyaev-list-rcu-rr.litmus  |  6 +--
 .../formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus      |  4 +-
 utilities/reorder_ltms.pl                          | 50 ++++++----------------
 4 files changed, 20 insertions(+), 46 deletions(-)

diff --git a/CodeSamples/formal/herd/C-RCU-remove.litmus b/CodeSamples/formal/herd/C-RCU-remove.litmus
index 6084f12..33c410f 100644
--- a/CodeSamples/formal/herd/C-RCU-remove.litmus
+++ b/CodeSamples/formal/herd/C-RCU-remove.litmus
@@ -26,6 +26,6 @@ P1(int **x, int *y, int *z)		//\lnlbl[P1start]
 	rcu_read_unlock();		//\lnlbl[rul]
 }					//\lnlbl[P1end]
 
-//\end[snippet][locationslabel=locations_,existslabel=exists_]
-locations [1:r1; x; y; z]
-exists (1:r2=0)
+//\end[snippet]
+locations [1:r1; x; y; z]	(* \lnlbl[locations_] *)
+exists (1:r2=0)			(* \lnlbl[exists_] *)
diff --git a/CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus b/CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus
index f0080c1..1a197bd 100644
--- a/CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus
+++ b/CodeSamples/formal/herd/C-RomanPenyaev-list-rcu-rr.litmus
@@ -54,6 +54,6 @@ P1(int **c, int **v, int **w, int **x, int **y)//\lnlbl[P1start]
 	smp_store_release(x, 0);	//\lnlbl[updfree]
 }					//\lnlbl[P1end]
 
-//\end[snippet][locationslabel=locations_,existslabel=exists_]
-locations [1:r1; c; v; w; x; y]
-exists (0:r1=0 \/ 0:r2=0 \/ 0:r3=0 \/ 0:r4=0)
+//\end[snippet]
+locations [1:r1; c; v; w; x; y]			(* \lnlbl[locations_] *)
+exists (0:r1=0 \/ 0:r2=0 \/ 0:r3=0 \/ 0:r4=0)	(* \lnlbl[exists_] *)
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus
index 32d8e52..3e9e023 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus
@@ -26,6 +26,6 @@ P1(int *sl, int *x0, int *x1)
 	smp_store_release(sl, 0);
 }
 
-//\end[snippet][filterlabel=filter_]
-filter (0:r2=0 /\ 1:r2=0)
+//\end[snippet]
+filter (0:r2=0 /\ 1:r2=0)	(* \lnlbl[filter_] *)
 exists (0:r1=0 /\ 1:r1=0)
diff --git a/utilities/reorder_ltms.pl b/utilities/reorder_ltms.pl
index 9999c29..dda646b 100755
--- a/utilities/reorder_ltms.pl
+++ b/utilities/reorder_ltms.pl
@@ -45,26 +45,23 @@ my $edit_line;
 my $first_line;
 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
+		# 3: final line
 
 while($line = <>) {
     if (eof) {
-	if ($line =~ /exists/) {
-	    chomp $line;
-	    print $line . $lnlbl_on_exists . "\n";
-	} 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;
+	if ($line =~ /\\lnlbl\[[^\]]*\]/) {
+	    $_ = $line ;
+	    s/\\lnlbl\[([^\]]*)\]/\\lnlbl\{$1\}/ ;
+	    $line = $_ ;
 	}
+	if ($line =~ /\(\*\s*\\lnlbl\{[^\}]*\}\s*\*\)/) {
+	    $_ = $line ;
+	    s/\(\*\s*(\\lnlbl\{[^\}]*\})\s*\*\)/\/\/$1/ ;
+	    $line = $_ ;
+	}
+	print $line ;
+	$status = 3;
 	last;
     }
     if ($status == 0) {
@@ -85,16 +82,6 @@ while($line = <>) {
 	    $_ = $line ;
 	    s/\\end\[snippet\]/\\end\{snippet\}/ ;
 	    $end_command = $_ ;
-	    if ($line =~ /existslabel=([^\],]+)/) {
-		$lnlbl_on_exists = "//\\lnlbl\{$1\}";
-	    }
-	    if ($line =~ /filterlabel=([^\],]+)/) {
-		$lnlbl_on_filter = "//\\lnlbl\{$1\}";
-	    }
-	    if ($line =~ /locationslabel=([^\],]+)/) {
-		$lnlbl_on_locations = "//\\lnlbl\{$1\}";
-	    }
-	    $status = 3;
 	    next;
 	} else {
 	    if ($line =~ /\\lnlbl\[[^\]]*\]/) {
@@ -109,19 +96,6 @@ while($line = <>) {
 	    }
 	    print $line ;
 	}
-    } elsif ($status == 3) {
-	if ($line =~ /exists/) {
-	    chomp $line;
-	    print $line . $lnlbl_on_exists . "\n";
-	} 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 4/4] styleguide: Loosen restriction on comment in litmus test

[Akira Yokosawa]

From f07d05ca837a57e07f7a87bcbac2bf034905adab Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 29 Nov 2018 22:20:18 +0900
Subject: [PATCH 4/4] styleguide: Loosen restriction on comment in litmus test

Reflect the change in the labeling of epilogue part of litmus
tests.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 appendix/styleguide/styleguide.tex | 25 ++++++++-----------------
 1 file changed, 8 insertions(+), 17 deletions(-)

diff --git a/appendix/styleguide/styleguide.tex b/appendix/styleguide/styleguide.tex
index 3fe79ce..517424b 100644
--- a/appendix/styleguide/styleguide.tex
+++ b/appendix/styleguide/styleguide.tex
@@ -511,8 +511,8 @@ at the beginning of a litmus test.
 
 Similarly, several tokens such as \qco{exists}, \qco{filter},
 and~\qco{locations} indicate the end of litmus test's body.
-Once one of them appears in a litmus test, no comment is
-allowed to appear thereafter.  Those tokens keep the same meaning
+Once one of them appears in a litmus test, comments should be
+ocaml style (\qco{(* ... *)}). Those tokens keep the same meaning
 even when they appear in comments!
 
 The pair of characters \qco{\{} and \qco{\}} also have special
@@ -520,7 +520,7 @@ meaning in the C flavour tests. They are used to seperate portions
 in a litmus test.
 
 First pair of \qco{\{} and \qco{\}} encloses initialization part.
-Comments in this part should be of the form \qco{(* ... *)}.
+Comments in this part should also be in the ocaml form.
 
 You can't use \qco{\{} and \qco{\}} in comments in litmus tests, either.
 
@@ -544,7 +544,7 @@ P0(int *x}
 
 [...]
 
-exists (0:r1=0)  // comment after test body
+exists (0:r1=0)  // C++ style comment after test body
 \end{VerbatimN}
 \end{linelabel}
 
@@ -576,20 +576,11 @@ P1(int *x0, int *x1)
 	r2 = READ_ONCE(*x0);
 }
 
-//\end[snippet][existslabel=exists_]
-exists (1:r2=0 /\ 0:r2=0)
+//\end[snippet]
+exists (1:r2=0 /\ 0:r2=0)  (* \lnlbl[exists_] *)
 \end{VerbatimN}
 \end{linelabel}
 
-To support labeling lines after the test body, \co{\\end[snippet]}
-can have following options:
-
-\begin{VerbatimU}
-exsitslabel=<label of exists>
-filterlabel=<label of filter>
-locationslabel=<label of locations>
-\end{VerbatimU}
-
 Example above is converted to the following intermediate code
 by a script \path{utilities/reorder_ltms.pl}.\footnote{
 	Currently, only C flavour litmus tests are supported.
@@ -624,8 +615,8 @@ P1(int *x0, int *x1)
 	r2 = READ_ONCE(*x0);
 }
 
-exists (1:r2=0 /\ 0:r2=0)\lnlbl{exists_}
-//\end{snippet}[existslabel=exists_]
+exists (1:r2=0 /\ 0:r2=0)  \lnlbl{exists_}
+//\end{snippet}
 \end{VerbatimN}
 \end{linelabel}
 
-- 
2.7.4

Re: [PATCH 0/4] Update snippets of litmus tests

[Paul E. McKenney]

On Fri, Nov 30, 2018 at 07:10:15AM +0900, Akira Yokosawa wrote:
> >From f07d05ca837a57e07f7a87bcbac2bf034905adab Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Fri, 30 Nov 2018 06:55:25 +0900
> Subject: [PATCH 0/4] Update snippets of litmus tests
> 
> Hi Paul,
> 
> RCU litmus tests recently added in "formal" did not compile
> by klitmus7. Patch #1 is my attempt to manage them klitmus7
> ready.
> 
> Patch #2 add recipe for klitmus7-ready tests. Such tests need
> to be manually added in a list.
> 
> In preparing Patch #3, I looked up your "litmus" repository
> and found that comments on "exists" clause are actually allowed
> in the form of "(* ... *)".  Patch #3 updates labels embedded
> in litmus tests. Patch #4 updates styleguide accordingly.
> 
>         Thanks, Akira

Queued and pushed, thank you!

And yes, I sometimes use existing litmus tests as reference manuals.

							Thanx, Paul

> --
> Akira Yokosawa (4):
>   formal: Make RCU litmus tests klitmus7 ready
>   CodeSamples/formal/herd: Add recipe for klitmus7-ready tests
>   Use '(* ... *)' style comments in epilogue of litmus tests
>   styleguide: Loosen restriction on comment in litmus test
> 
>  CodeSamples/formal/herd/C-RCU-remove.litmus        | 18 +++++---
>  .../formal/herd/C-RomanPenyaev-list-rcu-rr.litmus  | 28 ++++++++----
>  .../formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus      |  4 +-
>  CodeSamples/formal/herd/Makefile                   |  6 ++-
>  appendix/styleguide/styleguide.tex                 | 25 ++++-------
>  utilities/reorder_ltms.pl                          | 50 ++++++----------------
>  6 files changed, 57 insertions(+), 74 deletions(-)
> 
> -- 
> 2.7.4
>