>From 040963d9bd65a17500a5ccff5603505decc1e513 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
Date: Thu, 9 Mar 2017 23:54:32 +0900
Subject: [PATCH 4/5] formal: Convert to 'description'
These lists look better in "description" environment with
"nextline" style. The style is good because of variation of
label lengths. Note that colons at the tails of labels are removed.
Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
---
formal/dyntickrcu.tex | 14 +++++++-------
formal/spinhint.tex | 12 ++++++------
2 files changed, 13 insertions(+), 13 deletions(-)
diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 50e87d8..16d1f73 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -1890,33 +1890,33 @@ the NMI code path will also reference (but not modify) the
\co{dynticks_nesting} variable.
These variables are used as follows:
-\begin{itemize}
-\item \co{dynticks_nesting}:
+\begin{description}[style=nextline]
+\item [\tco{dynticks_nesting}]
This counts the number of reasons that the corresponding
CPU should be monitored for RCU read-side critical sections.
If the CPU is in dynticks-idle mode, then this counts the
irq nesting level, otherwise it is one greater than the
irq nesting level.
-\item \co{dynticks}:
+\item [\tco{dynticks}]
This counter's value is even if the corresponding CPU is
in dynticks-idle mode and there are no irq handlers currently
running on that CPU, otherwise the counter's value is odd.
In other words, if this counter's value is odd, then the
corresponding CPU might be in an RCU read-side critical section.
-\item \co{dynticks_nmi}:
+\item [\tco{dynticks_nmi}]
This counter's value is odd if the corresponding CPU is
in an NMI handler, but only if the NMI arrived while this
CPU was in dyntick-idle mode with no irq handlers running.
Otherwise, the counter's value will be even.
-\item \co{dynticks_snap}:
+\item [\tco{dynticks_snap}]
This will be a snapshot of the \co{dynticks} counter, but
only if the current RCU grace period has extended for too
long a duration.
-\item \co{dynticks_nmi_snap}:
+\item [\tco{dynticks_nmi_snap}]
This will be a snapshot of the \co{dynticks_nmi} counter, but
again only if the current RCU grace period has extended for too
long a duration.
-\end{itemize}
+\end{description}
If both \co{dynticks} and \co{dynticks_nmi} have taken on an even
value during a given time interval, then the corresponding CPU has
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 906de31..eb029ca 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -389,10 +389,10 @@ elaborate examples.
Given a source file \path{qrcu.spin}, one can use the following commands:
-\begin{itemize}
-\item \co{spin -a qrcu.spin}
+\begin{description}[style=nextline]
+\item [\tco{spin -a qrcu.spin}]
Create a file \path{pan.c} that fully searches the state machine.
-\item \co{cc -DSAFETY -o pan pan.c}
+\item [\tco{cc -DSAFETY -o pan pan.c}]
Compile the generated state-machine search. The \co{-DSAFETY}
generates optimizations that are appropriate if you have only
assertions (and perhaps \co{never} statements). If you have
@@ -405,7 +405,7 @@ Given a source file \path{qrcu.spin}, one can use the following commands:
An example situation where you cannot use \co{-DSAFETY} is
when checking for livelocks (AKA ``non-progress cycles'')
via \co{-DNP}.
-\item \co{./pan}
+\item [\tco{./pan}]
This actually searches the state space. The number of states
can reach into the tens of millions with very small state
machines, so you will need a machine with large memory.
@@ -431,13 +431,13 @@ Given a source file \path{qrcu.spin}, one can use the following commands:
you will also need the \co{-a} argument.
% forward reference to model: formal.2009.02.19a in
% /home/linux/git/userspace-rcu/formal-model.
-\item \co{spin -t -p qrcu.spin}
+\item [\tco{spin -t -p qrcu.spin}]
Given \co{trail} file output by a run that encountered an
error, output the sequence of steps leading to that error.
The \co{-g} flag will also include the values of changed
global variables, and the \co{-l} flag will also include
the values of changed local variables.
-\end{itemize}
+\end{description}
\subsubsection{Promela Peculiarities}
\label{sec:formal:Promela Peculiarities}
--
2.7.4
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
