From: SeongJae Park <sj38.park@xxxxxxxxx>
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@xxxxxxxxx>
---
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
