$\prop[r][j]\leftarrow S$\;\nllabel{code:prop-set}% \Comment{Record sender $j$'s proposal $S$ for round $r$}
\SetKwBlock{LocalVars}{Local Variables:}{}
\LocalVars{
$\mathit{unordered}\gets\emptyset$,
$\mathit{ordered}\gets\epsilon$,
$\mathit{delivered}\gets\epsilon$\;
$\mathit{prop}[r][j]\gets\bot,\ \forall r,j$\;
}
}
\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.
\vspace{0.3em}
\begin{algorithm}[H]\label{alg:ABroadcast}
\For{$r =1, 2, \ldots$}{
\caption{\ABbroadcast$(m)$ (at process $p_i$)}\label{alg:ab-bcast}
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.
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~\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.
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.
@@ -129,10 +119,10 @@ Each process $p_i$ maintains:
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.
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.
Some process invokes $\APPEND(r+1)$ at \ref{code:append-read}. Let $p_i$ be this process.
Some process invokes $\APPEND(r+1)$ at \ref{code:append-read}. Let $p_i$ be this process.
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$.
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 \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.
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:arb-crash} (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.
@@ -289,7 +279,7 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
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}).\\
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 Algorithm \ref{alg:rb-handler} and sets $\received\leftarrow\received\cup\{S\}$ with $m \in S$ (line~\ref{code:receivedConstruction}).
At $t_0$, $p_k$ executes Algorithm \ref{alg:arb-crash} and sets $\mathit{received}\leftarrow\mathit{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~\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}$.
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)$.
@@ -437,19 +427,25 @@ Which are cover by our FIFO-\ARB specification.
\subsubsection{Example executions}
\subsubsection{Example executions}
\begin{figure}
% \begin{figure}
\centering
% \centering
\resizebox{0.4\textwidth}{!}{
% \resizebox{0.4\textwidth}{!}{
\input{diagrams/nonBFT_behaviour.tex}
% \input{diagrams/nonBFT_behaviour.tex}
}
% }
\caption{Example execution of the ARB algorithm in a non-BFT setting}
%\caption{Example execution of the ARB algorithm in a non-BFT setting}
\end{figure}
% \end{figure}
\begin{figure}
% \begin{figure}
\centering
% \centering
\resizebox{0.4\textwidth}{!}{
% \resizebox{0.4\textwidth}{!}{
\input{diagrams/BFT_behaviour.tex}
% \input{diagrams/BFT_behaviour.tex}
}
% }
\caption{Example execution of the ARB algorithm with a byzantine process}
%\caption{Example execution of the ARB algorithm with a byzantine process}
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.
