>From 756c5ca8525904d2bc82941b990f70ac3c7dfe2f Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
Date: Sun, 2 Dec 2018 19:16:21 +0900
Subject: [PATCH 2/2] formal: Add C-Lock1 and C-Lock2 as proper litmus tests under CodeSamples
They are made klitmus7 ready and added to klitmus7-ready list in
the Makefile. Note that the list "LITMUS7_TEST" is now sorted
in alphabetical order. This make it easier to see the output of
klitmus7 test.
Also reference source file names from text (including RCU ones).
Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
---
CodeSamples/formal/herd/C-Lock1.litmus | 23 +++++++++++++
CodeSamples/formal/herd/C-Lock2.litmus | 23 +++++++++++++
CodeSamples/formal/herd/Makefile | 4 +--
formal/axiomatic.tex | 60 ++++------------------------------
4 files changed, 55 insertions(+), 55 deletions(-)
create mode 100644 CodeSamples/formal/herd/C-Lock1.litmus
create mode 100644 CodeSamples/formal/herd/C-Lock2.litmus
diff --git a/CodeSamples/formal/herd/C-Lock1.litmus b/CodeSamples/formal/herd/C-Lock1.litmus
new file mode 100644
index 0000000..5a1065d
--- /dev/null
+++ b/CodeSamples/formal/herd/C-Lock1.litmus
@@ -0,0 +1,23 @@
+C Lock1
+//\begin[snippet][labelbase=ln:formal:C-Lock1:whole,commandchars=\\\[\]]
+{
+}
+
+P0(int *x, spinlock_t *sp)
+{
+ spin_lock(sp);
+ WRITE_ONCE(*x, 1);
+ WRITE_ONCE(*x, 0);
+ spin_unlock(sp);
+}
+
+P1(int *x, spinlock_t *sp)
+{
+ int r1;
+
+ spin_lock(sp);
+ r1 = READ_ONCE(*x);
+ spin_unlock(sp);
+}
+//\end[snippet]
+exists (1:r1=1)
diff --git a/CodeSamples/formal/herd/C-Lock2.litmus b/CodeSamples/formal/herd/C-Lock2.litmus
new file mode 100644
index 0000000..dc28b24
--- /dev/null
+++ b/CodeSamples/formal/herd/C-Lock2.litmus
@@ -0,0 +1,23 @@
+C Lock2
+//\begin[snippet][labelbase=ln:formal:C-Lock2:whole,commandchars=\\\[\]]
+{
+}
+
+P0(int *x, spinlock_t *sp1)
+{
+ spin_lock(sp1);
+ WRITE_ONCE(*x, 1);
+ WRITE_ONCE(*x, 0);
+ spin_unlock(sp1);
+}
+
+P1(int *x, spinlock_t *sp2) // Buggy!
+{
+ int r1;
+
+ spin_lock(sp2);
+ r1 = READ_ONCE(*x);
+ spin_unlock(sp2);
+}
+//\end[snippet]
+exists (1:r1=1)
diff --git a/CodeSamples/formal/herd/Makefile b/CodeSamples/formal/herd/Makefile
index e23148e..cc022c5 100644
--- a/CodeSamples/formal/herd/Makefile
+++ b/CodeSamples/formal/herd/Makefile
@@ -37,7 +37,7 @@ LKMM_LIST := $(addprefix $(LKMM_DIR)/,$(LKMM_FILES))
HERD_DIR := $(shell pwd)
HERD7_CMD := $(shell which herd7)
KLITMUS7_CMD := $(shell which klitmus7)
-LITMUS7_TEST := $(notdir $(wildcard ../litmus/*.litmus))
+LITMUS7_TEST := $(sort $(notdir $(wildcard ../litmus/*.litmus)))
LITMUS7_HERD_TEST := $(addsuffix .herd,$(LITMUS7_TEST))
LITMUS7_HERD_OUT := $(addsuffix .out,$(LITMUS7_TEST))
HERD7_LITMUS := $(wildcard *.litmus)
@@ -49,7 +49,7 @@ ABSPERF_SHORT := $(filter-out $(ABSPERF_LONG),$(ABSPERF_TEST))
ABSPERF_OUT = absperf.out absperf-all.out
HERD7_TEST := $(filter-out $(ABSPERF_TEST),$(HERD7_LITMUS))
HERD7_OUT := $(HERD7_TEST:%.litmus=%.out)
-KLITMUS_READY = C-RCU-remove C-RomanPenyaev-list-rcu-rr
+KLITMUS_READY = C-Lock1 C-Lock2 C-RCU-remove C-RomanPenyaev-list-rcu-rr
KLITMUS_TEST := $(addsuffix .litmus,$(KLITMUS_READY))
.PHONY: all clean litmus2herd run-herd7 run-absperf run-absperf-all cross-klitmus
diff --git a/formal/axiomatic.tex b/formal/axiomatic.tex
index 65d1b6a..3d5ace0 100644
--- a/formal/axiomatic.tex
+++ b/formal/axiomatic.tex
@@ -138,31 +138,7 @@ This is now possible, as will be described in the following sections.
\label{sec:formal:Axiomatic Approaches and Locking}
\begin{listing}[tb]
-\begin{linelabel}[ln:formal:Locking Example]
-\begin{VerbatimL}[commandchars=\\\[\]]
-C Lock1
-
-{
-}
-
-P0(int *x, spinlock_t *sp)
-{
- spin_lock(sp);
- WRITE_ONCE(*x, 1);
- WRITE_ONCE(*x, 0);
- spin_unlock(sp);
-}
-
-P1(int *x, spinlock_t *sp)
-{
- spin_lock(sp);
- r1 = READ_ONCE(*x);
- spin_unlock(sp);
-}
-
-exists (1:r1=1)
-\end{VerbatimL}
-\end{linelabel}
+\input{CodeSamples/formal/herd/C-Lock1@xxxxxxxxx}
\caption{Locking Example}
\label{lst:formal:Locking Example}
\end{listing}
@@ -170,7 +146,7 @@ exists (1:r1=1)
Axiomatic approaches may also be applied to higher-level
languages and also to higher-level synchronization primitives, as
exemplified by the lock-based litmus test shown in
-Listing~\ref{lst:formal:Locking Example}.
+Listing~\ref{lst:formal:Locking Example} (\path{C-Lock1.litmus}).
As expected, the \co{herd} tool's output features the string \co{Never},
correctly indicating that \co{P1()} cannot see \co{x} having a value
of one.\footnote{
@@ -192,37 +168,13 @@ of one.\footnote{
} \QuickQuizEnd
\begin{listing}[tb]
-\begin{linelabel}[ln:formal:Broken Locking Example]
-\begin{VerbatimL}[commandchars=\\\[\]]
-C Lock2
-
-{
-}
-
-P0(int *x, spinlock_t *sp1)
-{
- spin_lock(sp1);
- WRITE_ONCE(*x, 1);
- WRITE_ONCE(*x, 0);
- spin_unlock(sp1);
-}
-
-P1(int *x, spinlock_t *sp2) // Buggy!
-{
- spin_lock(sp2);
- r1 = READ_ONCE(*x);
- spin_unlock(sp2);
-}
-
-exists (1:r1=1)
-\end{VerbatimL}
-\end{linelabel}
+\input{CodeSamples/formal/herd/C-Lock2@xxxxxxxxx}
\caption{Broken Locking Example}
\label{lst:formal:Broken Locking Example}
\end{listing}
Of course, if \co{P0()} and \co{P1()} use different locks, as shown in
-Listing~\ref{lst:formal:Broken Locking Example},
+Listing~\ref{lst:formal:Broken Locking Example} (\path{C-Lock2.litmus}),
then all bets are off.
And in this case, the \co{herd} tool's output features the string
\co{Sometimes}, correctly indicating that use of different locks allows
@@ -241,6 +193,7 @@ And in this case, the \co{herd} tool's output features the string
Axiomatic approaches can also analyze litmus tests involving RCU.
To that end,
Listing~\ref{lst:formal:Canonical RCU Removal Litmus Test}
+(\path{C-RCU-remove.litmus})
shows a litmus test corresponding to the canonical RCU-mediated
removal from a linked list.
Line~\lnref{head} shows \co{x} as the list head, initially
@@ -279,7 +232,8 @@ the \co{herd} output.
\begin{lineref}[ln:formal:C-RomanPenyaev-list-rcu-rr:whole]
A litmus test for a more complex example proposed by
Roman Penyaev~\cite{RomanPenyaev2018rrRCU} is shown in
-Listing~\ref{lst:formal:Complex RCU Litmus Test}.
+Listing~\ref{lst:formal:Complex RCU Litmus Test}
+(\path{C-RomanPenyaev-list-rcu-rr.litmus}).
In this example, readers (modeled by \co{P0()} on
lines~\lnref{P0start}--\lnref{P0end}) access a linked list
in a round-robin fashion by ``leaking'' a pointer to the last
--
2.7.4
