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

[SeongJae Park <sj@kernel.org>]

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