reorganisation
This commit is contained in:
Amaury
@ -0,0 +1,41 @@
|
||||
\resizebox{\columnwidth}{!}{
|
||||
\begin{tikzpicture}[
|
||||
roundnode/.style={circle, draw=black, fill=black, very thick, minimum size=1pt,},
|
||||
ignorednode/.style={circle, draw=black!20, fill=black!20, very thick, minimum size=1pt,},
|
||||
arrow/.style={|->, thick,},
|
||||
message/.style={->, blue!50, dashed, -{Circle[length=4pt,]}},
|
||||
]
|
||||
|
||||
\node[roundnode] (11) {};
|
||||
\node[left] at (11.west) {$p_0$};
|
||||
\node[above] at (11.north) {$w(1)$};
|
||||
\node[roundnode] (12) [right=of 11] {};
|
||||
\node[above] at (12.north) {$I(a)$};
|
||||
\node[roundnode] (13) [right=of 12] {};
|
||||
\node[above] at (13.north) {$r/(0,1)$};
|
||||
\node[roundnode] (14) [right=35pt of 13] {};
|
||||
\node[above] at (14.north) {$r/(1,2)^w$};
|
||||
|
||||
\draw[arrow] (11) -- (12);
|
||||
\draw[arrow] (12) -- (13);
|
||||
\draw[arrow] (13) -- (14);
|
||||
|
||||
\node[roundnode] (21) [below=of 11] {};
|
||||
\node[left] at (21.west) {$p_1$};
|
||||
\node[below] at (21.south) {$w(2)$};
|
||||
\node[roundnode] (22) [right=of 21] {};
|
||||
\node[below] at (22.south) {$R/\emptyset$};
|
||||
\node[roundnode] (23) [right=of 22] {};
|
||||
\node[below] at (23.south) {$r/(0,2)$};
|
||||
\node[roundnode] (24) [right=35pt of 23] {};
|
||||
\node[below] at (24.south) {$r/(1,2)^w$};
|
||||
|
||||
\draw[arrow] (21) -- (22);
|
||||
\draw[arrow] (22) -- (23);
|
||||
\draw[arrow] (23) -- (24);
|
||||
|
||||
\draw (24) -- (14);
|
||||
|
||||
\draw[dashed] ($(14)!0.5!(13) + (0,1)$) -- ++(0, -3.5);
|
||||
\end{tikzpicture}
|
||||
}
|
||||
178
docs/presentations/LIS/consistence_faible/wconsistence_properties/index.tex
Executable file
178
docs/presentations/LIS/consistence_faible/wconsistence_properties/index.tex
Executable file
@ -0,0 +1,178 @@
|
||||
\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}
|
||||
@ -0,0 +1,31 @@
|
||||
\resizebox{\columnwidth}{!}{%
|
||||
\begin{tikzpicture}[
|
||||
roundedrectangle/.style={draw, rounded corners, rectangle, minimum height=10pt, minimum width=20pt},
|
||||
invisible/.style={draw=none, fill=none},
|
||||
]
|
||||
|
||||
\node[invisible] (10) {};
|
||||
\node[roundedrectangle] (11) [right=60pt of 10] {\textcolor{blue}{$r_x(0,0)$}};
|
||||
\node[roundedrectangle, minimum width=100pt] (12) [right=50pt of 11] {$w_x(1)$};
|
||||
\node[invisible] (13) [right=100pt of 12] {};
|
||||
|
||||
\node[invisible] (20) [below=15pt of 10] {};
|
||||
\node[roundedrectangle] (21) [right=20pt of 20] {\textcolor{blue}{$r_x/(0,0)$}};
|
||||
\node[roundedrectangle] (22) [right=50pt of 21] {\textcolor{red}{$r_x/(0,1)$}};
|
||||
\node[roundedrectangle] (23) [right=15pt of 22] {\textcolor{red}{$r_x/(0,1)$}};
|
||||
\node[roundedrectangle] (24) [right=10pt of 23] {\textcolor{red}{$r_x/(0,1)$}};
|
||||
\node[roundedrectangle] (25) [right=20pt of 24] {\textcolor{red}{$r_x/(0,1)$}};
|
||||
\node[invisible] (26) [below=15pt of 13] {};
|
||||
|
||||
\node[invisible] (30) [below=15pt of 20] {};
|
||||
\node[roundedrectangle] (31) [right=30pt of 30] {\textcolor{blue}{$r_x/(0,0)$}};
|
||||
\node[roundedrectangle] (32) [right=55pt of 31] {\textcolor{blue}{$r_x/(0,0)$}};
|
||||
\node[roundedrectangle] (33) [right=15pt of 32] {\textcolor{red}{$r_x/(0,1)$}};
|
||||
\node[roundedrectangle] (34) [right=25pt of 33] {\textcolor{red}{$r_x/(0,1)$}};
|
||||
\node[invisible] (35) [below=15pt of 26] {};
|
||||
|
||||
\draw (10) -- (11) -- (12) -- (13);
|
||||
\draw (20) -- (21) -- (22) -- (23) -- (24) -- (25) -- (26);
|
||||
\draw (30) -- (31) -- (32) -- (33) -- (34) -- (35);
|
||||
\end{tikzpicture}
|
||||
}
|
||||
@ -0,0 +1,23 @@
|
||||
\resizebox{\columnwidth}{!}{%
|
||||
\begin{tikzpicture}[
|
||||
roundedrectangle/.style={draw, rounded corners, rectangle, minimum height=10pt, minimum width=20pt},
|
||||
invisible/.style={draw=none, fill=none},
|
||||
]
|
||||
|
||||
\node[invisible] (10) {};
|
||||
\node[roundedrectangle] (11) [right=60pt of 10] {\textcolor{blue}{$r_x(0,0)$}};
|
||||
\node[roundedrectangle, minimum width=100pt] (12) [right=50pt of 11] {$w_x(1)$};
|
||||
\node[invisible] (13) [right=100pt of 12] {};
|
||||
|
||||
\node[invisible] (20) [below=15pt of 10] {};
|
||||
\node[roundedrectangle] (21) [right=20pt of 20] {\textcolor{blue}{$r_x/(0,0)$}};
|
||||
\node[roundedrectangle] (22) [right=50pt of 21] {\textcolor{red!70}{$r_x/(0,1)$}};
|
||||
\node[roundedrectangle] (23) [right=15pt of 22] {\textcolor{blue!70}{$r_x/(0,0)$}};
|
||||
\node[roundedrectangle] (24) [right=10pt of 23] {\textcolor{blue!70}{$r_x/(0,0)$}};
|
||||
\node[roundedrectangle] (25) [right=20pt of 24] {\textcolor{red}{$r_x/(0,1)$}};
|
||||
\node[invisible] (26) [below=15pt of 13] {};
|
||||
|
||||
\draw (10) -- (11) -- (12) -- (13);
|
||||
\draw (20) -- (21) -- (22) -- (23) -- (24) -- (25) -- (26);
|
||||
\end{tikzpicture}
|
||||
}
|
||||
@ -0,0 +1,22 @@
|
||||
\resizebox{\columnwidth}{!}{%
|
||||
\begin{tikzpicture}[
|
||||
roundedrectangle/.style={draw, rounded corners, rectangle, minimum height=10pt, minimum width=20pt},
|
||||
invisible/.style={draw=none, fill=none},
|
||||
]
|
||||
|
||||
\node[invisible] (10) {};
|
||||
\node[roundedrectangle] (11) [right=60pt of 10] {\textcolor{blue}{$r_x(0,0)$}};
|
||||
\node[roundedrectangle, minimum width=100pt] (12) [right=50pt of 11] {$w_x(1)$};
|
||||
\node[invisible] (13) [right=65pt of 12] {};
|
||||
|
||||
\node[invisible] (20) [below=15pt of 10] {};
|
||||
\node[roundedrectangle] (21) [right=20pt of 20] {\textcolor{blue}{$r_x/(0,0)$}};
|
||||
\node[roundedrectangle] (22) [right=25pt of 21] {\textcolor{blue}{$r_x/(0,0)$}};
|
||||
\node[roundedrectangle] (23) [right=30pt of 22] {\textcolor{black!70}{$r_x/(?)$}};
|
||||
\node[roundedrectangle] (24) [right=55pt of 23] {\textcolor{red}{$r_x/(0,1)$}};
|
||||
\node[invisible] (25) [below=15pt of 13] {};
|
||||
|
||||
\draw (10) -- (11) -- (12) -- (13);
|
||||
\draw (20) -- (21) -- (22) -- (23) -- (24) -- (25);
|
||||
\end{tikzpicture}
|
||||
}
|
||||
@ -0,0 +1,34 @@
|
||||
\resizebox{\columnwidth}{!}{%
|
||||
\begin{tikzpicture}[
|
||||
roundnode/.style={circle, draw=black, fill=black, very thick, minimum size=1pt,},
|
||||
ignorednode/.style={circle, draw=black!20, fill=black!20, very thick, minimum size=1pt,},
|
||||
arrow/.style={|->, thick,},
|
||||
message/.style={->, blue!50, dashed, -{Circle[length=4pt,]}},
|
||||
]
|
||||
|
||||
\node[roundnode, draw=red, fill=red] (11) {};
|
||||
\node[left] at (11.west) {$p_0$};
|
||||
\node[above] at (11.north) {$w(1)$};
|
||||
\node[roundnode, draw=blue, fill=blue] (12) [right=of 11] {};
|
||||
\node[above] at (12.north) {$r/(0,0)$};
|
||||
\node[roundnode, draw=blue, fill=blue] (13) [right=of 12] {};
|
||||
\node[above] at (13.north) {$r/(0,2)^w$};
|
||||
|
||||
\draw[arrow] (11) -- (12);
|
||||
\draw[arrow] (12) -- (13);
|
||||
|
||||
\node[roundnode, draw=blue, fill=blue] (21) [below=of 11] {};
|
||||
\node[left] at (21.west) {$p_1$};
|
||||
\node[below] at (21.south) {$w(2)$};
|
||||
\node[roundnode, draw=red, fill=red] (22) [right=of 21] {};
|
||||
\node[below] at (22.south) {$r/(0,0)$};
|
||||
\node[roundnode, draw=red, fill=red] (23) [right=of 22] {};
|
||||
\node[below] at (23.south) {$r/(0,1)^w$};
|
||||
|
||||
\draw[arrow] (21) -- (22);
|
||||
\draw[arrow] (22) -- (23);
|
||||
|
||||
\draw[message] (11) -- ($(22)!0.5!(23)$);
|
||||
\draw[message] (21) -- ($(12)!0.5!(13)$);
|
||||
\end{tikzpicture}
|
||||
}
|
||||
@ -0,0 +1,31 @@
|
||||
\resizebox{\columnwidth}{!}{%
|
||||
\begin{tikzpicture}[
|
||||
roundnode/.style={circle, draw=black, fill=black, very thick, minimum size=1pt,},
|
||||
ignorednode/.style={circle, draw=black!20, fill=black!20, very thick, minimum size=1pt,},
|
||||
arrow/.style={|->, thick,},
|
||||
message/.style={->, blue!50, dashed, -{Circle[length=4pt,]}},
|
||||
]
|
||||
|
||||
\node[roundnode] (11) {};
|
||||
\node[left] at (11.west) {$p_0$};
|
||||
\node[above] at (11.north) {$w(1)$};
|
||||
\node[roundnode] (12) [right=of 11] {};
|
||||
\node[above] at (12.north) {$r/(0,1)$};
|
||||
\node[roundnode] (13) [right=of 12] {};
|
||||
\node[above] at (13.north) {$r/(2,1)^w$};
|
||||
|
||||
\draw[arrow] (11) -- (12);
|
||||
\draw[arrow] (12) -- (13);
|
||||
|
||||
\node[roundnode] (21) [below=of 11] {};
|
||||
\node[left] at (21.west) {$p_1$};
|
||||
\node[below] at (21.south) {$w(2)$};
|
||||
\node[roundnode] (22) [right=of 21] {};
|
||||
\node[below] at (22.south) {$r/(0,2)$};
|
||||
\node[roundnode] (23) [right=of 22] {};
|
||||
\node[below] at (23.south) {$r/(1,2)^w$};
|
||||
|
||||
\draw[arrow] (21) -- (22);
|
||||
\draw[arrow] (22) -- (23);
|
||||
\end{tikzpicture}
|
||||
}
|
||||
Reference in New Issue
Block a user