v1.1

declarative.tex

@@ -6,7 +6,7 @@
 %   \item \ldots
 %   \end{itemize}
 % \end{frame}
-\begin{frame}{We need to define fairness for different kinds of memory models}
+\begin{frame}{We've defined fairness for different kinds of memory models}
   \begin{center}
     \pause
     {\Large Operational models}:
@@ -63,7 +63,10 @@
     \pause
     \tikz[overlay,remember picture]{
       % \draw[frComp,bend right=120] (7, -1) edge node[] { } (7, 5);
-      \myrectMulti{Models}{(5, 0)}{SC: $acyclic(\lPO \cup \lRF \cup \lMO)$\\ TSO: $acyclic(\overline{\lPO} \cup \lRF \cup \lMO)$, $\overline{\lPO} \supset \lPO$}{6cm}{1cm}{white};
+      \myrectMulti{Models}{(5, 0)}
+      % {SC: $acyclic(\lPO \cup \lRF \cup \lMO)$\\ TSO: $acyclic(\overline{\lPO} \cup \lRF \cup \lMO)$, $\overline{\lPO} \supset \lPO$}
+      {TSO: $acyclic(\overline{\lPO} \cup \lRF \cup \lMO)$, $\overline{\lPO} \supset \lPO$}
+      {6cm}{1cm}{white};
     }
 
   \pause

loops_wmm.tex

@@ -1,3 +1,20 @@
+\begin{frame}{There are many concurrency semantics}
+  \todo{present this graphically}
+
+  \pause
+
+  Interleaving semantics (aka sequential consistency [Lamport 1979]) was the first one, but now there are others:
+  \pause
+
+  \begin{itemize}
+  \item \only<3>{{\colorbox{white}{tso [Owens et al. 2009]}}}\only<4>{{\colorbox{colorFR!50}{tso [Owens et al. 2009]}}}
+  \item ra (\todo{???})
+  \item rc11 [Lahav et al. 2017]
+  \item $\ldots$
+  \end{itemize}
+
+\end{frame}
+
 \begin{frame}{Spinlock may not terminate under other concurrency semantics}
   \spinlockLibClientII
   \pause
@@ -21,6 +38,14 @@
     \node at (\curEv-0.4, 0) {\ldots};
   \end{traceenv}
 
+  \onslide<4>{%
+    \tikz[overlay,remember picture]{
+    \node[fill=white,text=\colorTitleApprox,draw=none]
+    at ([xshift=2cm,yshift=3.4cm]current page.center){{\large(aka weak memory models)}};
+    }
+  }
+
+
 \end{frame}
 
 %%% Local Variables:

memory_fairness.tex

@@ -21,8 +21,8 @@
     \node at (\curEv-0.7, 1) {$\writeInst{l}{0}$ \stepcounter{evctr}};
     \node at (\curEv-0.7, 0) {\color{red} $CAS(l, 0, 1)$ \stepcounter{evctr}};
     \node at (\curEv-0.8, 1) {\color{blue} \underline{$\mathtt{prop}$} \stepcounter{evctr}};
-    \node at (\curEv-0.7, 0) {\color{blue} $CAS(l, 0, 1)$ \stepcounter{evctr}};
-    \node at (\curEv-0.7, 0) {\color{blue} $\writeInst{l}{0}$ \stepcounter{evctr}};
+    \node at (\curEv-0.7, 0) {$CAS(l, 0, 1)$ \stepcounter{evctr}};
+    \node at (\curEv-0.7, 0) {$\writeInst{l}{0}$ \stepcounter{evctr}};
   \end{traceenv}
 
 \end{frame}

practical.tex

@@ -1,10 +1,10 @@
-\begin{frame}{Declarative fairness definition simplifies termination proofs}
+\begin{frame}{We simplify termination proofs using the declarative fairness definition}
   \pause
   \spinlockLibClientIIVert
   \pause
   \begin{minipage}[c]{0.6\linewidth}
     \begin{restatable}{lem}{termination}
-      Under reasonable conditions$^*$, an infinite sequence of read events contains a read from $\lMO$-maximal write. \todo{Coq}
+      Under reasonable conditions$^*$, an infinite sequence of read events contains a read from $\lMO$-maximal write. \todo{better just place $\exists$ and Coq logo near the last rf}
     \end{restatable}
     \pause
 

terminates_sc.tex

@@ -1,11 +1,13 @@
-\begin{frame}{Spinlock terminates under sequential consistency \onslide<4->{[Lamport 1979], \ \ \ but now we use other semantics:}}
+% \begin{frame}{Spinlock terminates under sequential consistency \onslide<4->{[Lamport 1979], \ \ \ but now we use other semantics:}}
+\begin{frame}{Spinlock terminates under interleaving semantics}
   \only<1-3>{
 
 
   \spinlockLibClientII
   \pause
   \begin{minipage}[c]{0.4\linewidth}
     \begin{center}
+      \todo{animate this?}
       \scSystem      
     \end{center}
   \end{minipage}
@@ -34,14 +36,10 @@
 
   }
 
-  \only<4->{
-    \begin{itemize}
-    \item \only<4>{{\colorbox{white}{tso [Owens et al. 2009]}}}\only<5>{{\colorbox{colorFR!50}{tso [Owens et al. 2009]}}}
-    \item ra (\todo{???})
-    \item rc11 [Lahav et al. 2017]
-    \item $\ldots$
-    \end{itemize}
-  }
+  % \only<4->{
+  % }
+
+
   % \onslide<4>{%
   %   \tikz[overlay,remember picture]
   %   % \node[fill=white,text=\colorTitleApprox,draw=black]