>From 530d73392e389c1775946078391e9f017a4d9dad Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
Date: Sat, 14 Mar 2020 19:33:42 +0900
Subject: [PATCH 4/4] formal/axiomatic: Move table env next to QQA's first paragraph
Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
---
formal/axiomatic.tex | 31 ++++++++++++++++---------------
1 file changed, 16 insertions(+), 15 deletions(-)
diff --git a/formal/axiomatic.tex b/formal/axiomatic.tex
index 26e3f1ac..1565f413 100644
--- a/formal/axiomatic.tex
+++ b/formal/axiomatic.tex
@@ -188,6 +188,22 @@ And in this case, the \co{herd} tool's output features the string
Why bother modeling locking directly?
Why not simply emulate locking with atomic operations?
\QuickQuizAnswer{
+ In a word, performance, as can be seen in
+ Table~\ref{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
+ cat language.
+ The third column shows the 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}
+ 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
+ executions that fail to acquire the lock.
+
\begin{table}[tb]
\rowcolors{2}{}{lightgray}
\small
@@ -210,21 +226,6 @@ And in this case, the \co{herd} tool's output features the string
\caption{Locking: Modeling vs. Emulation Time (s)}
\label{tab:formal:Locking: Modeling vs. Emulation Time (s)}
\end{table}
- In a word, performance, as can be seen in
- Table~\ref{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
- cat language.
- The third column shows the 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}
- 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
- executions that fail to acquire the lock.
Note also that use of the \co{filter} clause is about twice
as fast as is use of the \co{exists} clause.
--
2.17.1
