From: "Paul E. McKenney" <paulmck@linux.ibm.com>
To: Akira Yokosawa <akiyks@gmail.com>
Cc: perfbook@vger.kernel.org
Subject: Re: [PATCH] formal/dyntickrcu: Mitigate ugliness of tall inline snippets
Date: Fri, 5 Apr 2019 19:05:39 -0700 [thread overview]
Message-ID: <20190406020539.GY14111@linux.ibm.com> (raw)
In-Reply-To: <1b15d6d0-55da-0fc6-67bb-0f30b4eb5fa9@gmail.com>
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
>
next prev parent reply other threads:[~2019-04-06 2:05 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-04-06 0:31 [PATCH] formal/dyntickrcu: Mitigate ugliness of tall inline snippets Akira Yokosawa
2019-04-06 2:05 ` Paul E. McKenney [this message]
2019-04-08 15:44 ` [PATCH 0/3] formal/dyntickrcu: Followup changes Akira Yokosawa
2019-04-08 15:46 ` [PATCH 1/3] formal/dyntickrcu: Fix the way to redefine VerbatimN Akira Yokosawa
2019-04-08 15:47 ` [PATCH 2/3] RCU.bib: Add entries of git commits of dyntickrcu fixes Akira Yokosawa
2019-04-08 15:48 ` [PATCH 3/3] formal/dyntickrcu: Cite " Akira Yokosawa
2019-04-08 18:42 ` [PATCH 0/3] formal/dyntickrcu: Followup changes Paul E. McKenney
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20190406020539.GY14111@linux.ibm.com \
--to=paulmck@linux.ibm.com \
--cc=akiyks@gmail.com \
--cc=perfbook@vger.kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox