hard push

This commit is contained in:
amaury
2024-12-17 14:57:43 +01:00
parent e51d7de452
commit ab70a09cbf
38 changed files with 2570 additions and 1 deletions

View File

@ -0,0 +1,14 @@
\begin{frame}
\frametitle{The Byzantine context associated with the weak consistency}
\begin{block}{Some questions about:}
\begin{itemize}
\item is the weak consistency introduces more or less possibility of malicious behaviors.
\item is the cost to make a system Byzantine Fault Tolerant is higher or lower with weak consistency.
\end{itemize}
\end{block}
The state of the art is poor about these questions and few formalized algorithms are available.
\end{frame}

View File

@ -0,0 +1,122 @@
\begin{frame}
\frametitle{The models of consistency}
\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 big family :
\begin{itemize}
\item Strong Consistency
\item Weak Consistency :
\begin{itemize}
\item Eventual Consistency (EC)
\item State Locality (SL)
\item Validity (V)
\end{itemize}
\end{itemize}
\end{block}
\end{columns}
\end{frame}
\begin{frame}
\frametitle{Eventual Consistency (EC)}
\begin{block}{Definition}
There exists a set of cofinite operations where each one must be justified with the same state.
\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)$ is a valid state justifying $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
There exists no state able to justify $E'$ because the two infinite reads are not consistent.
\end{columns}
\end{frame}
\begin{frame}
\frametitle{State Locality}
\begin{block}{Definition}
For all $p$, there exists one linearization that includes all the read operations of $p$. According to the local order of these reads. \\
\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
There exists no linearization of $p_1$ satisfying the definition of state locality
\end{columns}
\end{frame}
\begin{frame}
\frametitle{Validity (V)}
\begin{block}{Definition}
There exists a cofinite set of operations such as each of them must be justified by a linearization of all the write operations.
\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\}$. \\
There is no linearization of the write operation able to justify $r/(0,1)^\omega$.
\end{columns}
\end{frame}

View File

@ -0,0 +1,45 @@
\begin{frame}
\frametitle{Safety}
\begin{block}{Definition}
Each \textbf{read} operation made in the same \textbf{non-competitor} context provides the same result.
\end{block}
\begin{figure}
\input{schemas/linearisation_surete_hc}
\end{figure}
\end{frame}
\begin{frame}
\frametitle{Regularity}
\begin{block}{Definition}
An \textbf{reading operation concurrent with a writing operation} must provide the value \textbf{before or after the write}.
\end{block}
\begin{figure}
\input{schemas/linearisation_regularite_hc}
\end{figure}
\end{frame}
\begin{frame}
\frametitle{Atomicity}
\begin{block}{Definition}
If \textbf{two readings are non-competitor}, the second one must provide a value \textbf{at least as recent as} the previous one.
\end{block}
\begin{figure}
\input{schemas/linearisation_atomicite_hc}
\end{figure}
\end{frame}
\begin{frame}
\frametitle{Atomic Consistency ($C_\top$)}
\begin{block}{Définition}
Atomic consistency is the stronger consistency class.
\begin{itemize}
\item Provide an awful interactivity.
\item Need a strong synchronization between each operation.
\begin{itemize}
\item Each read or write operation locks the others and needs to wait for the release from the previous one.
\end{itemize}
\item He's used as a reference for the other consistency class.
\end{itemize}
\end{block}
\end{frame}

View File

@ -0,0 +1,8 @@
\subsection{Strong consistency}
\include{consistency/forte.tex}
\subsection{The compromises of the strong consistency}
\include{consistency/faible.tex}
\subsection{In a malicious context ?}
\include{consistency/byzantin.tex}