je rajoute un mecanisme de detection d'equivocation

Recherche/BFT-ARBover/5_BFT_ARB/index.tex

@@ -181,9 +181,11 @@ Each process $p_i$ maintains the following local variables:
     $\received \gets \emptyset$\;
     $\delivered \gets \emptyset$\;
     $\prop[r][j] \gets \bot, \forall r, j$\;
-    $W[r] \gets \bot, \forall r$\;
+    $W[r] \gets \bot, \forall r$; this is the set of the winners for the round $r$\\
+    $B[r] \gets \bot, \forall r$; this is the set of processes who have bahaved maliciously for round $r$\\
     $\resolved[r] \gets \bot, \forall r$\;
-    $Y[j]$ a Set of $n$ $\BFTDL$\;
+    $Y$ a $\BFTDL$ such that the value space is $\mathcal{R} \times \Pi$\;
+    $V$ a $\BFTDL$ such that the value space is $(\mathcal{R} \times \mathcal{M} \times \Pi)$\;
 \end{algorithm}
 
 \LinesNumbered
@@ -203,59 +205,71 @@ Each process $p_i$ maintains the following local variables:
     % \Statex \textbf{Proposer Job}
     \Fn{Propose($\bot$)}{
         $r \gets \texttt{last\_commited}$\;
-        \While{$S \neq \emptyset$ with $S \gets \received \setminus (\delivered \cup (\bigcup_{r' < r} \bigcup_{j \in W[r']} \prop[r'][j]))$}{
+        \While{$S \neq \emptyset$ with $S \gets \received \setminus (\delivered \cup (\bigcup_{r' < r} \bigcup_{\substack{(j,S')\in W[r']\\ j\notin B[r']\\ S' \in \prop[r'][j]}} S'))$}{
             % \Comment{PROP PHASE}\;
             \tcc*[f]{PROP PHASE}\\
-            $\RBcast(i, \texttt{PROP}, S, \current)$\;
+            $V.\BFTPROVE((r, S, i))$\;
-            \textbf{wait} until $|\{j: |\{k: (k, \PROVEtrace(r)) \in Y[j].\BFTREAD()\}| \geq t+1\}| \geq n - f$\;
+            $\RBcast(i, \texttt{PROP}, S, r)$\;
+            \textbf{wait} until $|\{j: \exists S, |\{k: (k,(r, S, j)) \in V.\BFTREAD()\}| \geq t+1\}| \geq n - t$\;
             % \Comment{COMMIT PHASE}
             \tcc*[f]{COMMIT PHASE}\\
-            \textbf{for each} $j \in \Pi$ \textbf{do} $Y[j].\BFTAPPEND(r)$
+            \For{\textbf{each} $j \in \Pi$}{
+                % $Y[j].\BFTAPPEND(r)$\;
+                $V.\BFTAPPEND((r, S, j))$\;
+                $Y.\BFTAPPEND((r, j))$\;
+            }
             $\RBcast(i, \texttt{COMMIT}, r)$\;
-            \textbf{wait} until $|\resolved[r]| \geq n - f$\;
+            \textbf{wait} until $|\resolved[r]| \geq n - t$\;
             % \Comment*{X PHASE}
-            \tcc*[f]{X PHASE}\\
+            % \tcc*[f]{X PHASE}\\
-            $W[r] \gets \{j: |\{k: (k, \PROVEtrace(r)) \in Y[j].\BFTREAD()\}| \geq t+1\}$\;
+            \BlankLine
+            $W[r] \gets \{(j, S): |\{k: (k, (r, S, j)) \in V.\BFTREAD()\}| \geq t+1\}$\;
+            $B[r] \gets \{j: |\{k: (k, (r, j)) \in Y.\BFTREAD()\}| \geq t+1\}$\;
             $r \gets r + 1$\;
         }
         $\texttt{last\_commited} \gets r$\;
     }
 \end{algorithm}
 
-% \renewcommand{\algletter}{C}
 \begin{algorithm}[H]
     \caption{$\ABdeliver()$ at process $p_i$}\label{alg:deliver-bft}
     \SetAlgoLined
     \Fn{ADeliver($\bot$)}{
         $r \gets \texttt{last\_delivered}$\;
-        \If{$|\resolved[r]| < n - f$}{
+        \If{$|\resolved[r]| < n - t$}{
             \Return{$\bot$}
         }
-        $W[r] \gets \{j: |\{k: (k, \PROVEtrace(r)) \in Y[j].\BFTREAD()\}| \geq t+1\}$\;
+        $W \gets \{(j, S): |\{k: (k, (r, S, j)) \in V.\BFTREAD()\}| \geq t+1\}$\;
-        \If{$\exists j \in W[r],\ \prop[r][j] = \bot$}{
+        $B \gets \{j: |\{k: (k, (r, j)) \in Y.\BFTREAD()\}| \geq t+1\}$\;
+
+        \If{$\exists (j, S) \in W, j \notin B, S \notin \prop[r][j]$}{
             \Return{$\bot$}
         }
-        $M \gets \bigcup_{j \in W[r]} \prop[r][j]$\;\nllabel{code:Mcompute}
+        \BlankLine
+        $M \gets \bigcup_{\substack{(j,S)\in W\\ j\notin B\\ S \in prop[r][j]}} S$\;\nllabel{code:Mcompute}
         $m \gets \ordered(M \setminus \delivered)[0]$\;
         % \Comment*{Set $m$ as the smaller message not already delivered}
         $\delivered \leftarrow \delivered \cup \{m\}$\;
         \If{$M \setminus \delivered = \emptyset$}{
             $\texttt{last\_delivered} \gets \texttt{last\_delivered} + 1$\;
-
         }
         % \Comment*{Check if all messages from round $r$ have been delivered}
         \Return{$m$}
     }
 \end{algorithm}
 
-% \renewcommand{\algletter}{D}
 \begin{algorithm}[H]
     \caption{RB handler at process $p_i$}\label{alg:rb-handler-bft}
     \SetAlgoLined
     \Upon{$Rdeliver(j, \texttt{PROP}, S, r)$}{
         $\received \gets \received \cup \{S\}$\;
-        $\prop[r][j] \gets S$\;
+        \uIf{$\prop[r][j] = \bot \vee (\{S' : (j, (r, S', j)) \in V.\BFTREAD()\} = \{S\})$}{
-        $Y[j].\BFTPROVE(r)$\;
+            $V.\BFTPROVE((r, S, j))$\;
+        }
+        \Else{
+            $Y.\BFTPROVE((r, j))$\;
+        }
+        $\prop[r][j] \gets \prop[r][j] \cup S$\;
         Propose()\;
     }