[PATCH] formal/dyntickrcu: Mitigate ugliness of tall inline snippets

[PATCH] formal/dyntickrcu: Mitigate ugliness of tall inline snippets

[Akira Yokosawa]

From 8f49523f66fb2281b4337ce57f6502400f0dcb9c Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sat, 6 Apr 2019 08:53:12 +0900
Subject: [PATCH] formal/dyntickrcu: Mitigate ugliness of tall inline snippets

In two-column layout, frames around snippets by \VerbatimN cause
column breaks of snippets look somewhat ugly.

As a mitigation, disable frame of \VerbatimN in this particular
section. Also use \VerbatimU for patch snippets to prevent
them from breaking other inline snippets in one-column layout.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
Hi Paul,

I know this is not ideal for you, but in one-column layout, the
column breaks of long snippets does not disturb me so much.

So this patch disables frame around \VerbatimN for two-column layout
to restore the looks in the old scheme.

Isn't this approach acceptable to you, at least as a workaround?

        Thanks, Akira
--
 formal/dyntickrcu.tex | 67 ++++++++++++++++++++++++-------------------
 1 file changed, 38 insertions(+), 29 deletions(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index c73cdd2f..94093ee9 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -1,5 +1,14 @@
 % formal/dyntickrcu.tex
 
+% Disable frame around VerbatimN in two-column layout
+\IfTwoColumn{
+\RecustomVerbatimEnvironment{VerbatimN}{Verbatim}%
+{numbers=left,numbersep=5pt,xleftmargin=10pt,xrightmargin=0pt,frame=none}
+\AtBeginEnvironment{VerbatimN}{%
+\renewcommand{\lnlbl}[1]{\raisebox{0pt}{\phantomsection\label{\lnlblbase:#1}}}%
+}
+}{}
+
 \subsection{Promela Parable: dynticks and Preemptible RCU}
 \label{sec:formal:Promela Parable: dynticks and Preemptible RCU}
 
@@ -1114,10 +1123,19 @@ states, passing without errors.
 
 \subsubsection{Lessons (Re)Learned}
 \label{sec:formal:Lessons (Re)Learned}
-\NoIndentAfterThis
 
-\begin{listing}[tbp]
-\begin{VerbatimL}[numbers=none]
+This effort provided some lessons (re)learned:
+
+\begin{enumerate}
+\item	{\bf Promela and Spin can verify interrupt\slash NMI\-/handler
+	interactions.}
+\item	{\bf Documenting code can help locate bugs.}
+	In this case, the documentation effort located
+	a misplaced memory barrier in
+	\co{rcu_enter_nohz()} and \co{rcu_exit_nohz()},
+	as shown by the following patch.
+
+\begin{VerbatimU}
  static inline void rcu_enter_nohz(void)
  {
 +       mb();
@@ -1131,38 +1149,20 @@ states, passing without errors.
         __get_cpu_var(dynticks_progress_counter)++;
 +       mb();
  }
-\end{VerbatimL}
-\caption{Memory-Barrier Fix Patch}
-\label{lst:formal:Memory-Barrier Fix Patch}
-\end{listing}
-
-\begin{listing}[tbp]
-\begin{VerbatimL}[numbers=none]
--       if ((curr - snap) > 2 || (snap & 0x1) == 0)
-+       if ((curr - snap) > 2 || (curr & 0x1) == 0)
-\end{VerbatimL}
-\caption{Variable-Name-Typo Fix Patch}
-\label{lst:formal:Variable-Name-Typo Fix Patch}
-\end{listing}
-
-This effort provided some lessons (re)learned:
+\end{VerbatimU}
 
-\begin{enumerate}
-\item	{\bf Promela and Spin can verify interrupt\slash NMI\-/handler
-	interactions.}
-\item	{\bf Documenting code can help locate bugs.}
-	In this case, the documentation effort located
-	a misplaced memory barrier in
-	\co{rcu_enter_nohz()} and \co{rcu_exit_nohz()},
-	as shown by the patch in
-	Listing~\ref{lst:formal:Memory-Barrier Fix Patch}.
 \item	{\bf Validate your code early, often, and up to the point
 	of destruction.}
 	This effort located one subtle bug in
 	\co{rcu_try_flip_waitack_needed()}
 	that would have been quite difficult to test or debug, as
-	shown by the patch in
-	Listing~\ref{lst:formal:Variable-Name-Typo Fix Patch}.
+	shown by the following patch.
+
+\begin{VerbatimU}
+-       if ((curr - snap) > 2 || (snap & 0x1) == 0)
++       if ((curr - snap) > 2 || (curr & 0x1) == 0)
+\end{VerbatimU}
+
 \item	{\bf Always verify your verification code.}
 	The usual way to do this is to insert a deliberate bug
 	and verify that the verification code catches it.  Of course,
@@ -1621,3 +1621,12 @@ where an NMI might change shared state at any point during execution of
 the \IRQ\ functions.
 
 Verification can be a good thing, but simplicity is even better.
+
+% Restore frame around VerbatimN in two-column layout
+\IfTwoColumn{
+\RecustomVerbatimEnvironment{VerbatimN}{Verbatim}%
+{numbers=left,numbersep=3pt,xleftmargin=5pt,xrightmargin=5pt,frame=single}
+\AtBeginEnvironment{VerbatimN}{%
+\renewcommand{\lnlbl}[1]{\raisebox{9pt}{\phantomsection\label{\lnlblbase:#1}}}%
+}
+}{}
-- 
2.17.1

Re: [PATCH] formal/dyntickrcu: Mitigate ugliness of tall inline snippets

[Paul E. McKenney]

On Sat, Apr 06, 2019 at 09:31:03AM +0900, Akira Yokosawa wrote:
> >From 8f49523f66fb2281b4337ce57f6502400f0dcb9c Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Sat, 6 Apr 2019 08:53:12 +0900
> Subject: [PATCH] formal/dyntickrcu: Mitigate ugliness of tall inline snippets
> 
> In two-column layout, frames around snippets by \VerbatimN cause
> column breaks of snippets look somewhat ugly.
> 
> As a mitigation, disable frame of \VerbatimN in this particular
> section. Also use \VerbatimU for patch snippets to prevent
> them from breaking other inline snippets in one-column layout.
> 
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> ---
> Hi Paul,
> 
> I know this is not ideal for you, but in one-column layout, the
> column breaks of long snippets does not disturb me so much.
> 
> So this patch disables frame around \VerbatimN for two-column layout
> to restore the looks in the old scheme.
> 
> Isn't this approach acceptable to you, at least as a workaround?

Looks good for now, thank you!  Longer term, I need to break up the
longer listings, but in the short term I need to finish several
changes that I have started.

							Thanx, Paul

>         Thanks, Akira
> --
>  formal/dyntickrcu.tex | 67 ++++++++++++++++++++++++-------------------
>  1 file changed, 38 insertions(+), 29 deletions(-)
> 
> diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
> index c73cdd2f..94093ee9 100644
> --- a/formal/dyntickrcu.tex
> +++ b/formal/dyntickrcu.tex
> @@ -1,5 +1,14 @@
>  % formal/dyntickrcu.tex
>  
> +% Disable frame around VerbatimN in two-column layout
> +\IfTwoColumn{
> +\RecustomVerbatimEnvironment{VerbatimN}{Verbatim}%
> +{numbers=left,numbersep=5pt,xleftmargin=10pt,xrightmargin=0pt,frame=none}
> +\AtBeginEnvironment{VerbatimN}{%
> +\renewcommand{\lnlbl}[1]{\raisebox{0pt}{\phantomsection\label{\lnlblbase:#1}}}%
> +}
> +}{}
> +
>  \subsection{Promela Parable: dynticks and Preemptible RCU}
>  \label{sec:formal:Promela Parable: dynticks and Preemptible RCU}
>  
> @@ -1114,10 +1123,19 @@ states, passing without errors.
>  
>  \subsubsection{Lessons (Re)Learned}
>  \label{sec:formal:Lessons (Re)Learned}
> -\NoIndentAfterThis
>  
> -\begin{listing}[tbp]
> -\begin{VerbatimL}[numbers=none]
> +This effort provided some lessons (re)learned:
> +
> +\begin{enumerate}
> +\item	{\bf Promela and Spin can verify interrupt\slash NMI\-/handler
> +	interactions.}
> +\item	{\bf Documenting code can help locate bugs.}
> +	In this case, the documentation effort located
> +	a misplaced memory barrier in
> +	\co{rcu_enter_nohz()} and \co{rcu_exit_nohz()},
> +	as shown by the following patch.
> +
> +\begin{VerbatimU}
>   static inline void rcu_enter_nohz(void)
>   {
>  +       mb();
> @@ -1131,38 +1149,20 @@ states, passing without errors.
>          __get_cpu_var(dynticks_progress_counter)++;
>  +       mb();
>   }
> -\end{VerbatimL}
> -\caption{Memory-Barrier Fix Patch}
> -\label{lst:formal:Memory-Barrier Fix Patch}
> -\end{listing}
> -
> -\begin{listing}[tbp]
> -\begin{VerbatimL}[numbers=none]
> --       if ((curr - snap) > 2 || (snap & 0x1) == 0)
> -+       if ((curr - snap) > 2 || (curr & 0x1) == 0)
> -\end{VerbatimL}
> -\caption{Variable-Name-Typo Fix Patch}
> -\label{lst:formal:Variable-Name-Typo Fix Patch}
> -\end{listing}
> -
> -This effort provided some lessons (re)learned:
> +\end{VerbatimU}
>  
> -\begin{enumerate}
> -\item	{\bf Promela and Spin can verify interrupt\slash NMI\-/handler
> -	interactions.}
> -\item	{\bf Documenting code can help locate bugs.}
> -	In this case, the documentation effort located
> -	a misplaced memory barrier in
> -	\co{rcu_enter_nohz()} and \co{rcu_exit_nohz()},
> -	as shown by the patch in
> -	Listing~\ref{lst:formal:Memory-Barrier Fix Patch}.
>  \item	{\bf Validate your code early, often, and up to the point
>  	of destruction.}
>  	This effort located one subtle bug in
>  	\co{rcu_try_flip_waitack_needed()}
>  	that would have been quite difficult to test or debug, as
> -	shown by the patch in
> -	Listing~\ref{lst:formal:Variable-Name-Typo Fix Patch}.
> +	shown by the following patch.
> +
> +\begin{VerbatimU}
> +-       if ((curr - snap) > 2 || (snap & 0x1) == 0)
> ++       if ((curr - snap) > 2 || (curr & 0x1) == 0)
> +\end{VerbatimU}
> +
>  \item	{\bf Always verify your verification code.}
>  	The usual way to do this is to insert a deliberate bug
>  	and verify that the verification code catches it.  Of course,
> @@ -1621,3 +1621,12 @@ where an NMI might change shared state at any point during execution of
>  the \IRQ\ functions.
>  
>  Verification can be a good thing, but simplicity is even better.
> +
> +% Restore frame around VerbatimN in two-column layout
> +\IfTwoColumn{
> +\RecustomVerbatimEnvironment{VerbatimN}{Verbatim}%
> +{numbers=left,numbersep=3pt,xleftmargin=5pt,xrightmargin=5pt,frame=single}
> +\AtBeginEnvironment{VerbatimN}{%
> +\renewcommand{\lnlbl}[1]{\raisebox{9pt}{\phantomsection\label{\lnlblbase:#1}}}%
> +}
> +}{}
> -- 
> 2.17.1
> 

[PATCH 0/3] formal/dyntickrcu: Followup changes

[Akira Yokosawa]

Hi Paul,

This is a followup patch set relative to the workaround patch
in this mail thread ("formal/dyntickrcu: Mitigate ugliness around
tall inline snippets").

Looks like you have not pushed it yet, though.

It turns out that I misunderstood the working of \AtBeginEnvironment{}
command, and patch #1 fixes the way to redefine VerbatimN environment.
I wanted to add a Fixes: tag, but I don't have the commit id, so
I put a stub of "xxxxxxxxxxxx" in the change log. Can you replace it
with the actual commit id?

Patches #2 and #3 add references to the git commits of the fixes to
bugs in preemptive RCU found by verification. The actual changes were
a little bit different from what are presented in inline snippets,
but I left the snippets as are.  As they are more than a decade
old, adding references should help the context look more real.

        Thanks, Akira
-- 
Akira Yokosawa (3):
  formal/dyntickrcu: Fix the way to redefine VerbatimN
  RCU.bib: Add entries of git commits of dyntickrcu fixes
  formal/dyntickrcu: Cite git commits of dyntickrcu fixes

 bib/RCU.bib           | 22 ++++++++++++++++++++++
 formal/dyntickrcu.tex | 12 ++++--------
 perfbook.tex          |  5 ++++-
 3 files changed, 30 insertions(+), 9 deletions(-)

-- 
2.17.1

[PATCH 1/3] formal/dyntickrcu: Fix the way to redefine VerbatimN

[Akira Yokosawa]

From 111d908f713435dfd62384eb1cc29a24268537ea Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 8 Apr 2019 21:20:14 +0900
Subject: [PATCH 1/3] formal/dyntickrcu: Fix the way to redefine VerbatimN

It turns out the \AtBeginEnvironment{} command accumulates specified
commands in a hook. By using a length variable within the patching
command, just setting the length is good enough in dyntickruc.tex.

"9pt" in the old code was a typo. It should have been "6pt".

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Fixes: xxxxxxxxxxxx ("formal/dyntickrcu: Mitigate ugliness around tall inline snippets")
---
 formal/dyntickrcu.tex | 8 ++------
 perfbook.tex          | 5 ++++-
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 94093ee9..0c09d1ce 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -4,9 +4,7 @@
 \IfTwoColumn{
 \RecustomVerbatimEnvironment{VerbatimN}{Verbatim}%
 {numbers=left,numbersep=5pt,xleftmargin=10pt,xrightmargin=0pt,frame=none}
-\AtBeginEnvironment{VerbatimN}{%
-\renewcommand{\lnlbl}[1]{\raisebox{0pt}{\phantomsection\label{\lnlblbase:#1}}}%
-}
+\setlength{\lnlblraise}{0pt}
 }{}
 
 \subsection{Promela Parable: dynticks and Preemptible RCU}
@@ -1626,7 +1624,5 @@ Verification can be a good thing, but simplicity is even better.
 \IfTwoColumn{
 \RecustomVerbatimEnvironment{VerbatimN}{Verbatim}%
 {numbers=left,numbersep=3pt,xleftmargin=5pt,xrightmargin=5pt,frame=single}
-\AtBeginEnvironment{VerbatimN}{%
-\renewcommand{\lnlbl}[1]{\raisebox{9pt}{\phantomsection\label{\lnlblbase:#1}}}%
-}
+\setlength{\lnlblraise}{6pt}
 }{}
diff --git a/perfbook.tex b/perfbook.tex
index dd4a8d42..641df90a 100644
--- a/perfbook.tex
+++ b/perfbook.tex
@@ -251,8 +251,11 @@
 %\fvset{fontsize=\scriptsize,numbers=left,numbersep=5pt,xleftmargin=9pt,obeytabs=true,tabsize=2}
 \newcommand{\lnlblbase}{}
 \newcommand{\lnlbl}[1]{\phantomsection\label{\lnlblbase:#1}}
+\newlength{\lnlblraise}
+\setlength{\lnlblraise}{6pt}
 \AtBeginEnvironment{VerbatimN}{%
-\renewcommand{\lnlbl}[1]{\raisebox{6pt}{\phantomsection\label{\lnlblbase:#1}}}%
+\renewcommand{\lnlbl}[1]{%
+\raisebox{\lnlblraise}{\phantomsection\label{\lnlblbase:#1}}}%
 }
 \newcommand{\lnrefbase}{}
 \newcommand{\lnref}[1]{\ref{\lnrefbase:#1}}
-- 
2.17.1

[PATCH 2/3] RCU.bib: Add entries of git commits of dyntickrcu fixes

[Akira Yokosawa]

From eca275e44ff447bdbd397411f363d816bcab25a4 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 9 Apr 2019 00:06:53 +0900
Subject: [PATCH 2/3] RCU.bib: Add entries of git commits of dyntickrcu fixes

These are to be cited in formal/dyntickrcu.tex.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 bib/RCU.bib | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/bib/RCU.bib b/bib/RCU.bib
index 7f0204f7..073b89ef 100644
--- a/bib/RCU.bib
+++ b/bib/RCU.bib
@@ -3063,3 +3063,25 @@ Read-Copy-Update {(RCU)}"
 ,year="2019"
 ,note="\url{https://lkml.org/lkml/2019/2/27/829}"
 }
+
+@unpublished{PaulEMcKenney2008commit:d7c0651390b6
+,Author="Paul E. McKenney"
+,Title="rcu: fix \co{rcu_try_flip_waitack_needed()} to prevent grace-period stall"
+,month="May"
+,day="12"
+,year="2008"
+,note="Git commit:
+\url{https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=d7c0651390b6}"
+,lastchecked="April 6, 2019"
+}
+
+@unpublished{PaulEMcKenney2008commit:ae66be9b71b1
+,Author="Paul E. McKenney"
+,Title="rcu: fix misplaced \co{mb()} in \co{rcu_enter/exit_nohz()}"
+,month="March"
+,day="19"
+,year="2008"
+,note="Git commit:
+\url{https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=ae66be9b71b1}"
+,lastchecked="April 6, 2019"
+}
\ No newline at end of file
-- 
2.17.1

[PATCH 3/3] formal/dyntickrcu: Cite git commits of dyntickrcu fixes

[Akira Yokosawa]

From ce3017c2ee2b9b52501cc5d6f9bf896486fe6ac4 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 9 Apr 2019 00:07:18 +0900
Subject: [PATCH 3/3] formal/dyntickrcu: Cite git commits of dyntickrcu fixes

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

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 0c09d1ce..2ba58cd3 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -1131,7 +1131,7 @@ This effort provided some lessons (re)learned:
 	In this case, the documentation effort located
 	a misplaced memory barrier in
 	\co{rcu_enter_nohz()} and \co{rcu_exit_nohz()},
-	as shown by the following patch.
+	as shown by the following patch~\cite{PaulEMcKenney2008commit:d7c0651390b6}.
 
 \begin{VerbatimU}
  static inline void rcu_enter_nohz(void)
@@ -1154,7 +1154,7 @@ This effort provided some lessons (re)learned:
 	This effort located one subtle bug in
 	\co{rcu_try_flip_waitack_needed()}
 	that would have been quite difficult to test or debug, as
-	shown by the following patch.
+	shown by the following patch~\cite{PaulEMcKenney2008commit:ae66be9b71b1}.
 
 \begin{VerbatimU}
 -       if ((curr - snap) > 2 || (snap & 0x1) == 0)
-- 
2.17.1

Re: [PATCH 0/3] formal/dyntickrcu: Followup changes

[Paul E. McKenney]

On Tue, Apr 09, 2019 at 12:44:20AM +0900, Akira Yokosawa wrote:
> Hi Paul,
> 
> This is a followup patch set relative to the workaround patch
> in this mail thread ("formal/dyntickrcu: Mitigate ugliness around
> tall inline snippets").
> 
> Looks like you have not pushed it yet, though.

You are right, I did miss that step!  Fixed.

> It turns out that I misunderstood the working of \AtBeginEnvironment{}
> command, and patch #1 fixes the way to redefine VerbatimN environment.
> I wanted to add a Fixes: tag, but I don't have the commit id, so
> I put a stub of "xxxxxxxxxxxx" in the change log. Can you replace it
> with the actual commit id?

Done!

> Patches #2 and #3 add references to the git commits of the fixes to
> bugs in preemptive RCU found by verification. The actual changes were
> a little bit different from what are presented in inline snippets,
> but I left the snippets as are.  As they are more than a decade
> old, adding references should help the context look more real.

I reworked #2 a bit to place the new citations in time order (along
with another that I had misplaced).

Queued and this time really pushed!  ;-)  Thank you!!!

						Thanx, Paul

>         Thanks, Akira
> -- 
> Akira Yokosawa (3):
>   formal/dyntickrcu: Fix the way to redefine VerbatimN
>   RCU.bib: Add entries of git commits of dyntickrcu fixes
>   formal/dyntickrcu: Cite git commits of dyntickrcu fixes
> 
>  bib/RCU.bib           | 22 ++++++++++++++++++++++
>  formal/dyntickrcu.tex | 12 ++++--------
>  perfbook.tex          |  5 ++++-
>  3 files changed, 30 insertions(+), 9 deletions(-)
> 
> -- 
> 2.17.1
> 
>