>From 267bc5727f8f50d389818c22c81ea9a6e1d810e4 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
Date: Mon, 13 Mar 2017 20:48:23 +0900
Subject: [PATCH v2 4/6] formal/spinhint: Reference by Figure labels
Reference to floating figures should be done by labels.
Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
---
formal/spinhint.tex | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index d6acef1..a18ae23 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -742,7 +742,9 @@ Lines~30 and~31 initialize the control variables,
lines~32-40 atomically sum the havelock array entries,
line~41 is the assertion, and line~42 exits the loop.
-We can run this model by placing the above two code fragments into
+We can run this model by placing the two code fragments of
+Figures~\ref{fig:analysis:Promela Code for Spinlock}
+and~\ref{fig:analysis:Promela Code to Test Spinlocks} into
files named \path{lock.h} and \path{lock.spin}, respectively, and then running
the following commands:
--
2.7.4
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
