Discussions of the Parallel Programming book
 help / color / mirror / Atom feed
* [PATCH 0/9] Update code snippet extraction scheme
@ 2018-09-23  7:21 Akira Yokosawa
  2018-09-23  7:22 ` [PATCH 1/9] fcvextract.pl: Use 'linelabel' env in extracted snippet Akira Yokosawa
                   ` (9 more replies)
  0 siblings, 10 replies; 11+ messages in thread
From: Akira Yokosawa @ 2018-09-23  7:21 UTC (permalink / raw)
  To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa

From df6459c699d373a247342b3a79d3bf7a239cfbe3 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sun, 23 Sep 2018 09:16:20 +0900
Subject: [PATCH 0/9] Update code snippet extraction scheme

Hi Paul,

This patch set updates scripts to extract code snippet from
source files under CodeSamples/.

Patch #1 fixes fcvextract.pl to use "linelabel" environment in
extracted .fcv files.

Patches #2 through #5 add capability to handle code snippets
other than C. Patch #2 is a simple update with a bug fix to
handle source files under deep sub-directories. 

One major obstacle was the restriction of comments in .litmus
files.

    1) We can't add comments at the beginning nor the end of
       a litmus test.
    2) There are a few tokens and characters we can't use in
       comments, i.e. "exists" or "filter" as a token in
       comment is not accepted by herd7, "{" and "}" characters
       sometimes cause error, comments of the form "(*" -- "*)"
       are not allowed in the C-language part of litmus test.

I ended up using comments of the form "//...", which has been
supported by herdtools7.

Patches #3 and #4 work around the restriction.

Patch #5 prevents a side-effect of doing "make" under
CodeSamples/formal/herd, which will convert litmus tests under
CodeSamples/formal/litmus so that they can be fed into herd7,
and cause the converted tests to have redundant
"\begin[snippet]" meta commands.

Patch #6 adds an option "style=" to the meta command
\begin{snippet}, which can be used to specify which of
Verbetim{L/N/U} is to be emitted. It also adds pass-through
handling of other options.

Patch #7 is not an update to the scripts, but a tweak in
appearance of VerbatimN and VerbatimU environments so that
inline snippets will have frames around them. 

Patches #8 and #9 are examples of actually extracting snippets
from .sh and .litmus files.

Effect of patch #7 can be seen in Section 4.1 (below the 1st
paragraph) and in Section 4.2.1 (above Quick Quiz 4.6) after
applying the whole patch set.  If you don't like the change,
feel free to omit #7.

By this update, hopefully, the new scheme should be able to
cover 99 percent of snippets. Although the scripts lack
rigorous checks of unexpected inputs.

        Thanks, Akira

Akira Yokosawa (9):
  fcvextract.pl: Use 'linelabel' env in extracted snippet
  Update build scripts to support code snippets other than 'C'
  Add scripts and recipes to work around restriction of herdtools7
  reorder_ltms.pl: Enable further labeling in litmus test snippet
  Exclude meta command lines in .litmus -> .litmus.herd conversion
  fcvextract.pl: Support 'style=' option and pass through other options
  Enable 'single' frame around inline code snippets
  toolsoftrade: Example of extraction of snippet from parallel.sh
  future/formalregress: Example of extraction of snippet from .litmus
    file

 .gitignore                                         |   1 +
 .../formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus      |   2 +
 CodeSamples/formal/herd/litmus2herd.sh             |   4 +-
 CodeSamples/toolsoftrade/parallel.sh               |  20 ++--
 Makefile                                           |  19 +++-
 future/formalregress.tex                           |  40 +------
 perfbook.tex                                       |   7 +-
 toolsoftrade/toolsoftrade.tex                      |  12 +--
 utilities/fcvextract.pl                            |  74 ++++++++++---
 utilities/gen_snippet_d.pl                         |  66 +++++++++++-
 utilities/reorder_ltms.pl                          | 117 +++++++++++++++++++++
 11 files changed, 281 insertions(+), 81 deletions(-)
 create mode 100755 utilities/reorder_ltms.pl

-- 
2.7.4


^ permalink raw reply	[flat|nested] 11+ messages in thread

* [PATCH 1/9] fcvextract.pl: Use 'linelabel' env in extracted snippet
  2018-09-23  7:21 [PATCH 0/9] Update code snippet extraction scheme Akira Yokosawa
@ 2018-09-23  7:22 ` Akira Yokosawa
  2018-09-23  7:24 ` [PATCH 2/9] Update build scripts to support code snippets other than 'C' Akira Yokosawa
                   ` (8 subsequent siblings)
  9 siblings, 0 replies; 11+ messages in thread
From: Akira Yokosawa @ 2018-09-23  7:22 UTC (permalink / raw)
  To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa

From 48dcad932a43762eab4f5f7b8d7845428136d612 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 29 Aug 2018 20:43:57 +0900
Subject: [PATCH 1/9] fcvextract.pl: Use 'linelabel' env in extracted snippet

For consistency with commit 6bf7a51b7b9d ("Add 'linelabel' and
'lineref' environment"), enclose "VerbatimL" env in "linelabel" env
in extracted code snippet.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 utilities/fcvextract.pl | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/utilities/fcvextract.pl b/utilities/fcvextract.pl
index 8c6025a..cba96e7 100755
--- a/utilities/fcvextract.pl
+++ b/utilities/fcvextract.pl
@@ -42,7 +42,7 @@
 # Verbatim environment of fancyvrb package):
 #
 # ---
-# \renewcommand{\lnlblbase}{ln:toolsoftrade:api-pthreads:waitall}
+# \begin{linelabel}[ln:toolsoftrade:api-pthreads:waitall]
 # \begin{VerbatimL}[commandchars=\%\[\]]
 # 	int pid;
 # 	int status;
@@ -57,6 +57,7 @@
 # 		}
 # 	}%lnlbl[loopb]
 # \end{VerbatimL}
+# \end{linelabel}
 # ---
 #
 # <snippet identifier> corresponds to a meta command embedded in
@@ -78,12 +79,12 @@
 # This script converts the \lnlbl{} commands with these charcters
 # reverse-converted.
 #
-# To make the actual labels to have the full form of:
+# To make the actual labels to have the full form of
 #
 #     "ln:<chapter>:<file name>:<function>:<line label>"
 #
-# in LaTeX processing, this script will generate a \renewcommand{}
-# command as shown above. The macro is used within \lnlbl{} command.
+# in LaTeX processing, this script will enclose the snippet with
+# a pair of \begin{linelabel} and \end{linelabel} as shown above.
 #
 # To omit a line in extracted snippet, put "\fcvexclude" in comment
 # on the line.
@@ -142,7 +143,7 @@ while($line = <>) {
 	print "% Do not edit!\n" ;
 	print "% Generated by utilities/fcvextract.pl.\n" ;
 	if ($line =~ /labelbase=([^,]+)/) {
-	    print "\\renewcommand\{\\lnlblbase\}\{$1\}\n" ;
+	    print "\\begin\{linelabel}\[$1\]\n" ;
 	}
 	print "\\begin\{VerbatimL\}" ;
 	if ($line =~ /commandchars=([^,]+).*\]$/) {
@@ -161,7 +162,7 @@ while($line = <>) {
     }
 }
 if ($extracting == 2) {
-    print "\\end\{VerbatimL\}\n" ;
+    print "\\end\{VerbatimL\}\n\\end\{linelabel\}\n" ;
     exit 0;
 } else {
     exit 1;
-- 
2.7.4



^ permalink raw reply related	[flat|nested] 11+ messages in thread

* [PATCH 2/9] Update build scripts to support code snippets other than 'C'
  2018-09-23  7:21 [PATCH 0/9] Update code snippet extraction scheme Akira Yokosawa
  2018-09-23  7:22 ` [PATCH 1/9] fcvextract.pl: Use 'linelabel' env in extracted snippet Akira Yokosawa
@ 2018-09-23  7:24 ` Akira Yokosawa
  2018-09-23  7:26 ` [PATCH 3/9] Add scripts and recipes to work around restriction of herdtools7 Akira Yokosawa
                   ` (7 subsequent siblings)
  9 siblings, 0 replies; 11+ messages in thread
From: Akira Yokosawa @ 2018-09-23  7:24 UTC (permalink / raw)
  To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa

From be808a5ec45f657689dab384e026011aa6b496df Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 29 Aug 2018 20:48:42 +0900
Subject: [PATCH 2/9] Update build scripts to support code snippets other than 'C'

Add code to fcvextract.pl to switch regex depending on the suffix
of source file. Supported suffixes are ".c", ".h", ".sh", ".spin",
and ".litmus".

Also fix gen_snippet_d.pl so that it works when a source file under
a deep sub-directory is specified.

Some of the <file name> part specified in the 2nd arg to fcvextract.pl
requires escaping. Specifically, "+" characters e.g. in "C-SB+o-o+o-o"
need escapes and should be specified as "C-SB\\+o-o\\+o-o" in the
argument. This escaping can be most easily done in Makefile by
using the $(subst ...) function.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 Makefile                   |  2 +-
 utilities/fcvextract.pl    | 26 ++++++++++++++++++++------
 utilities/gen_snippet_d.pl |  5 ++---
 3 files changed, 23 insertions(+), 10 deletions(-)

diff --git a/Makefile b/Makefile
index a88553b..588274a 100644
--- a/Makefile
+++ b/Makefile
@@ -264,7 +264,7 @@ CodeSamples/snippets.d: $(SOURCES_OF_SNIPPET) $(GEN_SNIPPET_D)
 
 $(FCVSNIPPETS):
 	@echo "$< --> $@"
-	@utilities/fcvextract.pl $< $(subst @,:,$(basename $(notdir $@))) > $@
+	utilities/fcvextract.pl $< $(subst +,\\+,$(subst @,:,$(basename $(notdir $@)))) > $@
 
 help:
 	@echo "Official targets (Latin Modern Typewriter for monospace font):"
diff --git a/utilities/fcvextract.pl b/utilities/fcvextract.pl
index cba96e7..740d358 100755
--- a/utilities/fcvextract.pl
+++ b/utilities/fcvextract.pl
@@ -96,6 +96,8 @@
 use strict;
 use warnings;
 
+my $src_file;
+my $lnlbl_re;
 my $line;
 my $edit_line;
 my $extract_labelbase;
@@ -111,13 +113,25 @@ my $file_name;
 my $func_name;
 my $label;
 
+$src_file = $ARGV[0];
 $extract_labelbase = $ARGV[1];
 
-$begin_re = '\\\begin\\{snippet\\}.*labelbase=[^,\\]]*' . $extract_labelbase . '[,\\]]' ;
-$end_re = '\\\end\\{snippet\\}';
+$begin_re = qr/\\begin\{snippet\}.*labelbase=[^,\]]*$extract_labelbase[,\]]/ ;
+$end_re = qr/\\end\{snippet\}/;
 
-#print $begin_re;
-#print "\n";
+if ($src_file =~ /.*\.h$/ ) {
+    $lnlbl_re = qr!(.*?)(\s*//\s*)\\lnlbl\{(.*)}\s*$!;
+} elsif ($src_file =~ /.*\.c$/ ) {
+    $lnlbl_re = qr!(.*?)(\s*//\s*)\\lnlbl\{(.*)}\s*$!;
+} elsif ($src_file =~ /.*\.spin$/ ) {
+    $lnlbl_re = qr!(.*?)(\s*//\s*)\\lnlbl\{(.*)}\s*$!;
+} elsif ($src_file =~ /.*\.sh$/ ) {
+    $lnlbl_re = qr!(.*?)(\s*#\s*)\\lnlbl\{(.*)}\s*$!;
+} elsif ($src_file =~ /.\.litmus$/ ) {
+    $lnlbl_re = qr!(.*?)(\s*\(\*\s*)\\lnlbl\{(.*)}\s*\*\)\s*$!;
+} else {
+    die ("unkown file suffix!");
+}
 
 while($line = <>) {
     if ($line =~ /$begin_re/) {
@@ -132,7 +146,7 @@ while($line = <>) {
 	}
 	if ($line =~ /\\fcvexclude/) {
 	    # skip this line
-	} elsif ($line =~ m!(.*?)(\s*//\s*)\\lnlbl\{(.*)}\s*$!) {
+	} elsif ($line =~ m!$lnlbl_re!) {
 	    $edit_line = $1 . $esc_bsl . "lnlbl" . $esc_open . $3 . $esc_close ;
 	    print $edit_line . "\n" ;
 	} else {
@@ -146,7 +160,7 @@ while($line = <>) {
 	    print "\\begin\{linelabel}\[$1\]\n" ;
 	}
 	print "\\begin\{VerbatimL\}" ;
-	if ($line =~ /commandchars=([^,]+).*\]$/) {
+	if ($line =~ /commandchars=([^,]+).*\]/) {
 	    $esc_char = $1 ;
 	    print "\[commandchars=" . $esc_char . "\]\n" ;
 	    $esc_bsl = substr $esc_char, 1, 1;
diff --git a/utilities/gen_snippet_d.pl b/utilities/gen_snippet_d.pl
index 55c1378..4de733a 100755
--- a/utilities/gen_snippet_d.pl
+++ b/utilities/gen_snippet_d.pl
@@ -15,7 +15,6 @@ use warnings;
 my @fcvsources;
 my $snippet_key;
 my $source;
-my $src_under_sub;
 
 $snippet_key = '\\begin\{snippet\}' ;
 @fcvsources = `grep -l -r -F $snippet_key CodeSamples` ;
@@ -30,13 +29,13 @@ foreach $source (@fcvsources) {
     my $snippet ;
     @snippet_commands1 = `grep -F $snippet_key $source` ;
     chomp @snippet_commands1 ;
-    $source =~ m!.*/([^/]+)/[^/]+! ;
+    $source =~ m!(.*/[^/]+)/[^/]+! ;
     $subdir = $1 ;
     foreach $snippet (@snippet_commands1) {
 	$snippet =~ /labelbase=.*:(.+:[^,\]]+)[,\]]/ ;
 	$_ = $1;
 	s/:/@/g ;
-	print "\\\n\tCodeSamples/$subdir/$_.fcv ";
+	print "\\\n\t$subdir/$_.fcv ";
     }
 }
 
-- 
2.7.4



^ permalink raw reply related	[flat|nested] 11+ messages in thread

* [PATCH 3/9] Add scripts and recipes to work around restriction of herdtools7
  2018-09-23  7:21 [PATCH 0/9] Update code snippet extraction scheme Akira Yokosawa
  2018-09-23  7:22 ` [PATCH 1/9] fcvextract.pl: Use 'linelabel' env in extracted snippet Akira Yokosawa
  2018-09-23  7:24 ` [PATCH 2/9] Update build scripts to support code snippets other than 'C' Akira Yokosawa
@ 2018-09-23  7:26 ` Akira Yokosawa
  2018-09-23  7:27 ` [PATCH 4/9] reorder_ltms.pl: Enable further labeling in litmus test snippet Akira Yokosawa
                   ` (6 subsequent siblings)
  9 siblings, 0 replies; 11+ messages in thread
From: Akira Yokosawa @ 2018-09-23  7:26 UTC (permalink / raw)
  To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa

From 124383d885da4117c390fd220d00a70231e7cc79 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 29 Aug 2018 20:55:38 +0900
Subject: [PATCH 3/9] Add scripts and recipes to work around restriction of herdtools7

It turned out that .litmus files do not have so much freedom
in placement of comments, and what words can appear in comments.

To work around the restriction, we need to add another route to
generate VerbatimL LaTeX sources (.fcv) from litmus tests (.litmus).

    .litmus -> .ltms
    .ltms   -> .fcv

In .litmus, we place a meta command to start a code snippet below
the line of "C foo-bar", which needs to be the first line in .litmus
file.

Also, as the "filter" and "exists" clause don't permit any comments
following the, we place a meta command to end a code snippet ahead
of the line of "exists" or "filter" clause.
And "{" and "}" in these meta commands sometimes cause error depending
on their positions. So we use the form of:

    \begin[snippet][option] -- \end[snippet]

in .litmus files.

For consistency, \lnlbl commands should be of the form of \lnlbl[bar].

NOTE:
    Comments of the form  "(* ... *)"  can not appear in C-language
    parts of litmus tests. The form of "//\lnlbl{bar}" is OK in
    C-language parts.

The reordering of these meta commands is handled by the new
script, utilities/reorder_ltms.pl. It also takes care of
"[" and "]" characters.

In summary, .litmus source should look like the following:

------------------------------------------------
C C-foo-bar
//\begin[snippet][labelbase=foo:bar,...]

{
}

[...]

    smp_mb(); //\lnlbl[fullbarrier]

[...]
}

//\end[snippet]
exists (1:r2=0 /\ 0:r2=0)
------------------------------------------------

This will result in a .ltms file:

------------------------------------------------
//\begin{snippet}[labelbase=foo:bar,...]
C C+foo-bar

{
}

[...]

    smp_mb(); //\lnlbl{fullbarrier}

[...]
}

exists (1:r2=0 /\ 0:r2=0)
//\end{snippet}
--- --- --- --- --- --- --- --- --- --- --- ---

.ltms -> .fcv conversion can be handled by the updated fcvextract.pl.

gen_snippet_d.pl and Makefile are updated accordingly.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 .gitignore                 |  1 +
 Makefile                   | 17 +++++++--
 utilities/fcvextract.pl    |  4 +-
 utilities/gen_snippet_d.pl | 61 +++++++++++++++++++++++++++++-
 utilities/reorder_ltms.pl  | 92 ++++++++++++++++++++++++++++++++++++++++++++++
 5 files changed, 169 insertions(+), 6 deletions(-)
 create mode 100755 utilities/reorder_ltms.pl

diff --git a/.gitignore b/.gitignore
index dde8523..1a40230 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,6 +18,7 @@
 *.epsi
 *.svgi
 *.fcv
+*.ltms
 perfbook_flat.tex
 qqz.tex
 contrib.tex
diff --git a/Makefile b/Makefile
index 588274a..72865d7 100644
--- a/Makefile
+++ b/Makefile
@@ -83,7 +83,10 @@ A2PING_GSCNFL := 0
 endif
 endif
 
-SOURCES_OF_SNIPPET := $(shell grep -r -l -F '\begin{snippet}' CodeSamples)
+SOURCES_OF_SNIPPET_ALL := $(shell grep -r -l -F '\begin{snippet}' CodeSamples)
+SOURCES_OF_LITMUS      := $(shell grep -r -l -F '\begin[snippet]' CodeSamples)
+SOURCES_OF_LTMS        := $(patsubst %.litmus,&.ltms,$(SOURCES_OF_LITMUS))
+SOURCES_OF_SNIPPET     := $(filter-out $(SOURCES_OF_LTMS),$(SOURCES_OF_SNIPPET_ALL)) $(SOURCES_OF_LITMUS)
 GEN_SNIPPET_D  = utilities/gen_snippet_d.pl utilities/gen_snippet_d.sh
 
 default = $(PERFBOOK_DEFAULT)
@@ -126,7 +129,7 @@ $(PDFTARGETS:.pdf=.aux): $(LATEXGENERATED) $(LATEXSOURCES)
 autodate.tex: perfbook.tex $(LATEXSOURCES) $(BIBSOURCES) $(SVGSOURCES) $(FIGSOURCES) $(DOTSOURCES) $(EPSORIGIN) $(SOURCES_OF_SNIPPET) utilities/fcvextract.pl
 	sh utilities/autodate.sh >autodate.tex
 
-perfbook_flat.tex: autodate.tex $(PDFTARGETS_OF_EPS) $(TARGETS_OF_SVG) $(FCVSNIPPETS)
+perfbook_flat.tex: autodate.tex $(PDFTARGETS_OF_EPS) $(TARGETS_OF_SVG) $(FCVSNIPPETS) $(FCVSNIPPETS_VIA_LTMS)
 ifndef LATEXPAND
 	$(error --> $@: latexpand not found. Please install it)
 endif
@@ -266,6 +269,14 @@ $(FCVSNIPPETS):
 	@echo "$< --> $@"
 	utilities/fcvextract.pl $< $(subst +,\\+,$(subst @,:,$(basename $(notdir $@)))) > $@
 
+$(FCVSNIPPETS_VIA_LTMS):
+	@echo "$< --> $@"
+	utilities/fcvextract.pl $< $(subst +,\\+,$(subst @,:,$(basename $(notdir $@)))) > $@
+
+$(FCVSNIPPETS_LTMS):
+	@echo "$< --> $@"
+	utilities/reorder_ltms.pl $< > $@
+
 help:
 	@echo "Official targets (Latin Modern Typewriter for monospace font):"
 	@echo "  Full,              Abbr."
@@ -296,7 +307,7 @@ clean:
 	find . -name '*.aux' -o -name '*.blg' \
 		-o -name '*.dvi' -o -name '*.log' \
 		-o -name '*.qqz' -o -name '*.toc' -o -name '*.bbl' \
-		-o -name '*.fcv' | xargs rm -f
+		-o -name '*.fcv' -o -name '*.ltms' | xargs rm -f
 	rm -f perfbook_flat.tex perfbook*.out perfbook-*.tex
 	rm -f $(LATEXGENERATED)
 	rm -f $(SVG_LARGE_BITMAP:%.svg=%.pdf) $(PNGTARGETS_OF_SVG)
diff --git a/utilities/fcvextract.pl b/utilities/fcvextract.pl
index 740d358..cb6869b 100755
--- a/utilities/fcvextract.pl
+++ b/utilities/fcvextract.pl
@@ -127,8 +127,8 @@ if ($src_file =~ /.*\.h$/ ) {
     $lnlbl_re = qr!(.*?)(\s*//\s*)\\lnlbl\{(.*)}\s*$!;
 } elsif ($src_file =~ /.*\.sh$/ ) {
     $lnlbl_re = qr!(.*?)(\s*#\s*)\\lnlbl\{(.*)}\s*$!;
-} elsif ($src_file =~ /.\.litmus$/ ) {
-    $lnlbl_re = qr!(.*?)(\s*\(\*\s*)\\lnlbl\{(.*)}\s*\*\)\s*$!;
+} elsif ($src_file =~ /.\.ltms$/ ) {
+    $lnlbl_re = qr!(.*?)(\s*//\s*)\\lnlbl\{(.*)}\s*$!;
 } else {
     die ("unkown file suffix!");
 }
diff --git a/utilities/gen_snippet_d.pl b/utilities/gen_snippet_d.pl
index 4de733a..d8e3bc7 100755
--- a/utilities/gen_snippet_d.pl
+++ b/utilities/gen_snippet_d.pl
@@ -13,12 +13,17 @@ use strict;
 use warnings;
 
 my @fcvsources;
+my @fcvsources_ltms;
 my $snippet_key;
+my $snippet_key_ltms;
 my $source;
 
 $snippet_key = '\\begin\{snippet\}' ;
+$snippet_key_ltms = '\\begin\[snippet\]' ;
 @fcvsources = `grep -l -r -F $snippet_key CodeSamples` ;
+@fcvsources_ltms = `grep -l -r -F $snippet_key_ltms CodeSamples` ;
 chomp @fcvsources ;
+chomp @fcvsources_ltms ;
 
 print "# Do not edit!\n" ;
 print "# Generated by utilities/gen_snippet_d.pl.\n\n" ;
@@ -27,6 +32,9 @@ foreach $source (@fcvsources) {
     my @snippet_commands1 ;
     my $subdir ;
     my $snippet ;
+    if ($source =~ /\.ltms$/) {
+	next;
+    }
     @snippet_commands1 = `grep -F $snippet_key $source` ;
     chomp @snippet_commands1 ;
     $source =~ m!(.*/[^/]+)/[^/]+! ;
@@ -38,14 +46,40 @@ foreach $source (@fcvsources) {
 	print "\\\n\t$subdir/$_.fcv ";
     }
 }
+print "\nFCVSNIPPETS_VIA_LTMS = " ;
+foreach $source (@fcvsources_ltms) {
+    my @snippet_commands1 ;
+    my $subdir ;
+    my $snippet ;
+    @snippet_commands1 = `grep -F $snippet_key_ltms $source` ;
+    chomp @snippet_commands1 ;
+    $source =~ m!(.*/[^/]+)/[^/]+! ;
+    $subdir = $1 ;
+    foreach $snippet (@snippet_commands1) {
+	$snippet =~ /labelbase=.*:(.+:[^,\]]+)[,\]]/ ;
+	$_ = $1;
+	s/:/@/g ;
+	print "\\\n\t$subdir/$_.fcv ";
+    }
+}
+print "\nFCVSNIPPETS_LTMS = " ;
+foreach $source (@fcvsources_ltms) {
+    $_ = $source ;
+    s/\.litmus$/\.ltms/ ;
+    print "\\\n\t$_";
+}
 
-print "\n\nEXTRACT = utilities/fcvextract.pl\n\n" ;
+print "\n\nEXTRACT = utilities/fcvextract.pl\n" ;
+print "REORDER_LTMS = utilities/reorder_ltms.pl\n\n" ;
 
 foreach $source (@fcvsources) {
     my @snippet_commands2 ;
     my $src_under_sub ;
     my $subdir ;
     my $snippet ;
+    if ($source =~ /\.ltms$/) {
+	next;
+    }
     @snippet_commands2 = `grep -F $snippet_key $source` ;
     chomp @snippet_commands2 ;
     $src_under_sub = $source ;
@@ -62,3 +96,28 @@ foreach $source (@fcvsources) {
 	print "$subdir/$_.fcv: $src_under_sub \$\(EXTRACT\)\n";
     }
 }
+foreach $source (@fcvsources_ltms) {
+    my @snippet_commands2 ;
+    my $src_under_sub ;
+    my $subdir ;
+    my $snippet ;
+    @snippet_commands2 = `grep -F $snippet_key_ltms $source` ;
+    chomp @snippet_commands2 ;
+    $src_under_sub = $source ;
+    $source =~ m!(.*/[^/]+)/[^/]+! ;
+    $subdir = $1 ;
+#    print @snippet_commands ;
+    foreach $snippet (@snippet_commands2) {
+	$_ = $src_under_sub ;
+	s/\.litmus$// ;
+	$src_under_sub = $_ ;
+	print "$src_under_sub.ltms: $src_under_sub.litmus \$\(REORDER_LTMS\)\n" ;
+	$snippet =~ /labelbase=.*:(.+:[^,\]]+)[,\]]/ ;
+	if (not defined $1) {
+	    die("Oops! Please try \"make clean; make\".\n") ;
+	}
+	$_ = $1;
+	s/:/@/g ;
+	print "$subdir/$_.fcv: $src_under_sub.ltms \$\(EXTRACT\)\n";
+    }
+}
diff --git a/utilities/reorder_ltms.pl b/utilities/reorder_ltms.pl
new file mode 100755
index 0000000..72d061b
--- /dev/null
+++ b/utilities/reorder_ltms.pl
@@ -0,0 +1,92 @@
+#!/usr/bin/perl
+# SPDX-License-Identifier: GPL-2.0-or-later
+#
+# Reorder meta command lines in .litmus source to work around
+# restrictions of herdtools7 where comments can be placed.
+#
+# .litmus files need to have "C foo-bar" at the very beginning.
+# They need to have an "exists" clause as the final line.
+#
+# Also, "{" and "}" in comments sometimes cause error depending
+# on their position. So we use "[" and "]" in .litmus files.
+#
+# Example:
+# Input
+# ------------------------------------------------------------
+# C C-foo-bar
+# //\begin[snippet][labelbase=ln:foo-bar,commandchars=\%\[\]]
+# [...]
+#     r1 = READ_ONCE(*x0);    //\lnlbl[read]
+# [...]
+# //\end[snippet]
+# exists (0:r1=0 /\ 1:r1=0)
+# ------------------------------------------------------------
+# Output
+# ------------------------------------------------------------
+# //\begin{snippet}[labelbase=ln:foo-bar,commandchars=\%\[\]]
+# C C-foo
+# [...]
+#     r1 = READ_ONCE(*x0);    //\lnlbl{read}
+# [...]
+# exists (0:r1=0 /\ 1:r1=0)
+# //\end{snippet}
+# ------------------------------------------------------------
+#
+# Copyright (C) Akira Yokosawa, 2018
+#
+# Authors: Akira Yokosawa <akiyks@gmail.com>
+
+use strict;
+use warnings;
+
+my $src_file = $ARGV[0];
+my $line;
+my $edit_line;
+my $first_line;
+my $end_command;
+my $lnlbl_command;
+my $status = 0;	# 0: just started, 1: first_line read; 2: begin line output,
+		# 3: end line read
+
+while($line = <>) {
+    if (eof) {
+	last;
+    }
+    if ($status == 0) {
+	$first_line = $line;
+	$status = 1;
+	print "// Do not edit!\n// Generated by utillities/reorder_ltms.pl\n";
+	next;
+    } elsif ($status == 1) {
+	$_ = $line;
+	s/\\begin\[snippet\]/\\begin\{snippet\}/;
+	$edit_line = $_ ;
+	print $edit_line ;
+	print $first_line ;
+	$status = 2;
+	next;
+    } elsif ($status == 2) {
+	if ($line =~ /\\end\[snippet\]/) {
+	    $_ = $line ;
+	    s/\\end\[snippet\]/\\end\{snippet\}/ ;
+	    $end_command = $_ ;
+	    $status = 3;
+	    next;
+	} else {
+	    if ($line =~ /\\lnlbl\[[^\]]*\]/) {
+		$_ = $line ;
+		s/\\lnlbl\[([^\]]*)\]/\\lnlbl\{$1\}/ ;
+		$line = $_ ;
+	    }
+	    print $line ;
+	}
+    } elsif ($status == 3) {
+	print $line ;
+    }
+}
+
+if ($status == 3) {
+    print $end_command;
+} else {
+    die ("Oops, something went wrong!");
+}
-- 
2.7.4



^ permalink raw reply related	[flat|nested] 11+ messages in thread

* [PATCH 4/9] reorder_ltms.pl: Enable further labeling in litmus test snippet
  2018-09-23  7:21 [PATCH 0/9] Update code snippet extraction scheme Akira Yokosawa
                   ` (2 preceding siblings ...)
  2018-09-23  7:26 ` [PATCH 3/9] Add scripts and recipes to work around restriction of herdtools7 Akira Yokosawa
@ 2018-09-23  7:27 ` Akira Yokosawa
  2018-09-23  7:29 ` [PATCH 5/9] Exclude meta command lines in .litmus -> .litmus.herd conversion Akira Yokosawa
                   ` (5 subsequent siblings)
  9 siblings, 0 replies; 11+ messages in thread
From: Akira Yokosawa @ 2018-09-23  7:27 UTC (permalink / raw)
  To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa

From 92a662ee9c74b45f3495784dc46587cd633603e3 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 29 Aug 2018 21:05:39 +0900
Subject: [PATCH 4/9] reorder_ltms.pl: Enable further labeling in litmus test snippet

In .litmus files, lines of "filter" and "exists" clauses can't
have their own comments to put labels.
To overcome this restriction, we add options "existslabel=foo"
and "filterlabel=bar" to the \end[snippet] meta command.

To put a label to an exists clause, you can put the label in
the form:

    ...
    \end[snippet][existslabel=foo]
    exists (1:r2=0 /\ 0:r2=0)
    [EOF]

This will be converted to:

    ...
    exists (1:r2=0 /\ 0:r2=0)\lnlbl{foo}
    \end{snippet}
    [EOF]

in .ltms file.

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

diff --git a/utilities/reorder_ltms.pl b/utilities/reorder_ltms.pl
index 72d061b..d4770d0 100755
--- a/utilities/reorder_ltms.pl
+++ b/utilities/reorder_ltms.pl
@@ -45,11 +45,22 @@ my $edit_line;
 my $first_line;
 my $end_command;
 my $lnlbl_command;
+my $lnlbl_on_exists = "";
+my $lnlbl_on_filter = "";
 my $status = 0;	# 0: just started, 1: first_line read; 2: begin line output,
 		# 3: end line read
 
 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";
+	} else {
+	    print $line;
+	}
 	last;
     }
     if ($status == 0) {
@@ -70,6 +81,12 @@ 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\}";
+	    }
 	    $status = 3;
 	    next;
 	} else {
@@ -81,7 +98,15 @@ while($line = <>) {
 	    print $line ;
 	}
     } elsif ($status == 3) {
-	print $line ;
+	if ($line =~ /exists/) {
+	    chomp $line;
+	    print $line . $lnlbl_on_exists . "\n";
+	} elsif ($line =~ /filter/) {
+	    chomp $line;
+	    print $line . $lnlbl_on_filter . "\n";
+	} else {
+	    print $line ;
+	}
     }
 }
 
-- 
2.7.4



^ permalink raw reply related	[flat|nested] 11+ messages in thread

* [PATCH 5/9] Exclude meta command lines in .litmus -> .litmus.herd conversion
  2018-09-23  7:21 [PATCH 0/9] Update code snippet extraction scheme Akira Yokosawa
                   ` (3 preceding siblings ...)
  2018-09-23  7:27 ` [PATCH 4/9] reorder_ltms.pl: Enable further labeling in litmus test snippet Akira Yokosawa
@ 2018-09-23  7:29 ` Akira Yokosawa
  2018-09-23  7:30 ` [PATCH 6/9] fcvextract.pl: Support 'style=' option and pass through other options Akira Yokosawa
                   ` (4 subsequent siblings)
  9 siblings, 0 replies; 11+ messages in thread
From: Akira Yokosawa @ 2018-09-23  7:29 UTC (permalink / raw)
  To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa

From cc8805ea5c2a65f60789adff102c64135bac1343 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 29 Aug 2018 21:15:54 +0900
Subject: [PATCH 5/9] Exclude meta command lines in .litmus -> .litmus.herd conversion

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/formal/herd/litmus2herd.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/CodeSamples/formal/herd/litmus2herd.sh b/CodeSamples/formal/herd/litmus2herd.sh
index ebcd01b..c1a69bc 100644
--- a/CodeSamples/formal/herd/litmus2herd.sh
+++ b/CodeSamples/formal/herd/litmus2herd.sh
@@ -17,4 +17,6 @@
 
 grep -n -A1 -B1 "api.h" $1 | \
 sed -n 's/^\([0-9]\{1,\}\).*/\1d/p' | \
-sed -f - $1 > $2
+sed -f - $1 | \
+sed -e '/\\begin\[snippet\]/d' | \
+sed -e '/\\end\[snippet\]/d' > $2
-- 
2.7.4



^ permalink raw reply related	[flat|nested] 11+ messages in thread

* [PATCH 6/9] fcvextract.pl: Support 'style=' option and pass through other options
  2018-09-23  7:21 [PATCH 0/9] Update code snippet extraction scheme Akira Yokosawa
                   ` (4 preceding siblings ...)
  2018-09-23  7:29 ` [PATCH 5/9] Exclude meta command lines in .litmus -> .litmus.herd conversion Akira Yokosawa
@ 2018-09-23  7:30 ` Akira Yokosawa
  2018-09-23  7:31 ` [PATCH 7/9] Enable 'single' frame around inline code snippets Akira Yokosawa
                   ` (3 subsequent siblings)
  9 siblings, 0 replies; 11+ messages in thread
From: Akira Yokosawa @ 2018-09-23  7:30 UTC (permalink / raw)
  To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa

From 4c276d2dc2b2d056354c3d21d6b9a0f857c36631 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 29 Aug 2018 21:16:42 +0900
Subject: [PATCH 6/9] fcvextract.pl: Support 'style=' option and pass through other options

"style=N" option will generate a "VerbatimN" environment.
"style=U" option will generate a "VerbatimU" environment.
Default is the "VerbatimL" environment.
Other options to a \begin{snippet} meta command are passed through
as options to "VerbatimL/N/U" environment.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 utilities/fcvextract.pl | 37 +++++++++++++++++++++++++++++++++----
 1 file changed, 33 insertions(+), 4 deletions(-)

diff --git a/utilities/fcvextract.pl b/utilities/fcvextract.pl
index cb6869b..ce549d3 100755
--- a/utilities/fcvextract.pl
+++ b/utilities/fcvextract.pl
@@ -112,6 +112,8 @@ my $dir_name;
 my $file_name;
 my $func_name;
 my $label;
+my $env_name = "VerbatimL" ;
+my $other_opts;
 
 $src_file = $ARGV[0];
 $extract_labelbase = $ARGV[1];
@@ -158,25 +160,52 @@ while($line = <>) {
 	print "% Generated by utilities/fcvextract.pl.\n" ;
 	if ($line =~ /labelbase=([^,]+)/) {
 	    print "\\begin\{linelabel}\[$1\]\n" ;
+	    $_ = $line ;
+	    s/labelbase=[^,\]]+,?// ;
+	    $line = $_ ;
 	}
-	print "\\begin\{VerbatimL\}" ;
+	if ($line =~ /style=N[,\]]/) {
+	    $env_name = "VerbatimN" ;
+	    $_ = $line ;
+	    s/style=N,?// ;
+	    $line = $_ ;
+	} elsif ($line =~ /style=U[,\]]/) {
+	    $env_name = "VerbatimU" ;
+	    $_ = $line ;
+	    s/style=U,?// ;
+	    $line = $_ ;
+	}
+	print "\\begin\{$env_name\}" ;
+
 	if ($line =~ /commandchars=([^,]+).*\]/) {
 	    $esc_char = $1 ;
-	    print "\[commandchars=" . $esc_char . "\]\n" ;
+	    print "\[commandchars=" . $esc_char ;
 	    $esc_bsl = substr $esc_char, 1, 1;
 	    $esc_open = substr $esc_char, 3, 1;
 	    $esc_close = substr $esc_char, 5, 1;
+	    $_ = $line ;
+	    s/commandchars=.{6},?// ;
+	    $line = $_ ;
 	} else {
 	    $esc_bsl = "\\" ;
 	    $esc_open = "\{" ;
 	    $esc_close = "\}" ;
-	    print "\n" ;
+	}
+	if ($line =~ /\[(.*)\]$/) {
+	    $_ = $1 ;
+	    s/,$// ;
+	    $other_opts = $_ ;
+	}
+	if ($other_opts ne '') {
+	    print ",$other_opts\]\n";
+	} else {
+	    print "\]\n";
 	}
 	$extracting = 2;
     }
 }
 if ($extracting == 2) {
-    print "\\end\{VerbatimL\}\n\\end\{linelabel\}\n" ;
+    print "\\end\{$env_name\}\n\\end\{linelabel\}\n" ;
     exit 0;
 } else {
     exit 1;
-- 
2.7.4



^ permalink raw reply related	[flat|nested] 11+ messages in thread

* [PATCH 7/9] Enable 'single' frame around inline code snippets
  2018-09-23  7:21 [PATCH 0/9] Update code snippet extraction scheme Akira Yokosawa
                   ` (5 preceding siblings ...)
  2018-09-23  7:30 ` [PATCH 6/9] fcvextract.pl: Support 'style=' option and pass through other options Akira Yokosawa
@ 2018-09-23  7:31 ` Akira Yokosawa
  2018-09-23  7:32 ` [PATCH 8/9] toolsoftrade: Example of extraction of snippet from parallel.sh Akira Yokosawa
                   ` (2 subsequent siblings)
  9 siblings, 0 replies; 11+ messages in thread
From: Akira Yokosawa @ 2018-09-23  7:31 UTC (permalink / raw)
  To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa

From b69a5a8bcb76b49c5f1f30ba31d7280a67c0b87d Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 30 Aug 2018 23:01:03 +0900
Subject: [PATCH 7/9] Enable 'single' frame around inline code snippets

Inline code snippets can have frames by modifying the definitions
of VerbatimN and VerbatimU environments.

Definition of \lnlbl{} command for VerbatimN needs tweaks to
raise the position of anchor a bit to compensate extra vertical
space around frame.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 perfbook.tex | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/perfbook.tex b/perfbook.tex
index 1dc72c2..3547f64 100644
--- a/perfbook.tex
+++ b/perfbook.tex
@@ -117,9 +117,9 @@
 {fontsize=\scriptsize,numbers=left,numbersep=5pt,xleftmargin=9pt,obeytabs=true,tabsize=2}
 \AfterEndEnvironment{VerbatimL}{\vspace*{-9pt}}
 \DefineVerbatimEnvironment{VerbatimN}{Verbatim}%
-{fontsize=\scriptsize,numbers=left,numbersep=5pt,xleftmargin=25pt,obeytabs=true,tabsize=2}
+{fontsize=\scriptsize,numbers=left,numbersep=3pt,xleftmargin=5pt,xrightmargin=5pt,obeytabs=true,tabsize=2,frame=single}
 \DefineVerbatimEnvironment{VerbatimU}{Verbatim}%
-{fontsize=\scriptsize,numbers=none,xleftmargin=15pt,obeytabs=true,tabsize=2,samepage=true}
+{fontsize=\scriptsize,numbers=none,xleftmargin=5pt,xrightmargin=5pt,obeytabs=true,tabsize=2,samepage=true,frame=single}
 
 \IfLmttForCode{
 \AtBeginEnvironment{verbatim}{\renewcommand{\ttdefault}{lmtt}}
@@ -242,6 +242,9 @@
 %\fvset{fontsize=\scriptsize,numbers=left,numbersep=5pt,xleftmargin=9pt,obeytabs=true,tabsize=2}
 \newcommand{\lnlblbase}{}
 \newcommand{\lnlbl}[1]{\phantomsection\label{\lnlblbase:#1}}
+\AtBeginEnvironment{VerbatimN}{%
+\renewcommand{\lnlbl}[1]{\raisebox{6pt}{\phantomsection\label{\lnlblbase:#1}}}%
+}
 \newcommand{\lnrefbase}{}
 \newcommand{\lnref}[1]{\ref{\lnrefbase:#1}}
 
-- 
2.7.4



^ permalink raw reply related	[flat|nested] 11+ messages in thread

* [PATCH 8/9] toolsoftrade: Example of extraction of snippet from parallel.sh
  2018-09-23  7:21 [PATCH 0/9] Update code snippet extraction scheme Akira Yokosawa
                   ` (6 preceding siblings ...)
  2018-09-23  7:31 ` [PATCH 7/9] Enable 'single' frame around inline code snippets Akira Yokosawa
@ 2018-09-23  7:32 ` Akira Yokosawa
  2018-09-23  7:34 ` [PATCH 9/9] future/formalregress: Example of extraction of snippet from .litmus file Akira Yokosawa
  2018-09-23 21:44 ` [PATCH 0/9] Update code snippet extraction scheme Paul E. McKenney
  9 siblings, 0 replies; 11+ messages in thread
From: Akira Yokosawa @ 2018-09-23  7:32 UTC (permalink / raw)
  To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa

From 0165c8b80522c46743850978e2756da2190a12ec Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 30 Aug 2018 22:40:40 +0900
Subject: [PATCH 8/9] toolsoftrade: Example of extraction of snippet from parallel.sh

This is a POC of extraction from a .sh file.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/toolsoftrade/parallel.sh | 20 +++++++++++---------
 toolsoftrade/toolsoftrade.tex        | 12 ++----------
 2 files changed, 13 insertions(+), 19 deletions(-)

diff --git a/CodeSamples/toolsoftrade/parallel.sh b/CodeSamples/toolsoftrade/parallel.sh
index 6b87a2a..760dda6 100644
--- a/CodeSamples/toolsoftrade/parallel.sh
+++ b/CodeSamples/toolsoftrade/parallel.sh
@@ -26,15 +26,17 @@ function compute_it {
 	sleep 5
 }
 
-echo Computing in parallel starting at `date`
-compute_it 1 > compute_it.1.out &
-compute_it 2 > compute_it.2.out &
-wait
-echo Computing in parallel finished at `date`
-echo Computation \"output\":
-cat compute_it.1.out
-cat compute_it.2.out
-rm compute_it.1.out compute_it.2.out
+# \begin{snippet}[labelbase=ln:toolsoftrade:parallel:compute_it,commandchars=\\\{\},style=N]
+echo Computing in parallel starting at `date`	#\fcvexclude
+compute_it 1 > compute_it.1.out &		#\lnlbl{comp1}
+compute_it 2 > compute_it.2.out &		#\lnlbl{comp2}
+wait						#\lnlbl{wait}
+echo Computing in parallel finished at `date`	#\fcvexclude
+echo Computation \"output\":			#\fcvexclude
+cat compute_it.1.out				#\lnlbl{cat1}
+cat compute_it.2.out				#\lnlbl{cat2}
+rm compute_it.1.out compute_it.2.out		#\fcvexclude
+# \end{snippet}
 
 echo
 echo Computing sequentially starting at `date`
diff --git a/toolsoftrade/toolsoftrade.tex b/toolsoftrade/toolsoftrade.tex
index ece92f1..d21bda0 100644
--- a/toolsoftrade/toolsoftrade.tex
+++ b/toolsoftrade/toolsoftrade.tex
@@ -42,15 +42,7 @@ For example, suppose that you had a program \co{compute_it}
 that you needed to run twice with two different sets of arguments.
 This can be accomplished using UNIX shell scripting as follows:
 
-\begin{linelabel}[ln:toolsoftrade:jobcontrol:script]
-\begin{VerbatimN}[commandchars=\\\{\}]
-compute_it 1 > compute_it.1.out & \lnlbl{comp1}
-compute_it 2 > compute_it.2.out & \lnlbl{comp2}
-wait \lnlbl{wait}
-cat compute_it.1.out \lnlbl{cat1}
-cat compute_it.2.out \lnlbl{cat2}
-\end{VerbatimN}
-\end{linelabel}
+\input{CodeSamples/toolsoftrade/parallel@compute_it.fcv}
 
 \begin{figure}[tb]
 \centering
@@ -59,7 +51,7 @@ cat compute_it.2.out \lnlbl{cat2}
 \label{fig:toolsoftrade:Execution Diagram for Parallel Shell Execution}
 \end{figure}
 
-\begin{lineref}[ln:toolsoftrade:jobcontrol:script]
+\begin{lineref}[ln:toolsoftrade:parallel:compute_it]
 Lines~\lnref{comp1} and~\lnref{comp2} launch two instances of this
 program, redirecting their
 output to two separate files, with the \co{&} character directing the
-- 
2.7.4



^ permalink raw reply related	[flat|nested] 11+ messages in thread

* [PATCH 9/9] future/formalregress: Example of extraction of snippet from .litmus file
  2018-09-23  7:21 [PATCH 0/9] Update code snippet extraction scheme Akira Yokosawa
                   ` (7 preceding siblings ...)
  2018-09-23  7:32 ` [PATCH 8/9] toolsoftrade: Example of extraction of snippet from parallel.sh Akira Yokosawa
@ 2018-09-23  7:34 ` Akira Yokosawa
  2018-09-23 21:44 ` [PATCH 0/9] Update code snippet extraction scheme Paul E. McKenney
  9 siblings, 0 replies; 11+ messages in thread
From: Akira Yokosawa @ 2018-09-23  7:34 UTC (permalink / raw)
  To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa

From df6459c699d373a247342b3a79d3bf7a239cfbe3 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Thu, 30 Aug 2018 22:59:44 +0900
Subject: [PATCH 9/9] future/formalregress: Example of extraction of snippet from .litmus file

This is a POC of including litmus test snippet extracted via
reorder_ltms.pl and fcvextract.pl.

As herdtools7 does not allow comment following a "filter" or
"exists" clause, we use an option "filterlabel" to the meta command
"\end[snippet]".

NOTE: Neither "exists" nor "filter" can appear as a token in
    comments of litmus test. "filter_" is OK. A token in comment?
    Don't ask me!

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 .../formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus      |  2 ++
 future/formalregress.tex                           | 40 +++-------------------
 2 files changed, 6 insertions(+), 36 deletions(-)

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 ae64726..32d8e52 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
@@ -1,4 +1,5 @@
 C C-SB+l-o-o-u+l-o-o-u-C
+// \begin[snippet][labelbase=ln:future:formalregress:C-SB+l-o-o-u+l-o-o-u-C:whole,commandchars=\%\[\]]
 
 {
 }
@@ -25,5 +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)
 exists (0:r1=0 /\ 1:r1=0)
diff --git a/future/formalregress.tex b/future/formalregress.tex
index 163237e..dd94c8c 100644
--- a/future/formalregress.tex
+++ b/future/formalregress.tex
@@ -188,41 +188,7 @@ is correct, and additional verification passes can verify correct
 use of the locking APIs.
 
 \begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}[\LstLineNo]
-C C-SB+l-o-o-u+l-o-o-u-C
-
-{
-}
-
-P0(int *sl, int *x0, int *x1)
-{
-  int r2;
-  int r1;
-
-  r2 = cmpxchg_acquire(sl, 0, 1);
-  WRITE_ONCE(*x0, 1);
-  r1 = READ_ONCE(*x1);
-  smp_store_release(sl, 0);
-}
-
-P1(int *sl, int *x0, int *x1)
-{
-  int r2;
-  int r1;
-
-  r2 = cmpxchg_acquire(sl, 0, 1);
-  WRITE_ONCE(*x1, 1);
-  r1 = READ_ONCE(*x0);
-  smp_store_release(sl, 0);
-}
-
-filter (0:r2=0 /\ 1:r2=0)
-exists (0:r1=0 /\ 1:r1=0)
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C@whole.fcv}
 \caption{Emulating Locking with \tco{cmpxchg_acquire()}}
 \label{lst:future:Emulating Locking with cmpxchg}
 \end{listing}
@@ -263,11 +229,13 @@ The difference is not insignificant: At four processes, the model
 is more than two orders of magnitude faster than emulation!
 
 \QuickQuiz{}
-	Why bother with a separate \co{filter} command on line~28 of
+\begin{lineref}[ln:future:formalregress:C-SB+l-o-o-u+l-o-o-u-C:whole]
+	Why bother with a separate \co{filter} command on line~\lnref{filter_} of
 	Listing~\ref{lst:future:Emulating Locking with cmpxchg}
 	instead of just adding the condition to the \co{exists} clause?
 	And wouldn't it be simpler to use \co{xchg_acquire()} instead
 	of \co{cmpxchg_acquire()}?
+\end{lineref}
 \QuickQuizAnswer{
 	The \co{filter} clause causes the \co{herd} tool to discard
 	executions at an earlier stage of processing than does
-- 
2.7.4



^ permalink raw reply related	[flat|nested] 11+ messages in thread

* Re: [PATCH 0/9] Update code snippet extraction scheme
  2018-09-23  7:21 [PATCH 0/9] Update code snippet extraction scheme Akira Yokosawa
                   ` (8 preceding siblings ...)
  2018-09-23  7:34 ` [PATCH 9/9] future/formalregress: Example of extraction of snippet from .litmus file Akira Yokosawa
@ 2018-09-23 21:44 ` Paul E. McKenney
  9 siblings, 0 replies; 11+ messages in thread
From: Paul E. McKenney @ 2018-09-23 21:44 UTC (permalink / raw)
  To: Akira Yokosawa; +Cc: perfbook

On Sun, Sep 23, 2018 at 04:21:05PM +0900, Akira Yokosawa wrote:
> >From df6459c699d373a247342b3a79d3bf7a239cfbe3 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Sun, 23 Sep 2018 09:16:20 +0900
> Subject: [PATCH 0/9] Update code snippet extraction scheme
> 
> Hi Paul,
> 
> This patch set updates scripts to extract code snippet from
> source files under CodeSamples/.
> 
> Patch #1 fixes fcvextract.pl to use "linelabel" environment in
> extracted .fcv files.
> 
> Patches #2 through #5 add capability to handle code snippets
> other than C. Patch #2 is a simple update with a bug fix to
> handle source files under deep sub-directories. 
> 
> One major obstacle was the restriction of comments in .litmus
> files.
> 
>     1) We can't add comments at the beginning nor the end of
>        a litmus test.
>     2) There are a few tokens and characters we can't use in
>        comments, i.e. "exists" or "filter" as a token in
>        comment is not accepted by herd7, "{" and "}" characters
>        sometimes cause error, comments of the form "(*" -- "*)"
>        are not allowed in the C-language part of litmus test.
> 
> I ended up using comments of the form "//...", which has been
> supported by herdtools7.
> 
> Patches #3 and #4 work around the restriction.
> 
> Patch #5 prevents a side-effect of doing "make" under
> CodeSamples/formal/herd, which will convert litmus tests under
> CodeSamples/formal/litmus so that they can be fed into herd7,
> and cause the converted tests to have redundant
> "\begin[snippet]" meta commands.
> 
> Patch #6 adds an option "style=" to the meta command
> \begin{snippet}, which can be used to specify which of
> Verbetim{L/N/U} is to be emitted. It also adds pass-through
> handling of other options.
> 
> Patch #7 is not an update to the scripts, but a tweak in
> appearance of VerbatimN and VerbatimU environments so that
> inline snippets will have frames around them. 
> 
> Patches #8 and #9 are examples of actually extracting snippets
> from .sh and .litmus files.
> 
> Effect of patch #7 can be seen in Section 4.1 (below the 1st
> paragraph) and in Section 4.2.1 (above Quick Quiz 4.6) after
> applying the whole patch set.  If you don't like the change,
> feel free to omit #7.
> 
> By this update, hopefully, the new scheme should be able to
> cover 99 percent of snippets. Although the scripts lack
> rigorous checks of unexpected inputs.

Very nice, thank you!!!  Queued and pushed.

							Thanx, Paul

>         Thanks, Akira
> 
> Akira Yokosawa (9):
>   fcvextract.pl: Use 'linelabel' env in extracted snippet
>   Update build scripts to support code snippets other than 'C'
>   Add scripts and recipes to work around restriction of herdtools7
>   reorder_ltms.pl: Enable further labeling in litmus test snippet
>   Exclude meta command lines in .litmus -> .litmus.herd conversion
>   fcvextract.pl: Support 'style=' option and pass through other options
>   Enable 'single' frame around inline code snippets
>   toolsoftrade: Example of extraction of snippet from parallel.sh
>   future/formalregress: Example of extraction of snippet from .litmus
>     file
> 
>  .gitignore                                         |   1 +
>  .../formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus      |   2 +
>  CodeSamples/formal/herd/litmus2herd.sh             |   4 +-
>  CodeSamples/toolsoftrade/parallel.sh               |  20 ++--
>  Makefile                                           |  19 +++-
>  future/formalregress.tex                           |  40 +------
>  perfbook.tex                                       |   7 +-
>  toolsoftrade/toolsoftrade.tex                      |  12 +--
>  utilities/fcvextract.pl                            |  74 ++++++++++---
>  utilities/gen_snippet_d.pl                         |  66 +++++++++++-
>  utilities/reorder_ltms.pl                          | 117 +++++++++++++++++++++
>  11 files changed, 281 insertions(+), 81 deletions(-)
>  create mode 100755 utilities/reorder_ltms.pl
> 
> -- 
> 2.7.4
> 


^ permalink raw reply	[flat|nested] 11+ messages in thread

end of thread, other threads:[~2018-09-24  3:43 UTC | newest]

Thread overview: 11+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2018-09-23  7:21 [PATCH 0/9] Update code snippet extraction scheme Akira Yokosawa
2018-09-23  7:22 ` [PATCH 1/9] fcvextract.pl: Use 'linelabel' env in extracted snippet Akira Yokosawa
2018-09-23  7:24 ` [PATCH 2/9] Update build scripts to support code snippets other than 'C' Akira Yokosawa
2018-09-23  7:26 ` [PATCH 3/9] Add scripts and recipes to work around restriction of herdtools7 Akira Yokosawa
2018-09-23  7:27 ` [PATCH 4/9] reorder_ltms.pl: Enable further labeling in litmus test snippet Akira Yokosawa
2018-09-23  7:29 ` [PATCH 5/9] Exclude meta command lines in .litmus -> .litmus.herd conversion Akira Yokosawa
2018-09-23  7:30 ` [PATCH 6/9] fcvextract.pl: Support 'style=' option and pass through other options Akira Yokosawa
2018-09-23  7:31 ` [PATCH 7/9] Enable 'single' frame around inline code snippets Akira Yokosawa
2018-09-23  7:32 ` [PATCH 8/9] toolsoftrade: Example of extraction of snippet from parallel.sh Akira Yokosawa
2018-09-23  7:34 ` [PATCH 9/9] future/formalregress: Example of extraction of snippet from .litmus file Akira Yokosawa
2018-09-23 21:44 ` [PATCH 0/9] Update code snippet extraction scheme Paul E. McKenney

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox