From b76313d2fcc4d2a55e848cabb645cf45009b6dbb Mon Sep 17 00:00:00 2001
From: thibauth <thibauth@30fcff6e-8de6-41c7-acce-77ff6d1dd07b>
Date: Fri, 2 Sep 2011 00:18:21 +0000
Subject: More slides

git-svn-id: https://scm.gforge.inria.fr/svn/pacemaker@72 30fcff6e-8de6-41c7-acce-77ff6d1dd07b
---
 stage/slides.tex | 142 +++++++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 127 insertions(+), 15 deletions(-)

(limited to 'stage/slides.tex')

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}
-- 
cgit v1.2.3-70-g09d2

