amaury_joly/bwconsistency
1
0
Fork 0
Code Issues 5 Pull Requests Packages Projects 3 Releases Wiki Activity

algorithmpseudocode -> algorithm2e

Browse Source
This commit is contained in:
Amaury JOLY
2026-02-22 22:27:01 +01:00
parent 268c30a112
commit cc22c9d7f3
4 changed files with 262 additions and 245 deletions
Download Patch File Download Diff File Expand all files Collapse all files

172
Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex
View File

@@ -11,76 +11,70 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\subsubsection{Variables} \subsubsection{Variables}
Each process $p_i$ maintains: Each process $p_i$ maintains:
%on met toutes les variables locales ici \LinesNotNumbered
\begin{algorithmic} \begin{algorithm}
\State $\received \gets \emptyset$ \Comment{Messages received via \RB but not yet delivered} $\received \gets \emptyset$\; %\Comment{Messages received via \RB but not yet delivered}
\State $\delivered \gets \emptyset$ \Comment{Messages already delivered} $\delivered \gets \emptyset$\; %\Comment{Messages already delivered}
\State $\prop[r][j] \gets \bot,\ \forall r,j$ \Comment{Proposal from process $j$ for round $r$} $\prop[r][j] \gets \bot,\ \forall r,j$\; %\Comment{Proposal from process $j$ for round $r$}
\State $\current \gets 0$ $\current \gets 0$\;
\end{algorithmic} \end{algorithm}
% \paragraph{DenyList.} The \DL is initialized empty. We assume $\Pi_M = \Pi_V = \Pi$ (all processes can invoke \APPEND and \PROVE). % \paragraph{DenyList.} The \DL is initialized empty. We assume $\Pi_M = \Pi_V = \Pi$ (all processes can invoke \APPEND and \PROVE).
\subsubsection{Handlers and Procedures} \subsubsection{Handlers and Procedures}
\renewcommand{\algletter}{A} \LinesNumbered
\begin{algorithm}[H] \begin{algorithm}[H]
\caption{\RB handler (at process $p_i$)}\label{alg:rb-handler} \caption{\RB handler (at process $p_i$)}\label{alg:rb-handler}
\begin{algorithmic}[1] \Fn{RBreceived($S, r, j$)}{
\Function{RBreceived}{$S, r, j$} $\received \leftarrow \received \cup \{S\}$\;\nllabel{code:receivedConstruction}
\State $\received \leftarrow \received \cup \{S\}$ $\prop[r][j] \leftarrow S$\;\nllabel{code:prop-set} % \Comment{Record sender $j$'s proposal $S$ for round $r$}
\State $\prop[r][j] \leftarrow S$ \Comment{Record sender $j$'s proposal $S$ for round $r$} }
\EndFunction
\end{algorithmic}
\end{algorithm} \end{algorithm}
% \paragraph{} An \ABbroadcast$(m)$ chooses the next open round from the \DL view, proposes all pending messages together with the new $m$, disseminates this proposal via \RB, then executes $\PROVE(r)$ followed by $\APPEND(r)$ to freeze the winners of the round. The loop polls \DL until (i) some winner’s proposal includes $m$ in a \emph{closed} round and (ii) all winners' proposals for closed rounds are known locally, ensuring eventual inclusion and delivery. % \paragraph{} An \ABbroadcast$(m)$ chooses the next open round from the \DL view, proposes all pending messages together with the new $m$, disseminates this proposal via \RB, then executes $\PROVE(r)$ followed by $\APPEND(r)$ to freeze the winners of the round. The loop polls \DL until (i) some winner’s proposal includes $m$ in a \emph{closed} round and (ii) all winners' proposals for closed rounds are known locally, ensuring eventual inclusion and delivery.
\renewcommand{\algletter}{B} \begin{algorithm}[H]\label{alg:ABroadcast}
\begin{algorithm}[H]
\caption{\ABbroadcast$(m)$ (at process $p_i$)}\label{alg:ab-bcast} \caption{\ABbroadcast$(m)$ (at process $p_i$)}\label{alg:ab-bcast}
\begin{algorithmic}[1] \Fn{ABbroadcast($m$)}{
\Function{ABbroadcast}{$m$} $P \leftarrow \READ()$\;\nllabel{code:set-up-read} %\Comment{Fetch latest \DL state to learn recent $\PROVE$ operations}
\State $P \leftarrow \READ()$ \Comment{Fetch latest \DL state to learn recent $\PROVE$ operations} $r_{max} \leftarrow \max(\{ r' : \exists j,\ (j,r') \in P \})$\;\nllabel{code:rmax-compute} %\Comment{Pick current open round}
\State $r_{max} \leftarrow \max(\{ r' : \exists j,\ (j,r') \in P \})$ \Comment{Pick current open round} $S \leftarrow (\received \setminus \delivered) \cup \{m\}$\;\nllabel{code:Sconstruction}
\State $S \leftarrow (\received \setminus \delivered) \cup \{m\}$ \Comment{Propose all pending messages plus the new $m$} %\Comment{Propose all pending messages plus the new $m$}
\vspace{1em} \vspace{1em}
\State $r \gets r_{max} - 1$ $r \gets r_{max} - 1$\;
\While{$((i, r) \not\in P\ \wedge (\nexists j, r': (j, r') \in P \wedge m \in \prop[r'][j]))$} \While{$((i, r) \not\in P\ \wedge (\nexists j, r': (j, r') \in P \wedge m \in \prop[r'][j]))$}{\nllabel{code:sumbited-check-loop}
\State $r \gets r + 1$ $r \gets r + 1$\;\nllabel{code:round-increment}
\State $\RBcast(S, r, i)$; $\PROVE(r)$; $\APPEND(r)$; $\RBcast(S, r, i)$; $\PROVE(r)$; $\APPEND(r)$;\;\nllabel{code:submit-proposition}
\State $P \leftarrow \READ()$ \Comment{Refresh local view of \DL} $P \leftarrow \READ()$\; % \Comment{Refresh local view of \DL}
\EndWhile }
\EndFunction }
\end{algorithmic}
\end{algorithm} \end{algorithm}
\renewcommand{\algletter}{C} \begin{algorithm}[H]\label{alg:ADeliver}
\begin{algorithm}[H]
\caption{\ABdeliver() at process $p_i$}\label{alg:delivery} \caption{\ABdeliver() at process $p_i$}\label{alg:delivery}
\begin{algorithmic}[1] \Fn{ABdeliver($\bot$)}{
\Function{ABdeliver}{} $r \gets \current$\;
\State $r \gets \current$ $P_r \gets \{(j,r): (j,r) \in \READ()\}$ \;
\State $P_r \gets \{(j,r): (j,r) \in \READ()\}$ \If{$P_r = \emptyset$}{\nllabel{code:check-if-winners}
\If{$P_r = \emptyset$} \Return{$\bot$}
\State \Return $\bot$ }
\EndIf $\APPEND(r)$; $P \gets \READ()$\; \nllabel{code:append-read}
\State $\APPEND(r)$; $P \gets \READ()$ $W_r \gets \{ j : (j, \PROVEtrace(r)) \in P \}$\;\nllabel{code:Wcompute}
\State $W_r \gets \{ j : (j, \PROVEtrace(r)) \in P \}$ \If{$\exists j \in W_r,\ \prop[r][j] = \bot$}{ \nllabel{code:check-winners-ack}
\If{$\exists j \in W_r,\ \prop[r][j] = \bot$} \Return{$\bot$}
\State \Return $\bot$ }
\EndIf $M_r \gets \bigcup_{j \in W_r} \prop[r][j]$\;\nllabel{code:Mcompute}
\State $M_r \gets \bigcup_{j \in W_r} \prop[r][j]$ $m \gets \ordered(M_r \setminus \delivered)[0]$\;\nllabel{code:next-msg-extraction}
\State $m \gets \ordered(M_r \setminus \delivered)[0]$ \Comment{Set $m$ as the smaller message not already delivered} %\Comment{Set $m$ as the smaller message not already delivered}
\State $\delivered \leftarrow \delivered \cup \{m\}$ $\delivered \leftarrow \delivered \cup \{m\}$\;
\If{$M_r \setminus \delivered = \emptyset$} \Comment{Check if all messages from round $r$ have been delivered} \If{$M_r \setminus \delivered = \emptyset$}{ %\Comment{Check if all messages from round $r$ have been delivered}
\State $\current \leftarrow \current + 1$ $\current \leftarrow \current + 1$
\EndIf }
\State \textbf{return} $m$ \Return{$m$}
\EndFunction }
\end{algorithmic}
\end{algorithm} \end{algorithm}
% ------------------------------------------------------------------------------ % ------------------------------------------------------------------------------
@@ -119,26 +113,26 @@ Each process $p_i$ maintains:
There are two possibilities for where $\APPEND^{(\star)}(r+1)$ is invoked. There are two possibilities for where $\APPEND^{(\star)}(r+1)$ is invoked.
\begin{itemize} \begin{itemize}
\item \textbf{Case Algorithm B :} \item \textbf{Case Algorithm \ref{alg:ABroadcast} :}
Some process executes the loop (lines B6-10) and invokes $\PROVE(r+1);\APPEND^{(\star)}(r+1)$ at line B8. Let $p_i$ be this process. Some process executes the loop at \ref{code:sumbited-check-loop} and invokes $\PROVE(r+1);\APPEND^{(\star)}(r+1)$ at line~\ref{code:submit-proposition}. Let $p_i$ be this process.
Immediately before line B8, line B7 sets $r\leftarrow r+1$, so the previous loop iteration targeted $r$. We consider two sub-cases. Immediately before line~\ref{code:submit-proposition}, line~\ref{code:round-increment} sets $r\leftarrow r+1$, so the previous loop iteration targeted $r$. We consider two sub-cases.
\begin{itemize} \begin{itemize}
\item \emph{(i) $p_i$ is not in its first loop iteration.} \item \emph{(i) $p_i$ is not in its first loop iteration.}
In the previous iteration, $p_i$ executed $\PROVE_i(r)$ at B8, followed (in program order) by $\APPEND_i(r)$. In the previous iteration, $p_i$ executed $\PROVE_i(r)$ at \ref{code:submit-proposition}, followed (in program order) by $\APPEND_i(r)$.
If round $r$ wasn't closed when $p_i$ execute $\PROVE_i(r)$ at B8, then the condition at B6 would be true hence the tuple $(i, r)$ should be visible in P which implies that $p_i$ should leave the loop at round $r$, contradicting the assumption that $p_i$ is now executing another iteration. If round $r$ wasn't closed when $p_i$ execute $\PROVE_i(r)$ at \ref{code:submit-proposition}, then the condition at \ref{code:sumbited-check-loop} would be true hence the tuple $(i, r)$ should be visible in P which implies that $p_i$ should leave the loop at round $r$, contradicting the assumption that $p_i$ is now executing another iteration.
Since the tuple is not visible, the $\PROVE_i(r)$ was invalid which implies by definition that an $\APPEND(r)$ already exists in $H$. Thus in this case $r$ is closed. Since the tuple is not visible, the $\PROVE_i(r)$ was invalid which implies by definition that an $\APPEND(r)$ already exists in $H$. Thus in this case $r$ is closed.
\item \emph{(ii) $p_i$ is in its first loop iteration.} \item \emph{(ii) $p_i$ is in its first loop iteration.}
To compute the value $r_{max}$, $p_i$ must have observed one or many $(\_ , r+1)$ in $P$ at B2/B3, issued by some processes (possibly different from $p_i$). Let's call $p_j$ the issuer of the first $\PROVE_j(r+1)$ in the linearization $H$. \\ To compute the value $r_{max}$, $p_i$ must have observed one or many $(\_ , r+1)$ in $P$ at \ref{code:rmax-compute}, issued by some processes (possibly different from $p_i$). Let's call $p_j$ the issuer of the first $\PROVE_j(r+1)$ in the linearization $H$. \\
When $p_j$ executed $P \gets \READ()$ at B2 and compute $r_{max}$ at B3, he observed no tuple $(\_,r+1)$ in $P$ because he's the issuer of the first one. So when $p_j$ executed the loop (B6–B10), he run it for the round $r$, didn't seen any $(j,r)$ in $P$ at B6, and then executed the first $\PROVE_j(r+1)$ at B8 in a second iteration. \\ When $p_j$ executed $P \gets \READ()$ at \ref{code:set-up-read} and compute $r_{max}$ at \ref{code:rmax-compute}, he observed no tuple $(\_,r+1)$ in $P$ because he's the issuer of the first one. So when $p_j$ executed the loop (\ref{code:sumbited-check-loop}), he run it for the round $r$, didn't seen any $(j,r)$ in $P$ at B6, and then executed the first $\PROVE_j(r+1)$ at \ref{code:submit-proposition} in a second iteration. \\
If round $r$ wasn't closed when $p_j$ execute $\PROVE_j(r)$ at B8, then the $(j, r)$ will be in $P$ and the condition at B6 should be true which implies that $p_j$ sould leave the loop at round $r$, contradicting the assumption that $p_j$ is now executing $\PROVE_j(r+1)$. In this case $r$ is closed. If round $r$ wasn't closed when $p_j$ execute $\PROVE_j(r)$ at \ref{code:submit-proposition}, then the $(j, r)$ will be in $P$ and the condition at \ref{code:sumbited-check-loop} should be true which implies that $p_j$ sould leave the loop at round $r$, contradicting the assumption that $p_j$ is now executing $\PROVE_j(r+1)$. In this case $r$ is closed.
\end{itemize} \end{itemize}
\item \textbf{Case Algorithm C :} \item \textbf{Case Algorithm \ref{alg:ADeliver} :}
Some process invokes $\APPEND(r+1)$ at C7. Let $p_i$ be this process. Some process invokes $\APPEND(r+1)$ at \ref{code:append-read}. Let $p_i$ be this process.
Line C7 is guarded by the condition at C5, which ensures that $p_i$ observed some $(\_,r+1)$ in $P$. Let $p_j$ be the issuer of the first $\PROVE_j(r+1)$ in the linearization $H$. Line~\ref{code:append-read} is guarded by the condition at \ref{code:check-if-winners}, which ensures that $p_i$ observed some $(\_,r+1)$ in $P$. Let $p_j$ be the issuer of the first $\PROVE_j(r+1)$ in the linearization $H$.
When $p_j$ executed $\PROVE_j(r+1)$ at B8, he observed no tuple $(\_,r+1)$ in $P$ at B6 because he's the issuer of the first one. By the same reasoning as in the Case Algorithm B (ii), $p_j$ must have observed that the round $r$ was closed. When $p_j$ executed $\PROVE_j(r+1)$ at \ref{code:submit-proposition}, he observed no tuple $(\_,r+1)$ in $P$ at \ref{code:check-if-winners} because he's the issuer of the first one. By the same reasoning as in the Case Algorithm \ref{alg:ABroadcast} (ii), $p_j$ must have observed that the round $r$ was closed.
% Line C7 is guarded by the presence of $\PROVE(r)$ in $P$ with $r=r+1$ (C5). % Line C7 is guarded by the presence of $\PROVE(r)$ in $P$ with $r=r+1$ (C5).
% Moreover, the local pointer $\textit{next}$ grow by increment of 1 and only advances after finishing the current round (C17), so if a process can reach $\textit{next}=r+1$ it implies that he has completed round $r$, which includes closing $r$ at C8 when $\PROVE(r)$ is observed. % Moreover, the local pointer $\textit{next}$ grow by increment of 1 and only advances after finishing the current round (C17), so if a process can reach $\textit{next}=r+1$ it implies that he has completed round $r$, which includes closing $r$ at C8 when $\PROVE(r)$ is observed.
% Hence $\APPEND^\star(r+1)$ implies a prior $\APPEND(r)$ in $H$, so $r$ is closed. % Hence $\APPEND^\star(r+1)$ implies a prior $\APPEND(r)$ in $H$, so $r$ is closed.
@@ -170,7 +164,7 @@ Each process $p_i$ maintains:
\end{proof} \end{proof}
\begin{lemma}[Well-defined winners]\label{lem:winners} \begin{lemma}[Well-defined winners]\label{lem:winners}
For any correct process $p_i$ and round $r$, if $p_i$ computes $W_r$ at line C8, then : For any correct process $p_i$ and round $r$, if $p_i$ computes $W_r$ at line~\ref{code:Wcompute}, then :
\begin{itemize} \begin{itemize}
\item $\Winners_r$ is defined; \item $\Winners_r$ is defined;
\item the computed $W_r$ is exactly $\Winners_r$. \item the computed $W_r$ is exactly $\Winners_r$.
@@ -178,9 +172,9 @@ Each process $p_i$ maintains:
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
Lets consider a correct process $p_i$ that reach line C8 to compute $W_r$. \\ Lets consider a correct process $p_i$ that reach line~\ref{code:Wcompute} to compute $W_r$. \\
By program order, $p_i$ must have executed $\APPEND_i(r)$ at C7 before, which implies by \Cref{def:closed-round} that round $r$ is closed at that point. So by \Cref{def:winner-invariant}, $\Winners_r$ is defined. \\ By program order, $p_i$ must have executed $\APPEND_i(r)$ at line~\ref{code:append-read} before, which implies by \Cref{def:closed-round} that round $r$ is closed at that point. So by \Cref{def:winner-invariant}, $\Winners_r$ is defined. \\
By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\_,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at C7 after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\_,r)$ such that By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\_,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at line~\ref{code:append-read} after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\_,r)$ such that
\[ \[
W_r = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r W_r = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r
\] \]
@@ -194,11 +188,11 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
Consider the round $r$ such that some process invokes $\APPEND(r)$. There are two possible cases Consider the round $r$ such that some process invokes $\APPEND(r)$. There are two possible cases
\begin{itemize} \begin{itemize}
\item \textbf{Case (B6) :} \item \textbf{Case (\ref{code:submit-proposition}) :}
There exists a process $p_i$ who's the issuer of the earliest $\APPEND^{(\star)}(r)$ in the DL linearization $H$. By program order, $p_i$ must have previously invoked $\PROVE_i(r)$ before invoking $\APPEND^{(\star)}(r)$ at B8. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by a correct process before $\APPEND^{(\star)}(r)$. There exists a process $p_i$ who's the issuer of the earliest $\APPEND^{(\star)}(r)$ in the DL linearization $H$. By program order, $p_i$ must have previously invoked $\PROVE_i(r)$ before invoking $\APPEND^{(\star)}(r)$ at line~\ref{code:submit-proposition}. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by a correct process before $\APPEND^{(\star)}(r)$.
\item \textbf{Case (C8) :} \item \textbf{Case (\ref{code:append-read}) :}
There exists a process $p_i$ that invoked $\APPEND^{(\star)}(r)$ at C7. Line C7 is guarded by the condition at C4, which ensures that $p$ observed some $(\_,r)$ in $P$. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by some process before $\APPEND^{(\star)}(r)$. There exists a process $p_i$ that invoked $\APPEND^{(\star)}(r)$ at . Line~\ref{code:append-read} is guarded by the condition at \ref{code:check-if-winners}, which ensures that $p$ observed some $(\_,r)$ in $P$. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by some process before $\APPEND^{(\star)}(r)$.
\end{itemize} \end{itemize}
In both cases, if some process invokes $\APPEND(r)$, then some process must have previously invoked $\PROVE(r)$. In both cases, if some process invokes $\APPEND(r)$, then some process must have previously invoked $\PROVE(r)$.
@@ -218,9 +212,9 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\end{lemma} \end{lemma}
\begin{proof}[Proof] \begin{proof}[Proof]
Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $i \in \Winners_r$, there exist a valid $\PROVE_i(r)$ such that $\PROVE_i(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order, if $i$ invoked a valid $\PROVE_i(r)$ at line B8 he must have invoked $\RBcast(S^{(i)}, r, i)$ directly before. Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $i \in \Winners_r$, there exist a valid $\PROVE_i(r)$ such that $\PROVE_i(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order, if $i$ invoked a valid $\PROVE_i(r)$ at line~\ref{code:submit-proposition} he must have invoked $\RBcast(S^{(i)}, r, i)$ directly before.
Let take a correct process $p_j$, by \RB \emph{Validity}, every correct process eventually receives $i$'s \RB message for round $r$, which sets $\prop[r][i]$ to a non-$\bot$ value at line A3. Let take a correct process $p_j$, by \RB \emph{Validity}, every correct process eventually receives $i$'s \RB message for round $r$, which sets $\prop[r][i]$ to a non-$\bot$ value at line~\ref{code:prop-set}.
\end{proof} \end{proof}
\begin{definition}[Messages invariant]\label{def:messages-invariant} \begin{definition}[Messages invariant]\label{def:messages-invariant}
@@ -232,13 +226,13 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\end{definition} \end{definition}
\begin{lemma}[Eventual proposal closure]\label{lem:eventual-closure} \begin{lemma}[Eventual proposal closure]\label{lem:eventual-closure}
If a correct process $p_i$ define $M_r$ at line C12, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. If a correct process $p_i$ define $M_r$ at line~\ref{code:Mcompute}, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
\end{lemma} \end{lemma}
\begin{proof}[Proof] \begin{proof}[Proof]
Let take a correct process $p_i$ that computes $M_r$ at line C12. By \Cref{lem:winners}, $p_i$ computation is the winner set $\Winners_r$. Let take a correct process $p_i$ that computes $M_r$ at line~\ref{code:Mcompute}. By \Cref{lem:winners}, $p_i$ computation is the winner set $\Winners_r$.
By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line C12 where $p_i$ computes $M_r$ is guarded by the condition at C9, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, $M_r = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]$, we have $\prop^{(i)}[r][j] \neq \bot$ for all $j \in \Winners_r$. By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line~\ref{code:Mcompute} where $p_i$ computes $M_r$ is guarded by the condition at line~\ref{code:check-winners-ack}, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, $M_r = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]$, we have $\prop^{(i)}[r][j] \neq \bot$ for all $j \in \Winners_r$.
\end{proof} \end{proof}
\begin{lemma}[Unique proposal per sender per round]\label{lem:unique-proposal} \begin{lemma}[Unique proposal per sender per round]\label{lem:unique-proposal}
@@ -246,18 +240,18 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\end{lemma} \end{lemma}
\begin{proof}[Proof] \begin{proof}[Proof]
By program order, any process $p_i$ invokes $\RBcast(S, r, i)$ at line B6 must be in the loop B5–B11. No matter the number of iterations of the loop, line B5 always uses the current value of $r$ which is incremented by 1 at each turn. Hence, in any execution, any process $p_i$ invokes $\RBcast(S, r, j)$ at most once for any round $r$. By program order, any process $p_i$ invokes $\RBcast(S, r, i)$ at line~\ref{code:submit-proposition} must be in the loop \ref{code:sumbited-check-loop}. No matter the number of iterations of the loop, line~\ref{code:sumbited-check-loop} always uses the current value of $r$ which is incremented by 1 at each turn. Hence, in any execution, any process $p_i$ invokes $\RBcast(S, r, j)$ at most once for any round $r$.
\end{proof} \end{proof}
\begin{lemma}[Proposal convergence]\label{lem:convergence} \begin{lemma}[Proposal convergence]\label{lem:convergence}
For any round $r$, for any correct processes $p_i$ that execute C12, we have For any round $r$, for any correct processes $p_i$ that execute line~\ref{code:Mcompute}, we have
\[ \[
M_r^{(i)} = \Messages_r M_r^{(i)} = \Messages_r
\] \]
\end{lemma} \end{lemma}
\begin{proof}[Proof] \begin{proof}[Proof]
Let take a correct process $p_i$ that compute $M_r$ at line C12. That implies that $p_i$ has defined $W_r$ at line C8. It implies that, by \Cref{lem:winners}, $r$ is closed and $W_r = \Winners_r$. \\ Let take a correct process $p_i$ that compute $M_r$ at line~\ref{code:Mcompute}. That implies that $p_i$ has defined $W_r$ at line~\ref{code:Wcompute}. It implies that, by \Cref{lem:winners}, $r$ is closed and $W_r = \Winners_r$. \\
By \Cref{lem:eventual-closure}, for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. By \Cref{lem:unique-proposal}, each winner $j$ invokes at most one $\RBcast(S^{(j)}, r, j)$, so $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined. Hence, when $p_i$ computes By \Cref{lem:eventual-closure}, for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. By \Cref{lem:unique-proposal}, each winner $j$ invokes at most one $\RBcast(S^{(j)}, r, j)$, so $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined. Hence, when $p_i$ computes
\[ \[
M_r^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r. M_r^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r.
@@ -272,10 +266,10 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
Fix a correct process $p_i$ that invokes $\ABbroadcast(m)$ and eventually exits the loop (B6–B10) at some round $r$. There are two possible cases. Fix a correct process $p_i$ that invokes $\ABbroadcast(m)$ and eventually exits the loop (\ref{code:sumbited-check-loop}) at some round $r$. There are two possible cases.
\begin{itemize} \begin{itemize}
\item \textbf{Case 1:} $p_i$ exits the loop because $(i, r) \in P$. In this case, by \Cref{def:winner-invariant}, $p_i$ is a winner in round $r$. By program order, $p_i$ must have invoked $\RBcast(S, r, i)$ at B8 before invoking $\PROVE_i(r)$. By line B4, $m \in S$. Hence there exist a closed round $r$ and $p_i$ is a correct process such that $i\in\Winners_r$. Hence, $i$ invokes $\RBcast(S, r, i)$ with $m\in S$. \item \textbf{Case 1:} $p_i$ exits the loop because $(i, r) \in P$. In this case, by \Cref{def:winner-invariant}, $p_i$ is a winner in round $r$. By program order, $p_i$ must have invoked $\RBcast(S, r, i)$ at \ref{code:submit-proposition} before invoking $\PROVE_i(r)$. By line~\ref{code:Sconstruction}, $m \in S$. Hence there exist a closed round $r$ and $p_i$ is a correct process such that $i\in\Winners_r$. Hence, $i$ invokes $\RBcast(S, r, i)$ with $m\in S$.
\item \textbf{Case 2:} $p_i$ exits the loop because $\exists j, r': (j, r') \in P \wedge m \in \prop[r'][j]$. In this case, by \Cref{lem:winners-propose} and \Cref{lem:unique-proposal} $p_j$ must have invoked a unique $\RBcast(S, r', j)$. Which set $\prop^{(i)}[r'][j] = S$ with $m \in S$. \item \textbf{Case 2:} $p_i$ exits the loop because $\exists j, r': (j, r') \in P \wedge m \in \prop[r'][j]$. In this case, by \Cref{lem:winners-propose} and \Cref{lem:unique-proposal} $p_j$ must have invoked a unique $\RBcast(S, r', j)$. Which set $\prop^{(i)}[r'][j] = S$ with $m \in S$.
\end{itemize} \end{itemize}
@@ -293,10 +287,10 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\begin{proof}[Proof] \begin{proof}[Proof]
Consider a correct process $p_i$ that invokes $\ABbroadcast(m)$. The statement is true if $\exists r_1$ such that $r_1 \geq r_{max}$ and if $(i, r_1) \in P$; or if $\exists r_2$ such that $r_2 \geq r_{max}$ and if $\exists j: (j, r_2) \in P \wedge m \in \prop[r_2][j]$ (like guarded at B8). Consider a correct process $p_i$ that invokes $\ABbroadcast(m)$. The statement is true if $\exists r_1$ such that $r_1 \geq r_{max}$ and if $(i, r_1) \in P$; or if $\exists r_2$ such that $r_2 \geq r_{max}$ and if $\exists j: (j, r_2) \in P \wedge m \in \prop[r_2][j]$ (like guarded at B8).
Consider that there exists no round $r_1$ such that $p_i$ invokes a valid $\PROVE(r_1)$. In this case $p_i$ invokes infinitely many $\RBcast(S, \_, i)$ at B6 with $m \in S$ (line B4).\\ Consider that there exists no round $r_1$ such that $p_i$ invokes a valid $\PROVE(r_1)$. In this case $p_i$ invokes infinitely many $\RBcast(S, \_, i)$ at line~\ref{code:submit-proposition} with $m \in S$ (line~\ref{code:Sconstruction}).\\
The assumption that no $\PROVE(r_1)$ invoked by $p$ is valid implies by \DL \emph{Validity} that for every round $r' \geq r_{max}$, there exists at least one $\APPEND(r')$ in the DL linearization, hence by \Cref{lem:nonempty} for every possible round $r'$ there at least a winner. Because there is an infinite number of rounds, and a finite number of processes, there exists at least one process $p_k$ that invokes infinitely many valid $\PROVE(r')$ and by extension infinitely many $\ABbroadcast(\_)$. By \RB \emph{Validity}, $p_k$ eventually receives $p_i$ 's \RB messages. Let call $t_0$ the time when $p_k$ receives $p_i$ 's \RB message. \\ The assumption that no $\PROVE(r_1)$ invoked by $p$ is valid implies by \DL \emph{Validity} that for every round $r' \geq r_{max}$, there exists at least one $\APPEND(r')$ in the DL linearization, hence by \Cref{lem:nonempty} for every possible round $r'$ there at least a winner. Because there is an infinite number of rounds, and a finite number of processes, there exists at least one process $p_k$ that invokes infinitely many valid $\PROVE(r')$ and by extension infinitely many $\ABbroadcast(\_)$. By \RB \emph{Validity}, $p_k$ eventually receives $p_i$ 's \RB messages. Let call $t_0$ the time when $p_k$ receives $p_i$ 's \RB message. \\
At $t_0$, $p_k$ executes \Cref{alg:rb-handler} and sets $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line A2). At $t_0$, $p_k$ executes Algorithm \ref{alg:rb-handler} and sets $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line~\ref{code:receivedConstruction}).
For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \texttt{RReceived()}, $p_k$ must include $m$ in his proposal $S$ at line B4 (because $m$ is pending in $j$'s $\received \setminus \delivered$ set). There exists a minimum round $r_2$ such that $p_k \in \Winners_{r_2}$ after $t_0$. By \Cref{lem:winners-propose}, eventually $\prop^{(i)}[r_2][k] \neq \bot$. By \Cref{lem:unique-proposal}, $\prop^{(i)}[r_2][k]$ is uniquely defined as the set $S$ proposed by $p_k$ at B6, which by \Cref{lem:inclusion} includes $m$. Hence eventually $m \in \prop^{(i)}[r_2][k]$ and $k \in \Winners_{r_2}$. For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \texttt{RReceived()}, $p_k$ must include $m$ in his proposal $S$ at line~\ref{code:Sconstruction} (because $m$ is pending in $j$'s $\received \setminus \delivered$ set). There exists a minimum round $r_2$ such that $p_k \in \Winners_{r_2}$ after $t_0$. By \Cref{lem:winners-propose}, eventually $\prop^{(i)}[r_2][k] \neq \bot$. By \Cref{lem:unique-proposal}, $\prop^{(i)}[r_2][k]$ is uniquely defined as the set $S$ proposed by $p_k$ at B6, which by \Cref{lem:inclusion} includes $m$. Hence eventually $m \in \prop^{(i)}[r_2][k]$ and $k \in \Winners_{r_2}$.
So if $p_i$ is a winner he satisfies the condition $(i, r_1) \in P$. And we show that if the first condition is never satisfied, the second one will eventually be satisfied. Hence either the first or the second condition will eventually be satisfied, and $p_i$ eventually exits the loop and returns from $\ABbroadcast(m)$. So if $p_i$ is a winner he satisfies the condition $(i, r_1) \in P$. And we show that if the first condition is never satisfied, the second one will eventually be satisfied. Hence either the first or the second condition will eventually be satisfied, and $p_i$ eventually exits the loop and returns from $\ABbroadcast(m)$.
\end{proof} \end{proof}
@@ -311,7 +305,7 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\RBcast(S, r, j)\quad\text{with}\quad m\in S. \RBcast(S, r, j)\quad\text{with}\quad m\in S.
\] \]
By \Cref{lem:eventual-closure}, when $p_q$ computes $M_r$ at line C12, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ invokes at most one $\RBcast(S, r, j)$, so $\prop[r][j]$ is uniquely defined. Hence, when $p_q$ computes By \Cref{lem:eventual-closure}, when $p_q$ computes $M_r$ at line~\ref{code:Mcompute}, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ invokes at most one $\RBcast(S, r, j)$, so $\prop[r][j]$ is uniquely defined. Hence, when $p_q$ computes
\[ \[
M_r = \bigcup_{k\in\Winners_r} \prop[r][k], M_r = \bigcup_{k\in\Winners_r} \prop[r][k],
\] \]
@@ -325,7 +319,7 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\begin{proof} \begin{proof}
Let consider two invokations of $\ABdeliver()$ made by the same correct process which returns $m$. Let call these two invocations respectively $\ABdeliver^{(A)}()$ and $\ABdeliver^{(B)}()$. Let consider two invokations of $\ABdeliver()$ made by the same correct process which returns $m$. Let call these two invocations respectively $\ABdeliver^{(A)}()$ and $\ABdeliver^{(B)}()$.
When $\ABdeliver^{(A)}()$ occurs, by program order and because it reached line C18 to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reached line C13 to extract the next message to deliver, it can't be $m$ because $m \not\in (M_r \setminus \{..., m, ...\})$. So a $\ABdeliver^{(B)}()$ which delivers $m$ can't occur. When $\ABdeliver^{(A)}()$ occurs, by program order and because it reached line C18 to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reached line~\ref{code:next-msg-extraction} to extract the next message to deliver, it can't be $m$ because $m \not\in (M_r \setminus \{..., m, ...\})$. So a $\ABdeliver^{(B)}()$ which delivers $m$ can't occur.
\end{proof} \end{proof}
\begin{lemma}[Total order]\label{lem:total-order} \begin{lemma}[Total order]\label{lem:total-order}
@@ -345,7 +339,7 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\begin{itemize} \begin{itemize}
\item \textbf{Case 1:} $r_1 < r_2$. By program order, any correct process must have waited to append in $\delivered$ every messages in $M_{r_1}$ (which contains $m_1$) to increment $\current$ and eventually set $\current = r_2$ to compute $M_{r_2}$ and then invoke the $ m_2 = \ABdeliver()$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ before $m_2$. \item \textbf{Case 1:} $r_1 < r_2$. By program order, any correct process must have waited to append in $\delivered$ every messages in $M_{r_1}$ (which contains $m_1$) to increment $\current$ and eventually set $\current = r_2$ to compute $M_{r_2}$ and then invoke the $ m_2 = \ABdeliver()$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ before $m_2$.
\item \textbf{Case 2:} $r_1 = r_2$. By \Cref{lem:convergence}, any correct process that computes $M_{r_1}$ at line C12 computes the same set of messages $\Messages_{r_1}$. By line C13 the messages are pull in a deterministic order defined by $\ordered(\_)$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ and $m_2$ in the deterministic order defined by $\ordered(\_)$. \item \textbf{Case 2:} $r_1 = r_2$. By \Cref{lem:convergence}, any correct process that computes $M_{r_1}$ at line~\ref{code:Mcompute} computes the same set of messages $\Messages_{r_1}$. By line~\ref{code:next-msg-extraction} the messages are pull in a deterministic order defined by $\ordered(\_)$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ and $m_2$ in the deterministic order defined by $\ordered(\_)$.
\end{itemize} \end{itemize}
In all possible cases, any correct process that delivers both $m_1$ and $m_2$ delivers $m_1$ and $m_2$ in the same order. In all possible cases, any correct process that delivers both $m_1$ and $m_2$ delivers $m_1$ and $m_2$ in the same order.
@@ -443,7 +437,7 @@ Which are cover by our FIFO-\ARB specification.
\subsubsection{Example executions} \subsubsection{Example executions}
\begin{figure}[H] \begin{figure}
\centering \centering
\resizebox{0.4\textwidth}{!}{ \resizebox{0.4\textwidth}{!}{
\input{diagrams/nonBFT_behaviour.tex} \input{diagrams/nonBFT_behaviour.tex}

199
Recherche/BFT-ARBover/5_BFT_ARB/index.tex
View File

@@ -53,42 +53,35 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
|\mathcal{U}| = \binom{|M|}{|M| - t}. |\mathcal{U}| = \binom{|M|}{|M| - t}.
\] \]
\begin{algorithmic}[1] \begin{algorithm}
% \renewcommand{\algletter}{}
\begin{algorithm}[H]
\caption{t-BFT-DL implementation using multiple DL objects} \caption{t-BFT-DL implementation using multiple DL objects}
% \caption{\BFTAPPEND} \Fn{$\BFTAPPEND(x)$}{
\Function{$\BFTAPPEND$}{x} \For{\textbf{each } $U \in \mathcal{U}$ st $i \in U$}{
\For{\textbf{each } $U \in \mathcal{U}$ st $i \in U$} $DL_U.\APPEND(x)$\;
\State $DL_U.\APPEND(x)$ }
\EndFor }
\EndFunction
\vspace{1em} \vspace{1em}
% \caption{\BFTPROVE} \Fn{$\BFTPROVE(x)$}{
\Function{$\BFTPROVE$}{x} $state \gets false$\;
\State $state \gets false$ \For{\textbf{each } $U \in \mathcal{U}$}{
\For{\textbf{each } $U \in \mathcal{U}$} $state \gets state \textbf{ OR } DL_U.\PROVE(x)$\;\nllabel{code:prove-or}
\State $state \gets state \textbf{ OR } DL_U.\PROVE(x)$ }
\EndFor \Return{$state$}\;
\State \Return $state$ }
\EndFunction
\vspace{1em} \vspace{1em}
% \caption{\BFTREAD} \Fn{$\BFTREAD()$}{
\Function{$\BFTREAD$}{$\bot$} $results \gets \emptyset$\;
\State $results \gets \emptyset$ \For{\textbf{each } $U \in \mathcal{U}$}{
\For{\textbf{each } $U \in \mathcal{U}$} $results \gets results \cup DL_U.\READ()$\;
\State $results \gets results \cup DL_U.\READ()$ }
\EndFor \Return{$results$}\;
\State \Return $results$ }
\EndFunction
\end{algorithm} \end{algorithm}
\end{algorithmic}
\begin{lemma}[BFT-PROVE Validity]\label{lem:bft-prove-validity} \begin{lemma}[BFT-PROVE Validity]\label{lem:bft-prove-validity}
The invocation of $op = \BFTPROVE(x)$ by a correct process is invalid iff there exist at least $t+1$ distinct processes in $M$ that invoked a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$. The invocation of $op = \BFTPROVE(x)$ by a correct process is invalid iff there exist at least $t+1$ distinct processes in $M$ that invoked a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$.
@@ -99,7 +92,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
\begin{itemize} \begin{itemize}
\item \textbf{Case (i): $|A|\ge t+1$.} \item \textbf{Case (i): $|A|\ge t+1$.}
Fix any $U\in\mathcal{U}$. $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND_j(x)$ triggers $DL_U.\APPEND(x)$, and because $\BFTAPPEND_j(x)\prec op$ in $\Seq$, this induces a valid $DL_U.\APPEND(x)$ that appears before the induced $DL_U.\PROVE(x)$ by $p_i$. By \textbf{PROVE Validity} of $\DL$, the induced $DL_U.\PROVE(x)$ is invalid. As this holds for every $U\in\mathcal{U}$, there is \emph{no} component $DL_U$ where $\PROVE(x)$ is valid, so the field $state$ at line DL9 is never becoming true, and $op$ return false. Fix any $U\in\mathcal{U}$. $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND_j(x)$ triggers $DL_U.\APPEND(x)$, and because $\BFTAPPEND_j(x)\prec op$ in $\Seq$, this induces a valid $DL_U.\APPEND(x)$ that appears before the induced $DL_U.\PROVE(x)$ by $p_i$. By \textbf{PROVE Validity} of $\DL$, the induced $DL_U.\PROVE(x)$ is invalid. As this holds for every $U\in\mathcal{U}$, there is \emph{no} component $DL_U$ where $\PROVE(x)$ is valid, so the field $state$ at line~\ref{code:prove-or} is never becoming true, and $op$ return false.
\item \textbf{Case (ii): $|A|\le t$.} \item \textbf{Case (ii): $|A|\le t$.}
There exists $U^\star\in\mathcal{U}$ such that $A\cap U^\star=\emptyset$. For any $j\in A$, we have $j\notin U^\star$, so $\BFTAPPEND_j(x)$ does \emph{not} call $DL_{U^\star}.\APPEND(x)$. Hence no valid $DL_{U^\star}.\APPEND(x)$ appears before the induced $DL_{U^\star}.\PROVE(x)$. Since also $i\in \Pi_V(DL_{U^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{U^\star}.\PROVE(x)$ is valid. Therefore, there exists a component with a valid $\PROVE(x)$, so $op$ is valid. There exists $U^\star\in\mathcal{U}$ such that $A\cap U^\star=\emptyset$. For any $j\in A$, we have $j\notin U^\star$, so $\BFTAPPEND_j(x)$ does \emph{not} call $DL_{U^\star}.\APPEND(x)$. Hence no valid $DL_{U^\star}.\APPEND(x)$ appears before the induced $DL_{U^\star}.\PROVE(x)$. Since also $i\in \Pi_V(DL_{U^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{U^\star}.\PROVE(x)$ is valid. Therefore, there exists a component with a valid $\PROVE(x)$, so $op$ is valid.
@@ -181,94 +174,96 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
\subsubsection{Variables} \subsubsection{Variables}
Each process $p_i$ maintains the following local variables: Each process $p_i$ maintains the following local variables:
\begin{algorithmic} \LinesNotNumbered
% \State $\current \gets 0$ \begin{algorithm}
\State $\texttt{last\_commited} \gets 0$ $\texttt{last\_commited} \gets 0$\;
\State $\texttt{last\_delivered} \gets 0$ $\texttt{last\_delivered} \gets 0$\;
\State $\received \gets \emptyset$ $\received \gets \emptyset$\;
\State $\delivered \gets \emptyset$ $\delivered \gets \emptyset$\;
\State $\prop[r][j] \gets \bot, \forall r, j$ $\prop[r][j] \gets \bot, \forall r, j$\;
\State $W[r] \gets \bot, \forall r$ $W[r] \gets \bot, \forall r$\;
\State $\resolved[r] \gets \bot, \forall r$ $\resolved[r] \gets \bot, \forall r$\;
\State $Y[j]$ \Comment{Set of $n$ \BFTDL{}} $Y[j]$ a Set of $n$ $\BFTDL$\;
\end{algorithmic} \end{algorithm}
\renewcommand{\algletter}{A} \LinesNumbered
\begin{algorithm}[H] \begin{algorithm}[H]
% \caption{ABroadcast$(m)$} \caption{$\ABbroadcast(m)$ at process $p_i$}\label{alg:broadcast-bft}
\begin{algorithmic}[1] \SetAlgoLined
\Function{ABroadcast}{$m$} \Fn{ABroadcast($m$)}{
\State $\received \gets \received \cup \{m\}$ $\received \gets \received \cup \{m\}$\;
\State \Call{Propose}{}() Propose()\;
\EndFunction }
\end{algorithmic}
\end{algorithm} \end{algorithm}
\renewcommand{\algletter}{B}
\begin{algorithm}[H] \begin{algorithm}[H]
\begin{algorithmic}[1] \caption{Propose($\bot$) at process $p_i$}\label{alg:propose-bft}
\Statex \textbf{Proposer Job} \SetAlgoLined
\Function{Propose}{$\bot$} % \Statex \textbf{Proposer Job}
\State $r \gets \texttt{last\_commited}$ \Fn{Propose($\bot$)}{
\While{$S \neq \emptyset$ with $S \gets \received \setminus (\delivered \cup (\bigcup_{r' < r} \bigcup_{j \in W[r']} \prop[r'][j]))$} $r \gets \texttt{last\_commited}$\;
\Statex \Comment{PROP PHASE} \While{$S \neq \emptyset$ with $S \gets \received \setminus (\delivered \cup (\bigcup_{r' < r} \bigcup_{j \in W[r']} \prop[r'][j]))$}{
\State $\RBcast(i, \texttt{PROP}, S, \current)$ % \Comment{PROP PHASE}\;
\State \textbf{wait} until $|\{j: |\{k: (k, \PROVEtrace(r)) \in Y[j].\BFTREAD()\}| \geq t+1\}| \geq n - f$ \tcc*[f]{PROP PHASE}\\
\Statex \Comment{COMMIT PHASE} $\RBcast(i, \texttt{PROP}, S, \current)$\;
\State \textbf{for each} $j \in \Pi$ \textbf{do} $Y[j].\BFTAPPEND(r)$ \textbf{wait} until $|\{j: |\{k: (k, \PROVEtrace(r)) \in Y[j].\BFTREAD()\}| \geq t+1\}| \geq n - f$\;
\State $\RBcast(i, \texttt{COMMIT}, r)$ % \Comment{COMMIT PHASE}
\State \textbf{wait} until $|\resolved[r]| \geq n - f$ \tcc*[f]{COMMIT PHASE}\\
\Statex \Comment{X PHASE} \textbf{for each} $j \in \Pi$ \textbf{do} $Y[j].\BFTAPPEND(r)$
\State $W[r] \gets \{j: |\{k: (k, \PROVEtrace(r)) \in Y[j].\BFTREAD()\}| \geq t+1\}$ $\RBcast(i, \texttt{COMMIT}, r)$\;
\State $r \gets r + 1$ \textbf{wait} until $|\resolved[r]| \geq n - f$\;
\EndWhile % \Comment*{X PHASE}
\State $\texttt{last\_commited} \gets r$ \tcc*[f]{X PHASE}\\
\EndFunction $W[r] \gets \{j: |\{k: (k, \PROVEtrace(r)) \in Y[j].\BFTREAD()\}| \geq t+1\}$\;
\end{algorithmic} $r \gets r + 1$\;
}
$\texttt{last\_commited} \gets r$\;
}
\end{algorithm} \end{algorithm}
\renewcommand{\algletter}{C} % \renewcommand{\algletter}{C}
\begin{algorithm}[H] \begin{algorithm}[H]
% \caption*{ADeliver$(m)$} \caption{$\ABdeliver()$ at process $p_i$}\label{alg:deliver-bft}
\begin{algorithmic}[1] \SetAlgoLined
\Function{ADeliver}{$\bot$} \Fn{ADeliver($\bot$)}{
\State $r \gets \texttt{last\_delivered}$ $r \gets \texttt{last\_delivered}$\;
\If{$|\resolved[r]| < n - f$} \If{$|\resolved[r]| < n - f$}{
\State \Return $\bot$ \Return{$\bot$}
\EndIf }
\State $W[r] \gets \{j: |\{k: (k, \PROVEtrace(r)) \in Y[j].\BFTREAD()\}| \geq t+1\}$ $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$} \If{$\exists j \in W[r],\ \prop[r][j] = \bot$}{
\State \Return $\bot$ \Return{$\bot$}
\EndIf }
\State $M \gets \bigcup_{j \in W[r]} \prop[r][j]$ $M \gets \bigcup_{j \in W[r]} \prop[r][j]$\;\nllabel{code:Mcompute}
\State $m \gets \ordered(M \setminus \delivered)[0]$ \Comment{Set $m$ as the smaller message not already delivered} $m \gets \ordered(M \setminus \delivered)[0]$\;
\State $\delivered \leftarrow \delivered \cup \{m\}$ % \Comment*{Set $m$ as the smaller message not already delivered}
\If{$M \setminus \delivered = \emptyset$} \Comment{Check if all messages from round $r$ have been delivered} $\delivered \leftarrow \delivered \cup \{m\}$\;
\State $\texttt{last\_delivered} \gets \texttt{last\_delivered} + 1$ \If{$M \setminus \delivered = \emptyset$}{
\EndIf $\texttt{last\_delivered} \gets \texttt{last\_delivered} + 1$\;
\State \textbf{return} $m$
\EndFunction }
\end{algorithmic} % \Comment*{Check if all messages from round $r$ have been delivered}
\Return{$m$}
}
\end{algorithm} \end{algorithm}
\renewcommand{\algletter}{D} % \renewcommand{\algletter}{D}
\begin{algorithm}[H] \begin{algorithm}[H]
% \caption*{RB handlers} \caption{RB handler at process $p_i$}\label{alg:rb-handler-bft}
\begin{algorithmic}[1] \SetAlgoLined
\Upon{$Rdeliver(j, \texttt{PROP}, S, r)$} \Upon{$Rdeliver(j, \texttt{PROP}, S, r)$}{
\State $\received \gets \received \cup \{S\}$ $\received \gets \received \cup \{S\}$\;
\State $\prop[r][j] \gets S$ $\prop[r][j] \gets S$\;
\State $Y[j].\BFTPROVE(r)$ $Y[j].\BFTPROVE(r)$\;
\State \Call{Propose}{}() Propose()\;
\EndUpon }
\vspace{1em} \vspace{1em}
\Upon{$Rdeliver(j, \texttt{COMMIT}, r)}$ \Upon{$Rdeliver(j, \texttt{COMMIT}, r)$}{
\State $\resolved[r] \gets \resolved[r] \cup \{j\}$ $\resolved[r] \gets \resolved[r] \cup \{j\}$\;
\EndUpon }
\end{algorithmic}
\end{algorithm} \end{algorithm}
\textbf{Everything below has to be updated} \textbf{Everything below has to be updated}
@@ -338,7 +333,7 @@ Each process $p_i$ maintains the following local variables:
\end{lemma} \end{lemma}
\begin{lemma}[BFT EVentual proposal closure]\label{lem:bft-eventual-proposal-closure} \begin{lemma}[BFT EVentual proposal closure]\label{lem:bft-eventual-proposal-closure}
If a correct process $p_i$ define $M$ at line C10, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. If a correct process $p_i$ define $M$ at line~\ref{code:Mcompute}, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
\end{lemma} \end{lemma}
\begin{lemma}[BFT Unique proposal per sender per round]\label{lem:bft-unique-proposal} \begin{lemma}[BFT Unique proposal per sender per round]\label{lem:bft-unique-proposal}

BIN
Recherche/BFT-ARBover/main.pdf
View File

Binary file not shown.

106
Recherche/BFT-ARBover/main.tex
View File

@@ -11,19 +11,13 @@
\usepackage{csquotes} \usepackage{csquotes}
\usepackage[hidelinks]{hyperref} \usepackage[hidelinks]{hyperref}
\usepackage[nameinlink,noabbrev]{cleveref} \usepackage[nameinlink,noabbrev]{cleveref}
\usepackage{algorithm} \usepackage[ruled, vlined, linesnumbered, algonl, titlenumbered]{algorithm2e}
\usepackage{algpseudocode}
\usepackage{graphicx} \usepackage{graphicx}
% Line-number prefix configuration (A/B/C)
\renewcommand{\thealgorithm}{\Alph{algorithm}} % Float labels: Algorithm A, B, C
\newcommand{\algletter}{}
\algrenewcommand\alglinenumber[1]{\scriptsize\textbf{\algletter}#1}
\algnewcommand\algorithmicupon{\textbf{upon}} \SetKwProg{Fn}{Function}{}{EndFunction}
% \algnewcommand\algorithmicdo{\textbf{do}} \SetKwFunction{Wait}{Wait Until}
\algdef{SE}[UPON]{Upon}{EndUpon}[1]{% \SetKwProg{Upon}{Upon}{}{EndUpon}
\algorithmicupon\ #1\ \algorithmicdo% \SetKwComment{Comment}{}{}
}{\textbf{end upon}}
\usepackage{tikz} \usepackage{tikz}
\graphicspath{{diagrams/out}} \graphicspath{{diagrams/out}}
@@ -103,6 +97,12 @@
\crefname{lemma}{Lemma}{Lemmas} \crefname{lemma}{Lemma}{Lemmas}
\crefname{definition}{Definition}{Definitions} \crefname{definition}{Definition}{Definitions}
\crefname{algorithm}{Algorithm}{Algorithms} \crefname{algorithm}{Algorithm}{Algorithms}
% Pour pouvoir referencer des lignes dans le pseudocode
% \crefname{ALC@Line}{Lignes}{Lignes}
% \Crefname{ALC@Line}{Ligne}{Lignes}
\crefname{AlgoLine}{ligne}{lignes}
\Crefname{AlgoLine}{Ligne}{Lignes}
% Code exécuté par tout processus p_i % Code exécuté par tout processus p_i
\begin{document} \begin{document}
@@ -182,44 +182,72 @@ Each process can invoke the following functions :
Such that : Such that :
% \begin{algorithm}[H]
% \caption{$\READ'() \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$}
% \begin{algorithmic}
% \Function{READ'}{}
% \State $j \gets$ the process invoking $\READ'()$
% \State $res \gets \emptyset$
% \ForAll{$i \in \{1, \dots, k\}$}
% \State $res \gets res \cup DL_i.\READ()$
% \EndFor
% \State \Return $res$
% \EndFunction
% \end{algorithmic}
% \end{algorithm}
% \begin{algorithm}[H]
% \caption{$\APPEND'(\sigma) \rightarrow ()$}
% \begin{algorithmic}
% \Function{APPEND'}{$\sigma$}
% \State $j \gets$ the process invoking $\APPEND'(\sigma)$
% \ForAll{$M_i \in \{M_k \in M : j \in M_k\}$}
% \State $DL_i.\APPEND(\sigma)$
% \EndFor
% \EndFunction
% \end{algorithmic}
% \end{algorithm}
% \begin{algorithm}[H]
% \caption{$\PROVE'(\sigma) \rightarrow \{0, 1\}$}
% \begin{algorithmic}
% \Function{PROVE'}{$\sigma$}
% \State $j \gets$ the process invoking $\PROVE'(\sigma)$
% \State $flag \gets false$
% \ForAll{$i \in \{1, \dots, k\}$}
% \State $flag \gets flag$ OR $DL_i.\PROVE(\sigma)$
% \EndFor
% \State \Return $flag$
% \EndFunction
% \end{algorithmic}
% \end{algorithm}
\begin{algorithm}[H] \begin{algorithm}[H]
\caption{$\READ'() \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$} \caption{$\READ'() \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$}
\begin{algorithmic} $j \gets$ the process invoking $\READ'()$\;
\Function{READ'}{} $res \gets \emptyset$\;
\State $j \gets$ the process invoking $\READ'()$ \ForAll{$i \in \{1, \dots, k\}$}{
\State $res \gets \emptyset$ $res \gets res \cup DL_i.\READ()$\;
\ForAll{$i \in \{1, \dots, k\}$} }
\State $res \gets res \cup DL_i.\READ()$ \Return{$res$}\;
\EndFor
\State \Return $res$
\EndFunction
\end{algorithmic}
\end{algorithm} \end{algorithm}
\begin{algorithm}[H] \begin{algorithm}[H]
\caption{$\APPEND'(\sigma) \rightarrow ()$} \caption{$\APPEND'(\sigma) \rightarrow ()$}
\begin{algorithmic} $j \gets$ the process invoking $\APPEND'(\sigma)$\;
\Function{APPEND'}{$\sigma$} \ForAll{$M_i \in \{M_k \in M : j \in M_k\}$}{
\State $j \gets$ the process invoking $\APPEND'(\sigma)$ $DL_i.\APPEND(\sigma)$\;
\ForAll{$M_i \in \{M_k \in M : j \in M_k\}$} }
\State $DL_i.\APPEND(\sigma)$
\EndFor
\EndFunction
\end{algorithmic}
\end{algorithm} \end{algorithm}
\begin{algorithm}[H] \begin{algorithm}[H]
\caption{$\PROVE'(\sigma) \rightarrow \{0, 1\}$} \caption{$\PROVE'(\sigma) \rightarrow \{0, 1\}$}
\begin{algorithmic} $j \gets$ the process invoking $\PROVE'(\sigma)$\;
\Function{PROVE'}{$\sigma$} $flag \gets false$\;
\State $j \gets$ the process invoking $\PROVE'(\sigma)$ \ForAll{$i \in \{1, \dots, k\}$}{
\State $flag \gets false$ $flag \gets flag$ OR $DL_i.\PROVE(\sigma)$\;
\ForAll{$i \in \{1, \dots, k\}$} }
\State $flag \gets flag$ OR $DL_i.\PROVE(\sigma)$ \Return{$flag$}\;
\EndFor
\State \Return $flag$
\EndFunction
\end{algorithmic}
\end{algorithm} \end{algorithm}
\subsection{Threshold Cryptography} \subsection{Threshold Cryptography}