bwconsistency/docs/presentations/LIS/vanderlinde/intro/rappel.tex

\begin{frame}
  \frametitle{Les modèles de cohérences}

  \begin{columns}
    \column{0.6\textwidth}
    \footnote{Perrin, \emph{Concurrence et cohérence dans les systèmes répartis}, 2017}
    \resizebox{\columnwidth}{!}{
      \includegraphics{images/carte_criteres.png}
    }

    \column{0.4\columnwidth}
    \begin{block}{Les classes de cohérences}
      2 Grandes familles :
      \begin{itemize}
        \item Cohérence Forte
        \item Cohérence Faible :
        \begin{itemize}
          \item Localité d'état (SL)
          \item Convergence (EC)
          \item Validité (V)
        \end{itemize}
      \end{itemize}
    \end{block}
  \end{columns}
\end{frame}

\begin{frame}
  \frametitle{Validité (V)}

  \begin{block}{Définition}
    Il existe, un ensemble cofini d'événement tel que pour chacun d'entre eux une linéarisation de toutes les opérations d'écriture les justifient. \\
  \end{block}

  \begin{columns}
    \column{0.4\columnwidth}
    \begin{tcolorbox}[colframe=green!50!black]
      \input{schemas/validite_hc_1}
    \end{tcolorbox}
    \column{0.5\columnwidth}
    \begin{math}
      \begin{array}{ll}
        E' = & \{r/(2,1)^\omega, r/(1,2)^\omega\}                             \\
             & w(2) \bullet w(1) \bullet \textcolor{red}{r/(2,1)^\omega} \\
             & w(1) \bullet w(2) \bullet \textcolor{red}{r/(1,2)^\omega} \\
      \end{array}
    \end{math}
  \end{columns}

  \begin{columns}
    \column{0.4\columnwidth}
    \begin{tcolorbox}[colframe=red!50!black]
      \input{schemas/validite_hc_2}
    \end{tcolorbox}
    \column{0.5\columnwidth}
    $E' = \{r/(0,1)^\omega, r/(1,2)^\omega\}$. \\
    Il n'existe pas de linéarisation des opérations d'écritures qui justifie $r/(0,1)^\omega$.
  \end{columns}
\end{frame}

\begin{frame}
  \frametitle{Localité d'état}

  \begin{block}{Définition}
    Pour tout processus $p$, il existe une linéarisation contenant toutes les lectures pures de $p$. Respectant l'ordre local de ces lectures. \\
  \end{block}

  \begin{columns}
    \column{0.4\columnwidth}
    \begin{tcolorbox}[colframe=green!50!black]
      \input{schemas/localiteetat_hc_1}
    \end{tcolorbox}
    \column{0.5\columnwidth}
    \begin{math}
      \begin{array}{l}
        \textcolor{blue}{C_{p_0} = \{r/(0,0), r/(0,2)^\omega, w(2)\}}, \\
        \textcolor{red}{C_{p_1} = \{r/(0,0), r/(0,1)^\omega, w(1)\}},  \\
        \textcolor{blue}{r/(0,0) \bullet w(2) \bullet r/(0,2)^\omega}  \\
        \textcolor{red}{r/(0,0) \bullet w(1) \bullet r/(0,1)^\omega}   \\
      \end{array}
    \end{math}
  \end{columns}

  \begin{columns}
    \column{0.4\columnwidth}
    \begin{tcolorbox}[colframe=red!50!black]
      \input{schemas/localiteetat_hc_2}
    \end{tcolorbox}
    \column{0.5\columnwidth}
    $E'_{p_0} = \{r/(0,0), r/(2,1)^\omega\},$ \newline
    $r/(0,0) \bullet w(2) \bullet w(1) \bullet r/(2,1)^\omega$  \newline
    $E'_{p_1} = \{r/(0,1), r/(2,1)^\omega\}$. \newline
    Il n'existe pas de linéarisation de $p_1$ respectant la localité d'état.
  \end{columns}
\end{frame}

\begin{frame}
  \frametitle{Convergence (EC)}

  \begin{block}{Définition}
    Il existe un ensemble cofini d'événements dont chacun peut être justifié par un seul et même état. \\
  \end{block}

  \begin{columns}
    \column{0.4\columnwidth}
    \begin{tcolorbox}[colframe=green!50!black]
      \input{schemas/convergence_hc_1}
    \end{tcolorbox}
    \column{0.5\columnwidth}
    $E' = \{r/(1,2)^\omega, r/(1,2)^\omega\}$ \newline
    $\delta = ((1,2), \emptyset)$ est un état possible justifiant $E'$.
  \end{columns}

  \begin{columns}
    \column{0.4\columnwidth}
    \begin{tcolorbox}[colframe=red!50!black]
      \input{schemas/convergence_hc_2}
    \end{tcolorbox}
    \column{0.5\columnwidth}
    $E' = \{r/(1,2)^\omega, r/(2,1)^\omega\}$. \newline
    Il n'existe aucun état possible justifiant $E'$ puisque deux lectures infinies sont incohérentes.
  \end{columns}
\end{frame}

\begin{frame}
  \frametitle{Cohérence Causale}

  \begin{columns}
    \column{0.6\textwidth}
    \resizebox{\columnwidth}{!}{
      \includegraphics{images/carte_criteres.png}
    }

    \column{0.4\columnwidth}
    \begin{block}{Les classes de la cohérence causale}
      \begin{itemize}
        \item \textbf{WCC}: Weak Causal Consistency (V)
        \item \textbf{CCv}: Causal Convergence (V, EC)
      \end{itemize}
    \end{block}

    On respecte les propriétés suivantes :
    \begin{itemize}
      \item Localité d'état (SL)
      \item Convergence (EC)
    \end{itemize}
  \end{columns}
\end{frame}