>From 305c387fd4b8e6d3c5599b4ddbd67a03d939f832 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
Date: Fri, 27 Sep 2019 22:02:41 +0900
Subject: [PATCH 5/6] ppcmem: Add Quick Quiz on lwsync in Listing 12.23
The "lwsync" in front of ll-sc in atomic_add_return() is not
good enough for Linux kernel's semantics.
Add a Quick Quiz on the use of lwsync.
Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
---
formal/ppcmem.tex | 18 ++++++++++++++++++
1 file changed, 18 insertions(+)
diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index d292b7da..a1960e2d 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -328,6 +328,24 @@ cannot happen.
as an exercise for the reader.
} \QuickQuizEnd
+\QuickQuiz{}
+ \begin{lineref}[ln:formal:PPCMEM Litmus Test]
+ Is the \co{lwsync} on \clnref{P0lwsync} in
+ \cref{lst:formal:PPCMEM Litmus Test} good enough?
+ \end{lineref}
+\QuickQuizAnswer{
+ It depends on the semantics you expect.
+ As is discussed in
+ \cref{chp:Advanced Synchronization: Memory Ordering},
+ Linux kernel's momory consistency model requires
+ value-returning atomic RMW operations to be fully ordered
+ on both sides. \co{lwsync} is insufficient in this case and
+ should be \co{sync} instead. It has since been fixed~%
+ \cite{BoqunFeng2015:powerpc:value-returning-atomics}
+ as a result of an email thread on a couple of other litmus
+ tests~\cite{Paulmck2015:powerpc:value-returning-atomics}.
+} \QuickQuizEnd
+
\subsection{PPCMEM Discussion}
\label{sec:formal:PPCMEM Discussion}
--
2.17.1
