[PATCH 0/7] Break and capitalize after colon, take three

[PATCH 0/7] Break and capitalize after colon, take three

[Akira Yokosawa]

Hi Paul,

Here are colon related changes though Chapter 17.
They don't alter appearance except for capitalization and minor
changes in Patch 3/7 mentioned below.

In Patch 2/7, "dynticks" behind a colon is enclosed by plain {}.
In Patch 3/7, messages from pan are enclosed by \co{}.
In Patch 6/7, "ppc64" behind a colon is enclosed by plain {}.
These are to escape checks by to-be-updated scripts.

The other patches are (hopefully) trivial.

My hope is to complete similar changes in Appendices soon.

FWIW, I have been working on the improvement of appearance of CJK
translations in kerneldoc (pdfdocs) recently [1], hence my low activity
in perfbook.

[1]: [PATCH v4 0/9] docs: pdfdocs: Improve font choice in CJK translations
    https://lore.kernel.org/linux-doc/39d0fb0f-b248-bca4-2dac-df69e8d697b1@gmail.com/#t

        Thanks, Akira
--
Akira Yokosawa (7):
  debugging: Break and capitalize after colon
  formal: Break and capitalize after colon
  formal: Use \co{} for pan messages containing colon
  together: Break and capitalize after colon
  advsync: Break and capitalize after colon
  memorder: Break and capitalize after colon
  easy, future: Break and capitalize after colon

 advsync/advsync.tex      |  31 +++++++-----
 advsync/rt.tex           |  72 +++++++++++++++------------
 debugging/debugging.tex  |  92 +++++++++++++++++++----------------
 easy/easy.tex            |   6 +--
 formal/axiomatic.tex     |   3 +-
 formal/dyntickrcu.tex    |  17 ++++---
 formal/formal.tex        |   7 ++-
 formal/ppcmem.tex        |   4 +-
 formal/spinhint.tex      |  44 ++++++++++-------
 future/cpu.tex           |   5 +-
 future/formalregress.tex |  24 +++++----
 future/htm.tex           |   8 +--
 future/tm.tex            |  30 +++++++-----
 memorder/memorder.tex    | 102 +++++++++++++++++++++++----------------
 together/applyrcu.tex    |   6 +--
 together/count.tex       |  10 ++--
 together/refcnt.tex      |   2 +-
 17 files changed, 269 insertions(+), 194 deletions(-)

-- 
2.17.1

[PATCH 1/7] debugging: Break and capitalize after colon

[Akira Yokosawa]

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 debugging/debugging.tex | 92 +++++++++++++++++++++++------------------
 1 file changed, 51 insertions(+), 41 deletions(-)

diff --git a/debugging/debugging.tex b/debugging/debugging.tex
index 87e21135..10b3f801 100644
--- a/debugging/debugging.tex
+++ b/debugging/debugging.tex
@@ -108,8 +108,9 @@ of meeting.
 Perhaps the set of software assistants are now available on smartphones
 will fare better, but as of 2021 reviews are mixed.
 That said, the developers working on them by all accounts still develop
-the old way: The assistants might well benefit end users, but not so
-much their own developers.
+the old way:
+The assistants might well benefit end users, but not so much their own
+developers.
 
 This human love of fragmentary plans deserves more explanation,
 especially given that it is a classic two-edged sword.
@@ -118,7 +119,8 @@ the person carrying out the plan will have (1)~common sense and (2)~a good
 understanding of the intent and requirements driving the plan.
 This latter assumption is especially likely to hold in the common case
 where the person doing the planning and the person carrying out the plan
-are one and the same:  In this case, the plan will be revised almost
+are one and the same:
+In this case, the plan will be revised almost
 subconsciously as obstacles arise, especially when that person has the
 a good understanding of the problem at hand.
 In fact, the love of fragmentary plans has served human beings well,
@@ -149,8 +151,8 @@ to start a difficult but worthwhile project.\footnote{
 	There are some famous exceptions to this rule of thumb.
 	Some people take on difficult or risky projects in order to at
 	least a temporarily escape from their depression.
-	Others have nothing to lose: the project is literally a matter
-	of life or death.}
+	Others have nothing to lose:
+	The project is literally a matter of life or death.}
 
 \QuickQuiz{
 	When in computing is it necessary to follow a
@@ -308,9 +310,10 @@ validation is just job for you.
 	Of course, one way to economize on destructiveness is to
 	generate the tests with the to-be-tested source code at hand,
 	which is called white-box testing (as opposed to black-box testing).
-	However, this is no panacea: You will find that it is all too
-	easy to find your thinking limited by what the program can handle,
-	thus failing to generate truly destructive inputs.
+	However, this is no panacea:
+	You will find that it is all too easy to find your thinking
+	limited by what the program can handle, thus failing to generate
+	truly destructive inputs.
 }\QuickQuizEnd
 
 But perhaps you are a super-programmer whose code is always perfect
@@ -595,7 +598,8 @@ asking a few questions:
 \item	Exactly when are they going to look?
 \end{enumerate}
 
-I was lucky:  There was someone out there who wanted the functionality
+I was lucky:
+There was someone out there who wanted the functionality
 provided by my patch, who had long experience with distributed filesystems,
 and who looked at my patch almost immediately.
 If no one had looked at my patch, there would have been no review, and
@@ -619,8 +623,9 @@ Still others test maintainer trees, which often have a similar time delay.
 Quite a few people don't test code until it is committed to mainline,
 or the master source tree (Linus's tree in the case of the Linux kernel).
 If your maintainer won't accept your patch until it has been tested,
-this presents you with a deadlock situation: your patch won't be accepted
-until it is tested, but it won't be tested until it is accepted.
+this presents you with a deadlock situation:
+Your patch won't be accepted until it is tested, but it won't be tested
+until it is accepted.
 Nevertheless, people who test mainline code are still relatively
 aggressive, given that many people and organizations do not test code
 until it has been pulled into a Linux distro.
@@ -648,9 +653,9 @@ you already have a good test suite.
 When all else fails, add a \co{printk()}!
 Or a \co{printf()}, if you are working with user-mode C-language applications.
 
-The rationale is simple: If you cannot figure out how execution reached
-a given point in the code, sprinkle print statements earlier in the
-code to work out what happened.
+The rationale is simple:
+If you cannot figure out how execution reached a given point in the code,
+sprinkle print statements earlier in the code to work out what happened.
 You can get a similar effect, and with more convenience and flexibility,
 by using a debugger such as gdb (for user applications) or kgdb
 (for debugging Linux kernels).
@@ -692,9 +697,9 @@ what it knows is almost always way more than your head can hold.
 For this reason, high-quality test suites normally come with sophisticated
 scripts to analyze the voluminous output.
 But beware---scripts will only notice what you tell them to.
-My rcutorture scripts are a case in point: Early versions of those
-scripts were quite satisfied with a test run in which RCU grace periods
-stalled indefinitely.
+My rcutorture scripts are a case in point:
+Early versions of those scripts were quite satisfied with a test run
+in which RCU grace periods stalled indefinitely.
 This of course resulted in the scripts being modified to detect RCU
 grace-period stalls, but this does not change the fact that the scripts
 will only detect problems that I make them detect.
@@ -829,8 +834,8 @@ This section covers inspection, walkthroughs, and self-inspection.
 \label{sec:debugging:Inspection}
 
 Traditionally, formal code inspections take place in face-to-face meetings
-with formally defined roles: moderator, developer, and one or two other
-participants.
+with formally defined roles:
+Moderator, developer, and one or two other participants.
 The developer reads through the code, explaining what it is doing and
 why it works.
 The one or two other participants ask questions and raise issues,
@@ -865,15 +870,18 @@ by the author's invalid assumptions, and who might also test the code.
 	\begin{enumerate}
 	\item	Testing for a non-zero denominator will prevent
 		divide-by-zero errors.
-		(Hint: Suppose that the test uses 64-bit arithmetic
+		(Hint:
+		Suppose that the test uses 64-bit arithmetic
 		but that the division uses 32-bit arithmetic.)
 	\item	Userspace can be trusted to zero out versioned data
 		structures used to communicate with the kernel.
-		(Hint: Sometimes userspace has no idea how large the
+		(Hint:
+		Sometimes userspace has no idea how large the
 		data structure is.)
 	\item	Outdated TCP duplicate selective acknowledgement (D-SACK)
 		packets can be completely ignored.
-		(Hint: These packets might also contain other information.)
+		(Hint:
+		These packets might also contain other information.)
 	\item	All CPUs are little-endian.
 	\item	Once a data structure is no longer needed, all of its
 		memory may be immediately freed.
@@ -1100,9 +1108,9 @@ Here are some time-tested ways of accomplishing this:
 	the problem.
 \item	Make extremely disciplined use of parallel-programming
 	primitives, so that the resulting code is easily seen to be correct.
-	But beware: It is always tempting to break the rules
-	``just a little bit'' to gain better performance or
-	scalability.
+	But beware:
+	It is always tempting to break the rules ``just a little bit''
+	to gain better performance or scalability.
 	Breaking the rules often results in general breakage.
 	That is, unless you carefully do the paperwork described in this
 	section.
@@ -1163,7 +1171,8 @@ Congratulations!!!
 \begin{figure}
 \centering
 \resizebox{3in}{!}{\includegraphics{cartoons/r-2014-Passed-the-stress-test}}
-\caption{Passed on Merits?  Or Dumb Luck?}
+\caption{Passed on Merits?
+			   Or Dumb Luck?}
 \ContributedBy{Figure}{fig:cpu:Passed-the-stress-test}{Melissa Broussard}
 \end{figure}
 
@@ -1213,11 +1222,11 @@ is required to attain absolute certainty.
 	Of course, if your code is small enough, formal validation
 	may be helpful, as discussed in
 	\cref{chp:Formal Verification}.
-	But beware: formal validation of your code will not find
-	errors in your assumptions, misunderstanding of the
-	requirements, misunderstanding of the software or hardware
-	primitives you use, or errors that you did not think to construct
-	a proof for.
+	But beware:
+	Formal validation of your code will not find errors in your
+	assumptions, misunderstanding of the requirements,
+	misunderstanding of the software or hardware primitives you use,
+	or errors that you did not think to construct a proof for.
 }\QuickQuizEnd
 
 But suppose that we are willing to give up absolute certainty in favor
@@ -1646,7 +1655,7 @@ The next section discusses counter-intuitive ways of improving this situation.
 \label{sec:debugging:Hunting Heisenbugs}
 
 This line of thought also helps explain heisenbugs:
-adding tracing and assertions can easily reduce the probability
+Adding tracing and assertions can easily reduce the probability
 of a bug appearing, which
 is why extremely lightweight tracing and assertion mechanism are
 so critically important.
@@ -1768,8 +1777,8 @@ or removal of a given delay.
 	Shame on you!
 	This is but one reason why you are supposed to keep the commits small.
 
-	And that is your answer: Break up the commit into bite-sized
-	pieces and bisect the pieces.
+	And that is your answer:
+	Break up the commit into bite-sized pieces and bisect the pieces.
 	In my experience, the act of breaking up the commit is often
 	sufficient to make the bug painfully obvious.
 }\QuickQuizEnd
@@ -1828,7 +1837,7 @@ If the program is structured such that it is difficult or impossible
 to apply much stress to a subsystem that is under suspicion,
 a useful anti-heisenbug is a stress test that tests that subsystem in
 isolation.
-The Linux kernel's rcutorture module takes exactly this approach with RCU:
+The Linux kernel's rcutorture module takes exactly this approach with RCU\@:
 Applying more stress to RCU than is feasible in a production environment
 increases the probability that RCU bugs will be found during testing
 rather than in production.\footnote{
@@ -2326,8 +2335,8 @@ the POSIX \co{sched_setscheduler()} system call.
 However, note that if you do this, you are implicitly taking on
 responsibility for avoiding infinite loops, because otherwise
 your test can prevent part of the kernel from functioning.
-This is an example of the Spiderman Principle: ``With great
-power comes great responsibility.''
+This is an example of the Spiderman Principle:
+``With great power comes great responsibility.''
 And although the default real-time throttling settings often address
 such problems, they might do so by causing your real-time threads
 to miss their deadlines.
@@ -2485,9 +2494,9 @@ larger measurements suggests that sorting the measurements in increasing
 order is likely to be productive.\footnote{
 	To paraphrase the old saying, ``Sort first and ask questions later.''}
 The fact that the measurement uncertainty is known allows us to accept
-measurements within this uncertainty of each other:  If the effects of
-interference are large compared to this uncertainty, this will ease
-rejection of bad data.
+measurements within this uncertainty of each other:
+If the effects of interference are large compared to this uncertainty,
+this will ease rejection of bad data.
 Finally, the fact that some fraction (for example, one third) can be
 assumed to be good allows us to blindly accept the first portion of the
 sorted list, and this data can then be used to gain an estimate of the
@@ -2591,7 +2600,8 @@ If \clnref{chk_max} determines that the candidate data value would exceed the
 lower bound on the upper bound (\co{maxdelta}) \emph{and}
 that the difference between the candidate data value
 and its predecessor exceeds the trend-break difference (\co{maxdiff}),
-then \clnref{break} exits the loop: We have the full good set of data.
+then \clnref{break} exits the loop:
+We have the full good set of data.
 
 \Clnrefrange{comp_stat:b}{comp_stat:e} then compute and print
 statistics.
-- 
2.17.1

[PATCH 2/7] formal: Break and capitalize after colon

[Akira Yokosawa]

Note: "dynticks" behind a colon is enclosed in plain {}.
This is to exclude it from checkscript.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/axiomatic.tex  |  3 ++-
 formal/dyntickrcu.tex | 17 +++++++++--------
 formal/formal.tex     |  7 +++++--
 formal/ppcmem.tex     |  4 ++--
 formal/spinhint.tex   | 40 ++++++++++++++++++++++++----------------
 5 files changed, 42 insertions(+), 29 deletions(-)

diff --git a/formal/axiomatic.tex b/formal/axiomatic.tex
index 12bba26c..175af54e 100644
--- a/formal/axiomatic.tex
+++ b/formal/axiomatic.tex
@@ -228,7 +228,8 @@ And in this case, the \co{herd} tool's output features the string
 	5 & 4.905 \\
 	\bottomrule
 \end{tabular}
-\caption{Locking: Modeling vs.\@ Emulation Time (s)}
+\caption{Locking:
+		  Modeling vs.\@ Emulation Time (s)}
 \label{tab:formal:Locking: Modeling vs. Emulation Time (s)}
 \end{table}
 
diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 6c4d2d6d..5113fd09 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -9,7 +9,8 @@
 \setlength{\lnlblraise}{0pt}
 }{}
 
-\subsection{Promela Parable: dynticks and Preemptible RCU}
+\subsection{Promela Parable:
+			     {dynticks} and Preemptible RCU}
 \label{sec:formal:Promela Parable: dynticks and Preemptible RCU}
 
 In early 2008, a preemptible variant of RCU was accepted into
@@ -624,10 +625,10 @@ over which RCU readers could plausibly persist.
 }\QuickQuizAnswer{
 	Recall that Promela and Spin trace out
 	every possible sequence of state changes.
-	Therefore, timing is irrelevant: Promela/Spin will be quite
-	happy to jam the entire rest of the model between those two
-	statements unless some state variable specifically prohibits
-	doing so.
+	Therefore, timing is irrelevant:
+	Promela/Spin will be quite happy to jam the entire rest of
+	the model between those two statements unless some state
+	variable specifically prohibits doing so.
 }\QuickQuizEnd
 
 The \co{dyntick_nohz()} Promela process implements
@@ -822,10 +823,10 @@ We also need to handle interrupts, a task taken up in the next section.
 
 There are a couple of ways to model interrupts in Promela:
 \begin{enumerate}
-\item	using C-preprocessor tricks to insert the interrupt handler
+\item	Using C-preprocessor tricks to insert the interrupt handler
 	between each and every statement of the \co{dynticks_nohz()}
 	process, or
-\item	modeling the interrupt handler with a separate process.
+\item	Modeling the interrupt handler with a separate process.
 \end{enumerate}
 
 A bit of thought indicated that the second approach would have a
@@ -1020,7 +1021,7 @@ set the \co{in_dyntick_irq} variable that is used by the
 variable, but only when in the outermost interrupt handler.
 
 \Clnref{cnd_ex} has the do-loop conditional for interrupt-exit modeling:
-as long as we have exited fewer interrupts than we have entered, it is
+As long as we have exited fewer interrupts than we have entered, it is
 legal to exit another interrupt.
 \Clnrefrange{atm3:b}{atm3:e}
 check the safety criterion, but only if we are exiting
diff --git a/formal/formal.tex b/formal/formal.tex
index 0f954861..ac897b9e 100644
--- a/formal/formal.tex
+++ b/formal/formal.tex
@@ -190,8 +190,11 @@ and the consequence that they imply:
 \end{description}
 
 From this viewpoint, any advances in validation and verification can
-have but two effects: (1)~An increase in the number of trivial programs or
-(2)~A decrease in the number of reliable programs.
+have but two effects:
+\begin{enumerate*}[(1)]
+\item An increase in the number of trivial programs or
+\item A decrease in the number of reliable programs.
+\end{enumerate*}
 Of course, the human race's increasing reliance on multicore systems and
 software provides extreme motivation for a very sharp increase in the
 number of trivial programs.
diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index f58f3700..8664ee4e 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -295,8 +295,8 @@ where the \co{...} stands for voluminous making-progress output.
 The list of states includes \co{0:r3=0; 1:r3=0;}, indicating once again
 that the old PowerPC implementation of \co{atomic_add_return()} does
 not act as a full barrier.
-The ``Sometimes'' on the last line confirms this: the assertion triggers
-for some executions, but not all of the time.
+The ``Sometimes'' on the last line confirms this:
+The assertion triggers for some executions, but not all of the time.
 
 \begin{listing}
 \begin{VerbatimL}[numbers=none,xleftmargin=0pt]
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 35fe895b..16f216e0 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -60,7 +60,8 @@ The remainder of this section describes how to use Promela to debug
 parallel algorithms, starting with simple examples and progressing to
 more complex uses.
 
-\subsubsection{Warm-Up: Non-Atomic Increment}
+\subsubsection{Warm-Up:
+			Non-Atomic Increment}
 \label{sec:formal:Warm-Up: Non-Atomic Increment}
 
 \begin{fcvref}[ln:formal:promela:increment:whole]
@@ -96,7 +97,8 @@ which is executed first.
 while \clnrefrange{assert:b}{assert:e}
 perform the assertion.
 Both are atomic blocks in order to avoid unnecessarily increasing
-the state space: because they are not part of the algorithm proper,
+the state space:
+Because they are not part of the algorithm proper,
 we lose no verification coverage by making them atomic.
 
 The \co{do-od} construct on \clnrefrange{dood1:b}{dood1:e}
@@ -148,8 +150,8 @@ assertion was violated.
 The ``Warning'' line reiterates that all was not well with our model.
 The second paragraph describes the type of state-search being carried out,
 in this case for assertion violations and invalid end states.
-The third paragraph gives state-size statistics: this small model had only
-45 states.
+The third paragraph gives state-size statistics:
+This small model had only 45 states.
 The final line shows memory usage.
 
 The \co{trail} file may be rendered human-readable as follows:
@@ -173,7 +175,8 @@ incrementer processes, both of which first fetched the counter,
 then both incremented and stored it, losing a count.
 The assertion then triggered, after which the global state is displayed.
 
-\subsubsection{Warm-Up: Atomic Increment}
+\subsubsection{Warm-Up:
+			Atomic Increment}
 \label{sec:formal:Warm-Up: Atomic Increment}
 
 It is easy to fix this example by placing the body of the incrementer
@@ -477,7 +480,8 @@ atomic {
 
 Now we are ready for further examples.
 
-\subsection{Promela Example: Locking}
+\subsection{Promela Example:
+			     Locking}
 \label{sec:formal:Promela Example: Locking}
 
 \begin{fcvref}[ln:formal:promela:lock:whole]
@@ -518,7 +522,7 @@ In any given Promela state, all processes agree on both the current
 state and the order of state changes that caused us to arrive at
 the current state.
 This is analogous to the ``sequentially consistent'' memory model
-used by a few computer systems (such as 1990s MIPS and PA-RISC).
+used by a few computer systems (such as 1990s MIPS and PA-RISC\@).
 As noted earlier, and as will be seen in a later example,
 weak memory ordering must be explicitly coded.
 
@@ -613,7 +617,8 @@ As expected, this run has no assertion failures (``errors: 0'').
 }\QuickQuizEndE
 }
 
-\subsection{Promela Example: QRCU}
+\subsection{Promela Example:
+			     QRCU}
 \label{sec:formal:Promela Example: QRCU}
 
 This final example demonstrates a real-world use of Promela on Oleg
@@ -691,9 +696,9 @@ The \co{readerprogress} array elements have values as follows,
 indicating the state of the corresponding reader:
 
 \begin{enumerate}[label={\arabic*}:,start=0,itemsep=0pt]
-\item	not yet started.
-\item	within QRCU read-side critical section.
-\item	finished with QRCU read-side critical section.
+\item	Not yet started.
+\item	Within QRCU read-side critical section.
+\item	Finished with QRCU read-side critical section.
 \end{enumerate}
 
 Finally, the \co{mutex} variable is used to serialize updaters' slowpaths.
@@ -1073,8 +1078,8 @@ state visible to either readers or other updaters.
 This means that any sequences of state changes can be carried
 out serially by a single updater due to the fact that Promela does a full
 state-space search.
-Therefore, at most two updaters are required: one to change state
-and a second to become confused.
+Therefore, at most two updaters are required:
+One to change state and a second to become confused.
 
 The situation with the readers is less clear-cut, as each reader
 does only a single read-side critical section then terminates.
@@ -1084,7 +1089,8 @@ in the counters.
 This is a fruitful avenue of investigation, in fact, it leads to
 the full proof of correctness described in the next section.
 
-\subsubsection{Alternative Approach: Proof of Correctness}
+\subsubsection{Alternative Approach:
+				     Proof of Correctness}
 \label{sec:formal:Alternative Approach: Proof of Correctness}
 
 An informal proof~\cite{PaulMcKenney2007QRCUpatch}
@@ -1128,7 +1134,8 @@ follows:
 Of course, not all parallel algorithms have such simple proofs.
 In such cases, it may be necessary to enlist more capable tools.
 
-\subsubsection{Alternative Approach: More Capable Tools}
+\subsubsection{Alternative Approach:
+				     More Capable Tools}
 \label{sec:formal:Alternative Approach: More Capable Tools}
 
 Although Promela and Spin are quite useful,
@@ -1153,7 +1160,8 @@ algorithms.
 
 Another approach might be to divide and conquer.
 
-\subsubsection{Alternative Approach: Divide and Conquer}
+\subsubsection{Alternative Approach:
+				     Divide and Conquer}
 \label{sec:formal:Alternative Approach: Divide and Conquer}
 
 It is often possible to break down a larger parallel algorithm into
-- 
2.17.1

[PATCH 3/7] formal: Use \co{} for pan messages containing colon

[Akira Yokosawa]

Messages inside \co{} will be ignored by the check scripts.

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

diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 16f216e0..c1fe2d40 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -275,7 +275,7 @@ Given a source file \path{qrcu.spin}, one can use the following commands:
 	10.5\,GB of memory even with the \co{-DCOLLAPSE} flag.
 
 	If you see a message from \co{./pan} saying:
-	``error: max search depth too small'', you need to increase
+	``\co{error: max search depth too small}'', you need to increase
 	the maximum depth by a \co{-mN} option for a complete search.
 	The default is \co{-m10000}.
 
@@ -582,7 +582,7 @@ cc -DSAFETY -o pan pan.c
 
 The output will look something like that shown in
 \cref{lst:formal:Output for Spinlock Test}.
-As expected, this run has no assertion failures (``errors: 0'').
+As expected, this run has no assertion failures (``\co{errors: 0}'').
 
 \QuickQuizSeries{%
 \QuickQuizB{
-- 
2.17.1

[PATCH 4/7] together: Break and capitalize after colon

[Akira Yokosawa]

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 together/applyrcu.tex |  6 +++---
 together/count.tex    | 10 +++++-----
 together/refcnt.tex   |  2 +-
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/together/applyrcu.tex b/together/applyrcu.tex
index 1f157a21..975a10a6 100644
--- a/together/applyrcu.tex
+++ b/together/applyrcu.tex
@@ -394,9 +394,9 @@ data element shown in
 The \co{meas_1}, \co{meas_2}, and \co{meas_3} fields are a set
 of correlated measurements that are updated periodically.
 It is critically important that readers see these three values from
-a single measurement update: If a reader sees an old value of
-\co{meas_1} but new values of \co{meas_2} and \co{meas_3}, that
-reader will become fatally confused.
+a single measurement update:
+If a reader sees an old value of \co{meas_1} but new values of
+\co{meas_2} and \co{meas_3}, that reader will become fatally confused.
 How can we guarantee that readers will see coordinated sets of these
 three values?\footnote{
 	This situation is similar to that described in
diff --git a/together/count.tex b/together/count.tex
index 882e975c..2650f5ba 100644
--- a/together/count.tex
+++ b/together/count.tex
@@ -46,16 +46,16 @@ which would be a severe bottleneck on large systems.
 
 Another approach is to ``just say no'' to counting, following the example
 of the \co{noatime} mount option.
-If this approach is feasible, it is clearly the best:  After all, nothing
-is faster than doing nothing.
+If this approach is feasible, it is clearly the best:
+After all, nothing is faster than doing nothing.
 If the lookup count cannot be dispensed with, read on!
 
 Any of the counters from \cref{chp:Counting}
 could be pressed into service, with the statistical counters described in
 \cref{sec:count:Statistical Counters} being perhaps the most common choice.
-However, this results in a large memory footprint: The number of counters
-required is the number of data elements multiplied by the number of
-threads.
+However, this results in a large memory footprint:
+The number of counters required is the number of data elements multiplied
+by the number of threads.
 
 If this memory overhead is excessive, then one approach is to keep
 per-core or even per-socket counters rather than per-CPU counters,
diff --git a/together/refcnt.tex b/together/refcnt.tex
index 5cdde7cc..b30acf5b 100644
--- a/together/refcnt.tex
+++ b/together/refcnt.tex
@@ -139,7 +139,7 @@ contain memory barriers, and all checked acquisition operations also
 contain memory barriers.
 Therefore, cases ``CA'' and ``MCA'' are equivalent to ``CAM'', so that
 there are sections below for only the first four cases and the sixth case:
-``$-$'', ``A'', ``AM'', ``CAM'', and ``M''.
+``$-$'', ``A'', ``AM'', ``CAM'', and ``M\@''.
 Later sections describe optimizations that can improve performance
 if reference acquisition and release is very frequent, and the
 reference count need be checked for zero only very rarely.
-- 
2.17.1

[PATCH 5/7] advsync: Break and capitalize after colon

[Akira Yokosawa]

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 advsync/advsync.tex | 31 +++++++++++--------
 advsync/rt.tex      | 72 ++++++++++++++++++++++++++-------------------
 2 files changed, 61 insertions(+), 42 deletions(-)

diff --git a/advsync/advsync.tex b/advsync/advsync.tex
index 48a71b74..f8750250 100644
--- a/advsync/advsync.tex
+++ b/advsync/advsync.tex
@@ -217,7 +217,8 @@ Although mutual exclusion is required to dequeue a single element
 (so that dequeue is blocking), it is possible to carry out a non-blocking
 removal of the entire contents of the queue.
 What is not possible is to dequeue any given element in a non-blocking
-manner: The enqueuer might have failed between \clnref{tail,pred} of the
+manner:
+The enqueuer might have failed between \clnref{tail,pred} of the
 listing, so that the element in question is only partially enqueued.
 This results in a half-NBS algorithm where enqueues are NBS but
 dequeues are blocking.
@@ -304,8 +305,9 @@ Here is one way that this scenario might play out:
 
 Note that both pushes and the popall all ran successfully despite the
 reuse of \Node{A}'s memory.
-This is an unusual property: Most data structures require protection
-against what is often called the ABA problem.
+This is an unusual property:
+Most data structures require protection against what is often called
+the ABA problem.
 
 But this property holds only for algorithm written in assembly
 language.
@@ -374,9 +376,12 @@ largely orthogonal to those that form the basis of real-time programming:
 	unconditional.
 \item	Real-time forward-progress guarantees are often conditioned on
 	environmental constraints, for example, only being honored:
-	(1)~For the highest-priority tasks,
-	(2)~When each CPU spends at least a certain fraction of its time idle,
-	and (3)~When I/O rates are below some specified maximum.
+	\begin{enumerate*}[(1)]
+	\item For the highest-priority tasks,
+	\item When each CPU spends at least a certain fraction of its time idle,
+	and
+	\item When I/O rates are below some specified maximum.
+	\end{enumerate*}
 	In contrast, NBS's forward-progress
 	guarantees are often unconditional, although recent NBS work
 	accommodates conditional
@@ -542,15 +547,17 @@ constraint that is often respected in practice.
 Other sets of constraints can permit blocking algorithms to
 achieve deterministic real-time response.
 For example, given:
-(1)~Fair locks granted in FIFO order within a given priority level,
-(2)~Priority inversion avoidance (for example, priority
+\begin{enumerate*}[(1)]
+\item Fair locks granted in FIFO order within a given priority level,
+\item Priority inversion avoidance (for example, priority
 inheritance~\cite{Takada:1995:RSN:527074.828566,Cai-DongWang1996PrioInherLock}
 or priority ceiling),
-(3)~A bounded number of threads,
-(4)~Bounded critical section durations,
-(5)~Bounded load,
+\item A bounded number of threads,
+\item Bounded critical section durations,
+\item Bounded load,
 and
-(6)~Absence of fail-stop bugs,
+\item Absence of fail-stop bugs,
+\end{enumerate*}
 lock-based applications can provide deterministic
 response times~\cite{BjoernBrandenburgPhD,DipankarSarma2004OLSscalability}.
 This approach of course blurs the distinction between blocking and wait-free
diff --git a/advsync/rt.tex b/advsync/rt.tex
index 3e62b6cb..24ba2a66 100644
--- a/advsync/rt.tex
+++ b/advsync/rt.tex
@@ -103,7 +103,8 @@ But your adversary can always get a bigger hammer.
 \begin{figure}
 \centering
 \resizebox{3in}{!}{\includegraphics{cartoons/realtime-lifesupport-nobomb}}
-\caption{Real-Time Response: Hardware Matters}
+\caption{Real-Time Response:
+			     Hardware Matters}
 \ContributedBy{Figure}{fig:advsync:Real-Time Response: Hardware Matters}{Melissa Broussard}
 \end{figure}
 
@@ -133,7 +134,8 @@ it can alert the hospital staff.
 \begin{figure*}
 \centering
 \resizebox{\textwidth}{!}{\rotatebox{90}{\includegraphics{cartoons/realtime-lazy-crop}}}
-\caption{Real-Time Response: Notification Insufficient}
+\caption{Real-Time Response:
+			     Notification Insufficient}
 \ContributedBy{Figure}{fig:advsync:Real-Time Response: Notification Insufficient}{Melissa Broussard}
 \end{figure*}
 
@@ -250,8 +252,9 @@ number of heating and cooling systems can counter the effects of temperature.
 In extreme cases, triple modular redundancy can reduce the probability that
 a fault in one part of the system will result in incorrect behavior from
 the overall system.
-However, all of these methods have one thing in common:  Although they
-can reduce the probability of failure, they cannot reduce it to zero.
+However, all of these methods have one thing in common:
+Although they can reduce the probability of failure, they cannot reduce
+it to zero.
 
 These environmental challenges are often met via robust hardware, however,
 the workload and application constraints in the next two sections are
@@ -374,21 +377,23 @@ have a much higher probability of missing tight deadlines.
 Similarly, a read from a tightly coupled solid-state disk (SSD) could be
 expected to complete much more quickly than that same read to an old-style
 USB-connected rotating-rust disk drive.\footnote{
-	Important safety tip:  Worst-case response times from USB devices
-	can be extremely long.
+	Important safety tip:
+	Worst-case response times from USB devices can be extremely long.
 	Real-time systems should therefore take care to place any USB
 	devices well away from critical paths.}
 
 Some real-time applications pass through different phases of operation.
 For example, a real-time system controlling a plywood lathe that peels
 a thin sheet of wood (called ``veneer'') from a spinning log must:
-(1)~Load the log into the lathe,
-(2)~Position the log on the lathe's chucks so as to expose the largest
+\begin{enumerate*}[(1)]
+\item Load the log into the lathe,
+\item Position the log on the lathe's chucks so as to expose the largest
 cylinder contained within that log to the blade,
-(3)~Start spinning the log,
-(4)~Continuously vary the knife's position so as to peel the log into veneer,
-(5)~Remove the remaining core of the log that is too small to peel, and
-(6)~Wait for the next log.
+\item Start spinning the log,
+\item Continuously vary the knife's position so as to peel the log into veneer,
+\item Remove the remaining core of the log that is too small to peel, and
+\item Wait for the next log.
+\end{enumerate*}
 Each of these six phases of operation might well have its own set of
 deadlines and environmental constraints,
 for example, one would expect phase~4's deadlines to be much more severe
@@ -1075,8 +1080,8 @@ might starve the interrupt handler, for example, preventing networking
 code from running, in turn making it very difficult to debug the problem.
 Developers must therefore take great care when writing high-priority
 real-time code.
-This has been dubbed the \emph{Spiderman principle}: With great power
-comes great responsibility.
+This has been dubbed the \emph{Spiderman principle}:
+With great power comes great responsibility.
 
 \paragraph{Priority inheritance} is used to handle priority inversion,
 which can be caused by, among other things, locks acquired by
@@ -1177,12 +1182,15 @@ priority-inversion conundrum:
 	However, this approach clearly and severely limits read-side
 	scalability.
 	The Linux kernel's \rt\ patchset was long able to live with this
-	limitation for several reasons: (1)~Real-time systems have
-	traditionally been relatively small, (2)~Real-time systems
-	have generally focused on process control, thus being unaffected
-	by scalability limitations in the I/O subsystems, and
-	(3)~Many of the Linux kernel's reader-writer locks have been
+	limitation for several reasons:
+	\begin{enumerate*}[(1)]
+	\item Real-time systems have traditionally been relatively small,
+	\item Real-time systems have generally focused on process control,
+	thus being unaffected by scalability limitations in the
+	I/O subsystems, and
+	\item Many of the Linux kernel's reader-writer locks have been
 	converted to RCU\@.
+	\end{enumerate*}
 
 	However, the day came when it was absolutely necessary to
 	permit concurrent readers, as described in the text following
@@ -1267,12 +1275,14 @@ A preemptible RCU implementation was therefore added to the Linux kernel.
 This implementation avoids the need to individually track the state of
 each and every task in the kernel by keeping lists of tasks that have
 been preempted within their current RCU read-side critical sections.
-A grace period is permitted to end: (1)~Once all CPUs have completed any
-RCU read-side critical sections that were in effect before the start
-of the current grace period and
-(2)~Once all tasks that were preempted
+A grace period is permitted to end:
+\begin{enumerate*}[(1)]
+\item Once all CPUs have completed any RCU read-side critical sections
+that were in effect before the start of the current grace period and
+\item Once all tasks that were preempted
 while in one of those pre-existing critical sections have removed
 themselves from their lists.
+\end{enumerate*}
 A simplified version of this implementation is shown in
 \cref{lst:advsync:Preemptible Linux-Kernel RCU}.
 \begin{fcvref}[ln:advsync:Preemptible Linux-Kernel RCU]
@@ -1351,9 +1361,9 @@ callback invocation.
 \paragraph{Preemptible spinlocks}
 are an important part of the \rt\ patchset due to the long-duration
 spinlock-based critical sections in the Linux kernel.
-This functionality has not yet reached mainline: Although they are a
-conceptually simple substitution of sleeplocks for spinlocks, they have
-proven relatively controversial.
+This functionality has not yet reached mainline:
+Although they are a conceptually simple substitution of sleeplocks
+for spinlocks, they have proven relatively controversial.
 In addition the real-time functionality that is already in the mainline
 Linux kernel suffices for a great many use cases, which slowed the \rt\
 patchset's development rate in the early
@@ -1755,9 +1765,10 @@ reads sensor data, computes a control law, and writes control output.
 If the hardware registers providing sensor data and taking control
 output are mapped into the application's address space, this loop
 might be completely free of system calls.
-But beware of the Spiderman principle: With great power comes great
-responsibility, in this case the responsibility to avoid bricking the
-hardware by making inappropriate references to the hardware registers.
+But beware of the Spiderman principle:
+With great power comes great responsibility, in this case the
+responsibility to avoid bricking the hardware by making inappropriate
+references to the hardware registers.
 
 This arrangement is often run on bare metal, without the benefits of
 (or the interference from) an operating system.
@@ -1985,7 +1996,8 @@ on \clnrefrange{upd:b}{upd:e}.
 This example shows how RCU can provide deterministic read-side
 data-structure access to real-time programs.
 
-\subsection{Real Time vs.~Real Fast: How to Choose?}
+\subsection{Real Time vs.~Real Fast:
+				     How to Choose?}
 \label{sec:advsync:Real Time vs. Real Fast: How to Choose?}
 
 The choice between real-time and real-fast computing can be a difficult one.
-- 
2.17.1

[PATCH 6/7] memorder: Break and capitalize after colon

[Akira Yokosawa]

Note: "ppc64" behind a colon is enclosed in plain {}.
This is to exclude it from checkscript.

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 memorder/memorder.tex | 102 +++++++++++++++++++++++++-----------------
 1 file changed, 60 insertions(+), 42 deletions(-)

diff --git a/memorder/memorder.tex b/memorder/memorder.tex
index 6cac66b7..1d810b51 100644
--- a/memorder/memorder.tex
+++ b/memorder/memorder.tex
@@ -62,7 +62,8 @@ provides some useful rules of thumb.
 	full rewrite!
 }\QuickQuizEnd
 
-\section{Ordering: Why and How?}
+\section{Ordering:
+		   Why and How?}
 \label{sec:memorder:Ordering: Why and How?}
 %
 \epigraph{Nothing is orderly till people take hold of it.
@@ -97,7 +98,8 @@ even on relatively strongly ordered systems such as x86.
 
 \begin{listing}
 \input{CodeSamples/formal/litmus/C-SB+o-o+o-o@whole.fcv}
-\caption{Memory Misordering: Store-Buffering Litmus Test}
+\caption{Memory Misordering:
+			     Store-Buffering Litmus Test}
 \label{lst:memorder:Memory Misordering: Store-Buffering Litmus Test}
 \end{listing}
 
@@ -128,8 +130,8 @@ value 2 occurred less frequently, in this case, only 167 times.\footnote{
 	Please note that results are sensitive to the exact hardware
 	configuration,
 	how heavily the system is loaded, and much else besides.}
-The lesson here is clear: Increased counter-intuitivity does not necessarily
-imply decreased probability!
+The lesson here is clear:
+Increased counter-intuitivity does not necessarily imply decreased probability!
 % Run on June 23, 2017:
 % litmus7 -r 1000 -carch X86 C-SB+o-o+o-o.litmus
 % Test C-SB+o-o+o-o Allowed
@@ -182,10 +184,11 @@ from multiple CPUs to a set of shared variables.
 In cache-coherent systems, if the caches hold multiple copies of a given
 variable, all the copies of that variable must have the same value.
 This works extremely well for concurrent loads, but not so well for
-concurrent stores:  Each store must do something about all
-copies of the old value (another cache miss!), which, given the finite
-speed of light and the atomic nature of matter, will be slower
-than impatient software hackers would like.
+concurrent stores:
+Each store must do something about all copies of the old value
+(another cache miss!), which, given the finite speed of light and
+the atomic nature of matter, will be slower than impatient software
+hackers would like.
 
 \begin{figure}
 \centering
@@ -241,7 +244,8 @@ in turn cause serious confusion, as fancifully illustrated in
 	\bottomrule
 \end{tabular}
 }
-\caption{Memory Misordering: Store-Buffering Sequence of Events}
+\caption{Memory Misordering:
+			     Store-Buffering Sequence of Events}
 \label{tab:memorder:Memory Misordering: Store-Buffering Sequence of Events}
 \end{table*}
 
@@ -283,8 +287,8 @@ each load immediately returns the cached value, which in both cases
 is zero.
 \end{fcvref}
 
-But the CPUs are not done yet: Sooner or later, they must empty their
-store buffers.
+But the CPUs are not done yet:
+Sooner or later, they must empty their store buffers.
 Because caches move data around in relatively large blocks called
 \emph{cachelines}, and because each cacheline can hold several
 variables, each CPU must get the cacheline into its own cache so
@@ -346,7 +350,8 @@ thus allowing you to stop reading this section.
 
 \begin{listing}
 \input{CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o@whole.fcv}
-\caption{Memory Ordering: Store-Buffering Litmus Test}
+\caption{Memory Ordering:
+			  Store-Buffering Litmus Test}
 \label{lst:memorder:Memory Ordering: Store-Buffering Litmus Test}
 \end{listing}
 
@@ -402,7 +407,8 @@ barrier-free code in
 	\bottomrule
 \end{tabular}
 }
-\caption{Memory Ordering: Store-Buffering Sequence of Events}
+\caption{Memory Ordering:
+			  Store-Buffering Sequence of Events}
 \label{tab:memorder:Memory Ordering: Store-Buffering Sequence of Events}
 \end{table*}
 
@@ -1308,9 +1314,11 @@ in pre-v4.15 Linux kernels.
 	lst:memorder:S Address-Dependency Litmus Test}?
 }\QuickQuizAnswerB{
 	Answering this requires identifying three major groups of platforms:
-	(1)~Total-store-order (TSO) platforms,
-	(2)~Weakly ordered platforms, and
-	(3)~DEC Alpha.
+	\begin{enumerate*}[(1)]
+	\item Total-store-order (TSO) platforms,
+	\item Weakly ordered platforms, and
+	\item DEC Alpha.
+	\end{enumerate*}
 
 	\begin{fcvref}[ln:memorder:Enforced Ordering of Message-Passing Address-Dependency Litmus Test (Before v4.15)]
 	The TSO platforms order all pairs of memory references except for
@@ -1333,8 +1341,8 @@ in pre-v4.15 Linux kernels.
 	unrelated accesses.
 	However, the address dependencies in
 	\cref{lst:memorder:Enforced Ordering of Message-Passing Address-Dependency Litmus Test (Before v4.15),%
-	lst:memorder:S Address-Dependency Litmus Test}
-	are not unrelated: There is an address dependency.
+	lst:memorder:S Address-Dependency Litmus Test} are not unrelated:
+	There is an address dependency.
 	The hardware tracks dependencies and maintains the needed
 	ordering.
 
@@ -1388,9 +1396,10 @@ be fragile and easily broken by compiler optimizations, as discussed in
 A \emph{data dependency} occurs when the value returned by a load
 instruction is used to compute the data stored by a later store
 instruction.
-Note well the ``data'' above: If the value returned by a load
-was instead used to compute the address used by a later store
-instruction, that would instead be an address dependency.
+Note well the ``data'' above:
+If the value returned by a load was instead used to compute the address
+used by a later store instruction, that would instead be an address
+dependency.
 
 \begin{listing}
 \input{CodeSamples/formal/litmus/C-LB+o-r+o-data-o@whole.fcv}
@@ -1458,8 +1467,8 @@ compiler from breaking them.
 A \emph{control dependency} occurs when the value returned by a load
 instruction is tested to determine whether or not a later store instruction
 is executed.
-Note well the ``later store instruction'': Many platforms do not respect
-load-to-load control dependencies.
+Note well the ``later store instruction'':
+Many platforms do not respect load-to-load control dependencies.
 
 \begin{listing}
 \input{CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o@whole.fcv}
@@ -1754,7 +1763,8 @@ line} to carry this new value to them.
 	\bottomrule
 \end{tabular}
 }
-\caption{Memory Ordering: WRC Sequence of Events}
+\caption{Memory Ordering:
+			  WRC Sequence of Events}
 \label{tab:memorder:Memory Ordering: WRC Sequence of Events}
 \end{table*}
 
@@ -2015,7 +2025,7 @@ The cycle in
 goes through \co{P0()} (\clnref{P0:st,P0:sr}), \co{P1()} (\clnref{P1:la,P1:ld}),
 \co{P2()} (\clnref{P2:st,P2:mb,P2:ld}), and back to \co{P0()} (\clnref{P0:st}).
 The \co{exists} clause delineates this cycle:
-the \co{1:r1=1} indicates that the \co{smp_load_acquire()} on \clnref{P1:la}
+The \co{1:r1=1} indicates that the \co{smp_load_acquire()} on \clnref{P1:la}
 returned the value stored by the \co{smp_store_release()} on \clnref{P0:sr},
 the \co{1:r2=0} indicates that the \co{WRITE_ONCE()} on \clnref{P2:st} came
 too late to affect the value returned by the \co{READ_ONCE()} on \clnref{P1:ld},
@@ -2286,7 +2296,8 @@ as shown in
 As with the previous example, \co{smp_store_release()}'s cumulativity
 combined with the temporal nature of the release-acquire chain
 prevents the \co{exists} clause on \clnref{exists} from triggering.
-But beware: Adding a second store-to-store step would allow the correspondingly
+But beware:
+Adding a second store-to-store step would allow the correspondingly
 updated \co{exists} clause to trigger.
 \end{fcvref}
 
@@ -2589,8 +2600,9 @@ if (p == &reserve_int) {
 	supplied in registers.
 	However, there is clearly no ordering between the pointer
 	load on \clnref{deref1} and the dereference on \clnref{deref2}.
-	Please note that this is simply an example: There are a great
-	many other ways to break dependency chains with comparisons.
+	Please note that this is simply an example:
+	There are a great many other ways to break dependency chains
+	with comparisons.
 	\end{fcvref}
 \end{enumerate}
 
@@ -3285,12 +3297,14 @@ As described in
 \cref{sec:defer:RCU Fundamentals},
 the fundamental property of RCU grace periods is this straightforward
 two-part guarantee:
-(1)~If any part of a given RCU read-side critical section precedes
+\begin{enumerate*}[(1)]
+\item If any part of a given RCU read-side critical section precedes
 the beginning of a given grace period, then the entirety of that
 critical section precedes the end of that grace period.
-(2)~If any part of a given RCU read-side critical section follows
+\item If any part of a given RCU read-side critical section follows
 the end of a given grace period, then the entirety of that
 critical section follows the beginning of that grace period.
+\end{enumerate*}
 These guarantees are summarized in
 \cref{fig:memorder:RCU Grace-Period Ordering Guarantees},
 where the grace period is denoted by the dashed arrow between the
@@ -3370,8 +3384,8 @@ In particular, despite their names, they do not act like locks, as can
 be seen in
 \cref{lst:memorder:RCU Readers Provide No Lock-Like Ordering}
 (\path{C-LB+rl-o-o-rul+rl-o-o-rul.litmus}).
-This litmus test's cycle is allowed: Both instances of the \co{r1}
-register can have final values of 1.
+This litmus test's cycle is allowed:
+Both instances of the \co{r1} register can have final values of 1.
 
 \begin{listing}
 \input{CodeSamples/formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul@whole.fcv}
@@ -3414,7 +3428,8 @@ This should be no surprise given the information presented in
 \label{lst:memorder:RCU Updaters Provide Full Ordering}
 \end{listing}
 
-\subsubsection{RCU Readers: Before and After}
+\subsubsection{RCU Readers:
+			    Before and After}
 \label{sec:memorder:RCU Readers: Before and After}
 
 Before reading this section, it would be well to reflect on the distinction
@@ -3690,9 +3705,10 @@ makes it clear that adding a third reader would allow the cycle.
 This is because this third reader could end before the end of \co{P0()}'s
 grace period, and thus start before the beginning of that same grace
 period.
-This in turn suggests the general rule, which is:  In these sorts of RCU-only
-litmus tests, if there are at least as many RCU grace periods as there
-are RCU read-side critical sections, the cycle is forbidden.\footnote{
+This in turn suggests the general rule, which is:
+In these sorts of RCU-only litmus tests, if there are at least as many
+RCU grace periods as there are RCU read-side critical sections,
+the cycle is forbidden.\footnote{
 	Interestingly enough, Alan Stern proved that within the context
 	of LKMM, the two-part fundamental property of RCU expressed
 	in \cref{sec:defer:RCU Fundamentals} actually implies
@@ -4253,7 +4269,8 @@ different set of memory-barrier instructions~\cite{ARMv7A:2010}:
 	restricted to only writes (similar to the Alpha \co{wmb}
 	and the \Power{} \co{eieio} instructions).
 	In addition, \ARM\ allows \IX{cache coherence} to have one of three
-	scopes: single processor, a subset of the processors
+	scopes:
+	Single processor, a subset of the processors
 	(``inner'') and global (``outer'').
 \item	[\tco{DSB}] (data synchronization barrier) causes the specified
 	type of operations to actually complete before any subsequent
@@ -4633,8 +4650,9 @@ Unfortunately, none of these instructions line up exactly with Linux's
 {\tt wmb()} primitive, which requires {\em all} stores to be ordered,
 but does not require the other high-overhead actions of the {\tt sync}
 instruction.
-But there is no choice: ppc64 versions of {\tt wmb()} and {\tt mb()} are
-defined to be the heavyweight {\tt sync} instruction.
+But there is no choice:
+{ppc64} versions of {\tt wmb()} and {\tt mb()} are defined to be the
+heavyweight {\tt sync} instruction.
 However, Linux's \co{smp_wmb()} instruction is never used for MMIO
 (since a driver must carefully order MMIOs in UP as well as
 SMP kernels, after all), so it is defined to be the lighter weight
@@ -4867,7 +4885,7 @@ this, keeping in mind that the C11 standard's memory model does \emph{not}
 fully respect dependencies.
 Therefore, a dependency leading to a load must be headed by
 a \co{READ_ONCE()} or an \co{rcu_dereference()}:
-a plain C-language load is not sufficient.
+A plain C-language load is not sufficient.
 In addition, carefully review
 \cref{sec:memorder:Address- and Data-Dependency Difficulties,%
 sec:memorder:Control-Dependency Calamities}, because
@@ -4945,8 +4963,8 @@ example of a reads-from (rf) link, a load-to-store link is an example
 of a from-reads (fr) link, and a store-to-store link is an example of
 a coherence (co) link.
 
-One final word of advice: Use of raw memory-ordering primitives is
-a last resort.
+One final word of advice:
+Use of raw memory-ordering primitives is a last resort.
 It is almost always better to use existing primitives, such as locking
 or RCU, thus letting those primitives do the memory ordering for you.
 
-- 
2.17.1

[PATCH 7/7] easy, future: Break and capitalize after colon

[Akira Yokosawa]

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 easy/easy.tex            |  6 +++---
 future/cpu.tex           |  5 +++--
 future/formalregress.tex | 24 +++++++++++++++---------
 future/htm.tex           |  8 ++++----
 future/tm.tex            | 30 +++++++++++++++++++-----------
 5 files changed, 44 insertions(+), 29 deletions(-)

diff --git a/easy/easy.tex b/easy/easy.tex
index 5ef4d4df..75da6aea 100644
--- a/easy/easy.tex
+++ b/easy/easy.tex
@@ -32,9 +32,9 @@ This means that creating an easy-to-use API requires that you understand
 your intended users well enough to know what is easy for them.
 Which might or might not have anything to do with what is easy for you.
 
-The following question illustrates this point: ``Given a randomly chosen
-person among everyone alive today, what one change would
-improve that person's life?''
+The following question illustrates this point:
+``Given a randomly chosen person among everyone alive today, what one
+change would improve that person's life?''
 
 There is no single change that would be guaranteed to help everyone's life.
 After all, there is an extremely wide range of people, with a correspondingly
diff --git a/future/cpu.tex b/future/cpu.tex
index 02d383da..27b0d796 100644
--- a/future/cpu.tex
+++ b/future/cpu.tex
@@ -98,8 +98,9 @@ they would need to embrace parallelism, and so it was some time before
 this community concluded that the ``free lunch'' of
 \IXaltr{Moore's-Law}{Moore's Law}-induced
 CPU core-clock frequency increases was well and truly finished.
-Never forget: belief is an emotion, not necessarily the result of a
-rational technical thought process!
+Never forget:
+Belief is an emotion, not necessarily the result of a rational technical
+thought process!
 
 \subsection{Multithreaded Mania}
 \label{sec:future:Multithreaded Mania}
diff --git a/future/formalregress.tex b/future/formalregress.tex
index f7de68bd..60a0fdb0 100644
--- a/future/formalregress.tex
+++ b/future/formalregress.tex
@@ -5,7 +5,8 @@
 \section{Formal Regression Testing?}
 \label{sec:future:Formal Regression Testing?}
 %
-\epigraph{Theory without experiments: Have we gone too far?}
+\epigraph{Theory without experiments:
+	  Have we gone too far?}
 	 {\emph{Michael Mitzenmacher}}
 
 Formal verification has long proven useful in a number of production
@@ -38,7 +39,8 @@ start~\cite[slide 34]{PaulEMcKenney2015DagstuhlVerification}:
 \end{enumerate}
 
 This list builds on, but is somewhat more modest than, Richard Bornat's
-dictum: ``Formal-verification researchers should verify the code that
+dictum:
+``Formal-verification researchers should verify the code that
 developers write, in the language they write it in, running in the
 environment that it runs in, as they write it.''
 The following sections discuss each of the above requirements, followed
@@ -202,7 +204,8 @@ could be verified, with or without continued improvements in
 heuristics.
 
 However, the flip side of combinatorial explosion is Philip II of
-Macedon's timeless advice: ``Divide and rule.''
+Macedon's timeless advice:
+``Divide and rule.''
 If a large program can be divided and the pieces verified, the result
 can be combinatorial \emph{implosion}~\cite{PaulEMcKenney2011Verico}.
 One natural place to divide is on API boundaries, for example, those
@@ -233,7 +236,8 @@ use of the locking APIs.
 	5 & 4.905 &        \\
 	\bottomrule
 \end{tabular}
-\caption{Emulating Locking: Performance (s)}
+\caption{Emulating Locking:
+			    Performance (s)}
 \label{tab:future:Emulating Locking: Performance (s)}
 \end{table}
 
@@ -249,8 +253,9 @@ primitives, but these primitives can also be emulated using
 compares the performance and scalability of using the model's
 \co{spin_lock()} and \co{spin_unlock()} against emulating these
 primitives as shown in the listing.
-The difference is not insignificant: At four processes, the model
-is more than two orders of magnitude faster than emulation!
+The difference is not insignificant:
+At four processes, the model is more than two orders of magnitude
+faster than emulation!
 
 \QuickQuiz{
 \begin{fcvref}[ln:future:formalregress:C-SB+l-o-o-u+l-o-o-u-C:whole]
@@ -288,7 +293,8 @@ is more than two orders of magnitude faster than emulation!
 	5 & 4.905 &        &         &        &        \\
 	\bottomrule
 \end{tabular}
-\caption{Emulating Locking: Performance Comparison (s)}
+\caption{Emulating Locking:
+			    Performance Comparison (s)}
 \label{tab:future:Emulating Locking: Performance Comparison (s)}
 \end{table}
 
@@ -456,8 +462,8 @@ decreased the reliability of the overall software.
 	We don't, but it does not matter.
 
 	To see this, note that the 7\,\% figure only applies to injected
-	bugs that were subsequently located: It necessarily ignores
-	any injected bugs that were never found.
+	bugs that were subsequently located:
+	It necessarily ignores any injected bugs that were never found.
 	Therefore, the MTBF statistics of known bugs is likely to be
 	a good approximation of that of the injected bugs that are
 	subsequently located.
diff --git a/future/htm.tex b/future/htm.tex
index 7458f436..c42ba49e 100644
--- a/future/htm.tex
+++ b/future/htm.tex
@@ -184,8 +184,8 @@ in the next section.
 \subsection{HTM Weaknesses WRT Locking}
 \label{sec:future:HTM Weaknesses WRT Locking}
 
-The concept of HTM is quite simple: A group of accesses and updates to
-memory occurs atomically.
+The concept of HTM is quite simple:
+A group of accesses and updates to memory occurs atomically.
 However, as is the case with many simple ideas, complications arise
 when you apply it to real systems in the real world.
 These complications are as follows:
@@ -499,8 +499,8 @@ interrupts, traps, and exceptions (thus prohibiting system calls).
 Note that buffered I/O can be accommodated by HTM transactions as
 long as the buffer fill/flush operations occur extra-transactionally.
 The reason that this works is that adding data to and removing data
-from the buffer is revocable: Only the actual buffer fill/flush
-operations are irrevocable.
+from the buffer is revocable:
+Only the actual buffer fill/flush operations are irrevocable.
 Of course, this buffered-I/O approach has the effect of including the I/O
 in the transaction's footprint, increasing the size of the transaction
 and thus increasing the probability of failure.
diff --git a/future/tm.tex b/future/tm.tex
index f9a4017a..3ec08a81 100644
--- a/future/tm.tex
+++ b/future/tm.tex
@@ -556,9 +556,13 @@ unknowable at compile time.
 So, what happens if a dynamically loaded function is invoked within
 a transaction?
 
-This question has two parts: (a)~how do you dynamically link and load a
-function within a transaction and (b)~what do you do about the unknowable
-nature of the code within this function?
+This question has two parts:
+\begin{enumerate*}[(a)]
+\item How do you dynamically link and load a function within a transaction
+and
+\item What do you do about the unknowable nature of the code within
+this function?
+\end{enumerate*}
 To be fair, item (b) poses some challenges for locking and userspace-RCU
 as well, at least in theory.
 For example, the dynamically linked function might introduce a \IX{deadlock}
@@ -587,8 +591,9 @@ Options for part (b), the inability to detect TM-unfriendly operations
 in a not-yet-loaded function, possibilities include the following:
 
 \begin{enumerate}
-\item	Just execute the code: if there are any TM-unfriendly operations
-	in the function, simply abort the transaction.
+\item	Just execute the code:
+	If there are any TM-unfriendly operations in the function,
+	simply abort the transaction.
 	Unfortunately, this approach makes it impossible for the compiler
 	to determine whether a given group of transactions may be safely
 	composed.
@@ -748,9 +753,9 @@ It is also possible to acquire locks while holding hazard pointers and
 within sequence-lock read-side critical sections.
 But what happens when you attempt to acquire a lock from within a transaction?
 
-In theory, the answer is trivial: simply manipulate the data structure
-representing the lock as part of the transaction, and everything works
-out perfectly.
+In theory, the answer is trivial:
+Simply manipulate the data structure representing the lock as part of
+the transaction, and everything works out perfectly.
 In practice, a number of non-obvious complications~\cite{Volos2008TRANSACT}
 can arise, depending on implementation details of the TM system.
 These complications can be resolved, but at the cost of a 45\,\% increase in
@@ -1211,21 +1216,24 @@ And vice versa.
 \begin{figure}
 \centering
 \resizebox{2.7in}{!}{\includegraphics{cartoons/TM-the-reality-conflict}}
-\caption{The STM Reality: Conflicts}
+\caption{The STM Reality:
+			  Conflicts}
 \ContributedBy{Figure}{fig:future:The STM Reality: Conflicts}{Melissa Broussard}
 \end{figure}
 
 \begin{figure}
 \centering
 \resizebox{3in}{!}{\includegraphics{cartoons/TM-the-reality-nonidempotent}}
-\caption{The STM Reality: Irrevocable Operations}
+\caption{The STM Reality:
+			  Irrevocable Operations}
 \ContributedBy{Figure}{fig:future:The STM Reality: Irrevocable Operations}{Melissa Broussard}
 \end{figure}
 
 \begin{figure}
 \centering
 \resizebox{2.7in}{!}{\includegraphics{cartoons/TM-the-reality-realtime}}
-\caption{The STM Reality: Realtime Response}
+\caption{The STM Reality:
+			  Realtime Response}
 \ContributedBy{Figure}{fig:future:The STM Reality: Realtime Response}{Melissa Broussard}
 \end{figure}
 
-- 
2.17.1

Re: [PATCH 0/7] Break and capitalize after colon, take three

[Paul E. McKenney]

On Tue, Aug 10, 2021 at 01:33:44PM +0900, Akira Yokosawa wrote:
> Hi Paul,
> 
> Here are colon related changes though Chapter 17.
> They don't alter appearance except for capitalization and minor
> changes in Patch 3/7 mentioned below.
> 
> In Patch 2/7, "dynticks" behind a colon is enclosed by plain {}.
> In Patch 3/7, messages from pan are enclosed by \co{}.
> In Patch 6/7, "ppc64" behind a colon is enclosed by plain {}.
> These are to escape checks by to-be-updated scripts.
> 
> The other patches are (hopefully) trivial.

Queued and pushed, thank you!

> My hope is to complete similar changes in Appendices soon.

Looking forward to it!

> FWIW, I have been working on the improvement of appearance of CJK
> translations in kerneldoc (pdfdocs) recently [1], hence my low activity
> in perfbook.
> 
> [1]: [PATCH v4 0/9] docs: pdfdocs: Improve font choice in CJK translations
>     https://lore.kernel.org/linux-doc/39d0fb0f-b248-bca4-2dac-df69e8d697b1@gmail.com/#t

Nice!!!

							Thanx, Paul

>         Thanks, Akira
> --
> Akira Yokosawa (7):
>   debugging: Break and capitalize after colon
>   formal: Break and capitalize after colon
>   formal: Use \co{} for pan messages containing colon
>   together: Break and capitalize after colon
>   advsync: Break and capitalize after colon
>   memorder: Break and capitalize after colon
>   easy, future: Break and capitalize after colon
> 
>  advsync/advsync.tex      |  31 +++++++-----
>  advsync/rt.tex           |  72 +++++++++++++++------------
>  debugging/debugging.tex  |  92 +++++++++++++++++++----------------
>  easy/easy.tex            |   6 +--
>  formal/axiomatic.tex     |   3 +-
>  formal/dyntickrcu.tex    |  17 ++++---
>  formal/formal.tex        |   7 ++-
>  formal/ppcmem.tex        |   4 +-
>  formal/spinhint.tex      |  44 ++++++++++-------
>  future/cpu.tex           |   5 +-
>  future/formalregress.tex |  24 +++++----
>  future/htm.tex           |   8 +--
>  future/tm.tex            |  30 +++++++-----
>  memorder/memorder.tex    | 102 +++++++++++++++++++++++----------------
>  together/applyrcu.tex    |   6 +--
>  together/count.tex       |  10 ++--
>  together/refcnt.tex      |   2 +-
>  17 files changed, 269 insertions(+), 194 deletions(-)
> 
> -- 
> 2.17.1
>