v1.2.1

fresheed · Sep 23, 2021 · 7e11350 · 7e11350
1 parent dad2d97
commit 7e11350
Show file tree

Hide file tree

Showing 5 changed files with 43 additions and 41 deletions.
diff --git a/conclusion.tex b/conclusion.tex
@@ -11,8 +11,8 @@
 
 \end{frame}
 
-% \begin{frame}{Takeaway}
-\begin{frame}
+\begin{frame}{Takeaway}
+% \begin{frame}
 
   % {\large Summary:}
   % \begin{itemize}
@@ -21,27 +21,9 @@
   % \item Which is used to prove lock algorithms termination.
   % \end{itemize}
 
-  \begin{center}
-    \spinlockClientIIExpanded
-    \vspace{0.5cm}
-    terminates because
-  \end{center}
-
   \begin{columns}
-    \begin{column}{0.4\linewidth}      
-      \scalebox{0.5}{\begin{traceenv}{1.4}{0.9}
-        \stepcounter{evctr}
-        \node at (\curEv-0.5, 1) {$CAS(l, 0, 1)$ \stepcounter{evctr}};
-        \node at (\curEv-0.7, 0) {$CAS(l, 0, 1)$ \stepcounter{evctr}};
-        \node at (\curEv-0.4, 0) {$CAS(l, 0, 1)$ \stepcounter{evctr}};
-        \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{something \ happens}$} \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}};
-      \end{traceenv}
-      }
+    \begin{column}{0.5\linewidth}      
+      \scalebox{0.7}{\fairTrace}
     \end{column}    
     \begin{column}{0.4\linewidth}
       \renewcommand{\hof}{2}
@@ -52,6 +34,7 @@
         \spinlockContraGraphRelationsI
         \spinlockContraGraphEventsII
         \spinlockContraGraphRelationsII
+        \spinlockContraGraphContra
       \end{tikzpicture}
       }
     \end{column}

diff --git a/declarative.tex b/declarative.tex
@@ -1,21 +1,23 @@
-\begin{frame}
-  \begin{center}
-    {\Large Fairness for \textit{operational} (interleaving-based) models:}
-    \vspace{0.25cm}
-    \pause
+\newcommand{\fairTrace}{
     \begin{traceenv}{1.4}{0.9}
     \stepcounter{evctr}
     \node at (\curEv-0.5, 1) {$\ulab{}{l}{0}{1}$ \stepcounter{evctr}};
     \node at (\curEv-0.7, 0) {$\rlab{}{l}{1}$ \stepcounter{evctr}};
     \node at (\curEv-0.4, 0) {$\rlab{}{l}{1}$ \stepcounter{evctr}};
     \node at (\curEv-0.7, 1) {$\wlab{}{l}{0}$ \stepcounter{evctr}};
     \node at (\curEv-0.7, 0) {$\rlab{}{l}{1}$ \stepcounter{evctr}};
-    \node at (\curEv-0.8, 1) {\color{blue} \underline{$\mathtt{something \ happens}$} \stepcounter{evctr}};
-
+    \node at (\curEv-0.8, 1) {\color{blue} \underline{$\mathtt{prop}$} \stepcounter{evctr}};    
     \node at (\curEv-0.7, 0) {$\ulab{}{l}{0}{1}$ \stepcounter{evctr}};
-    \node at (\curEv-0.7, 0) {$\wlab{}{l}{0}$ \stepcounter{evctr}};
+    \node at (\curEv-0.7, 0) {$\wlab{}{l}{0}$};
   \end{traceenv}
+}
 
+\begin{frame}
+  \begin{center}
+    {\Large Fairness for \textit{operational} (interleaving-based) models:}
+    \vspace{0.25cm}
+    \pause
+    \fairTrace
   \vspace{1cm}
   \pause
   {\Large Fairness for \textit{declarative} models: ???}

diff --git a/oopsla.tex b/oopsla.tex
@@ -9,14 +9,14 @@
 \newcommand{\vof}{0.5}
 
 % \date{} \frame{\titlepage} %1
-\input{terminates_sc} % 2
+% \input{terminates_sc} % 2
 % \input{loops_wmm} % 3
 % \input{memory_fairness} % 4
-% \input{declarative} % 5
+\input{declarative} % 5
 % \input{fairness_decl} % 6
 % \input{universal} % 7
 % \input{practical} % 8
-% \input{conclusion} % 9
+\input{conclusion} % 9
 
 \end{document} 
 

diff --git a/programs.tex b/programs.tex
@@ -197,6 +197,8 @@
 
       \drf{U1}{R21}; \drf{U1}{R22};
       \dmo[bend left=30]{W0}{U1}; \dmo[bend right=30]{U1}{W1};
+
+      \dfr{R21}{W1}{}; \dfr{R22}{W1}{};
 }
 \newcommand{\spinlockContraGraphRelationsII}{
   \drf{W1}{R24};

diff --git a/terminates_sc.tex b/terminates_sc.tex
@@ -1,26 +1,41 @@
-% \begin{frame}{Spinlock terminates under sequential consistency \onslide<4->{[Lamport 1979], \ \ \ but now we use other semantics:}}
-\begin{frame}{Spinlock terminates under interleaving semantics}
-
+\begin{frame}
   \begin{columns}
 
     \begin{column}{0.4\linewidth}
       \only<1-3>{
         \spinlockClientIICS        
         \begin{tikzpicture}[xscale=1, yscale=1]
-          \node (P1) at (0, 0) {\includegraphics[width=0.9\textwidth]{terminated.png}};
           \onslide<2-3>{
+            \node (P1) at (0, 0) {\includegraphics[width=0.9\textwidth]{terminated.png}};
+            }
+          \onslide<3>{
             \node (P2) at (0, 0) {\includegraphics[width=0.7\textwidth]{pending.png}};
             }
         \end{tikzpicture}
       }
-      \only<4->{\spinlockClientIIExpanded}
     \end{column}
 
     \begin{column}{0.5\linewidth}
-      \only<2>{
+      \only<3>{
         Multiple existing mutual exclusion lock implementations hang if too few fences are used (Oberhauser et al. [2021])
       }
-      \only<5->{
+    \end{column}
+
+  \end{columns}
+
+\end{frame}
+
+% \begin{frame}{Spinlock terminates under sequential consistency \onslide<4->{[Lamport 1979], \ \ \ but now we use other semantics:}}
+\begin{frame}{Spinlock terminates under interleaving semantics}
+
+  \begin{columns}
+
+    \begin{column}{0.4\linewidth}
+      \spinlockClientIIExpanded
+    \end{column}
+
+    \begin{column}{0.5\linewidth}
+      \only<2->{
         \scSystem
       }
     \end{column}
@@ -29,7 +44,7 @@
 
   \vspace{0.5cm}
 
-  \onslide<6->{
+  \onslide<3->{
   \begin{center}
     \begin{traceenv}{1.5}{0.9}
       \stepcounter{evctr}