diff options
Diffstat (limited to 'stage/slides.tex')
| -rw-r--r-- | stage/slides.tex | 142 |
1 files changed, 127 insertions, 15 deletions
diff --git a/stage/slides.tex b/stage/slides.tex index 0010998..aac372d 100644 --- a/stage/slides.tex +++ b/stage/slides.tex @@ -3,9 +3,17 @@ \usepackage[french]{babel} \usepackage{amsmath} \usepackage{graphicx} -\usepackage{pst-all} +\usepackage{tikz} \usetheme{Boadilla} \usecolortheme{beaver} +\usepackage{listings} +\lstdefinelanguage{pseudo} + {morekeywords={if, then, else, end, let, and, or, for, in, while}} +\lstset{escapechar=?, mathescape=true, language=pseudo, basicstyle=\tiny, keywordstyle=\bfseries} +\renewcommand{\lstlistingname}{Spec.} + + + \title[Pacemaker]{Pacemaker : preuves et mesures de disponibilité dans les réseaux pair-à-pair} \author{Thibaut Horel} \institute[stage INRIA Saclay]{Stage de MPRI sous la direction de Fabrice Le Fessant} @@ -133,24 +141,128 @@ $1$ choisit un secret $S$ et le diffuse. \end{column} \begin{column}{0.55\textwidth} -\begin{figure} -\psset{linewidth=0.6pt} - \psmatrix[mnode=circle,colsep=30pt,rowsep=20pt] -[name=1]1\\[0pt] -[name=2]2\\[0pt] -[name=3]3\\[0pt] -\endpsmatrix -\psset{nodesep=0pt,arrows=->, - labelsep=2pt,shortput=nab} -%\visible<4->{\ncarc[arcangle=15]{0}{1}^{a}} -\ncline{1}{2} -\ncline{2}{3} -%\visible<2->{\nccurve[angleA=140,angleB=220,ncurv=5]{0}{0}_{b}} -\end{figure} + +\begin{tikzpicture} +\matrix [nodes=draw,circle,ampersand replacement=\&,row sep=1cm] +{ +\node (a) {1}; \\ +\node (b) {2}; \\ +\node (c) {3}; \\ +}; +\draw [->] (a.south); +\end{tikzpicture} + \end{column} \end{columns} \end{frame} +\begin{frame}{Fonctionnement suite} +t +\end{frame} + +\begin{frame}[fragile]{Spécification} +\begin{columns}[t] +\begin{column}{0.48\textwidth} + +\begin{block}{\tiny{Serveur au début de la ronde $i$}} +\begin{lstlisting} + let phase$^i$ = SEEDING; + let seed$^i$ = random_seed(); + let S$^i_{seed}$ = sign($\langle$$i$|seed$^i$|$T^i$$\rangle$, KS$_{priv}$); + let M$^i_{seed}$ = Seed($i$, seed$^i$, $T^i$, S$^i_{seed}$); + let map$^i$ = $\emptyset$; + $\forall q \in$ NS$_{server}$, send($q$, M$^i_{seed}$); + + wait $T^i$; +\end{lstlisting} +\end{block} + +\begin{block}{\tiny{Toutes les $\Delta << T^i$ secondes chez le pair $p$}} +\begin{lstlisting} + if phase$^i$ = SEEDING then + let H$^i$ = hash(map$^i$); + let M$^i_{seedreply}$ = SeedReply($i$, H$^i$); + nreplies$^i$ = nreplies$^i+1$; + replies$^i$[nreplies$^i$] = (H$^i$, map$^i$); + $\forall q \in$ NS$_p$, send($q$, M$^i_{seedreply}$); + end if +\end{lstlisting} +\end{block} +\end{column} + +\begin{column}{0.48\textwidth} +\begin{block}{\tiny{Pair $p$ à la réception de \textsf{Seed($i$, seed$^i$, $T^i$, S$^i_{seed}$)}}} +\begin{lstlisting} + if + verify(S$^i_{seed}$, $\langle$$i$|seed$^i$|$T^i$$\rangle$, KS$_{pub}$) + then + $\forall q \in$ NS$_p$, send($q$, M$^i_{seed}$); + let S$^i_p$ = sign($\langle$$i$|seed$^i$$\rangle$, K$^p_{priv}$); + let map$^i$ = {$p \rightarrow$hash(S$^i_p$)}; + let nreplies$^i$ = 0; + let replies$^i$ = $\emptyset$; + let included$^i$ = $\bot$; + let duration$^i$ = $T^i$; + let phase$^i$ = SEEDING; + end if +\end{lstlisting} +\end{block} + +\begin{block}{\tiny{Réception de \textsf{SeedReply($i$, X$_q$)} depuis le pair $q$}} +\begin{lstlisting} + if phase$^i$ = SEEDING then + map$^i$ = $\{ q \rightarrow $X$_q \} \oplus$map$^i$; + end if +\end{lstlisting} +\end{block} +\end{column} +\end{columns} +\end{frame} + +\begin{frame}[fragile]{Spécification (suite)} +\begin{columns}[t] +\begin{column}{0.45\textwidth} +\begin{block}{\tiny{Serveur après avoir attendu pendant $T^i$}} +\begin{lstlisting} +phase$^i$ = PULSE; +let H$^i$ = hash(map$^i$); +let branch$^i$ = $\emptyset$; +branch$^i$[0] = map$^i$; +let S$^i_{pulse}$ = sign($\langle$$i$|seed$^i$|H$^i$$\rangle$, KS$_{priv}$); +let M$^i_{pulse}$ = Pulse($i$,seed$^i$,branch$^i$,S$^i_{pulse}$); +$\forall q \in$ NS$_{server}$, send($q$, M$^i_{pulse}$); +\end{lstlisting} +\end{block} +\end{column} + +\begin{column}{0.54\textwidth} +\begin{block}{\tiny{Réception de \textsf{Pulse($i$, seed$^i$, branch$^i$, S$^i_{pulse}$)}}} +\begin{lstlisting} +if + verify(S$^i_{pulse}$,$\langle$$i$|seed$^i$|hash(branch$^i$[0])$\rangle$,KS$_{pub}$) and + phase$^i$ = SEEDING or phase$^i$ = PULSE +then + phase$^i$ = PULSE; + let level = length(branch$^i$)-1; + if + $\exists$ {$p$ $\rightarrow$ H$^i$} $\in$ branch$^i$[level] and + $\exists\; n\; |$replies[$n$] = (H$^i$, oldmap$^i$) and + included$^i < n$ and + $\forall n\in$[1..level],hash(branch$^i$[n])$\in$branch$^i$[n-1] + then + branch$^i$[level+1] = oldmap$^i$; + let M$^i_{pulse}$ = Pulse($i$, seed$^i$, branch'$^i$, S$^i_{pulse}$); + History[$i$] = ($i$, seed$^i$, branch'$^i$, S$^i_p$, S$^i_{pulse}$); + included$^i$ = $n$; + $\forall q \in$ NS$_p$, send($q$, M$^i_{pulse}$); + end if +end if +\end{lstlisting} + +\end{block} +\end{column} +\end{columns} +\end{frame} \section{Résultats} \end{document} |