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

\begin{frame}
    \frametitle{Linéarisation}
    % \begin{itemize}
    % \end{itemize}
\end{frame}

\begin{frame}
    \frametitle{Sureté}
    \begin{block}{Définition}
        Toute lécture réalisé dans un même environement non-concurrent est identique.
    \end{block}
    \begin{figure}
        \include{wconsitence_properties/linearisation_surete_hc}
    \end{figure}
\end{frame}

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

\begin{frame}
    \frametitle{Atomicité}
    \begin{block}{Définition}
        Une lécture concurrente à une écriture peut lire soit la valeur avant l'écriture, soit la valeur après l'écriture.
    \end{block}
    \begin{figure}              
        \include{wconsitence_properties/linearisation_atomicite_hc}
    \end{figure}
\end{frame}

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

    \begin{columns}
        \column{0.4\textwidth}
        \include{wconsitence_properties/convergence_hc}%
        \column{0.5\textwidth}
        Il existe un ensemble cofini d'évenements dont chacun peut être justifier par la même linéarisation. \\
        \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}


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

    \begin{columns}
        \column{0.4\textwidth}
        \include{wconsitence_properties/validite_hc}
        \column{0.6\textwidth}
        Il existe, un ensemble cofini d'évenement tels que pour chacun d'entre eux une linéarisations de toutes les opérations d'écriture les justifient. \\
        \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{Localité d'état (LS)}

    \begin{columns}
        \column{0.4\textwidth}
        \include{wconsitence_properties/localiteetat_hc}
        \column{0.6\textwidth}
        Pour tout processus $p$, il existe une linéarisation contenant toutes les lectures pures de $p$ rendant l'histoire cohérente. \\
        \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}