* [PATCH 1/4] formal: Make RCU litmus tests klitmus7 ready
2018-11-29 22:10 [PATCH 0/4] Update snippets of litmus tests Akira Yokosawa
@ 2018-11-29 22:11 ` Akira Yokosawa
2018-11-29 22:12 ` [PATCH 2/4] CodeSamples/formal/herd: Add recipe for klitmus7-ready tests Akira Yokosawa
` (3 subsequent siblings)
4 siblings, 0 replies; 6+ messages in thread
From: Akira Yokosawa @ 2018-11-29 22:11 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 6+ messages in thread* [PATCH 2/4] CodeSamples/formal/herd: Add recipe for klitmus7-ready tests
2018-11-29 22:10 [PATCH 0/4] Update snippets of litmus tests Akira Yokosawa
2018-11-29 22:11 ` [PATCH 1/4] formal: Make RCU litmus tests klitmus7 ready Akira Yokosawa
@ 2018-11-29 22:12 ` Akira Yokosawa
2018-11-29 22:14 ` [PATCH 3/4] Use '(* ... *)' style comments in epilogue of litmus tests Akira Yokosawa
` (2 subsequent siblings)
4 siblings, 0 replies; 6+ messages in thread
From: Akira Yokosawa @ 2018-11-29 22:12 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 6+ messages in thread* [PATCH 3/4] Use '(* ... *)' style comments in epilogue of litmus tests
2018-11-29 22:10 [PATCH 0/4] Update snippets of litmus tests Akira Yokosawa
2018-11-29 22:11 ` [PATCH 1/4] formal: Make RCU litmus tests klitmus7 ready Akira Yokosawa
2018-11-29 22:12 ` [PATCH 2/4] CodeSamples/formal/herd: Add recipe for klitmus7-ready tests Akira Yokosawa
@ 2018-11-29 22:14 ` Akira Yokosawa
2018-11-29 22:15 ` [PATCH 4/4] styleguide: Loosen restriction on comment in litmus test Akira Yokosawa
2018-11-30 0:22 ` [PATCH 0/4] Update snippets of litmus tests Paul E. McKenney
4 siblings, 0 replies; 6+ messages in thread
From: Akira Yokosawa @ 2018-11-29 22:14 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 6+ messages in thread* [PATCH 4/4] styleguide: Loosen restriction on comment in litmus test
2018-11-29 22:10 [PATCH 0/4] Update snippets of litmus tests Akira Yokosawa
` (2 preceding siblings ...)
2018-11-29 22:14 ` [PATCH 3/4] Use '(* ... *)' style comments in epilogue of litmus tests Akira Yokosawa
@ 2018-11-29 22:15 ` Akira Yokosawa
2018-11-30 0:22 ` [PATCH 0/4] Update snippets of litmus tests Paul E. McKenney
4 siblings, 0 replies; 6+ messages in thread
From: Akira Yokosawa @ 2018-11-29 22:15 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 6+ messages in thread* Re: [PATCH 0/4] Update snippets of litmus tests
2018-11-29 22:10 [PATCH 0/4] Update snippets of litmus tests Akira Yokosawa
` (3 preceding siblings ...)
2018-11-29 22:15 ` [PATCH 4/4] styleguide: Loosen restriction on comment in litmus test Akira Yokosawa
@ 2018-11-30 0:22 ` Paul E. McKenney
4 siblings, 0 replies; 6+ messages in thread
From: Paul E. McKenney @ 2018-11-30 0:22 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
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
>
^ permalink raw reply [flat|nested] 6+ messages in thread