clean de l'algo

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

@@ -172,98 +172,73 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
 
 \subsection{Algorithm}
 
-\subsubsection{Variables}
-Each process $p_i$ maintains the following local variables:
-\LinesNotNumbered
-\begin{algorithm}
-    $\texttt{last\_commited} \gets 0$\;
-    $\texttt{last\_delivered} \gets 0$\;
-    $\received \gets \emptyset$\;
-    $\delivered \gets \emptyset$\;
-    $\prop[r][j] \gets \bot, \forall r, j$\;
-    $W[r] \gets \bot, \forall r$\;
-    $\resolved[r] \gets \bot, \forall r$\;
-    $Y[j]$ a Set of $n$ $\BFTDL$\;
-\end{algorithm}
-
-\LinesNumbered
 \begin{algorithm}[H]
-    \caption{$\ABbroadcast(m)$ at process $p_i$}\label{alg:broadcast-bft}
+    \caption{t-BFT ARB at process $p_i$}\label{alg:bft-arb}
-    \SetAlgoLined
-    \Fn{ABroadcast($m$)}{
-        $\received \gets \received \cup \{m\}$\;
-        Propose()\;
-    }
-\end{algorithm}
 
-
+    \SetKwBlock{LocalVars}{Local Variables:}{}
-\begin{algorithm}[H]
+    \LocalVars{
-    \caption{Propose($\bot$) at process $p_i$}\label{alg:propose-bft}
+        $\texttt{unordered} \gets \emptyset$,
-    \SetAlgoLined
+        $\texttt{ordered} \gets \emptyset$,
-    % \Statex \textbf{Proposer Job}
+        $\texttt{delivered} \gets \emptyset$\;
-    \Fn{Propose($\bot$)}{
+        $\prop[r][j] \gets \bot, \forall r, j \in \pi \times \mathbb{N}$\;
-        $r \gets \texttt{last\_commited}$\;
+        $\texttt{done}[r] \gets \emptyset,$
-        \While{$S \neq \emptyset$ with $S \gets \received \setminus (\delivered \cup (\bigcup_{r' < r} \bigcup_{j \in W[r']} \prop[r'][j]))$}{
+        $\texttt{validate}[r] \gets \emptyset, \forall r \in \mathbb{N}$\;
-            % \Comment{PROP PHASE}\;
+        % $\texttt{winners}[r] \gets \emptyset, \forall r$\;
-            \tcc*[f]{PROP PHASE}\\
-            $\RBcast(i, \texttt{PROP}, S, \current)$\;
-            \textbf{wait} until $|\{j: |\{k: (k, \PROVEtrace(r)) \in Y[j].\BFTREAD()\}| \geq t+1\}| \geq n - f$\;
-            % \Comment{COMMIT PHASE}
-            \tcc*[f]{COMMIT PHASE}\\
-            \textbf{for each} $j \in \Pi$ \textbf{do} $Y[j].\BFTAPPEND(r)$
-            $\RBcast(i, \texttt{COMMIT}, r)$\;
-            \textbf{wait} until $|\resolved[r]| \geq n - f$\;
-            % \Comment*{X PHASE}
-            \tcc*[f]{X PHASE}\\
-            $W[r] \gets \{j: |\{k: (k, \PROVEtrace(r)) \in Y[j].\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$}{
-            \Return{$\bot$}
-        }
-        $W[r] \gets \{j: |\{k: (k, \PROVEtrace(r)) \in Y[j].\BFTREAD()\}| \geq t+1\}$\;
-        \If{$\exists j \in W[r],\ \prop[r][j] = \bot$}{
-            \Return{$\bot$}
-        }
-        $M \gets \bigcup_{j \in W[r]} \prop[r][j]$\;\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$\;
-        $Y[j].\BFTPROVE(r)$\;
-        Propose()\;
     }
 
     \vspace{1em}
 
-    \Upon{$Rdeliver(j, \texttt{COMMIT}, r)$}{
+    \For{$r = 1, 2, \ldots$}{
-        $\resolved[r] \gets \resolved[r] \cup \{j\}$\;
+        \textbf{wait until} $\texttt{unordered} \setminus \texttt{ordered} \neq \emptyset$\;
+        $S \gets \texttt{unordered} \setminus \texttt{ordered}$\;
+        $\RBcast(i, \texttt{PROP}, S, r)$\;
+
+        \textbf{wait until} $|\texttt{validate}(r)| > n - t$\;
+        $\texttt{validate}[r] \gets \texttt{validate}(r)$\;
+
+        \ForEach{$j \in \Pi$}{
+            $\BFTAPPEND(\langle j, r\rangle)$\;
+        }
+
+        \ForEach{$j \in \Pi$}{
+            $\texttt{send}(j, \texttt{DONE}, r)$\;
+        }
+        \textbf{wait until} $|\texttt{done}[r]| > n - t$\;
+
+        $\texttt{winners}[r] \gets \texttt{validate}(r)$\;
+
+        \textbf{wait until} $\forall j \in \texttt{winners}[r],\ \prop[r][j] \neq \bot$\;
+        $M \gets \bigcup_{j \in \texttt{winners}[r]} \prop[r][j]$\;\nllabel{code:Mcompute}
+        $\texttt{ordered} \gets \texttt{ordered} \cup \ordered(M)$\;
     }
+
+    \Fn{\texttt{validate}($r$)}{
+        \Return{$\{j: |\{k: (k, \PROVEtrace(r)) \in \BFTREAD()\}| \geq t+1\}$}\;
+    }
+
+    \Upon{$\textbf{ABCAST}(m)$}{
+        $\texttt{unordered} \gets \texttt{unordered} \cup \{m\}$\;
+    }
+
+    \Upon{$\texttt{rdeliver}(\texttt{PROP}, S, \langle j, r \rangle)$ from process $p_j$}{
+        $\texttt{unordered} \gets \texttt{unordered} \cup S$\;
+        $\prop[r][j] \gets S$\;
+        $\BFTPROVE(r)$\;
+    }
+
+    \Upon{$\texttt{receive}(\texttt{DONE}, r)$ from process $p_j$}{
+        $\texttt{done}[r] \gets \texttt{done}[r] \cup \{j\}$\;
+    }
+
+    \Upon{$\textbf{ADELIVER}()$}{
+        \If{$\texttt{ordered} \setminus \texttt{delivered} = \emptyset$}{
+            \Return{$\bot$}
+        }
+        $m \gets \ordered(\texttt{ordered} \setminus \texttt{delivered})[0]$\;
+        $\texttt{delivered} \gets \texttt{delivered} \cup \{m\}$\;
+        \Return{$m$}
+    }
+    
 \end{algorithm}
 
 \textbf{Everything below has to be updated}