* [PATCH 1/8] reorder_ltms.pl: Add 'locationslabel=' option to \end[snippet]
2018-10-31 15:08 [PATCH 0/8] Improve conversion of litmus test snippet Akira Yokosawa
@ 2018-10-31 15:09 ` Akira Yokosawa
2018-10-31 15:10 ` [PATCH 2/8] CodeSamples/formal: Add C-RCU-remove.litmus Akira Yokosawa
` (7 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Akira Yokosawa @ 2018-10-31 15:09 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 10+ messages in thread* [PATCH 2/8] CodeSamples/formal: Add C-RCU-remove.litmus
2018-10-31 15:08 [PATCH 0/8] Improve conversion of litmus test snippet Akira Yokosawa
2018-10-31 15:09 ` [PATCH 1/8] reorder_ltms.pl: Add 'locationslabel=' option to \end[snippet] Akira Yokosawa
@ 2018-10-31 15:10 ` Akira Yokosawa
2018-10-31 15:12 ` [PATCH 3/8] CodeSamples/formal/herd: Add recipe for native .litmus tests Akira Yokosawa
` (6 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Akira Yokosawa @ 2018-10-31 15:10 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 10+ messages in thread* [PATCH 3/8] CodeSamples/formal/herd: Add recipe for native .litmus tests
2018-10-31 15:08 [PATCH 0/8] Improve conversion of litmus test snippet Akira Yokosawa
2018-10-31 15:09 ` [PATCH 1/8] reorder_ltms.pl: Add 'locationslabel=' option to \end[snippet] Akira Yokosawa
2018-10-31 15:10 ` [PATCH 2/8] CodeSamples/formal: Add C-RCU-remove.litmus Akira Yokosawa
@ 2018-10-31 15:12 ` Akira Yokosawa
2018-10-31 15:13 ` [PATCH 4/8] formal/axiomatic: Import snippet from C-RCU-remove.litmus Akira Yokosawa
` (5 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Akira Yokosawa @ 2018-10-31 15:12 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 10+ messages in thread* [PATCH 4/8] formal/axiomatic: Import snippet from C-RCU-remove.litmus
2018-10-31 15:08 [PATCH 0/8] Improve conversion of litmus test snippet Akira Yokosawa
` (2 preceding siblings ...)
2018-10-31 15:12 ` [PATCH 3/8] CodeSamples/formal/herd: Add recipe for native .litmus tests Akira Yokosawa
@ 2018-10-31 15:13 ` Akira Yokosawa
2018-10-31 15:13 ` [PATCH 5/8] CodeSamples/formal: Add C-RomanPenyanev-list-rcu-rr.litmus Akira Yokosawa
` (4 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Akira Yokosawa @ 2018-10-31 15:13 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 10+ messages in thread* [PATCH 5/8] CodeSamples/formal: Add C-RomanPenyanev-list-rcu-rr.litmus
2018-10-31 15:08 [PATCH 0/8] Improve conversion of litmus test snippet Akira Yokosawa
` (3 preceding siblings ...)
2018-10-31 15:13 ` [PATCH 4/8] formal/axiomatic: Import snippet from C-RCU-remove.litmus Akira Yokosawa
@ 2018-10-31 15:13 ` Akira Yokosawa
2018-10-31 15:14 ` [PATCH 6/8] formal/axiomatic: Import snippet from C-RomanPenyanev-list-rcu-rr.litmus Akira Yokosawa
` (3 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Akira Yokosawa @ 2018-10-31 15:13 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 10+ messages in thread* [PATCH 6/8] formal/axiomatic: Import snippet from C-RomanPenyanev-list-rcu-rr.litmus
2018-10-31 15:08 [PATCH 0/8] Improve conversion of litmus test snippet Akira Yokosawa
` (4 preceding siblings ...)
2018-10-31 15:13 ` [PATCH 5/8] CodeSamples/formal: Add C-RomanPenyanev-list-rcu-rr.litmus Akira Yokosawa
@ 2018-10-31 15:14 ` Akira Yokosawa
2018-10-31 15:15 ` [PATCH 7/8] formal/axiomatic: Convert snippets of IRIW tests to new scheme Akira Yokosawa
` (2 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Akira Yokosawa @ 2018-10-31 15:14 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 10+ messages in thread* [PATCH 7/8] formal/axiomatic: Convert snippets of IRIW tests to new scheme
2018-10-31 15:08 [PATCH 0/8] Improve conversion of litmus test snippet Akira Yokosawa
` (5 preceding siblings ...)
2018-10-31 15:14 ` [PATCH 6/8] formal/axiomatic: Import snippet from C-RomanPenyanev-list-rcu-rr.litmus Akira Yokosawa
@ 2018-10-31 15:15 ` Akira Yokosawa
2018-10-31 15:16 ` [PATCH 8/8] formal/axiomatic: Fill in missing ')' Akira Yokosawa
2018-10-31 16:28 ` [PATCH 0/8] Improve conversion of litmus test snippet Paul E. McKenney
8 siblings, 0 replies; 10+ messages in thread
From: Akira Yokosawa @ 2018-10-31 15:15 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 10+ messages in thread* [PATCH 8/8] formal/axiomatic: Fill in missing ')'
2018-10-31 15:08 [PATCH 0/8] Improve conversion of litmus test snippet Akira Yokosawa
` (6 preceding siblings ...)
2018-10-31 15:15 ` [PATCH 7/8] formal/axiomatic: Convert snippets of IRIW tests to new scheme Akira Yokosawa
@ 2018-10-31 15:16 ` Akira Yokosawa
2018-10-31 16:28 ` [PATCH 0/8] Improve conversion of litmus test snippet Paul E. McKenney
8 siblings, 0 replies; 10+ messages in thread
From: Akira Yokosawa @ 2018-10-31 15:16 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 10+ messages in thread* Re: [PATCH 0/8] Improve conversion of litmus test snippet
2018-10-31 15:08 [PATCH 0/8] Improve conversion of litmus test snippet Akira Yokosawa
` (7 preceding siblings ...)
2018-10-31 15:16 ` [PATCH 8/8] formal/axiomatic: Fill in missing ')' Akira Yokosawa
@ 2018-10-31 16:28 ` Paul E. McKenney
8 siblings, 0 replies; 10+ messages in thread
From: Paul E. McKenney @ 2018-10-31 16:28 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
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
>
^ permalink raw reply [flat|nested] 10+ messages in thread