bwconsistency/docs/présentation_consistence_faible/wconsistence_properties/index.tex

\begin{frame}
    \frametitle{Linéarisation}
    \begin{block}{Définition}
        Un ensemble d'événement est dit linéarisable s'il existe une séquence d'événement qui respecte les 3 propriétés suivantes :
        \begin{itemize}
            \item \textbf{Sûreté}
            \item \textbf{Régularité}
            \item \textbf{Atomicité}
        \end{itemize}
    \end{block}
\end{frame}

\begin{frame}
    \frametitle{Sûreté}
    \begin{block}{Définition}
        Toute lecture réalisée dans un même environnement non-concurrent est identique.
    \end{block}
    \begin{figure}
        \include{wconsistence_properties/linearisation_surete_hc}
    \end{figure}
\end{frame}

\begin{frame}
    \frametitle{Régularité}
    \begin{block}{Définition}
        Une lecture concurrente à une écriture peut lire soit la valeur avant l'écriture, soit la valeur après l'écriture.
    \end{block}
    \begin{figure}
        \include{wconsistence_properties/linearisation_regularite_hc}
    \end{figure}
\end{frame}

\begin{frame}
    \frametitle{Atomicité}
    \begin{block}{Définition}
        Si deux lectures ne sont pas concurrente la deuxième doit retourner une valeur au moins aussi récente que la première.
    \end{block}
    \begin{figure}
        \include{wconsistence_properties/linearisation_atomicite_hc}
    \end{figure}
\end{frame}

\begin{frame}
    \frametitle{Les classes de cohérence}
    \begin{columns}
        \column{0.5\textwidth}
        \resizebox{\columnwidth}{!}{
            \includegraphics{images/carte_criteres.png}
        }

        \column{0.5\textwidth}
        Une approche pour définir la cohérence d'un algorithme est de placer l'histoire concurrente qu'il produit dans une classe de cohérence. \\
        Nous pouvons définir 3 classes de cohérence : %citer Perrin
        \begin{itemize}
            \item La \textbf{Localité d'état} (LS)
            \item La \textbf{Validité} (V)
            \item La \textbf{Convergence} (EC)
        \end{itemize}
    \end{columns}


\end{frame}

\begin{frame}
    \frametitle{Localité d'état (LS)}

    \begin{columns}
        \column{0.4\textwidth}
        \include{wconsistence_properties/localiteetat_hc}
        \column{0.6\textwidth}
        \begin{block}{Définition}
            Pour tout processus $p$, il existe une linéarisation contenant toutes les lectures pures de $p$. \\
        \end{block}
        \begin{math}
            \begin{array}{ll}
                e.g.: & \textcolor{blue}{C_{p_1} = \{r/(0,0), r/(0,2)^w, w(2)\}}, \\
                      & \textcolor{red}{C_{p_2} = \{r/(0,0), r/(0,1)^w, w(1)\}},  \\
                      & \textcolor{blue}{r/(0,0) \bullet w(2) \bullet r/(0,2)^w}  \\
                      & \textcolor{red}{r/(0,0) \bullet w(1) \bullet r/(0,1)^w}   \\
            \end{array}
        \end{math}
    \end{columns}


    \begin{flushright}
        \begin{math}
            LS = \left\{
            \begin{array}{l}
                \mathcal{T} \rightarrow \mathcal{P}(\mathcal{H}) \\
                T \rightarrow \left\{
                \begin{tabular}{lll}
                    $H \in \mathcal{H}:$ & \multicolumn{2}{l}{$\forall p \in \mathcal{P}_H, \exists C_p \subset E_H,$}                                                       \\
                                         &                                                                             & $\hat{Q}_{T,H} \subset C_p$                         \\
                                         & $\land$                                                                     & $lin(H[p \cap C_p / C_p]) \cap L(T) \neq \emptyset$ \\
                \end{tabular}
                \right.                                          \\
            \end{array}
            \right.
        \end{math}
    \end{flushright}
\end{frame}


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

    \begin{columns}
        \column{0.4\textwidth}
        \include{wconsistence_properties/validite_hc}
        \column{0.6\textwidth}
        \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{math}
            \begin{array}{ll}
                e.g.: & E' = \{r/(2,1)^w, r/(1,2)^w\}                        \\
                      & w(2) \bullet w(1) \bullet \textcolor{red}{r/(2,1)^w} \\
                      & w(1) \bullet w(2) \bullet \textcolor{red}{r/(1,2)^w} \\
            \end{array}
        \end{math}
    \end{columns}


    \begin{flushright}
        \begin{math}
            V = \left\{
            \begin{array}{l}
                \mathcal{T} \rightarrow \mathcal{P}(\mathcal{H}) \\
                T \rightarrow \left\{
                \begin{array}{lll}
                    H \in \mathcal{H}: & \multicolumn{2}{l}{|U_{T,H}| = \infty}                                                                       \\
                                       & \lor                                   & \exists E' \subset E_H, (|E_H \setminus E'| < \infty                \\
                                       &                                        & \land \forall e \in E', lin(H[E_H / {e}]) \cap L(T) \neq \emptyset) \\
                \end{array}
                \right.                                          \\
            \end{array}
            \right.
        \end{math}
    \end{flushright}
\end{frame}


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

    \begin{columns}
        \column{0.4\textwidth}
        \include{wconsistence_properties/convergence_hc}%
        \column{0.5\textwidth}
        \begin{block}{Définition}
            Il existe un ensemble cofini d'événements dont chacun peut être justifié par une seule linéarisation. \\
        \end{block}
        \begin{math}
            \begin{array}{ll}
                e.g.: & E' = \{r/(1,2)^w, r/(1,2)^w\}                        \\
                      & w(1) \bullet w(2) \bullet \textcolor{red}{r/(1,2)^w} \\
            \end{array}
        \end{math}
    \end{columns}


    \begin{flushright}
        \begin{math}
            EC = \left\{
            \begin{array}{l}
                \mathcal{T} \rightarrow \mathcal{P}(\mathcal{H}) \\
                T \rightarrow \left\{
                \begin{array}{lll}
                    H \in \mathcal{H}: & \multicolumn{2}{l}{|U_{T,H}| = \infty}                                                                                  \\
                                       & \lor                                   & \exists E' \subset E_H, |E_H \setminus E'| < \infty                            \\
                                       &                                        & \land \displaystyle\bigcap_{e \in E'} \delta_T^{-1}(\lambda(e)) \neq \emptyset \\
                \end{array}
                \right.                                          \\
            \end{array}
            \right.
        \end{math}
    \end{flushright}
\end{frame}