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

remove RB for crash algorithms + some syntaxes fix in BFT algo

Browse Source
This commit is contained in:
Amaury JOLY
2026-03-16 09:15:07 +00:00
parent bee54232af
commit d629de3670
6 changed files with 179 additions and 192 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -1,4 +1,4 @@
We present below an example of implementation of Atomic Reliable Broadcast (\ARB) using a Reliable Broadcast (\RB) primitive and a DenyList (\DL) object according to the model and notations defined in Section 2.
We present below an example of implementation of Atomic Reliable Broadcast (\ARB) using point-to-point reliable, error-free channels and a DenyList (\DL) object according to the model and notations defined in Section 2.
\subsection{Algorithm}
@@ -28,14 +28,17 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\For{$r = 1, 2, \ldots$}{
\textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
$S \leftarrow (\unordered \setminus \ordered)$\;\nllabel{code:Sconstruction}
$\RBcast(\texttt{PROP}, S, \langle r, i \rangle)$; $\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition}
\lForEach{$j \in \Pi$}{
$\send(\texttt{PROP}, S, \langle r, i \rangle) \textbf{ to } p_j$
}
$\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition}
$\winners[r] \gets \{ j : (j, r) \in \READ() \}$\;\nllabel{code:Wcompute}
\textbf{wait until} $\forall j \in \winners[r],\ \prop[r][j] \neq \bot$\;\nllabel{code:check-winners-ack}
$M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute-dl}
$\ordered \leftarrow \ordered \cdot \ordered(M)$\;\nllabel{code:next-msg-extraction}
$\ordered \leftarrow \ordered \cdot \order(M)$\;\nllabel{code:next-msg-extraction}
}
\vspace{0.3em}
@@ -46,7 +49,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\vspace{0.3em}
\Upon{$\rdeliver(\texttt{PROP}, S, \langle r, j \rangle)$ from process $p_j$}{
\Upon{$\receive(\texttt{PROP}, S, \langle r, j \rangle)$ from process $p_j$}{
$\unordered \leftarrow \unordered \cup \{S\}$\;\nllabel{code:receivedConstruction}
$\prop[r][j] \leftarrow S$\;\nllabel{code:prop-set}
}
@@ -54,7 +57,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\vspace{0.3em}
\Upon{$\ABdeliver()$}{
\If{$\ordered \setminus \delivered = \emptyset$}{
\lIf{$\ordered \setminus \delivered = \emptyset$}{
\Return{$\bot$}
}
let $m$ be the first element in $(\ordered \setminus \delivered$)\;\nllabel{code:adeliver-extract}
@@ -109,7 +112,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\end{definition}
\begin{lemma}[Invariant view of closure]\label{lem:closure-view}
For any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\_,\PROVEtrace(r))$ in their \DL view.
For any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\ \cdot,r)$ in their \DL view.
\end{lemma}
\begin{proof}
@@ -117,7 +120,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
Consider any correct process $p_i$ that invokes $\READ()$ after $\APPEND^\star(r)$ in the DL linearization. Since $\APPEND^\star(r)$ invalidates all subsequent $\PROVE(r)$, the set of valid tuples $(\_,r)$ retrieved by a $\READ()$ after $\APPEND^\star(r)$ is fixed and identical across all correct processes.
Therefore, for any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\_,\PROVEtrace(r))$ in their \DL view.
Therefore, for any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\ \cdot,r )$ in their \DL view.
\end{proof}
\begin{lemma}[Well-defined winners]\label{lem:winners}
@@ -131,7 +134,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\begin{proof}
Lets consider a correct process $p_i$ that reach line~\ref{code:Wcompute} to compute $\winners[r]$. \\
By program order, $p_i$ must have executed $\APPEND_i(r)$ at line~\ref{code:submit-proposition} 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 line~\ref{code:Wcompute} 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 $(\ \cdot,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at line~\ref{code:Wcompute} after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\ \cdot ,r)$ such that
\[
\winners[r] = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r
\]
@@ -150,13 +153,13 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\end{proof}
\begin{lemma}[Winners must propose]\label{lem:winners-propose}
For any closed round $r$, $\forall i \in \Winners_r$, process $p_i$ must have invoked a $\RBcast(PROP, S^{(i)}, \langle r, i \rangle)$ and hence any correct will eventually set $\prop[r][i]$ to a non-$\bot$ value.
For any closed round $r$, $\forall i \in \Winners_r$, process $p_i$ must have sent messages to all processes $j \in \Pi$, and hence any correct process $p_j$ will eventually receive $p_i$'s message for round $r$ and set $\prop[r][i]$ to a non-$\bot$ value.
\end{lemma}
\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~\ref{code:submit-proposition} he must have invoked $\RBcast(PROP, S^{(i)}, \langle r, i \rangle)$ 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~\ref{code:prop-set}.
Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $i \in \Winners_r$, there exists a valid $\PROVE_i(r)$ such that $\PROVE_i(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order in Algorithm~\ref{alg:arb-crash}, $p_i$ must have sent messages to all $j \in \Pi$ at line~\ref{code:submit-proposition} before invoking $\PROVE(r)$.
If $p_i$ is a correct process that completed sending to all processes, then by the reliable and error-free nature of the communication channels, every correct process $p_j$ will eventually receive $p_i$'s message, which sets $\prop[r][i] \leftarrow S$ at line~\ref{code:prop-set}. If $p_i$ crashes before sending to all processes, then $p_i$ cannot invoke a valid $\PROVE_i(r)$ afterwards, contradicting the assumption that $i \in \Winners_r$. Hence $p_i$ must have completed sending to all processes.
\end{proof}
\begin{definition}[Messages invariant]\label{def:messages-invariant}
@@ -174,17 +177,17 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\begin{proof}[Proof]
Let take a correct process $p_i$ that computes $M$ at line~\ref{code:Mcompute-dl}. 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~\ref{code:Mcompute-dl} where $p_i$ computes $M$ 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 = \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-dl} where $p_i$ computes $M$ is guarded by the condition at line~\ref{code:check-winners-ack}, which ensures that $p_i$ has received messages from every winner $j \in \Winners_r$. By \Cref{lem:winners-propose}, each winner $j$ has sent messages to all processes including $p_i$. Thus, by the reliable and error-free nature of the channels, if $p_i$ is correct, it will eventually receive $j$'s message, setting $\prop^{(i)}[r][j] \neq \bot$ at line~\ref{code:prop-set}. Hence, $\prop^{(i)}[r][j] \neq \bot$ for all $j \in \Winners_r$.
\end{proof}
\begin{lemma}[Unique proposal per sender per round]\label{lem:unique-proposal}
For any round $r$ and any process $p_i$, $p_i$ invokes at most one $\RBcast(PROP, S, \langle r, i \rangle)$.
For any round $r$ and any process $p_i$, $p_i$ sends messages to all processes at most once for each round.
\end{lemma}
\begin{proof}[Proof]
In Algorithm~\ref{alg:arb-crash}, the only place where a process $p_i$ can invoke $\RBcast(PROP, S, \langle r, i \rangle)$ is at line~\ref{code:submit-proposition}, which appears inside the main loop indexed by rounds $r = 1, 2, \ldots$.
In Algorithm~\ref{alg:arb-crash}, the only place where a process $p_i$ can send messages to all processes is at line~\ref{code:submit-proposition}, which appears inside the main loop indexed by rounds $r = 1, 2, \ldots$.
Each iteration of this loop processes exactly one round value $r$, and within that iteration, line~\ref{code:submit-proposition} is executed at most once. Since the loop variable $r$ takes each value $1, 2, \ldots$ at most once during the execution, process $p_i$ invokes $\RBcast(PROP, S, \langle r, i \rangle)$ at most once for any given round $r$.
Each iteration of this loop processes exactly one round value $r$, and within that iteration, messages are sent at most once (before the $\PROVE(r)$ and $\APPEND(r)$ calls). Since the loop variable $r$ takes each value $1, 2, \ldots$ at most once during the execution, process $p_i$ sends messages at most once for any given round $r$.
\end{proof}
\begin{lemma}[Proposal convergence]\label{lem:convergence}
@@ -196,31 +199,28 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\begin{proof}[Proof]
Let take a correct process $p_i$ that compute $M$ at line~\ref{code:Mcompute-dl}. That implies that $p_i$ has defined $\winners r$ at line~\ref{code:Wcompute}. It implies that, by \Cref{lem:winners}, $r$ is closed and $\winners_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(PROP, S^{(j)}, \langle r, j \rangle)$, 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$ sends messages to all processes at most once per round. Thus, $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined as the messages sent by $j$ in that round. Hence, when $p_i$ computes
\[
M^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r.
\]
\end{proof}
\begin{lemma}[Inclusion]\label{lem:inclusion}
If some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a process $j\in\Winners_r$ such that $p_j$ invokes
\[
\RBcast(PROP, S, \langle r, j \rangle)\quad\text{for some S with}\quad m\in S.
\]
If some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a process $j\in\Winners_r$ such that $p_j$ sends a proposal $S$ to all processes at line~\ref{code:submit-proposition} with $m\in S$.
\end{lemma}
\begin{proof}
Let $p_i$ be a correct process that invokes $\ABbroadcast(m)$. By the handler at line~\ref{code:abbroadcast-add}, $m$ is added to $\unordered$. Since $p_i$ is correct, it continues executing the main loop.
Consider any iteration of the loop where $p_i$ executes line~\ref{code:Sconstruction} while $m \in (\unordered \setminus \ordered)$. At that iteration, for some round $r$, process $p_i$ constructs $S$ containing $m$ and invokes $\RBcast(PROP, S, \langle r, i \rangle)$ at line~\ref{code:submit-proposition}.
Consider any iteration of the loop where $p_i$ executes line~\ref{code:Sconstruction} while $m \in (\unordered \setminus \ordered)$. At that iteration, for some round $r$, process $p_i$ constructs $S$ containing $m$ and sends $S$ to all processes at line~\ref{code:submit-proposition}.
We distinguish two cases:
\begin{itemize}
\item \textbf{Case 1: $p_i$ is a winner.} If $p_i \in \Winners_r$ for this round $r$, then by \Cref{def:winner-invariant} and program order, $p_i$ has invoked $\RBcast(PROP, S, \langle r, i \rangle)$ with $m \in S$, and the lemma holds with $j = i$.
\item \textbf{Case 1: $p_i$ is a winner.} If $p_i \in \Winners_r$ for this round $r$, then by \Cref{def:winner-invariant} and program order, $p_i$ has sent proposal $S$ to all processes with $m \in S$, and the lemma holds with $j = i$.
\item \textbf{Case 2: $p_i$ is not a winner.} If $p_i \notin \Winners_r$, then by the \RB \emph{Validity} property, all correct processes eventually \rdeliver $p_i$'s message. By line~\ref{code:receivedConstruction}, each correct process $p_k$ adds $m$ to its own $\unordered$ set. Hence every correct process will eventually attempt to broadcast $m$ in some subsequent round.
\item \textbf{Case 2: $p_i$ is not a winner.} If $p_i \notin \Winners_r$, then $p_i$ is still a correct process, so it has sent its proposal $S$ (containing $m$) to all processes in $\Pi$. By the reliable and error-free nature of the communication channels, all correct processes will eventually receive $p_i$'s message. By line~\ref{code:receivedConstruction}, each correct process $p_k$ adds $m$ to its own $\unordered$ set. Hence every correct process will eventually attempt to broadcast $m$ in some subsequent round.
Since there are infinitely many rounds and finitely many processes, and by \Cref{lem:nonempty} every closed round has at least one winner, there must exist a round $r'$ and a correct process $p_j \in \Winners_{r'}$ such that $m \in (\unordered \setminus \ordered)$ when $p_j$ constructs its proposal $S$ at line~\ref{code:Sconstruction} for round $r'$. Hence $p_j$ invokes $\RBcast(PROP, S, \langle r', j \rangle)$ with $m \in S$.
Since there are infinitely many rounds and finitely many processes, and by \Cref{lem:nonempty} every closed round has at least one winner, there must exist a round $r'$ and a correct process $p_j \in \Winners_{r'}$ such that $m \in (\unordered \setminus \ordered)$ when $p_j$ constructs its proposal $S$ at line~\ref{code:Sconstruction} for round $r'$. Hence $p_j$ sends messages $S$ with $m \in S$ at line~\ref{code:submit-proposition}.
\end{itemize}
In both cases, there exists a round and a winner whose proposal includes $m$.
@@ -239,12 +239,9 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\end{lemma}
\begin{proof}[Proof]
Let $p_i$ a correct process that invokes $\ABbroadcast(m)$ and $p_q$ a correct process that infinitely invokes $\ABdeliver()$. By \Cref{lem:inclusion}, there exist a closed round $r$ and a correct process $j\in\Winners_r$ such that $p_j$ invokes
\[
\RBcast(PROP, S, \langle r, j \rangle)\quad\text{with}\quad m\in S.
\]
Let $p_i$ a correct process that invokes $\ABbroadcast(m)$ and $p_q$ a correct process that infinitely invokes $\ABdeliver()$. By \Cref{lem:inclusion}, there exist a closed round $r$ and a correct process $j\in\Winners_r$ such that $p_j$ sends a proposal $S$ to all processes with $m\in S$.
By \Cref{lem:eventual-closure}, when $p_q$ computes $M$ at line~\ref{code:Mcompute-dl}, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ invokes at most one $\RBcast(PROP, S, \langle r, j \rangle)$, so $\prop[r][j]$ is uniquely defined. Hence, when $p_q$ computes
By \Cref{lem:eventual-closure}, when $p_q$ computes $M$ at line~\ref{code:Mcompute-dl}, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ sends messages at most once per round, so $\prop[r][j]$ is uniquely defined as the proposal sent by $j$. Hence, when $p_q$ computes
\[
M = \bigcup_{k\in\Winners_r} \prop[r][k],
\]
@@ -266,13 +263,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\end{lemma}
\begin{proof}
Consider a correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exists a closed rounds $r_1$ and $r_2$ and correct processes $k_1 \in \Winners_{r_1}$ and $k_2 \in \Winners_{r_2}$ such that
\[
\RBcast(PROP, S_1, \langle r_1, k_1 \rangle)\quad\text{with}\quad m_1\in S_1,
\]
\[
\RBcast(PROP, S_2, \langle r_2, k_2 \rangle)\quad\text{with}\quad m_2\in S_2.
\]
Consider a correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exists closed rounds $r_1$ and $r_2$ and correct processes $k_1 \in \Winners_{r_1}$ and $k_2 \in \Winners_{r_2}$ such that $p_{k_1}$ and $p_{k_2}$ send proposals $S_1$ and $S_2$ respectively, with $m_1\in S_1$ and $m_2\in S_2$.
Let consider two cases :
\begin{itemize}
@@ -285,32 +276,32 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\end{proof}
\begin{theorem}[\ARB]
Under the assumed $\DL$ synchrony and $\RB$ reliability, the algorithm implements Atomic Reliable Broadcast.
In a crash asynchronous message-passing system with reliable, error-free communication channels, assuming a synchronous DenyList ($\DL$) object, the algorithm implements Atomic Reliable Broadcast.
\end{theorem}
\begin{proof}
We show that the algorithm satisfies the properties of Atomic Reliable Broadcast under the assumed $\DL$ synchrony and $\RB$ reliability.
We show that the algorithm satisfies the properties of Atomic Reliable Broadcast under the assumed $\DL$ synchrony and reliable channel assumption.
First, by \Cref{lem:bcast-termination}, if a correct process invokes $\ABbroadcast(m)$, then it eventually returns from this invocation.
Moreover, \Cref{lem:validity} states that if a correct process invokes $\ABbroadcast(m)$, then every correct process that invokes $\ABdeliver()$ infinitely often eventually delivers $m$.
This gives the usual Validity property of $\ARB$.
Concerning Integrity and No-duplicates, the construction only ever delivers messages that have been obtained from the underlying $\RB$ primitive.
By the Integrity property of $\RB$, every such message was previously $\RBcast$ by some process, so no spurious messages are delivered.
Concerning Integrity and No-duplicates, the construction only ever delivers messages that have been obtained from processes that constructed and sent them in the algorithm.
Every delivered message was previously sent by some process at line~\ref{code:submit-proposition}, so no spurious messages are delivered.
In addition, \Cref{lem:no-duplication} states that no correct process delivers the same message more than once.
Together, these arguments yield the Integrity and No-duplicates properties required by $\ARB$.
For the ordering guarantees, \Cref{lem:total-order} shows that for any two messages $m_1$ and $m_2$ delivered by correct processes, every correct process that delivers both $m_1$ and $m_2$ delivers them in the same order.
Hence all correct processes share a common total order on delivered messages.
All the above lemmas are proved under the assumptions that $\DL$ satisfies the required synchrony properties and that the underlying primitive is a Reliable Broadcast ($\RB$) with Integrity, No-duplicates and Validity.
All the above lemmas are proved under the assumptions that $\DL$ satisfies the required synchrony properties and that the communication channels are reliable and error-free (no message loss or corruption).
Therefore, under these assumptions, the algorithm satisfies Validity, Integrity/No-duplicates, and total order, and hence implements Atomic Reliable Broadcast, as claimed.
\end{proof}
\subsection{Reciprocity}
% ------------------------------------------------------------------------------
So far, we assumed the existence of a synchronous DenyList ($\DL$) object and showed how to upgrade a Reliable Broadcast ($\RB$) primitive into FIFO Atomic Reliable Broadcast ($\ARB$). We now briefly argue that, conversely, an $\ARB$ primitive is strong enough to implement a synchronous $\DL$ object.
So far, we assumed the existence of a synchronous DenyList ($\DL$) object and showed how to build an Atomic Reliable Broadcast ($\ARB$) primitive using reliable, error-free point-to-point channels. We now briefly argue that, conversely, an $\ARB$ primitive is strong enough to implement a synchronous $\DL$ object.
\xspace
@@ -346,7 +337,7 @@ Which are cover by our FIFO-\ARB specification.
\begin{itemize}[leftmargin=*]
\item \textbf{Termination.} The liveness of \ARB ensures that each $\ABbroadcast$ invocation by a correct process eventually returns, and the corresponding operation is eventually delivered and applied at all correct processes. Thus every $\APPEND$, $\PROVE$, and $\READ$ operation invoked by a correct process eventually returns.
\item \textbf{APPEND/PROVE/READ Validity.} The local code that forms \ABbroadcast requests can achieve the same preconditions as in the abstract \DL specification (e.g., $p\in\Pi_M$, $x\in S$ for $\APPEND(x)$). Once an operation is delivered, its effect and return value are exactly those of the sequential \DL specification applied in the common order.
\item \textbf{PROVE Anti-Flickering.} In the sequential \DL specification, once an element $x$ has been appended, all subsequent $\PROVE(x)$ are invalid forever. Since all replicas apply operations in the same order, this property holds in every execution of the replicated implementation: after the first linearization point of $\APPEND(x)$, no later $\PROVE(x)$ can return ``valid'' at any correct process.
\item \textbf{PROVE Anti-Flickering.} In the sequential \DL specification, once an element $x$ has been appended, all subsequent $\PROVE(x)$ are invalid forever. Since all replicas apply operations in the same order, this property holds in every execution of the replicated implementation: after the first linearization point of $\APPEND(x)$, no later $\PROVE(x)$ can return valid at any correct process.
\end{itemize}
Formally, we can describe the \DL object with the state machine approach for