loops_wmm.tex

\begin{frame}{There are many modern 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}

  \begin{tikzpicture}[xscale=1, yscale=1]
    \node (SC) at (-1.5, 1) {Sequential consistency};
    \node (SCdate) at (-1.5, 0) {1979};
    \node (E1) at (-2.5, 0.5) {}; \node (E2) at (10, 0.5) {};

    \onslide<2->{
      \draw[time] (E1) edge node[] { } (E2);
    }

    \onslide<3->{
    \node (TSO) at (5, 1) {x86-TSO};
    \node (TSOdate) at (5, 0) {2009};
    }

    \onslide<4->{
    \node (Promising) at (7, 1) {Promising};
    \node (RC11) at (7, 1.5) {RC11};
    \node (RC11date) at (7, 0) {2017};
    }

    \onslide<5->{
    \node (WMO) at (9, 1) {WeakestMO};
    \node (WMOdate) at (9, 0) {2019};
    }

    \onslide<6->{
    \node (More) at (10.5, 0.5) {{\Large \ldots}};    
  }

  \onslide<7->{
  \draw [decorate,decoration={brace,amplitude=10pt,mirror,raise=4pt},yshift=0pt,draw=gray]
  (4, -1) -- (11, -1) node [black,midway,xshift=0.0cm,yshift=-1cm] {{\color{gray} Weak memory models}};
  }
  \end{tikzpicture}

  
\end{frame}

% \begin{frame}{Spinlock may not terminate under weak memory models without memory fairness}
%   \begin{frame}{Spinlock termination under TSO requires memory fairness}
\begin{frame}{Spinlock may not terminate under TSO\onslide<16->{ without \underline{memory fairness}}}

  \only<3->{\selectI \upd{\progPosI}{I}}
  \only<4->{\upd{\progPosI}{II}}
  \only<5->{\selectII \upd{\progPosII}{I}}
  \only<6->{\upd{\progPosII}{II}}
  \only<7->{\upd{\progPosII}{I}}
  \only<8->{\upd{\progPosII}{II}}
  \only<9->{\selectI \upd{\progPosI}{IV}}
  \only<10->{\selectII \upd{\progPosII}{I}}
  \only<11->{\upd{\progPosII}{II}}
  \only<12->{\upd{\progPosII}{I}}
  \only<13->{\upd{\progPosII}{II}}
  \only<14->{\upd{\progPosII}{I}}
  \only<15->{\upd{\progPosII}{II}}
  % 
  \only<17->{\upd{\progPosII}{I}}
  \only<18->{\upd{\progPosII}{II}}
  \only<19->{\upd{\progPosII}{IV}}

  
  \begin{columns}

    \begin{column}{0.4\linewidth}
      % \spinlockClientIIExpanded
      \spinlockClientIIExpandedIter
    \end{column}

    \begin{column}{0.5\linewidth}
      \tsoSystem
    \end{column}

  \end{columns}

  \vspace{0.5cm}

  \pause
  \begin{traceenv}{1.2}{0.9}
    \stepcounter{evctr}
    \onslide<4->{\node at (\curEv, 1) {$\ulab{}{l}{0}{1}$ \stepcounter{evctr}};}
    \onslide<6->{\node at (\curEv-0.5, 0) {$\rlab{}{l}{1}$ \stepcounter{evctr}};}
    \onslide<8->{\node at (\curEv-0.3, 0) {$\rlab{}{l}{1}$ \stepcounter{evctr}};}
    \onslide<9->{\node at (\curEv-0.5, 1) {$\wlab{}{l}{0}$ \stepcounter{evctr}};}
    \onslide<11->{\node at (\curEv-0.5, 0) {$\rlab{}{l}{1}$ \stepcounter{evctr}};}
    \onslide<13->{\node at (\curEv-0.9, 0) {\ldots};}
    \onslide<15->{\node at (\curEv-0.3, 0) {$\rlab{}{l}{1}$ \stepcounter{evctr}};}
    \onslide<16->{\node at (\curEv-0.8, 1) {\color{blue} \underline{$\mathtt{prop}$} \stepcounter{evctr}};}
    \onslide<18->{\node at (\curEv-0.7, 0) {$\ulab{}{l}{0}{1}$ \stepcounter{evctr}};}
    \onslide<19->{\node at (\curEv-0.4, 0) {$\wlab{}{l}{0}$};}
  \end{traceenv}

  

\end{frame}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "oopsla"
%%% End: