[PATCH 00/12] formal: Trivial fixups

[PATCH 00/12] formal: Trivial fixups

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

This patchset contains trivial fixups for formal/, which found from
its Korean translation[1].

[1] https://github.com/sjp38/perfbook-ko_KR

SeongJae Park (12):
  formal/formal: Drop cppmem from 'Special-Purpose State-Space Search'
    section explanation
  formal/spinhint: Use \qco{} instead of ``\co{}''
  formal/spinhint: Enclose example code snippets with \co{}
  formal/spinhint: Do not call 2013 paper as recent
  formal/dyntickrcu: Quote 'trail' file consistently
  formal/dyntickrcu: Use \qco{} instead of ``\co{}''
  formal/ppcmem: Use uppercase 'S' for Spin
  formal/ppcmem: Use \qco{} instead of ``\co{}''
  formal/ppcmem: Add missed non-breakable spaces
  formal/ppcmem: Enclose example code snippets with \co{}
  formal/ppcmem: s/powerpc/PowerPC/ on sentences
  formal/ppcmem: Fix label name for Fail1:

 formal/axiomatic.tex  | 30 +++++++++++++++---------------
 formal/dyntickrcu.tex | 10 +++++-----
 formal/formal.tex     |  2 +-
 formal/ppcmem.tex     | 26 +++++++++++++-------------
 formal/spinhint.tex   | 16 ++++++++--------
 5 files changed, 42 insertions(+), 42 deletions(-)

-- 
2.17.1

[PATCH 01/12] formal/formal: Drop cppmem from 'Special-Purpose State-Space Search' section explanation

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

The advance explanation of 'Special-Purpose State-Space Search' section
says it will introduce both ppcmem and cppmem, but the section
introduces ppcmem only.  Fix the sentence.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/formal.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/formal.tex b/formal/formal.tex
index 895d2ba7..13dcf071 100644
--- a/formal/formal.tex
+++ b/formal/formal.tex
@@ -28,7 +28,7 @@ A number of such tools exist, for example,
 \cref{sec:formal:State-Space Search} provides an
 introduction to the general-purpose state-space search tools Promela and Spin,
 \cref{sec:formal:Special-Purpose State-Space Search}
-similarly introduces the special-purpose ppcmem and cppmem tools,
+similarly introduces the special-purpose ppcmem tool,
 \cref{sec:formal:Axiomatic Approaches}
 looks at an example axiomatic approach,
 \cref{sec:formal:SAT Solvers}
-- 
2.17.1

[PATCH 02/12] formal/spinhint: Use \qco{} instead of ``\co{}''

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

A few sentences in spinhint.tex are using ``\co{}'', which can be
shortenized with \qco{}.  Use the shorter one.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/spinhint.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index afdd275e..0371f570 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:
-	``\co{error: max search depth too small}'', you need to increase
+	\qco{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}.
 
@@ -325,7 +325,7 @@ Promela will provide some surprises to people used to coding in C,
 C++, or Java.
 
 \begin{enumerate}
-\item	In C, ``\co{;}'' terminates statements.
+\item	In C, \qco{;} terminates statements.
 	In Promela it separates them.
 	Fortunately, more recent versions of Spin have become
 	much more forgiving of ``extra'' semicolons.
@@ -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 (``\co{errors: 0}'').
+As expected, this run has no assertion failures (\qco{errors: 0}).
 
 \QuickQuizSeries{%
 \QuickQuizB{
-- 
2.17.1

[PATCH 03/12] formal/spinhint: Enclose example code snippets with \co{}

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

A few sentences in spinhint.tex are not enclosing example code snippets
with \co{}.  Enclose those for better readability and consistency.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/spinhint.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 0371f570..b740384d 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -397,8 +397,8 @@ The following tricks can help you to abuse Promela safely:
 
 \begin{enumerate}
 \item	Memory reordering.
-	Suppose you have a pair of statements copying globals x and y
-	to locals r1 and r2, where ordering matters (e.g., unprotected
+	Suppose you have a pair of statements copying globals \co{x} and \co{y}
+	to locals \co{r1} and \co{r2}, where ordering matters (e.g., unprotected
 	by locks), but where you have no \IXpl{memory barrier}.
 	This can be modeled in Promela as follows:
 
@@ -552,12 +552,12 @@ unclaiming it on \clnref{unclaim}, and releasing it on \clnref{unlock}.
 
 \begin{fcvref}[ln:formal:promela:lock:spin:init]
 The init block on \clnrefrange{b}{e} initializes the current locker's
-havelock array entry on \clnref{array}, starts the current locker on
+\co{havelock} array entry on \clnref{array}, starts the current locker on
 \clnref{start}, and advances to the next locker on \clnref{next}.
 Once all locker processes are spawned, the \co{do-od} loop
 moves to \clnref{chkassert}, which checks the assertion.
 \Clnref{sum,j} initialize the control variables,
-\clnrefrange{atm:b}{atm:e} atomically sum the havelock array entries,
+\clnrefrange{atm:b}{atm:e} atomically sum the \co{havelock} array entries,
 \clnref{assert} is the assertion, and \clnref{break} exits the loop.
 \end{fcvref}
 
-- 
2.17.1

[PATCH 04/12] formal/spinhint: Do not call 2013 paper as recent

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

A sentence in spinhint.tex is mentioning Jade Alglave's 2013 paper as
recent one.  It's a decade ago, so drop the word, 'recent'.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/spinhint.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index b740384d..9bb5f574 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -1178,7 +1178,7 @@ easier to understand.
 Is QRCU really correct?
 We have a Promela-based mechanical proof and a by-hand proof that both
 say that it is.
-However, a recent paper by \pplsur{Jade}{Alglave} et al.~\cite{JadeAlglave2013-cav}
+However, a paper by \pplsur{Jade}{Alglave} et al.~\cite{JadeAlglave2013-cav}
 says otherwise (see Section~5.1 of the paper at the bottom of page~12).
 Which is it?
 
-- 
2.17.1

[PATCH 05/12] formal/dyntickrcu: Quote 'trail' file consistently

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

A sentence in dyntickrcu quotes 'trail' keyword with `` and '', while
another one doesn't.   Do quote consistently.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/dyntickrcu.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index bee5b4da..25012738 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -534,7 +534,7 @@ through preemptible RCU's grace-period processing.
 
 \begin{fcvref}[ln:formal:promela:dyntick:dyntickRCU-base:grace_period]
 \Clnrefrange{print:b}{print:e} print out the loop limit
-(but only into the .trail file
+(but only into the ``.trail'' file
 in case of error) and models a line of code
 from \co{rcu_try_flip_idle()} and its call to
 \co{dyntick_save_progress_counter()}, which takes a
-- 
2.17.1

[PATCH 06/12] formal/dyntickrcu: Use \qco{} instead of ``\co{}''

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

A few sentences in dyntickrcu.tex are using ``\co{}'', which can be
shortenized with \qco{}.  Use the shorter one.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/dyntickrcu.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 25012738..42c0c55c 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -890,12 +890,12 @@ statements in that group execute atomically.
 %
 \QuickQuizE{
 	But what if the \co{dynticks_nohz()} process had
-	``if'' or ``do'' statements with conditions,
+	\qco{if} or \qco{do} statements with conditions,
 	where the statement bodies of these constructs
 	needed to execute non-atomically?
 }\QuickQuizAnswerE{
 	One approach, as we will see in a later section,
-	is to use explicit labels and ``goto'' statements.
+	is to use explicit labels and \qco{goto} statements.
 	For example, the construct:
 
 \begin{VerbatimU}
@@ -921,7 +921,7 @@ statements in that group execute atomically.
 \end{VerbatimU}
 
 	However, it is not clear that the macro is helping much in the case
-	of the ``if'' statement, so these sorts of situations will
+	of the \qco{if} statement, so these sorts of situations will
 	be open-coded in the following sections.
 }\QuickQuizEndE
 }
@@ -1067,7 +1067,7 @@ to \co{EXECUTE_IRQ()} as follows:
 \input{CodeSamples/formal/promela/dyntick/dyntickRCU-irq-nmi-ssl@dyntick_irq.fcv}
 
 \begin{fcvref}[ln:formal:promela:dyntick:dyntickRCU-irq-nmi-ssl:dyntick_irq]
-Note that we have open-coded the ``if'' statements
+Note that we have open-coded the \qco{if} statements
 (for example, \clnrefrange{stmt1:b}{stmt1:e}).
 In addition, statements that process strictly local state
 (such as \clnref{inc_i}) need not exclude \co{dyntick_nmi()}.
-- 
2.17.1

[PATCH 07/12] formal/ppcmem: Use uppercase 'S' for Spin

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

A few sentences in ppcmem.tex are using lowercase 's' for Spin, while
other sentences in other tex files are using the uppercase 'S'.
Consistently use uppercase 'S'.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/ppcmem.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 9f584b15..62a45383 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -7,7 +7,7 @@
 %
 \epigraph{Jack of all trades, master of none.}{Unknown}
 
-Although Promela and spin allow you to verify pretty much any (smallish)
+Although Promela and Spin allow you to verify pretty much any (smallish)
 algorithm, their very generality can sometimes be a curse.
 For example, Promela does not understand memory models or any sort
 of reordering semantics.
@@ -403,7 +403,7 @@ These tools do have some intrinsic limitations:
 	running on small numbers of threads.
 	Larger examples result
 	in state-space explosion, just as with similar tools such as
-	Promela and spin.
+	Promela and Spin.
 \item	The full state-space search does not give any indication of how
 	each offending state was reached.
 	That said, once you realize that the state is in fact reachable,
-- 
2.17.1

[PATCH 08/12] formal/ppcmem: Use \qco{} instead of ``\co{}''

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

A few sentences in ppcmem.tex are using ``\co{}'', which can be
shortenized with \qco{}.  Use the shorter one.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/ppcmem.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 62a45383..9acd4dba 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -65,8 +65,8 @@ discusses the implications.
 An example PowerPC litmus test for PPCMEM is shown in
 \cref{lst:formal:PPCMEM Litmus Test}.
 The ARM interface works the same way, but with \ARM\ instructions
-substituted for the Power instructions and with the initial ``PPC''
-replaced by ``ARM''.
+substituted for the Power instructions and with the initial \qco{PPC}
+replaced by \qco{ARM}.
 
 \begin{listing}
 \begin{fcvlabel}[ln:formal:PPCMEM Litmus Test]
@@ -98,8 +98,8 @@ exists						@lnlbl[assert:b]
 \end{listing}
 
 \begin{fcvref}[ln:formal:PPCMEM Litmus Test]
-In the example, \clnref{type} identifies the type of system (``ARM'' or
-``PPC'') and contains the title for the model.
+In the example, \clnref{type} identifies the type of system (\qco{ARM} or
+\co{PPC}) and contains the title for the model.
 \Clnref{altname} provides a place for an
 alternative name for the test, which you will usually want to leave
 blank as shown in the above example.
@@ -412,7 +412,7 @@ These tools do have some intrinsic limitations:
 \item	These tools are not much good for complex data structures, although
 	it is possible to create and traverse extremely simple linked
 	lists using initialization statements of the form
-	``\co{x=y; y=z; z=42;}''.
+	\qco{x=y; y=z; z=42;}.
 \item	These tools do not handle memory mapped I/O or device registers.
 	Of course, handling such things would require that they be
 	formalized, which does not appear to be in the offing.
-- 
2.17.1

[PATCH 09/12] formal/ppcmem: Add missed non-breakable spaces

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

A few sentences in ppcmem.tex are missing non-breakable spaces.  Add
those.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/ppcmem.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 9acd4dba..c3f5f943 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -110,13 +110,13 @@ Comments can be inserted between
 each is of the form
 \co{P:R=V}, where \co{P} is the process identifier, \co{R} is the register
 identifier, and \co{V} is the value.
-For example, process 0's register r3 initially contains the value~2.
+For example, process~0's register r3 initially contains the value~2.
 If the value is a variable (\co{x}, \co{y}, or \co{z} in the example)
 then the register is initialized to the address of the variable.
 It is also possible to initialize the contents of variables, for example,
 \co{x=1} initializes the value of \co{x} to~1.
 Uninitialized variables default to the value zero, so that in the
-example, \co{x}, \co{y}, and \co{z} are all initially zero.
+example, \co{x}, \co{y}, and~\co{z} are all initially zero.
 
 \Clnref{procid} provides identifiers for the two processes, so that
 the \co{0:r3=2} on \clnref{init:0} could instead have been written
-- 
2.17.1

[PATCH 10/12] formal/ppcmem: Enclose example code snippets with \co{}

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

A few sentences in ppcmem.tex are not enclosing example code snippets
with \co{}.  Enclose those for better readability and consistency.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/axiomatic.tex | 30 +++++++++++++++---------------
 formal/ppcmem.tex    |  6 +++---
 2 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/formal/axiomatic.tex b/formal/axiomatic.tex
index 80c5cafa..c970d3bb 100644
--- a/formal/axiomatic.tex
+++ b/formal/axiomatic.tex
@@ -70,7 +70,7 @@ One such approach is the axiomatic approach of
 which creates a set of axioms to represent the memory model and then
 converts litmus tests to theorems that might be proven or disproven
 over this set of axioms.
-The resulting tool, called ``herd'',  conveniently takes as input the
+The resulting tool, called \qco{herd},  conveniently takes as input the
 same litmus tests as PPCMEM, including the IRIW litmus test shown in
 \cref{lst:formal:IRIW Litmus Test}.
 
@@ -106,27 +106,27 @@ exists
 \label{lst:formal:Expanded IRIW Litmus Test}
 \end{listing}
 
-However, where PPCMEM requires 14 CPU hours to solve IRIW, herd does so
+However, where PPCMEM requires 14 CPU hours to solve IRIW, \co{herd} does so
 in 17 milliseconds, which represents a speedup of more than six orders
 of magnitude.
 That said, the problem is exponential in nature, so we should expect
-herd to exhibit exponential slowdowns for larger problems.
+\co{herd} to exhibit exponential slowdowns for larger problems.
 And this is exactly what happens, for example, if we add four more writes
 per writing CPU as shown in
 \cref{lst:formal:Expanded IRIW Litmus Test},
-herd slows down by a factor of more than 50,000, requiring more than
+\co{herd} slows down by a factor of more than 50,000, requiring more than
 15 \emph{minutes} of CPU time.
 Adding threads also results in exponential
 slowdowns~\cite{PaulEMcKenney2014weakaxiom}.
 
-Despite their exponential nature, both PPCMEM and herd have proven quite
+Despite their exponential nature, both PPCMEM and \co{herd} have proven quite
 useful for checking key parallel algorithms, including the queued-lock
 handoff on x86 systems.
-The weaknesses of the herd tool are similar to those of PPCMEM, which
+The weaknesses of the \co{herd} tool are similar to those of PPCMEM, which
 were described in
 \cref{sec:formal:PPCMEM Discussion}.
 There are some obscure (but very real) cases for which the PPCMEM and
-herd tools disagree, and as of 2021 many but not all of these disagreements
+\co{herd} tools disagree, and as of 2021 many but not all of these disagreements
 was resolved.
 
 It would be helpful if the litmus tests could be written in C
@@ -189,18 +189,18 @@ And in this case, the \co{herd} tool's output features the string
 }\QuickQuizAnswer{
 	In a word, performance, as can be seen in
 	\cref{tab:formal:Locking: Modeling vs. Emulation Time (s)}.
-	The first column shows the number of herd processes modeled.
-	The second column shows the herd runtime when modeling
-	\co{spin_lock()} and \co{spin_unlock()} directly in herd's
+	The first column shows the number of \co{herd} processes modeled.
+	The second column shows the \co{herd} runtime when modeling
+	\co{spin_lock()} and \co{spin_unlock()} directly in \co{herd}'s
 	cat language.
-	The third column shows the herd runtime when emulating
+	The third column shows the \co{herd} runtime when emulating
 	\co{spin_lock()} with \co{cmpxchg_acquire()} and \co{spin_unlock()}
-	with \co{smp_store_release()}, using the herd \co{filter}
+	with \co{smp_store_release()}, using the \co{herd} \co{filter}
 	clause to reject executions that fail to acquire the lock.
 	The fourth column is like the third, but using \co{xchg_acquire()}
 	instead of \co{cmpxchg_acquire()}.
 	The fifth and sixth columns are like the third and fourth,
-	but instead using the herd \co{exists} clause to reject
+	but instead using the \co{herd} \co{exists} clause to reject
 	executions that fail to acquire the lock.
 
 \begin{table}
@@ -245,8 +245,8 @@ And in this case, the \co{herd} tool's output features the string
 	of magnitude faster than modeling emulated locking.
 	This should also be no surprise, as direct modeling raises
 	the level of abstraction, thus reducing the number of events
-	that herd must model.
-	Because almost everything that herd does is of exponential
+	that \co{herd} must model.
+	Because almost everything that \co{herd} does is of exponential
 	computational complexity, modest reductions in the number of
 	events produces exponentially large reductions in runtime.
 
diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index c3f5f943..25d07c34 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -110,7 +110,7 @@ Comments can be inserted between
 each is of the form
 \co{P:R=V}, where \co{P} is the process identifier, \co{R} is the register
 identifier, and \co{V} is the value.
-For example, process~0's register r3 initially contains the value~2.
+For example, process~0's register \co{r3} initially contains the value~2.
 If the value is a variable (\co{x}, \co{y}, or \co{z} in the example)
 then the register is initialized to the address of the variable.
 It is also possible to initialize the contents of variables, for example,
@@ -156,11 +156,11 @@ That said, too-free use of branches will expand the state space.
 Use of loops is a particularly good way to explode your state space.
 
 \Clnrefrange{assert:b}{assert:e} show the assertion, which in this case
-indicates that we are interested in whether P0's and P1's r3 registers
+indicates that we are interested in whether P0's and P1's \co{r3} registers
 can both contain zero after both threads complete execution.
 This assertion is important because there are a number of use cases
 that would fail miserably if both P0 and P1 saw zero in their
-respective r3 registers.
+respective \co{r3} registers.
 
 This should give you enough information to construct simple litmus tests.
 Some additional documentation is available, though much of this
-- 
2.17.1

[PATCH 11/12] formal/ppcmem: s/powerpc/PowerPC/ on sentences

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

Most sentences are using 'PowerPC' while a sentence in ppcmem.tex is
using 'powerpc'.  Use 'PowerPC' consistently.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/ppcmem.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 25d07c34..181ca7c6 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -204,7 +204,7 @@ and \clnref{P1lwz} is equivalent to the C statement \co{r3=x}.
 	the one that is the \co{Fail1:} label?
 	\end{fcvref}
 }\QuickQuizAnswer{
-	The implementation of powerpc version of \co{atomic_add_return()}
+	The implementation of PowerPC version of \co{atomic_add_return()}
 	loops when the \co{stwcx} instruction fails, which it communicates
 	by setting non-zero status in the condition-code register,
 	which in turn is tested by the \co{bne} instruction.
-- 
2.17.1

[PATCH 12/12] formal/ppcmem: Fix label name for Fail1:

[SeongJae Park]

From: SeongJae Park <sj38.park@gmail.com>

A sentence is calling 'Fail1:' label as 'Fail:'.  Fix it.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/ppcmem.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 181ca7c6..10526bca 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -209,7 +209,7 @@ and \clnref{P1lwz} is equivalent to the C statement \co{r3=x}.
 	by setting non-zero status in the condition-code register,
 	which in turn is tested by the \co{bne} instruction.
 	Because actually modeling the loop would result in state-space
-	explosion, we instead branch to the \co{Fail:} label,
+	explosion, we instead branch to the \co{Fail1:} label,
 	terminating the model with the initial value of~2 in P0's \co{r3}
 	register, which will not trigger the exists assertion.
 
-- 
2.17.1

Re: [PATCH 00/12] formal: Trivial fixups

[Paul E. McKenney]

On Sat, Apr 08, 2023 at 10:32:57AM -0700, SeongJae Park wrote:
> From: SeongJae Park <sj38.park@gmail.com>
> 
> This patchset contains trivial fixups for formal/, which found from
> its Korean translation[1].
> 
> [1] https://github.com/sjp38/perfbook-ko_KR

Queued and pushed, thank you!!!

							Thanx, Paul

> SeongJae Park (12):
>   formal/formal: Drop cppmem from 'Special-Purpose State-Space Search'
>     section explanation
>   formal/spinhint: Use \qco{} instead of ``\co{}''
>   formal/spinhint: Enclose example code snippets with \co{}
>   formal/spinhint: Do not call 2013 paper as recent
>   formal/dyntickrcu: Quote 'trail' file consistently
>   formal/dyntickrcu: Use \qco{} instead of ``\co{}''
>   formal/ppcmem: Use uppercase 'S' for Spin
>   formal/ppcmem: Use \qco{} instead of ``\co{}''
>   formal/ppcmem: Add missed non-breakable spaces
>   formal/ppcmem: Enclose example code snippets with \co{}
>   formal/ppcmem: s/powerpc/PowerPC/ on sentences
>   formal/ppcmem: Fix label name for Fail1:
> 
>  formal/axiomatic.tex  | 30 +++++++++++++++---------------
>  formal/dyntickrcu.tex | 10 +++++-----
>  formal/formal.tex     |  2 +-
>  formal/ppcmem.tex     | 26 +++++++++++++-------------
>  formal/spinhint.tex   | 16 ++++++++--------
>  5 files changed, 42 insertions(+), 42 deletions(-)
> 
> -- 
> 2.17.1
>