[PATCH 0/4] formal/spinhint: Clarify hashtable sizes used in tables

[PATCH 0/4] formal/spinhint: Clarify hashtable sizes used in tables

[Akira Yokosawa]

Hi Paul,

In your wordsmithing, there was confusion of hashtable sizes used in
Tables 12.2 and 12.3. Patch #1 attempts to clarify the point. It also
adds a footnote and fixes a few trivial typos.

Patch #2 is a minor tweak to use "lmtt" font for code snippets
imported by \VerbatimInput{} command. This fixes font of Listing 12.3
for experimental targets such as "msnt" and "1csf".

Patch #3 fixes font choice of snippets in experimental targets "msns"
(original monospace font of "courier") and "mss" (previous monospace
font choice of "scaled courier"), which have kept using those fonts for code
snippets. As is mentioned in the change log, there are a lot of overfills
in code snippets. On the other hand, the font used in the target "msn"
(monospace narrow) is narrower than the "lmtt" font and it should be OK
to use it in code snippets.

Patch #4 resolves the warning from "make" due to a stray litmus test
"C-SB+o-rcusync-o+rl-rul-o.litmus". My guess is that this file was
unintentionally sneaked into the repository in commit 4a6337b85633
("memorder: Cover litmus tests for accesses outside of RCU readers").
But you may have an idea what the test of that name should look like.
If this is the case, please update the test instead of applying this
patch.

        Thanks, Akira
--
Akira Yokosawa (4):
  formal/spinhint: Clarify hashtable sizes used in Tables 12.2 and 12.3
  Set default fontfamily for snippets of 'fancyvrb'
  Change monospace font of snippets for targets 'mss', 'msns', and 'msn'
  memorder: Remove 'snippet' meta command in stray litmus test

 CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus |  2 --
 Makefile                                                 | 11 +++++------
 formal/spinhint.tex                                      | 14 ++++++++------
 perfbook.tex                                             |  5 +----
 4 files changed, 14 insertions(+), 18 deletions(-)

-- 
2.7.4

[PATCH 1/4] formal/spinhint: Clarify hashtable sizes used in Tables 12.2 and 12.3

[Akira Yokosawa]

From 4f0d8e38e9de5f9597ac7573a48cb64f2bb7e93f Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 12 Feb 2019 20:55:52 +0900
Subject: [PATCH 1/4] formal/spinhint: Clarify hashtable sizes used in Tables 12.2 and 12.3

Also add a footnote to mention the possibility of impractically
long runtime, and fix trivial typos.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/spinhint.tex | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 5e19247..7c08115 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -893,8 +893,8 @@ updaters, however, simple extrapolation indicates that this will
 require about half a terabyte of memory.
 What to do?
 
-It turns out that \co{./pan} gives advice when ti runs out of memory,
-for example, when attempting to run three readers and updaters:
+It turns out that \co{./pan} gives advice when it runs out of memory,
+for example, when attempting to run three readers and three updaters:
 
 \begin{VerbatimU}
 hint: to reduce memory, recompile with
@@ -939,7 +939,7 @@ lower than the \co{-DCOLLAPSE} usage of about half a terabyte.
 	in memory occupied by the states!
 	Is the state-space search \emph{really} exhaustive???
 \QuickQuizAnswer{
-	According Spin's documentation, yes, is.
+	According to Spin's documentation, yes, it is.
 
 \begin{listing}
 \VerbatimInput[numbers=none,fontsize=\scriptsize]{CodeSamples/formal/promela/qrcu.spin.col-ma.diff.lst}
@@ -1011,11 +1011,12 @@ summarizes the Spin results with \co{-DCOLLAPSE} and \co{-DMA=N}
 compiler flags.
 The memory usage is obtained with minimal sufficient
 search depths and \co{-DMA=N} parameters shown in the table.
-As was the case for \co{-DCOLLAPSE}, hash table sizes are tweaked by
+Hashtable sizes of \co{-DCOLLAPSE} are tweaked by
 the \co{-wN} option of \co{./pan} to avoid using too much
 memory hashing small state spaces.
 Hence the memory usage is smaller than what is shown in
-Table~\ref{tab:advsync:Memory Usage of QRCU Model}.
+Table~\ref{tab:advsync:Memory Usage of QRCU Model}, where the
+hashtable size starts from the default of \co{-w24}.
 The runtime is from a \Power{9} server, which shows that \co{-DMA=N}
 suffers up to about an order of magnitude higher CPU overhead
 than does \co{-DCOLLAPSE}, but on the other hand reduces memroy overhead
@@ -1023,7 +1024,8 @@ by well over an order of magnitude.
 
 So far so good.
 But adding a few more updaters or readers would exhaust memory, even
-with \co{-DMA=N}.
+with \co{-DMA=N}.\footnote{
+	Or, runtime would become too long to be practical.}
 So what to do?
 Here are some possible approaches:
 
-- 
2.7.4

[PATCH 2/4] Set default fontfamily for snippets of 'fancyvrb'

[Akira Yokosawa]

From 025355ead8a24d953771fc44066f20efa91e9897 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 12 Feb 2019 21:04:37 +0900
Subject: [PATCH 2/4] Set default fontfamily for snippets of 'fancyvrb'

Defaults of environments derived from "Verbatim" as well
as \VerbatimInput{} can be set globally by a "\fvset{}" macro.

\VerbatimImput{} was not covered by the old code.

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

diff --git a/perfbook.tex b/perfbook.tex
index 9caeee8..edf18d5 100644
--- a/perfbook.tex
+++ b/perfbook.tex
@@ -131,10 +131,7 @@
 \AtBeginEnvironment{tabularx}{\renewcommand{\ttdefault}{lmtt}}
 \AtBeginEnvironment{minipage}{\renewcommand{\ttdefault}{lmtt}}
 \AtBeginEnvironment{listing}{\renewcommand{\ttdefault}{lmtt}}
-\AtBeginEnvironment{Verbatim}{\renewcommand{\ttdefault}{lmtt}}
-\AtBeginEnvironment{VerbatimL}{\renewcommand{\ttdefault}{lmtt}}
-\AtBeginEnvironment{VerbatimN}{\renewcommand{\ttdefault}{lmtt}}
-\AtBeginEnvironment{VerbatimU}{\renewcommand{\ttdefault}{lmtt}}
+\fvset{fontfamily=lmtt}
 }{}
 
 \IfTblCpTop{
-- 
2.7.4

[PATCH 3/4] Change monospace font of snippets for targets 'mss', 'msns', and 'msn'

[Akira Yokosawa]

From f696c13873b1458800d56f0151885e49abf5d5ec Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 12 Feb 2019 21:06:28 +0900
Subject: [PATCH 3/4] Change monospace font of snippets for targets 'mss', 'msns', and 'msn'

Now that code snippets assume "lmtt" (Latin Modern Typewriter)
font to decide where to fold long lines, "mss" and "msns" targets
have frequent overfulls of snippets in 2c layout.
Remove on-the-fly sed script keeping \ttdefault unchanged for
snippets in these two targets.

"msn" target's monospace font "nimbusmononarrow" (Narrow Courier
Clone) is narrower than "lmtt". This font can be a good candidate
for code snippets in the future. To allow us to see how it looks
like, add the on-the-fly sed script to "msn" instead.

Note: "nimbusmonoarrow" is not available on TeX Live 2013/Debian.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 Makefile | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/Makefile b/Makefile
index c15678b..7a6d156 100644
--- a/Makefile
+++ b/Makefile
@@ -159,12 +159,10 @@ perfbook-hb.tex: perfbook.tex
 	sed -e 's/,twocolumn/&,letterpaperhb/' -e 's/setboolean{hardcover}{false}/setboolean{hardcover}{true}/' < $< > $@
 
 perfbook-msns.tex: perfbook.tex
-	sed -e 's/%msfontstub/\\usepackage{courier}/' \
-	    -e 's/{lmttforcode}{true}/{lmttforcode}{false}/' < $< > $@
+	sed -e 's/%msfontstub/\\usepackage{courier}/' < $< > $@
 
 perfbook-mss.tex: perfbook.tex
-	sed -e 's/%msfontstub/\\usepackage[scaled=.94]{couriers}/' \
-	    -e 's/{lmttforcode}{true}/{lmttforcode}{false}/' < $< > $@
+	sed -e 's/%msfontstub/\\usepackage[scaled=.94]{couriers}/' < $< > $@
 
 perfbook-mstx.tex: perfbook.tex
 	sed -e 's/%msfontstub/\\renewcommand*\\ttdefault{txtt}/' < $< > $@
@@ -174,7 +172,8 @@ perfbook-msr.tex: perfbook.tex
 	@echo "## This target requires font package nimbus15. ##"
 
 perfbook-msn.tex: perfbook.tex
-	sed -e 's/%msfontstub/\\usepackage{nimbusmononarrow}/' < $< > $@
+	sed -e 's/%msfontstub/\\usepackage{nimbusmononarrow}/' \
+	    -e 's/{lmttforcode}{true}/{lmttforcode}{false}/' < $< > $@
 	@echo "## This target requires font package nimbus15. ##"
 
 perfbook-msnt.tex: perfbook.tex
@@ -291,7 +290,7 @@ help:
 	@echo "  \"msn\" doesn't cover bold face for monospace."
 	@echo "  \"1csf\" requires \"newtxsf\"."
 	@echo
-	@echo "All targets except for \"msns\" and \"mss\" use \"Latin Modern Typewriter\" font"
+	@echo "All targets except for \"msn\" use \"Latin Modern Typewriter\" font"
 	@echo "for code snippets."
 
 clean:
-- 
2.7.4

[PATCH 4/4] memorder: Remove 'snippet' meta command in stray litmus test

[Akira Yokosawa]

From 0ddf5c5ea4a66a0d6bff1b6c0ce32682459c20ad Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 12 Feb 2019 23:18:29 +0900
Subject: [PATCH 4/4] memorder: Remove 'snippet' meta command in stray litmus test

C-SB+o-rcusync-o+rl-rul-o.litmus is identical to
C-SB+o-rcusync-o+rl-o-rul-o.litmus and causes "make" to emit
warning:

    target 'CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-rul-o@whole.fcv'
    given more than once in the same rule

This commit removes "snippet" meta commands in the test.
Just removing the file can cause a build error afterward.
A "make clean" will resolve the error, but keeping the file
looks like a reasonable approach to avoid surprising people.
The file can be removed in the near future when most active
users have updated snippets.d.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus | 2 --
 1 file changed, 2 deletions(-)

diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
index a39baf3..2407a51 100644
--- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
+++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
@@ -1,5 +1,4 @@
 C C-SB+o-rcusync-o+rl-o-rul-o
-//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+rl-o-rul-o:whole,commandchars=\@\[\]]
 {
 }
 
@@ -19,5 +18,4 @@ P1(uintptr_t *x0, uintptr_t *x1)
 	uintptr_t r2 = READ_ONCE(*x0);
 }
 
-//\end[snippet]
 exists (1:r2=0 /\ 0:r2=0)
-- 
2.7.4

Re: [PATCH 4/4] memorder: Remove 'snippet' meta command in stray litmus test

[Paul E. McKenney]

On Wed, Feb 13, 2019 at 12:39:38AM +0900, Akira Yokosawa wrote:
> >From 0ddf5c5ea4a66a0d6bff1b6c0ce32682459c20ad Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Tue, 12 Feb 2019 23:18:29 +0900
> Subject: [PATCH 4/4] memorder: Remove 'snippet' meta command in stray litmus test
> 
> C-SB+o-rcusync-o+rl-rul-o.litmus is identical to
> C-SB+o-rcusync-o+rl-o-rul-o.litmus and causes "make" to emit
> warning:
> 
>     target 'CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-rul-o@whole.fcv'
>     given more than once in the same rule
> 
> This commit removes "snippet" meta commands in the test.
> Just removing the file can cause a build error afterward.
> A "make clean" will resolve the error, but keeping the file
> looks like a reasonable approach to avoid surprising people.
> The file can be removed in the near future when most active
> users have updated snippets.d.

Unless I am confused, this litmus test appears as Listing 15.37.
That said, its discussion does not reference any line numbers, so
the snippet comments could reasonably be removed.  Or maybe I should
instead upgrade the discussion to include line numbers.

So what am I missing here?

							Thanx, Paul

> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> ---
>  CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus | 2 --
>  1 file changed, 2 deletions(-)
> 
> diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
> index a39baf3..2407a51 100644
> --- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
> +++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
> @@ -1,5 +1,4 @@
>  C C-SB+o-rcusync-o+rl-o-rul-o
> -//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+rl-o-rul-o:whole,commandchars=\@\[\]]
>  {
>  }
>  
> @@ -19,5 +18,4 @@ P1(uintptr_t *x0, uintptr_t *x1)
>  	uintptr_t r2 = READ_ONCE(*x0);
>  }
>  
> -//\end[snippet]
>  exists (1:r2=0 /\ 0:r2=0)
> -- 
> 2.7.4
> 
> 

Re: [PATCH 0/4] formal/spinhint: Clarify hashtable sizes used in tables

[Paul E. McKenney]

On Wed, Feb 13, 2019 at 12:31:22AM +0900, Akira Yokosawa wrote:
> Hi Paul,
> 
> In your wordsmithing, there was confusion of hashtable sizes used in
> Tables 12.2 and 12.3. Patch #1 attempts to clarify the point. It also
> adds a footnote and fixes a few trivial typos.
> 
> Patch #2 is a minor tweak to use "lmtt" font for code snippets
> imported by \VerbatimInput{} command. This fixes font of Listing 12.3
> for experimental targets such as "msnt" and "1csf".
> 
> Patch #3 fixes font choice of snippets in experimental targets "msns"
> (original monospace font of "courier") and "mss" (previous monospace
> font choice of "scaled courier"), which have kept using those fonts for code
> snippets. As is mentioned in the change log, there are a lot of overfills
> in code snippets. On the other hand, the font used in the target "msn"
> (monospace narrow) is narrower than the "lmtt" font and it should be OK
> to use it in code snippets.
> 
> Patch #4 resolves the warning from "make" due to a stray litmus test
> "C-SB+o-rcusync-o+rl-rul-o.litmus". My guess is that this file was
> unintentionally sneaked into the repository in commit 4a6337b85633
> ("memorder: Cover litmus tests for accesses outside of RCU readers").
> But you may have an idea what the test of that name should look like.
> If this is the case, please update the test instead of applying this
> patch.

I applied #1 with tweaks and #2 and #3 as is.  I am holding off on #4
for the moment because it looks to me that it is being used.  So please
check my tweaks to #1 and my reasoning on #4.

							Thanx, Paul

>         Thanks, Akira
> --
> Akira Yokosawa (4):
>   formal/spinhint: Clarify hashtable sizes used in Tables 12.2 and 12.3
>   Set default fontfamily for snippets of 'fancyvrb'
>   Change monospace font of snippets for targets 'mss', 'msns', and 'msn'
>   memorder: Remove 'snippet' meta command in stray litmus test
> 
>  CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus |  2 --
>  Makefile                                                 | 11 +++++------
>  formal/spinhint.tex                                      | 14 ++++++++------
>  perfbook.tex                                             |  5 +----
>  4 files changed, 14 insertions(+), 18 deletions(-)
> 
> -- 
> 2.7.4
> 

Re: [PATCH 4/4] memorder: Remove 'snippet' meta command in stray litmus test

[Akira Yokosawa]

On 2019/02/12 08:16:31 -0800, Paul E. McKenney wrote:
> On Wed, Feb 13, 2019 at 12:39:38AM +0900, Akira Yokosawa wrote:
>> >From 0ddf5c5ea4a66a0d6bff1b6c0ce32682459c20ad Mon Sep 17 00:00:00 2001
>> From: Akira Yokosawa <akiyks@gmail.com>
>> Date: Tue, 12 Feb 2019 23:18:29 +0900
>> Subject: [PATCH 4/4] memorder: Remove 'snippet' meta command in stray litmus test
>>
>> C-SB+o-rcusync-o+rl-rul-o.litmus is identical to
>> C-SB+o-rcusync-o+rl-o-rul-o.litmus and causes "make" to emit
>> warning:
>>
>>     target 'CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-rul-o@whole.fcv'
>>     given more than once in the same rule
>>
>> This commit removes "snippet" meta commands in the test.
>> Just removing the file can cause a build error afterward.
>> A "make clean" will resolve the error, but keeping the file
>> looks like a reasonable approach to avoid surprising people.
>> The file can be removed in the near future when most active
>> users have updated snippets.d.
> 
> Unless I am confused, this litmus test appears as Listing 15.37.

Listing 15.37 is "C-SB+o-rcusync-o+rl-o-rul-o".
The file I modified is "C-SB+o-rcusync-o+rl-rul-o.litmus" (note the
missing "-o-" in the final part") but contains the same test
"C-SB+o-rcusync-o+rl-o-rul-o". There exists
C-SB+o-rcusync-o+rl-o-rul-o.litmus which contains the same test
"C-SB+o-rcusync-o+rl-o-rul-o". So C-SB+o-rcusync-o+rl-rul-o.litmus
can be safely removed. But this patch removes the snippet meta-commands
instead.

Have I made the point clearer?

        Thanks, Akira

> That said, its discussion does not reference any line numbers, so
> the snippet comments could reasonably be removed.  Or maybe I should
> instead upgrade the discussion to include line numbers.
> 
> So what am I missing here?
> 
> 							Thanx, Paul
> 
>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
>> ---
>>  CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus | 2 --
>>  1 file changed, 2 deletions(-)
>>
>> diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
>> index a39baf3..2407a51 100644
>> --- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
>> +++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
>> @@ -1,5 +1,4 @@
>>  C C-SB+o-rcusync-o+rl-o-rul-o
>> -//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+rl-o-rul-o:whole,commandchars=\@\[\]]
>>  {
>>  }
>>  
>> @@ -19,5 +18,4 @@ P1(uintptr_t *x0, uintptr_t *x1)
>>  	uintptr_t r2 = READ_ONCE(*x0);
>>  }
>>  
>> -//\end[snippet]
>>  exists (1:r2=0 /\ 0:r2=0)
>> -- 
>> 2.7.4
>>
>>
> 

Re: [PATCH 4/4] memorder: Remove 'snippet' meta command in stray litmus test

[Paul E. McKenney]

On Wed, Feb 13, 2019 at 07:11:02AM +0900, Akira Yokosawa wrote:
> On 2019/02/12 08:16:31 -0800, Paul E. McKenney wrote:
> > On Wed, Feb 13, 2019 at 12:39:38AM +0900, Akira Yokosawa wrote:
> >> >From 0ddf5c5ea4a66a0d6bff1b6c0ce32682459c20ad Mon Sep 17 00:00:00 2001
> >> From: Akira Yokosawa <akiyks@gmail.com>
> >> Date: Tue, 12 Feb 2019 23:18:29 +0900
> >> Subject: [PATCH 4/4] memorder: Remove 'snippet' meta command in stray litmus test
> >>
> >> C-SB+o-rcusync-o+rl-rul-o.litmus is identical to
> >> C-SB+o-rcusync-o+rl-o-rul-o.litmus and causes "make" to emit
> >> warning:
> >>
> >>     target 'CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-rul-o@whole.fcv'
> >>     given more than once in the same rule
> >>
> >> This commit removes "snippet" meta commands in the test.
> >> Just removing the file can cause a build error afterward.
> >> A "make clean" will resolve the error, but keeping the file
> >> looks like a reasonable approach to avoid surprising people.
> >> The file can be removed in the near future when most active
> >> users have updated snippets.d.
> > 
> > Unless I am confused, this litmus test appears as Listing 15.37.
> 
> Listing 15.37 is "C-SB+o-rcusync-o+rl-o-rul-o".
> The file I modified is "C-SB+o-rcusync-o+rl-rul-o.litmus" (note the
> missing "-o-" in the final part") but contains the same test
> "C-SB+o-rcusync-o+rl-o-rul-o". There exists
> C-SB+o-rcusync-o+rl-o-rul-o.litmus which contains the same test
> "C-SB+o-rcusync-o+rl-o-rul-o". So C-SB+o-rcusync-o+rl-rul-o.litmus
> can be safely removed. But this patch removes the snippet meta-commands
> instead.
> 
> Have I made the point clearer?

You have!  My confusion stemmed from the fact that these two files
are identical, as you say:

CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus

I was searching based on the name within the file rather than the
filename.  In short, we can just get rid of the unused file.

Apologies for my confusion!

							Thanx, Paul

>         Thanks, Akira
> 
> > That said, its discussion does not reference any line numbers, so
> > the snippet comments could reasonably be removed.  Or maybe I should
> > instead upgrade the discussion to include line numbers.
> > 
> > So what am I missing here?
> > 
> > 							Thanx, Paul
> > 
> >> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> >> ---
> >>  CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus | 2 --
> >>  1 file changed, 2 deletions(-)
> >>
> >> diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
> >> index a39baf3..2407a51 100644
> >> --- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
> >> +++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
> >> @@ -1,5 +1,4 @@
> >>  C C-SB+o-rcusync-o+rl-o-rul-o
> >> -//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+rl-o-rul-o:whole,commandchars=\@\[\]]
> >>  {
> >>  }
> >>  
> >> @@ -19,5 +18,4 @@ P1(uintptr_t *x0, uintptr_t *x1)
> >>  	uintptr_t r2 = READ_ONCE(*x0);
> >>  }
> >>  
> >> -//\end[snippet]
> >>  exists (1:r2=0 /\ 0:r2=0)
> >> -- 
> >> 2.7.4
> >>
> >>
> > 
> 

Re: [PATCH 4/4] memorder: Remove 'snippet' meta command in stray litmus test

[Paul E. McKenney]

On Tue, Feb 12, 2019 at 03:45:42PM -0800, Paul E. McKenney wrote:
> On Wed, Feb 13, 2019 at 07:11:02AM +0900, Akira Yokosawa wrote:
> > On 2019/02/12 08:16:31 -0800, Paul E. McKenney wrote:
> > > On Wed, Feb 13, 2019 at 12:39:38AM +0900, Akira Yokosawa wrote:
> > >> >From 0ddf5c5ea4a66a0d6bff1b6c0ce32682459c20ad Mon Sep 17 00:00:00 2001
> > >> From: Akira Yokosawa <akiyks@gmail.com>
> > >> Date: Tue, 12 Feb 2019 23:18:29 +0900
> > >> Subject: [PATCH 4/4] memorder: Remove 'snippet' meta command in stray litmus test
> > >>
> > >> C-SB+o-rcusync-o+rl-rul-o.litmus is identical to
> > >> C-SB+o-rcusync-o+rl-o-rul-o.litmus and causes "make" to emit
> > >> warning:
> > >>
> > >>     target 'CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-rul-o@whole.fcv'
> > >>     given more than once in the same rule
> > >>
> > >> This commit removes "snippet" meta commands in the test.
> > >> Just removing the file can cause a build error afterward.
> > >> A "make clean" will resolve the error, but keeping the file
> > >> looks like a reasonable approach to avoid surprising people.
> > >> The file can be removed in the near future when most active
> > >> users have updated snippets.d.
> > > 
> > > Unless I am confused, this litmus test appears as Listing 15.37.
> > 
> > Listing 15.37 is "C-SB+o-rcusync-o+rl-o-rul-o".
> > The file I modified is "C-SB+o-rcusync-o+rl-rul-o.litmus" (note the
> > missing "-o-" in the final part") but contains the same test
> > "C-SB+o-rcusync-o+rl-o-rul-o". There exists
> > C-SB+o-rcusync-o+rl-o-rul-o.litmus which contains the same test
> > "C-SB+o-rcusync-o+rl-o-rul-o". So C-SB+o-rcusync-o+rl-rul-o.litmus
> > can be safely removed. But this patch removes the snippet meta-commands
> > instead.
> > 
> > Have I made the point clearer?
> 
> You have!  My confusion stemmed from the fact that these two files
> are identical, as you say:
> 
> CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
> CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus
> 
> I was searching based on the name within the file rather than the
> filename.  In short, we can just get rid of the unused file.
> 
> Apologies for my confusion!

And I have removed it with your Reported-by, and thank you for catching this!

							Thanx, Paul