diff --git a/Recherche/BFT-ARBover/5_BFT_ARB/index.tex b/Recherche/BFT-ARBover/5_BFT_ARB/index.tex index 3fd930a..7cf55cc 100644 --- a/Recherche/BFT-ARBover/5_BFT_ARB/index.tex +++ b/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} - \SetAlgoLined - \Fn{ABroadcast($m$)}{ - $\received \gets \received \cup \{m\}$\; - Propose()\; - } -\end{algorithm} + \caption{t-BFT ARB at process $p_i$}\label{alg:bft-arb} - -\begin{algorithm}[H] - \caption{Propose($\bot$) at process $p_i$}\label{alg:propose-bft} - \SetAlgoLined - % \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]))$}{ - % \Comment{PROP PHASE}\; - \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()\; + \SetKwBlock{LocalVars}{Local Variables:}{} + \LocalVars{ + $\texttt{unordered} \gets \emptyset$, + $\texttt{ordered} \gets \emptyset$, + $\texttt{delivered} \gets \emptyset$\; + $\prop[r][j] \gets \bot, \forall r, j \in \pi \times \mathbb{N}$\; + $\texttt{done}[r] \gets \emptyset,$ + $\texttt{validate}[r] \gets \emptyset, \forall r \in \mathbb{N}$\; + % $\texttt{winners}[r] \gets \emptyset, \forall r$\; } \vspace{1em} - \Upon{$Rdeliver(j, \texttt{COMMIT}, r)$}{ - $\resolved[r] \gets \resolved[r] \cup \{j\}$\; + \For{$r = 1, 2, \ldots$}{ + \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} diff --git a/Recherche/BFT-ARBover/main.pdf b/Recherche/BFT-ARBover/main.pdf index 1de9260..6959644 100644 Binary files a/Recherche/BFT-ARBover/main.pdf and b/Recherche/BFT-ARBover/main.pdf differ