* [PATCH 0/6] Misc updates and fixes
@ 2017-03-13 22:43 Akira Yokosawa
2017-03-13 22:44 ` [PATCH 1/6] runlatex.sh: Refactor further Akira Yokosawa
` (6 more replies)
0 siblings, 7 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-13 22:43 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 93e02eca9bb8361be47e0936f5d2ca56586bc093 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 14 Mar 2017 07:38:12 +0900
Subject: [PATCH 0/6] Misc updates and fixes
Hi Paul,
This patch set contains misc updates and fixes I noticed
while comparing current perfbook contents and your draft LWN article.
Thanks, Akira
--
Akira Yokosawa (6):
runlatex.sh: Refactor further
formal/spinhint: Fix typo
formal/spinhint: Adjust option of enumerate list
formal/spinhint: Refer explicit Figure labels
advsync/memorybarriers: Refer explicit Figure label
advsync/memorybarriers: Distinguish 'CPU family' from 'CPU'
advsync/memorybarriers.tex | 13 +++++++------
formal/spinhint.tex | 16 +++++++++-------
utilities/runlatex.sh | 27 +++++++++++++++++----------
3 files changed, 33 insertions(+), 23 deletions(-)
--
2.7.4
^ permalink raw reply [flat|nested] 15+ messages in thread
* [PATCH 1/6] runlatex.sh: Refactor further
2017-03-13 22:43 [PATCH 0/6] Misc updates and fixes Akira Yokosawa
@ 2017-03-13 22:44 ` Akira Yokosawa
2017-03-13 22:45 ` [PATCH 2/6] formal/spinhint: Fix typo Akira Yokosawa
` (5 subsequent siblings)
6 siblings, 0 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-13 22:44 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From a87bed749d870ce45fd7b328f4099a58271dfa20 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 13 Mar 2017 20:42:39 +0900
Subject: [PATCH 1/6] runlatex.sh: Refactor further
This won't result in reducing line count, but is worth doing.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
utilities/runlatex.sh | 27 +++++++++++++++++----------
1 file changed, 17 insertions(+), 10 deletions(-)
diff --git a/utilities/runlatex.sh b/utilities/runlatex.sh
index e6b3938..cece545 100644
--- a/utilities/runlatex.sh
+++ b/utilities/runlatex.sh
@@ -39,6 +39,17 @@ diff_warning () {
fi
}
+identical_warnings () {
+ if test -r $basename-warning-prev.log
+ then
+ if test "$iter" -gt "$min_iter" && diff_warning
+ then
+ return 0 ;
+ fi
+ fi
+ return 1 ;
+}
+
iterate_latex () {
pdflatex $basename > /dev/null 2>&1 < /dev/null || :
if grep -q '! Emergency stop.' $basename.log
@@ -76,27 +87,23 @@ rm -f $basename-first.log
iter=2
echo "pdflatex 2 for $basename.pdf # for possible bib update"
iterate_latex
+min_iter=2
while grep -q 'LaTeX Warning: There were undefined references' $basename.log
do
- if test -r $basename-warning-prev.log
+ if identical_warnings
then
- if test "$iter" -gt 2 && diff_warning
- then
- break
- fi
+ break
fi
iter=`expr $iter + 1`
echo "pdflatex $iter for $basename.pdf # remaining undefined refs"
iterate_latex
done
+min_iter=3
while grep -q 'LaTeX Warning: Label(s) may have changed' $basename.log
do
- if test -r $basename-warning-prev.log
+ if identical_warnings
then
- if test "$iter" -gt 3 && diff_warning
- then
- break
- fi
+ break
fi
iter=`expr $iter + 1`
echo "pdflatex $iter for $basename.pdf # label(s) may have changed"
--
2.7.4
^ permalink raw reply related [flat|nested] 15+ messages in thread
* [PATCH 2/6] formal/spinhint: Fix typo
2017-03-13 22:43 [PATCH 0/6] Misc updates and fixes Akira Yokosawa
2017-03-13 22:44 ` [PATCH 1/6] runlatex.sh: Refactor further Akira Yokosawa
@ 2017-03-13 22:45 ` Akira Yokosawa
2017-03-13 22:46 ` [PATCH 3/6] formal/spinhint: Adjust option of enumerate list Akira Yokosawa
` (4 subsequent siblings)
6 siblings, 0 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-13 22:45 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 32cf4c216eb3b0c8395ecff9ffa2e53e1e415c89 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 13 Mar 2017 20:47:29 +0900
Subject: [PATCH 2/6] formal/spinhint: Fix typo
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 87a7040..a10b57b 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -854,8 +854,8 @@ latencies of most other RCU implementations.
\item There are \co{qrcu_read_lock()} and \co{qrcu_read_unlock()}
primitives that delimit QRCU read-side critical sections.
The corresponding \co{qrcu_struct} must be passed into
- these primitives, and the return value from \co{rcu_read_lock()}
- must be passed to \co{rcu_read_unlock()}.
+ these primitives, and the return value from \co{qrcu_read_lock()}
+ must be passed to \co{qrcu_read_unlock()}.
For example:
--
2.7.4
^ permalink raw reply related [flat|nested] 15+ messages in thread
* [PATCH 3/6] formal/spinhint: Adjust option of enumerate list
2017-03-13 22:43 [PATCH 0/6] Misc updates and fixes Akira Yokosawa
2017-03-13 22:44 ` [PATCH 1/6] runlatex.sh: Refactor further Akira Yokosawa
2017-03-13 22:45 ` [PATCH 2/6] formal/spinhint: Fix typo Akira Yokosawa
@ 2017-03-13 22:46 ` Akira Yokosawa
2017-03-13 22:47 ` [PATCH 4/6] formal/spinhint: Refer explicit Figure labels Akira Yokosawa
` (3 subsequent siblings)
6 siblings, 0 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-13 22:46 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From fe01252839978d67b611eafca1c49e8772582fd2 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 13 Mar 2017 20:47:56 +0900
Subject: [PATCH 3/6] formal/spinhint: Adjust option of enumerate list
This enumeration list can be optimized by specifying starting
count and label format. It is also better to use a narrower
item separation.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
formal/spinhint.tex | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index a10b57b..d6acef1 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -924,10 +924,10 @@ sections).
The \co{readerprogress} array elements have values as follows,
indicating the state of the corresponding reader:
-\begin{enumerate}
-\item 0: not yet started.
-\item 1: within QRCU read-side critical section.
-\item 2: finished with QRCU read-side critical section.
+\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.
\end{enumerate}
Finally, the \co{mutex} variable is used to serialize updaters' slowpaths.
--
2.7.4
^ permalink raw reply related [flat|nested] 15+ messages in thread
* [PATCH 4/6] formal/spinhint: Refer explicit Figure labels
2017-03-13 22:43 [PATCH 0/6] Misc updates and fixes Akira Yokosawa
` (2 preceding siblings ...)
2017-03-13 22:46 ` [PATCH 3/6] formal/spinhint: Adjust option of enumerate list Akira Yokosawa
@ 2017-03-13 22:47 ` Akira Yokosawa
2017-03-13 22:48 ` [PATCH 5/6] advsync/memorybarriers: Refer explicit Figure label Akira Yokosawa
` (2 subsequent siblings)
6 siblings, 0 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-13 22:47 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 7211be04d75a719b92754c2d14d7d23e5656be30 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 13 Mar 2017 20:48:23 +0900
Subject: [PATCH 4/6] formal/spinhint: Refer explicit Figure labels
Referring floating figures should be done by labels.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
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
^ permalink raw reply related [flat|nested] 15+ messages in thread
* [PATCH 5/6] advsync/memorybarriers: Refer explicit Figure label
2017-03-13 22:43 [PATCH 0/6] Misc updates and fixes Akira Yokosawa
` (3 preceding siblings ...)
2017-03-13 22:47 ` [PATCH 4/6] formal/spinhint: Refer explicit Figure labels Akira Yokosawa
@ 2017-03-13 22:48 ` Akira Yokosawa
2017-03-13 22:49 ` [PATCH 6/6] advsync/memorybarriers: Distinguish 'CPU family' from 'CPU' Akira Yokosawa
2017-03-14 12:37 ` [PATCH v2 0/6] Misc updates Akira Yokosawa
6 siblings, 0 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-13 22:48 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From c6cab8f8a30053825be79d4701ade5e847b64fb3 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 13 Mar 2017 20:50:12 +0900
Subject: [PATCH 5/6] advsync/memorybarriers: Refer explicit Figure label
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
advsync/memorybarriers.tex | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
index 98f7787..85e9162 100644
--- a/advsync/memorybarriers.tex
+++ b/advsync/memorybarriers.tex
@@ -1135,7 +1135,8 @@ appears to be maintained. Similarly, the compiler may also arrange the
instructions it emits in any order it likes, provided it doesn't affect the
apparent operation of the program.
-So in the above diagram, the effects of the memory operations performed by a
+So in Figure~\ref{fig:advsync:Abstract Memory Access Model},
+the effects of the memory operations performed by a
CPU are perceived by the rest of the system as the operations cross the
interface between the CPU and rest of the system (the dotted lines).
--
2.7.4
^ permalink raw reply related [flat|nested] 15+ messages in thread
* [PATCH 6/6] advsync/memorybarriers: Distinguish 'CPU family' from 'CPU'
2017-03-13 22:43 [PATCH 0/6] Misc updates and fixes Akira Yokosawa
` (4 preceding siblings ...)
2017-03-13 22:48 ` [PATCH 5/6] advsync/memorybarriers: Refer explicit Figure label Akira Yokosawa
@ 2017-03-13 22:49 ` Akira Yokosawa
2017-03-14 12:37 ` [PATCH v2 0/6] Misc updates Akira Yokosawa
6 siblings, 0 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-13 22:49 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 93e02eca9bb8361be47e0936f5d2ca56586bc093 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 13 Mar 2017 20:50:56 +0900
Subject: [PATCH 6/6] advsync/memorybarriers: Distinguish 'CPU family' from 'CPU'
In these paragraphs, "CPU" stands for either "CPU core" or
"CPU family". Explicitly use "CPU family" for the latter.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
advsync/memorybarriers.tex | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
index 85e9162..15ed1f6 100644
--- a/advsync/memorybarriers.tex
+++ b/advsync/memorybarriers.tex
@@ -415,11 +415,11 @@ If you just want to be told what the rules are rather than suffering
through the actual derivation,
please feel free to skip to Section~\ref{sec:advsync:A Few Simple Rules}.
-The exact semantics of memory barriers vary wildly from one CPU to
+The exact semantics of memory barriers vary wildly from one CPU family to
another, so portable code must rely only on the least-common-denominator
semantics of memory barriers.
-Fortunately, all CPUs impose the following rules:
+Fortunately, all CPU families impose the following rules:
\begin{enumerate}
\item All accesses by a given CPU will appear to that CPU to have
occurred in program order.
@@ -442,9 +442,9 @@ Each of these properties is described in the following sections.
A given CPU will see its own accesses as occurring in ``program order'',
as if the CPU was executing only one instruction at a time with no
reordering or speculation.
-For older CPUs, this restriction is necessary for binary compatibility,
+For older CPU families, this restriction is necessary for binary compatibility,
and only secondarily for the sanity of us software types.
-There have been a few CPUs that violate this rule to a limited extent,
+There have been a few CPU families that violate this rule to a limited extent,
but in those cases, the compiler has been responsible
for ensuring that ordering is explicitly enforced as needed.
@@ -511,7 +511,7 @@ of an external logic analyzer
However, if CPU~2's access to B sees the result of CPU~1's access
to B, then CPU~2's access to A is guaranteed to see the result of
CPU~1's access to A.
-Although some CPUs' memory barriers do in fact provide stronger,
+Although some CPU families' memory barriers do in fact provide stronger,
unconditional ordering guarantees, portable code may rely only
on this weaker if-then conditional ordering guarantee.
--
2.7.4
^ permalink raw reply related [flat|nested] 15+ messages in thread
* [PATCH v2 0/6] Misc updates
2017-03-13 22:43 [PATCH 0/6] Misc updates and fixes Akira Yokosawa
` (5 preceding siblings ...)
2017-03-13 22:49 ` [PATCH 6/6] advsync/memorybarriers: Distinguish 'CPU family' from 'CPU' Akira Yokosawa
@ 2017-03-14 12:37 ` Akira Yokosawa
2017-03-14 12:38 ` [PATCH v2 1/6] runlatex.sh: Refactor further Akira Yokosawa
` (5 more replies)
6 siblings, 6 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-14 12:37 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From ad3fca471bd3a6178f7988bbe5c9ab903f86722a Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 14 Mar 2017 21:30:58 +0900
Subject: [PATCH v2 0/6] Misc updates
Hi Paul,
I fixed grammatical errors in commit logs.
No change in diffs.
Thanks, Akira
--
Akira Yokosawa (6):
runlatex.sh: Refactor further
formal/spinhint: Fix typo
formal/spinhint: Adjust option of enumerate list
formal/spinhint: Reference by Figure labels
advsync/memorybarriers: Reference by Figure label
advsync/memorybarriers: Distinguish 'CPU family' from 'CPU'
advsync/memorybarriers.tex | 13 +++++++------
formal/spinhint.tex | 16 +++++++++-------
utilities/runlatex.sh | 27 +++++++++++++++++----------
3 files changed, 33 insertions(+), 23 deletions(-)
--
2.7.4
^ permalink raw reply [flat|nested] 15+ messages in thread
* [PATCH v2 1/6] runlatex.sh: Refactor further
2017-03-14 12:37 ` [PATCH v2 0/6] Misc updates Akira Yokosawa
@ 2017-03-14 12:38 ` Akira Yokosawa
2017-03-14 16:30 ` Paul E. McKenney
2017-03-14 12:39 ` [PATCH v2 2/6] formal/spinhint: Fix typo Akira Yokosawa
` (4 subsequent siblings)
5 siblings, 1 reply; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-14 12:38 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From a87bed749d870ce45fd7b328f4099a58271dfa20 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 13 Mar 2017 20:42:39 +0900
Subject: [PATCH v2 1/6] runlatex.sh: Refactor further
This won't result in reducing line count, but is worth doing.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
utilities/runlatex.sh | 27 +++++++++++++++++----------
1 file changed, 17 insertions(+), 10 deletions(-)
diff --git a/utilities/runlatex.sh b/utilities/runlatex.sh
index e6b3938..cece545 100644
--- a/utilities/runlatex.sh
+++ b/utilities/runlatex.sh
@@ -39,6 +39,17 @@ diff_warning () {
fi
}
+identical_warnings () {
+ if test -r $basename-warning-prev.log
+ then
+ if test "$iter" -gt "$min_iter" && diff_warning
+ then
+ return 0 ;
+ fi
+ fi
+ return 1 ;
+}
+
iterate_latex () {
pdflatex $basename > /dev/null 2>&1 < /dev/null || :
if grep -q '! Emergency stop.' $basename.log
@@ -76,27 +87,23 @@ rm -f $basename-first.log
iter=2
echo "pdflatex 2 for $basename.pdf # for possible bib update"
iterate_latex
+min_iter=2
while grep -q 'LaTeX Warning: There were undefined references' $basename.log
do
- if test -r $basename-warning-prev.log
+ if identical_warnings
then
- if test "$iter" -gt 2 && diff_warning
- then
- break
- fi
+ break
fi
iter=`expr $iter + 1`
echo "pdflatex $iter for $basename.pdf # remaining undefined refs"
iterate_latex
done
+min_iter=3
while grep -q 'LaTeX Warning: Label(s) may have changed' $basename.log
do
- if test -r $basename-warning-prev.log
+ if identical_warnings
then
- if test "$iter" -gt 3 && diff_warning
- then
- break
- fi
+ break
fi
iter=`expr $iter + 1`
echo "pdflatex $iter for $basename.pdf # label(s) may have changed"
--
2.7.4
^ permalink raw reply related [flat|nested] 15+ messages in thread
* [PATCH v2 2/6] formal/spinhint: Fix typo
2017-03-14 12:37 ` [PATCH v2 0/6] Misc updates Akira Yokosawa
2017-03-14 12:38 ` [PATCH v2 1/6] runlatex.sh: Refactor further Akira Yokosawa
@ 2017-03-14 12:39 ` Akira Yokosawa
2017-03-14 12:40 ` [PATCH v2 3/6] formal/spinhint: Adjust option of enumerate list Akira Yokosawa
` (3 subsequent siblings)
5 siblings, 0 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-14 12:39 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 32cf4c216eb3b0c8395ecff9ffa2e53e1e415c89 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 13 Mar 2017 20:47:29 +0900
Subject: [PATCH v2 2/6] formal/spinhint: Fix typo
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 87a7040..a10b57b 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -854,8 +854,8 @@ latencies of most other RCU implementations.
\item There are \co{qrcu_read_lock()} and \co{qrcu_read_unlock()}
primitives that delimit QRCU read-side critical sections.
The corresponding \co{qrcu_struct} must be passed into
- these primitives, and the return value from \co{rcu_read_lock()}
- must be passed to \co{rcu_read_unlock()}.
+ these primitives, and the return value from \co{qrcu_read_lock()}
+ must be passed to \co{qrcu_read_unlock()}.
For example:
--
2.7.4
^ permalink raw reply related [flat|nested] 15+ messages in thread
* [PATCH v2 3/6] formal/spinhint: Adjust option of enumerate list
2017-03-14 12:37 ` [PATCH v2 0/6] Misc updates Akira Yokosawa
2017-03-14 12:38 ` [PATCH v2 1/6] runlatex.sh: Refactor further Akira Yokosawa
2017-03-14 12:39 ` [PATCH v2 2/6] formal/spinhint: Fix typo Akira Yokosawa
@ 2017-03-14 12:40 ` Akira Yokosawa
2017-03-14 12:41 ` [PATCH v2 4/6] formal/spinhint: Reference by Figure labels Akira Yokosawa
` (2 subsequent siblings)
5 siblings, 0 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-14 12:40 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From fe01252839978d67b611eafca1c49e8772582fd2 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 13 Mar 2017 20:47:56 +0900
Subject: [PATCH v2 3/6] formal/spinhint: Adjust option of enumerate list
This enumeration list can be optimized by specifying starting
count and label format. It is also better to use a narrower
item separation.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
formal/spinhint.tex | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index a10b57b..d6acef1 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -924,10 +924,10 @@ sections).
The \co{readerprogress} array elements have values as follows,
indicating the state of the corresponding reader:
-\begin{enumerate}
-\item 0: not yet started.
-\item 1: within QRCU read-side critical section.
-\item 2: finished with QRCU read-side critical section.
+\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.
\end{enumerate}
Finally, the \co{mutex} variable is used to serialize updaters' slowpaths.
--
2.7.4
^ permalink raw reply related [flat|nested] 15+ messages in thread
* [PATCH v2 4/6] formal/spinhint: Reference by Figure labels
2017-03-14 12:37 ` [PATCH v2 0/6] Misc updates Akira Yokosawa
` (2 preceding siblings ...)
2017-03-14 12:40 ` [PATCH v2 3/6] formal/spinhint: Adjust option of enumerate list Akira Yokosawa
@ 2017-03-14 12:41 ` Akira Yokosawa
2017-03-14 12:42 ` [PATCH v2 5/6] advsync/memorybarriers: Reference by Figure label Akira Yokosawa
2017-03-14 12:43 ` [PATCH v2 6/6] advsync/memorybarriers: Distinguish 'CPU family' from 'CPU' Akira Yokosawa
5 siblings, 0 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-14 12:41 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 267bc5727f8f50d389818c22c81ea9a6e1d810e4 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
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@gmail.com>
---
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
^ permalink raw reply related [flat|nested] 15+ messages in thread
* [PATCH v2 5/6] advsync/memorybarriers: Reference by Figure label
2017-03-14 12:37 ` [PATCH v2 0/6] Misc updates Akira Yokosawa
` (3 preceding siblings ...)
2017-03-14 12:41 ` [PATCH v2 4/6] formal/spinhint: Reference by Figure labels Akira Yokosawa
@ 2017-03-14 12:42 ` Akira Yokosawa
2017-03-14 12:43 ` [PATCH v2 6/6] advsync/memorybarriers: Distinguish 'CPU family' from 'CPU' Akira Yokosawa
5 siblings, 0 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-14 12:42 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From e495d83986561ebddebc268abdd82284060f1a50 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 13 Mar 2017 20:50:12 +0900
Subject: [PATCH v2 5/6] advsync/memorybarriers: Reference by Figure label
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
advsync/memorybarriers.tex | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
index 98f7787..85e9162 100644
--- a/advsync/memorybarriers.tex
+++ b/advsync/memorybarriers.tex
@@ -1135,7 +1135,8 @@ appears to be maintained. Similarly, the compiler may also arrange the
instructions it emits in any order it likes, provided it doesn't affect the
apparent operation of the program.
-So in the above diagram, the effects of the memory operations performed by a
+So in Figure~\ref{fig:advsync:Abstract Memory Access Model},
+the effects of the memory operations performed by a
CPU are perceived by the rest of the system as the operations cross the
interface between the CPU and rest of the system (the dotted lines).
--
2.7.4
^ permalink raw reply related [flat|nested] 15+ messages in thread
* [PATCH v2 6/6] advsync/memorybarriers: Distinguish 'CPU family' from 'CPU'
2017-03-14 12:37 ` [PATCH v2 0/6] Misc updates Akira Yokosawa
` (4 preceding siblings ...)
2017-03-14 12:42 ` [PATCH v2 5/6] advsync/memorybarriers: Reference by Figure label Akira Yokosawa
@ 2017-03-14 12:43 ` Akira Yokosawa
5 siblings, 0 replies; 15+ messages in thread
From: Akira Yokosawa @ 2017-03-14 12:43 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From ad3fca471bd3a6178f7988bbe5c9ab903f86722a Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 13 Mar 2017 20:50:56 +0900
Subject: [PATCH v2 6/6] advsync/memorybarriers: Distinguish 'CPU family' from 'CPU'
In these paragraphs, "CPU" stands for either "CPU core" or
"CPU family". Explicitly use "CPU family" for the latter.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
advsync/memorybarriers.tex | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
index 85e9162..15ed1f6 100644
--- a/advsync/memorybarriers.tex
+++ b/advsync/memorybarriers.tex
@@ -415,11 +415,11 @@ If you just want to be told what the rules are rather than suffering
through the actual derivation,
please feel free to skip to Section~\ref{sec:advsync:A Few Simple Rules}.
-The exact semantics of memory barriers vary wildly from one CPU to
+The exact semantics of memory barriers vary wildly from one CPU family to
another, so portable code must rely only on the least-common-denominator
semantics of memory barriers.
-Fortunately, all CPUs impose the following rules:
+Fortunately, all CPU families impose the following rules:
\begin{enumerate}
\item All accesses by a given CPU will appear to that CPU to have
occurred in program order.
@@ -442,9 +442,9 @@ Each of these properties is described in the following sections.
A given CPU will see its own accesses as occurring in ``program order'',
as if the CPU was executing only one instruction at a time with no
reordering or speculation.
-For older CPUs, this restriction is necessary for binary compatibility,
+For older CPU families, this restriction is necessary for binary compatibility,
and only secondarily for the sanity of us software types.
-There have been a few CPUs that violate this rule to a limited extent,
+There have been a few CPU families that violate this rule to a limited extent,
but in those cases, the compiler has been responsible
for ensuring that ordering is explicitly enforced as needed.
@@ -511,7 +511,7 @@ of an external logic analyzer
However, if CPU~2's access to B sees the result of CPU~1's access
to B, then CPU~2's access to A is guaranteed to see the result of
CPU~1's access to A.
-Although some CPUs' memory barriers do in fact provide stronger,
+Although some CPU families' memory barriers do in fact provide stronger,
unconditional ordering guarantees, portable code may rely only
on this weaker if-then conditional ordering guarantee.
--
2.7.4
^ permalink raw reply related [flat|nested] 15+ messages in thread
* Re: [PATCH v2 1/6] runlatex.sh: Refactor further
2017-03-14 12:38 ` [PATCH v2 1/6] runlatex.sh: Refactor further Akira Yokosawa
@ 2017-03-14 16:30 ` Paul E. McKenney
0 siblings, 0 replies; 15+ messages in thread
From: Paul E. McKenney @ 2017-03-14 16:30 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Tue, Mar 14, 2017 at 09:38:31PM +0900, Akira Yokosawa wrote:
> >From a87bed749d870ce45fd7b328f4099a58271dfa20 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Mon, 13 Mar 2017 20:42:39 +0900
> Subject: [PATCH v2 1/6] runlatex.sh: Refactor further
>
> This won't result in reducing line count, but is worth doing.
I applied and pushed this v2 series, thank you!
Thanx, Paul
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> ---
> utilities/runlatex.sh | 27 +++++++++++++++++----------
> 1 file changed, 17 insertions(+), 10 deletions(-)
>
> diff --git a/utilities/runlatex.sh b/utilities/runlatex.sh
> index e6b3938..cece545 100644
> --- a/utilities/runlatex.sh
> +++ b/utilities/runlatex.sh
> @@ -39,6 +39,17 @@ diff_warning () {
> fi
> }
>
> +identical_warnings () {
> + if test -r $basename-warning-prev.log
> + then
> + if test "$iter" -gt "$min_iter" && diff_warning
> + then
> + return 0 ;
> + fi
> + fi
> + return 1 ;
> +}
> +
> iterate_latex () {
> pdflatex $basename > /dev/null 2>&1 < /dev/null || :
> if grep -q '! Emergency stop.' $basename.log
> @@ -76,27 +87,23 @@ rm -f $basename-first.log
> iter=2
> echo "pdflatex 2 for $basename.pdf # for possible bib update"
> iterate_latex
> +min_iter=2
> while grep -q 'LaTeX Warning: There were undefined references' $basename.log
> do
> - if test -r $basename-warning-prev.log
> + if identical_warnings
> then
> - if test "$iter" -gt 2 && diff_warning
> - then
> - break
> - fi
> + break
> fi
> iter=`expr $iter + 1`
> echo "pdflatex $iter for $basename.pdf # remaining undefined refs"
> iterate_latex
> done
> +min_iter=3
> while grep -q 'LaTeX Warning: Label(s) may have changed' $basename.log
> do
> - if test -r $basename-warning-prev.log
> + if identical_warnings
> then
> - if test "$iter" -gt 3 && diff_warning
> - then
> - break
> - fi
> + break
> fi
> iter=`expr $iter + 1`
> echo "pdflatex $iter for $basename.pdf # label(s) may have changed"
> --
> 2.7.4
>
>
^ permalink raw reply [flat|nested] 15+ messages in thread
end of thread, other threads:[~2017-03-14 16:30 UTC | newest]
Thread overview: 15+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2017-03-13 22:43 [PATCH 0/6] Misc updates and fixes Akira Yokosawa
2017-03-13 22:44 ` [PATCH 1/6] runlatex.sh: Refactor further Akira Yokosawa
2017-03-13 22:45 ` [PATCH 2/6] formal/spinhint: Fix typo Akira Yokosawa
2017-03-13 22:46 ` [PATCH 3/6] formal/spinhint: Adjust option of enumerate list Akira Yokosawa
2017-03-13 22:47 ` [PATCH 4/6] formal/spinhint: Refer explicit Figure labels Akira Yokosawa
2017-03-13 22:48 ` [PATCH 5/6] advsync/memorybarriers: Refer explicit Figure label Akira Yokosawa
2017-03-13 22:49 ` [PATCH 6/6] advsync/memorybarriers: Distinguish 'CPU family' from 'CPU' Akira Yokosawa
2017-03-14 12:37 ` [PATCH v2 0/6] Misc updates Akira Yokosawa
2017-03-14 12:38 ` [PATCH v2 1/6] runlatex.sh: Refactor further Akira Yokosawa
2017-03-14 16:30 ` Paul E. McKenney
2017-03-14 12:39 ` [PATCH v2 2/6] formal/spinhint: Fix typo Akira Yokosawa
2017-03-14 12:40 ` [PATCH v2 3/6] formal/spinhint: Adjust option of enumerate list Akira Yokosawa
2017-03-14 12:41 ` [PATCH v2 4/6] formal/spinhint: Reference by Figure labels Akira Yokosawa
2017-03-14 12:42 ` [PATCH v2 5/6] advsync/memorybarriers: Reference by Figure label Akira Yokosawa
2017-03-14 12:43 ` [PATCH v2 6/6] advsync/memorybarriers: Distinguish 'CPU family' from 'CPU' Akira Yokosawa
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox