Compare commits
18 Commits
f5e0d90fb4
...
main
| Author | SHA1 | Date | |
|---|---|---|---|
|
216083a4cb | ||
|
|
d4856e9707 | ||
|
|
d629de3670 | ||
|
|
bee54232af | ||
|
|
9a9d7af098 | ||
|
|
61282a0737 | ||
|
|
e4e3abad91 | ||
|
|
55fa76a272 | ||
|
|
d9848967b8 | ||
|
|
cc22c9d7f3 | ||
|
|
268c30a112 | ||
|
|
921dd502e3 | ||
|
|
8ae05ff173 | ||
|
|
945d830e89 | ||
|
|
ea8826c4f5 | ||
|
|
3e8aec36a2 | ||
|
|
d5a865dd0a | ||
|
|
f2cc294232 |
@@ -225,7 +225,7 @@ Each process $p_i$ maintains:
|
||||
% ------------------------------------------------------------------------------
|
||||
\section{Correctness}
|
||||
|
||||
\begin{lemma}[Stable round closure]\label{lem:closure-stable}
|
||||
\begin{lemma}[Stable round closure]\label{rem:closure-stable}
|
||||
If a round $r$ is closed, then there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid.
|
||||
Once closed, a round never becomes open again.
|
||||
\end{lemma}
|
||||
|
||||
@@ -1,22 +1,25 @@
|
||||
\subsection{Reliable Broadcast (RB)}
|
||||
\subsection{DenyList Object}
|
||||
|
||||
\RB provides the following properties in the model.
|
||||
\begin{itemize}[leftmargin=*]
|
||||
\item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ \RBreceived_i(m) \Rightarrow \exists p_j:\ \RBcast_j(m)$.
|
||||
\item \textbf{No-duplicates}: No message is received more than once at any process.
|
||||
\item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
|
||||
\end{itemize}
|
||||
|
||||
\subsection{Group Election Object}
|
||||
|
||||
We consider a Groupe Election object ($\GE[r]$) per round $r \in \mathcal{R}$ with the following properties.
|
||||
|
||||
There are three operations: $\CANDIDATE(r), \CLOSE(r)$ and $\READGE(r)$ such that:
|
||||
\begin{itemize}
|
||||
\item \textbf{Termination.} A $\CANDIDATE(r), \CLOSE(r)$ or $\READGE(r)$ operation invoked by a correct process always returns.
|
||||
\item \textbf{Election.} If there exists at least one $\CLOSE(r)$ operation and let $\CLOSE(r)^\star$ denote the first $\CLOSE(r)$ in the linearization order. If some correct process $p$ invokes $\CANDIDATE(r)$ and the invocation of $\CANDIDATE(r)$ appears before $\CLOSE(r)^\star$ in the linearization order, then $\Winners_r \neq \emptyset$.
|
||||
\item \textbf{Prefix Inclusion.} If $\CLOSE(r)^\star$ exists, then there exists a set $\Winners_r \subseteq \Pi$ such that, for any process $p_j$: $p_j \in \Winners_r$ iff $p_j$ invokes $\CANDIDATE(r)$ and its $\CANDIDATE(r)$ operation is linearized before $\CLOSE(r)^\star$.
|
||||
\item \textbf{Stability.} If $\CLOSE(r)^\star$ exists, then every $\READGE(r)$ operation linearized after
|
||||
$\CLOSE(r)^\star$ returns exactly $\Winners_r$.
|
||||
\item \textbf{READ Validity.} The invocation of $op = \READGE(r)$ by a process $p$ returns the list of valid invocations of $\CANDIDATE(r)$ that appears before $op$ in the linearization order along with the names of the processes that invoked each operation.
|
||||
\end{itemize}
|
||||
We assume a linearizable DenyList (\DL) object, following the specification in~\cite{frey:disc23}, with the following properties.
|
||||
|
||||
The DenyList object type supports three operations: $\APPEND$, $\PROVE$, and $\READ$. These operations appear as if executed in a sequence $\Seq$ such that:
|
||||
\begin{itemize}
|
||||
\item \textbf{Termination.} A $\PROVE$, an $\APPEND$, or a $\READ$ operation invoked by a correct process always returns.
|
||||
\item \textbf{APPEND Validity.} The invocation of $\APPEND(x)$ by a process $p$ is valid if:
|
||||
\begin{itemize}
|
||||
\item $p \in \Pi_M \subseteq \Pi$; \textbf{and}
|
||||
\item $x \in S$, where $S$ denote the universe of valid entries to be appended to the DenyList.
|
||||
\end{itemize}
|
||||
Otherwise, the operation is invalid.
|
||||
\item \textbf{PROVE Validity.} Let $op$ the invocation of $\PROVE(x)$ by a process $p_i$. We said $op$ to be invalid, if and only if:
|
||||
\begin{itemize}
|
||||
\item $p \not\in \Pi_V \subseteq \Pi$; \textbf{or}
|
||||
\item A valid $\APPEND(x)$ appears before $op$ in $\Seq$.
|
||||
\end{itemize}
|
||||
Otherwise, the operation is said to be valid.
|
||||
\item \textbf{PROVE Anti-Flickering.} If the invocation of a operation $op = \PROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\PROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
|
||||
\item \textbf{READ Validity.} The invocation of $op = \READ()$ by a process $p \in \pi_V$ returns the list of valid invocations of $\PROVE$ that appears before $op$ in $\Seq$ along with the names of the processes that invoked each operation.
|
||||
% \item \textbf{Anonymity.} Let us assume the process $p$ invokes a $\PROVE(v)$ operation. If the process $p'$ invokes a $\READ()$ operation, then $p'$ cannot learn the value $v$ unless $p$ leaks additional information.
|
||||
\end{itemize}
|
||||
|
||||
We assume that $\Pi_M = \Pi_V = \Pi$ (all processes can invoke $\APPEND$ and $\PROVE$).
|
||||
11
Recherche/BFT-ARBover/3_ARB_Def/index.tex
Normal file
11
Recherche/BFT-ARBover/3_ARB_Def/index.tex
Normal file
@@ -0,0 +1,11 @@
|
||||
|
||||
Processes export \ABbroadcast$(m)$ and $m = \ABdeliver()$. We adopt the standard Atomic Broadcast specification of~\cite{Defago2004}. \ARB requires the following properties:
|
||||
\begin{itemize}[leftmargin=*]
|
||||
\item \textbf{Total Order}:
|
||||
\begin{equation*}
|
||||
\forall m_1,m_2,\ \forall p_i,p_j:\ \ (m_1 = \ABdeliver_i()) \prec (m_2 = \ABdeliver_i()) \Rightarrow (m_1 = \ABdeliver_j()) \prec (m_2 = \ABdeliver_j())
|
||||
\end{equation*}
|
||||
\item \textbf{Integrity}: Every message delivered was previously broadcast. $\forall p_i:\ m = \ABdeliver_i() \Rightarrow \exists p_j:\ \ABbroadcast_j(m)$.
|
||||
\item \textbf{No-duplicates}: No message is delivered more than once at any process.
|
||||
\item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually delivers $m$.
|
||||
\end{itemize}
|
||||
@@ -1,132 +0,0 @@
|
||||
|
||||
\begin{definition}
|
||||
We assume a synchronous DenyList (\DL) object as in~\cite{frey:disc23} with the following properties.
|
||||
|
||||
The DenyList object type supports three operations: $\APPEND$, $\PROVE$, and $\READ$. These operations appear as if executed in a sequence $\Seq$ such that:
|
||||
\begin{itemize}
|
||||
\item \textbf{Termination.} A $\PROVE$, an $\APPEND$, or a $\READ$ operation invoked by a correct process always returns.
|
||||
\item \textbf{APPEND Validity.} The invocation of $\APPEND(x)$ by a process $p$ is valid if:
|
||||
\begin{itemize}
|
||||
\item $p \in \Pi_M \subseteq \Pi$; \textbf{and}
|
||||
\item $x \in S$, where $S$ is a predefined set.
|
||||
\end{itemize}
|
||||
Otherwise, the operation is invalid.
|
||||
\item \textbf{PROVE Validity.} If the invocation of a $op = \PROVE(x)$ by a correct process $p$ is not valid, then:
|
||||
\begin{itemize}
|
||||
\item $p \not\in \Pi_V \subseteq \Pi$; \textbf{or}
|
||||
\item A valid $\APPEND(x)$ appears before $op$ in $\Seq$.
|
||||
\end{itemize}
|
||||
Otherwise, the operation is valid.
|
||||
\item \textbf{PROVE Anti-Flickering.} If the invocation of a operation $op = \PROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\PROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
|
||||
\item \textbf{READ Validity.} The invocation of $op = \READ()$ by a process $p \in \pi_V$ returns the list of valid invocations of $\PROVE$ that appears before $op$ in $\Seq$ along with the names of the processes that invoked each operation.
|
||||
item \textbf{Anonymity.} Let us assume the process $p$ invokes a $\PROVE(v)$ operation. If the process $p'$ invokes a $\READ()$ operation, then $p'$ cannot learn the value $v$ unless $p$ leaks additional information.
|
||||
\end{itemize}
|
||||
|
||||
We assume that $\Pi_M = \Pi_V = \Pi$ (all processes can invoke \APPEND and \PROVE).
|
||||
\end{definition}
|
||||
|
||||
\begin{lemma}[From DenyList to Group Election]\label{lem:dl-to-ge}
|
||||
For any fixed value $r \in S$, one DenyList object can be used to wait-free implement a Group Election object $\GE[r]$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
We implement the operations of $\GE[r]$ using the operations of the
|
||||
DenyList as follows.
|
||||
|
||||
\begin{algorithmic}
|
||||
\Function{CANDIDATE}{$r$}
|
||||
\State $\PROVE(r)$
|
||||
\EndFunction
|
||||
\vspace{1em}
|
||||
\Function{CLOSE}{$r$}
|
||||
\State $\APPEND(r)$
|
||||
\EndFunction
|
||||
\vspace{1em}
|
||||
\Function{READGE}{$r$}
|
||||
\State $P \gets \READ()$
|
||||
\State \Return $\{ j : (j,\PROVEtrace(r)) \in P \}$
|
||||
\EndFunction
|
||||
\end{algorithmic}
|
||||
|
||||
\paragraph{Termination.} Termination follows from the Termination property of DenyList operations. Consider now a fixed sequential history $\mathsf{Seq}$ of the DenyList.
|
||||
\paragraph{Prefix Inclusion.} Let $\APPEND(r)^\star$ denote the first valid $\APPEND(r)$ in $\mathsf{Seq}$, if it exists. From the PROVE Validity and anti-flickering properties of the DenyList, a process $p_j$ has a valid $\PROVE(r)$ in $\mathsf{Seq}$ if and only if its $\PROVE(r)$ invocation appears before $\APPEND(r)^\star$ in $\mathsf{Seq}$.
|
||||
Hence, by construction, $p_j \in \Winners_r$ iff $p_j$ invokes $\CANDIDATE(r)$ and its $\CANDIDATE(r)$ is linearized before $\CLOSE(r)^\star$ where we identify $\CLOSE(r)^\star$ with $\APPEND(r)^\star$. This is exactly the Prefix inclusion property.
|
||||
\paragraph{Stability.} Moreover, after $\APPEND(r)^\star$, no new $\PROVE(r)$ can become valid (anti-flickering), so every subsequent $\READ^\star()$
|
||||
returns the same set of valid $\PROVE(r)$ invocations. Consequently,
|
||||
every $\READGE(r)$ linearized after $\CLOSE(r)^\star$ returns the same
|
||||
set $\Winners_r$, which proves Stability.
|
||||
\paragraph{Election.} Finally, if some process invokes $\CANDIDATE(r)$ before $\CLOSE(r)^\star$, its proof is valid and thus appears in the set returned by $\READ^\star()$. Hence $\Winners_r \neq \emptyset$, which proves Election.
|
||||
\paragraph{Validity.} Validity is immediate from the construction of $\Winners_r$: a process belongs to $\Winners_r$ only if it invoked $\PROVE(r)$, i.e., only if it invoked $\CANDIDATE(r)$.
|
||||
|
||||
Thus the constructed object satisfies all properties of a Group Election object.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[From Group Election to DenyList]\label{lem:ge-to-dl}
|
||||
Fix a value $r \in S$. A Group Election object $\GE[r]$ can be used to wait-free implement an DenyList.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
We implement the DenyList for value $r$ as follows.
|
||||
We use one Group Election object $\GE[r]$.
|
||||
|
||||
The operations are implemented as follows.
|
||||
|
||||
\begin{algorithmic}
|
||||
\Function{APPEND}{$r$}
|
||||
\State $\CLOSE(r)$
|
||||
\EndFunction
|
||||
\vspace{1em}
|
||||
\Function{PROVE}{$r$}
|
||||
\State $\CANDIDATE(r)$
|
||||
\State $W_r \gets \READGE(r)$
|
||||
\If{$p \in W_r$}
|
||||
\State \Return \texttt{True}
|
||||
\Else
|
||||
\State \Return \texttt{False}
|
||||
\EndIf
|
||||
\EndFunction
|
||||
\vspace{1em}
|
||||
\Function{READ}{$ $}
|
||||
\State $W \gets \bigcup_{\forall r \in S}\READGE(r)$
|
||||
\State \Return $\{(p,r) \mid p \in W_r\}$
|
||||
\EndFunction
|
||||
\end{algorithmic}
|
||||
|
||||
\paragraph{Termination.} Termination follows from the Termination property of Group Election operations. Consider now a fixed sequential history $\mathsf{Seq}$ of the Group Election.
|
||||
|
||||
\paragraph{APPEND Validity.} By construction, any process invoking $\APPEND(r)$ invokes $\CLOSE(r)$. By definition of Group Election, $\CLOSE(r)$ is always valid.
|
||||
|
||||
\paragraph{PROVE Validity.} By definition $\Pi_V = \Pi$, so any process invoking $\PROVE(r)$ is in $\Pi_V$. So the case $p \not\in \Pi_V$ cannot happen. Now, if some process invokes $\APPEND(r)$ before the invocation of $\PROVE(r)$ in $\mathsf{Seq}$, then by the Prefix Inclusion property of Group Election, the set $\Winners_r$ is already fixed and any subsequent $\CANDIDATE(r)$ cannot be in $\Winners_r$. Hence the invocation of $\PROVE(r)$ is invalid. Conversely, if no $\APPEND(r)$ appears before $\PROVE(r)$ in $\mathsf{Seq}$, then by the Election property of Group Election, if some correct process invoked $\CANDIDATE(r)$ before any $\CLOSE(r)$, then $\Winners_r \neq \emptyset$ and hence the invoking process belongs to $\Winners_r$. Thus its invocation of $\PROVE(r)$ is valid. This proves PROVE Validity.
|
||||
|
||||
\paragraph{PROVE Anti-Flickering.} If some invocation of $\PROVE(r)$ is invalid, then some $\APPEND(r)$ must have appeared before it in $\mathsf{Seq}$. By the Prefix Inclusion property of Group Election, the set $\Winners_r$ is fixed after the first $\CLOSE(r)$, so any subsequent $\CANDIDATE(r)$ cannot be in $\Winners_r$. Hence any subsequent invocation of $\PROVE(r)$ is also invalid. This proves PROVE Anti-Flickering.
|
||||
|
||||
\paragraph{READ Validity.} Finally, by construction, the invocation of $\READ()$ returns the list of valid invocations of $\PROVE$ that appear before it in $\mathsf{Seq}$ along with the names of the processes that invoked each operation. This proves READ Validity.
|
||||
|
||||
\end{proof}
|
||||
|
||||
\begin{theorem}[Consensus number of Group Election]\label{thm:ge-consensus}
|
||||
Let $|\Pi_V| = k$. The Group Election object type with verifier set $\Pi_V$
|
||||
has consensus number $k$. In particular, when $\Pi_V = \Pi$, the consensus
|
||||
number of Group Election is $|\Pi|$.
|
||||
\end{theorem}
|
||||
|
||||
\begin{proof}
|
||||
We first recall that, for a DenyList object with $|\Pi_V| = k$ (a
|
||||
$k$-DenyList), the consensus number is exactly $k$.
|
||||
|
||||
\paragraph{Lower bound.}
|
||||
By Lemma~\ref{lem:dl-to-ge}, for any fixed value $r \in S$, one $k$-DenyList object can be used to wait-free implement a Group Election object $\GE[r]$ over the same set of processes. Since the k-DenyList has consensus number $k$, it follows that the Group Election type has consensus number at least $k$.
|
||||
|
||||
\paragraph{Upper bound.}
|
||||
Conversely, by Lemma~\ref{lem:ge-to-dl}, one Group Election object
|
||||
can be used to wait-free implement a DenyList object restricted to value $r$.
|
||||
This restricted DenyList satisfies the same specification as the original k-DenyList on value $r$, and in particular it has consensus number $k$. Therefore, the consensus
|
||||
number of the Group Election type cannot exceed $k$.
|
||||
|
||||
\medskip
|
||||
Combining the two bounds, we obtain that the consensus number of the Group
|
||||
Election object type is exactly $k = |\Pi_V|$. When we instantiate
|
||||
$\Pi_V = \Pi$, we get that the consensus number of Group Election is $|\Pi|$.
|
||||
\end{proof}
|
||||
|
||||
|
||||
@@ -1,6 +0,0 @@
|
||||
|
||||
Processes export \ABbroadcast$(m)$ and \ABdeliver$(m)$. \ARB requires total order:
|
||||
\begin{equation*}
|
||||
\forall m_1,m_2,\ \forall p_i,p_j:\ \ \ABdeliver_i(m_1) < \ABdeliver_i(m_2) \Rightarrow \ABdeliver_j(m_1) < \ABdeliver_j(m_2),
|
||||
\end{equation*}
|
||||
plus Integrity/No-duplicates/Validity (inherited from \RB and the construction).
|
||||
374
Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex
Normal file
374
Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex
Normal file
@@ -0,0 +1,374 @@
|
||||
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}
|
||||
|
||||
\begin{definition}[Closed round]\label{def:closed-round}
|
||||
Given a \DL{} linearization $H$, a round $r\in\mathcal{R}$ is \emph{closed} in $H$ if $H$ contains an operation $\APPEND(r)$.
|
||||
Equivalently, there exists a time after which every $\PROVE(r)$ is invalid in $H$.
|
||||
\end{definition}
|
||||
|
||||
% \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}
|
||||
|
||||
\begin{algorithm}[H]
|
||||
\caption{ARB at process $p_i$}\label{alg:arb-crash}
|
||||
% \SetAlgoLined
|
||||
|
||||
\SetKwBlock{LocalVars}{Local Variables:}{}
|
||||
\LocalVars{
|
||||
$\unordered \gets \emptyset$,
|
||||
$\ordered \gets \epsilon$,
|
||||
$\delivered \gets \epsilon$\;
|
||||
$\prop[r][j] \gets \bot,\ \forall r,j$\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\For{$r = 1, 2, \ldots$}{
|
||||
\textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
|
||||
$S \leftarrow (\unordered \setminus \ordered)$\;\nllabel{code:Sconstruction}
|
||||
\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 \order(M)$\;\nllabel{code:next-msg-extraction}
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\ABbroadcast(m)$}{
|
||||
$\unordered \gets \unordered \cup \{m\}$\;\nllabel{code:abbroadcast-add}
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\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}
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\ABdeliver()$}{
|
||||
\lIf{$\ordered \setminus \delivered = \emptyset$}{
|
||||
\Return{$\bot$}
|
||||
}
|
||||
let $m$ be the first element in $(\ordered \setminus \delivered$)\;\nllabel{code:adeliver-extract}
|
||||
$\delivered \gets \delivered \cdot m$\;\nllabel{code:adeliver-mark}
|
||||
\Return{$m$}
|
||||
}
|
||||
|
||||
\end{algorithm}
|
||||
|
||||
\paragraph{Algorithm intuition.}
|
||||
The crash-tolerant algorithm is organized around round closure and winner extraction. By \Cref{def:closed-round,def:first-append,lem:closure-view,lem:winners}, once a round is closed, every correct process eventually reads the same winner set $\Winners_r$. By \Cref{lem:nonempty}, this set is never empty, and by \Cref{lem:winners-propose} every winner has necessarily sent its proposal to all processes before becoming a winner, exactly because sending precedes $\PROVE(r)$ and $\APPEND(r)$ at line~\ref{code:submit-proposition}. Under reliable channels, these winner proposals are eventually received by every correct process, so the waiting condition at line~\ref{code:check-winners-ack} eventually becomes true, which is formalized by \Cref{lem:eventual-closure}. Then, by \Cref{lem:convergence}, all correct processes compute the same set $M$ at line~\ref{code:Mcompute-dl}, and because line~\ref{code:next-msg-extraction} applies the same deterministic ordering function, they append messages in the same order; this is exactly the core mechanism later used in \Cref{lem:validity,lem:no-duplication,lem:total-order}.
|
||||
|
||||
\subsection{Correctness}
|
||||
|
||||
\begin{definition}[First APPEND]\label{def:first-append}
|
||||
Given a \DL{} linearization $H$, for any closed round $r\in\mathcal{R}$, we denote by $\APPEND^{(\star)}(r)$ the earliest $\APPEND(r)$ in $H$.
|
||||
\end{definition}
|
||||
|
||||
\begin{remark}[Stable round closure]\label{rem:closure-stable}
|
||||
If a round $r$ is closed, then there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid.
|
||||
Once closed, a round never becomes open again.
|
||||
\end{remark}
|
||||
|
||||
\begin{proof}
|
||||
By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the linearization $H$. \\
|
||||
$H$ is a total order of operations, the set of $\APPEND(r)$ operations is totally ordered, and hence there exists a smallest $\APPEND(r)$ in $H$. We denote this operation $\APPEND^{(\star)}(r)$ and $t_0$ its linearization point. \\
|
||||
By the validity property of \DL, a $\PROVE(r)$ is valid iff $\PROVE(r) \prec \APPEND^{(\star)}(r)$. Thus, after $t_0$, no $\PROVE(r)$ can be valid. \\
|
||||
$H$ is a immutable grow-only history, and hence once closed, a round never becomes open again. \\
|
||||
Hence there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid and the closure is stable.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Across rounds]\label{lem:across}
|
||||
If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$, r' is also closed.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
\emph{Base.} For a closed round $r=0$, the set $\{r' \in \mathcal{R} : r' < r\}$ is empty, so the claim holds.
|
||||
|
||||
\emph{Induction step.} Assume $r+1$ is closed. By \cref{def:first-append}, there exists an earliest operation $\APPEND^{(\star)}(r+1)$ in the \DL linearization $H$. Let $p_j$ be the process that invokes this operation.
|
||||
|
||||
In Algorithm~\ref{alg:arb-crash}, the call to $\APPEND(\cdot)$ appears at line~\ref{code:submit-proposition}, inside the loop indexed by rounds $1,2,\ldots$. Therefore, if $p_j$ reaches line~\ref{code:submit-proposition} for round $r+1$, then in the previous loop iteration (round $r$) process order implies that $p_j$ has already invoked $\APPEND(r)$ at the same line.
|
||||
|
||||
Hence an $\APPEND(r)$ exists in $H$, so round $r$ is closed by \cref{def:closed-round}. We proved:
|
||||
\[
|
||||
(r+1\ \text{closed}) \Rightarrow (r\ \text{closed}).
|
||||
\]
|
||||
By repeated application, if some round $r$ is closed, then every round $r' < r$ is also closed.
|
||||
\end{proof}
|
||||
|
||||
\begin{definition}[Winner Invariant]\label{def:winner-invariant}
|
||||
For any closed round $r$, define
|
||||
\[
|
||||
\Winners_r \triangleq \{ j : \PROVE_j(r) \prec \APPEND^\star(r) \}
|
||||
\]
|
||||
called the unique set of winners of round $r$.
|
||||
\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 $(\ \cdot,r)$ in their \DL view.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let's take a closed round $r$. By \Cref{def:first-append}, there exists $\APPEND^{(\star)}(r)$ the earliest $\APPEND(r)$ in the DL linearization.
|
||||
|
||||
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 $(\ \cdot,r )$ in their \DL view.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Well-defined winners]\label{lem:winners}
|
||||
For any correct process $p_i$ and round $r$, if $p_i$ computes $\winners[r]$ at line~\ref{code:Wcompute}, then :
|
||||
\begin{itemize}
|
||||
\item $\Winners_r$ is defined;
|
||||
\item the computed $\winners[r]$ is exactly $\Winners_r$.
|
||||
\end{itemize}
|
||||
\end{lemma}
|
||||
|
||||
\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 $(\ \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
|
||||
\]
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Winners are non-empty]\label{lem:nonempty}
|
||||
For any closed round $r$, there exists at least one process $p_j$ that invoked $\PROVE_j(r) \prec \APPEND^\star(r)$, so $\Winners_r \neq \emptyset$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}[Proof]
|
||||
Let $r$ be a closed round. By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the \DL linearization $H$. Let $p_i$ be the process invoking the earliest such operation, $\APPEND^{(\star)}(r)$.
|
||||
|
||||
By program order in Algorithm~\ref{alg:arb-crash}, the call to $\APPEND(\cdot)$ at line~\ref{code:submit-proposition} is immediately preceded by $\PROVE(r)$. Thus $p_i$ must have invoked $\PROVE_i(r)$ before $\APPEND^{(\star)}(r)$, and by the sequence of code at line~\ref{code:submit-proposition}, this $\PROVE_i(r)$ executes before $\APPEND^{(\star)}(r)$ in the linearization.
|
||||
|
||||
By \Cref{def:winner-invariant}, $p_i \in \Winners_r$. Hence $\Winners_r \neq \emptyset$.
|
||||
\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 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 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}
|
||||
For any closed round $r$ and any correct process $p_i$ such that $\forall j \in \Winners_r : prop^{(i)}[r][j] \neq \bot$, define
|
||||
\[
|
||||
\Messages_r \triangleq \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]
|
||||
\]
|
||||
as the set of messages proposed by the winners of round $r$.
|
||||
\end{definition}
|
||||
|
||||
\begin{lemma}[Eventual proposal closure]\label{lem:eventual-closure}
|
||||
If a correct process $p_i$ define $M$ at line~\ref{code:Mcompute-dl}, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
|
||||
\end{lemma}
|
||||
|
||||
\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 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$ 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 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, 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}
|
||||
For any round $r$, for any correct processes $p_i$ that execute line~\ref{code:Mcompute-dl}, we have
|
||||
\[
|
||||
M^{(i)} = \Messages_r
|
||||
\]
|
||||
\end{lemma}
|
||||
|
||||
\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$ 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$ 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 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 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 $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$ 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$.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Broadcast Termination]\label{lem:bcast-termination}
|
||||
A correct process which invokes $\ABbroadcast(m)$ eventually exits the function and returns.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}[Proof]
|
||||
By Algorithm~\ref{alg:arb-crash}, the handler for $\ABbroadcast(m)$ at line~\ref{code:abbroadcast-add} performs a single local operation: adding $m$ to the local set $\unordered$. This operation terminates immediately and the function returns.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Validity]\label{lem:validity}
|
||||
If a correct process $p$ invokes $\ABbroadcast(m)$, then every correct process that invokes a infinitely many times $\ABdeliver()$ eventually delivers $m$.
|
||||
\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$ 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$ 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],
|
||||
\]
|
||||
we have $m \in \prop[r][j] = S$, so $m \in M$. By \Cref{lem:convergence}, $M$ is invariant so each computation of $M$ by a correct process includes $m$. At each invocation of $m' = \ABdeliver()$, $m'$ is added to $\delivered$ until $M \subseteq \delivered$. Once this happens we're assured that there exists an invocation of $\ABdeliver()$ which return $m$. Hence $m$ is well delivered.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[No duplication]\label{lem:no-duplication}
|
||||
No correct process delivers the same message more than once.
|
||||
\end{lemma}
|
||||
|
||||
\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)}()$.
|
||||
|
||||
When $\ABdeliver^{(A)}()$ occurs, by program order and because it reached line~\ref{code:adeliver-mark} to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reached line~\ref{code:adeliver-extract} to extract the next message to deliver, it can't be $m$ because $m \not\in (\ordered \setminus \delivered)$. So a $\ABdeliver^{(B)}()$ which delivers $m$ can't occur.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Total order]\label{lem:total-order}
|
||||
For any two messages $m_1$ and $m_2$ delivered by correct processes, if a correct process $p_i$ delivers $m_1$ before $m_2$, then any correct process $p_j$ that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
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}
|
||||
\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$ (which contains $m_1$) to increment $\current$ and eventually set $\current = r_2$ to compute $M$ 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$ at line~\ref{code:Mcompute-dl} 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}
|
||||
|
||||
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.
|
||||
\end{proof}
|
||||
|
||||
\begin{theorem}[\ARB]
|
||||
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 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 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 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 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
|
||||
|
||||
\paragraph{DenyList as a deterministic state machine.}
|
||||
Without anonymity, the \DL specification defines a
|
||||
deterministic abstract object: given a sequence $\Seq$ of operations
|
||||
$\APPEND(x)$, $\PROVE(x)$, and $\READ()$, the resulting sequence of return
|
||||
values and the evolution of the abstract state (set of appended elements,
|
||||
history of operations) are uniquely determined.
|
||||
|
||||
\paragraph{State machine replication over \ARB.}
|
||||
Assume a system that exports a FIFO-\ARB primitive with the guarantees that if a correct process invokes $\ABbroadcast(m)$, then every correct process eventually $\ABdeliver(m)$ and the invocation eventually returns.
|
||||
Following the classical \emph{state machine replication} approach described by Schneider~\cite{Schneider90}, we can implement a fault-tolerant service by ensuring the following properties:
|
||||
\begin{quote}
|
||||
\textbf{Agreement.} Every nonfaulty state machine replica receives every request. \\
|
||||
\textbf{Order.} Every nonfaulty state machine replica processes the requests it receives in
|
||||
the same relative order.
|
||||
\end{quote}
|
||||
|
||||
Which are cover by our FIFO-\ARB specification.
|
||||
|
||||
\paragraph{Correctness.}
|
||||
|
||||
|
||||
\begin{theorem}[From \ARB to synchronous \DL]\label{thm:arb-to-dl}
|
||||
In an asynchronous message-passing system with crash failures, assume a FIFO Atomic Reliable Broadcast primitive (in the standard Total Order / Atomic Broadcast sense of~\cite{Defago2004}) with Integrity, No-duplicates, Validity, and the liveness of $\ABbroadcast$. Then there exists an implementation of a DenyList object that satisfies Termination, Validity, and Anti-flickering properties.
|
||||
\end{theorem}
|
||||
|
||||
\begin{proof}
|
||||
Because the \DL object is deterministic, all correct processes see the same sequence of operations and compute the same sequence of states and return values. We obtain:
|
||||
|
||||
\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.
|
||||
\end{itemize}
|
||||
|
||||
Formally, we can describe the \DL object with the state machine approach for
|
||||
crash-fault, asynchronous message-passing systems with a total order broadcast
|
||||
layer~\cite{Schneider90}.
|
||||
\end{proof}
|
||||
|
||||
\subsubsection{Example executions}
|
||||
|
||||
% \begin{figure}
|
||||
% \centering
|
||||
% \resizebox{0.4\textwidth}{!}{
|
||||
% \input{diagrams/nonBFT_behaviour.tex}
|
||||
% }
|
||||
% \caption{Example execution of the ARB algorithm in a non-BFT setting}
|
||||
% \end{figure}
|
||||
|
||||
|
||||
% \begin{figure}
|
||||
% \centering
|
||||
% \resizebox{0.4\textwidth}{!}{
|
||||
% \input{diagrams/BFT_behaviour.tex}
|
||||
% }
|
||||
% \caption{Example execution of the ARB algorithm with a byzantine process}
|
||||
% \end{figure}
|
||||
|
||||
|
||||
% font en fonctin de lusage
|
||||
|
||||
% winner invariant
|
||||
% order invariant
|
||||
@@ -1,19 +0,0 @@
|
||||
In this part we're using the consensus number of the GE Object to show that it's possible to implement F-ARB with RB and our defined object. Also we present an algorithm which achieve this in section 7.
|
||||
|
||||
\begin{theorem}[RB + Group Election implements F-ARB]\label{thm:ge-to-farb}
|
||||
In an asynchronous message-passing system with crash failure. We can wait-free implement a FIFO-Atomic Reliable Broadcast from a Reliable Broadcast (RB) primitive and one Group Election object $\GE[r]$ per round $r \in \mathbb{N}$.
|
||||
\end{theorem}
|
||||
|
||||
\begin{proof}
|
||||
By Theorem~\ref{thm:ge-consensus}, the Group Election object type with verifier set $\Pi_V$ has consensus number $|\Pi_V|$. In particular, when $\Pi_V = \Pi$, using one instance $\GE[r]$ per round $r$ we can implement wait-free consensus among all processes in~$\Pi$.
|
||||
|
||||
It is well known that, in a crash-prone asynchronous message-passing system, consensus and atomic (total order) broadcast are equivalent (defago et al): given consensus, one can implement atomic broadcast by using an infinite sequence of consensus instances to decide the sequence of messages to deliver, and conversely atomic broadcast can be used to implement consensus by deciding a single value in the first
|
||||
position of the total order.
|
||||
|
||||
In our setting, we already have a Reliable Broadcast (RB) primitive, which provides RB-Validity, RB-Agreement, and RB-Integrity for the dissemination of messages. Using the consensus power provided by the Group Election objects, we can therefore apply the standard reduction from consensus to atomic broadcast: each position (or \emph{slot}) in the global delivery sequence is chosen by a consensus instance, whose proposals are messages that have been RB-delivered but not yet ordered. This yields an atomic
|
||||
reliable broadcast (ARB) primitive.
|
||||
|
||||
To obtain FIFO-Atomic Reliable Broadcast (F-ARB), it suffices to enforce per-sender FIFO order on top of ARB. This can be done in the usual way by tagging each message broadcast by a process $p_i$ with a local sequence number $s \in \mathbb{N}$, and by ensuring that only the message with the smallest pending sequence number for $p_i$ is ever proposed to a consensus instance. As a result, for every sender $p_i$, messages with tags $(p_i,s)$ and $(p_i,t)$ with $s < t$ are decided (and thus delivered) in this order at all processes.
|
||||
|
||||
Hence, RB plus Group Election objects is sufficient to implement FIFO-Atomic Reliable Broadcast.
|
||||
\end{proof}
|
||||
559
Recherche/BFT-ARBover/5_BFT_ARB/index.tex
Normal file
559
Recherche/BFT-ARBover/5_BFT_ARB/index.tex
Normal file
@@ -0,0 +1,559 @@
|
||||
|
||||
\subsection{Model extension}
|
||||
We extend the crash model of Section 1 (same process universe, asynchronous setting, uniquely identifiable messages, and reliable point-to-point channels) with Byzantine faults and Byzantine-resilient dissemination primitives.
|
||||
|
||||
\paragraph{Failure threshold.} At most $t$ processes may be Byzantine, and we assume $n > 3t$, following standard asynchronous Byzantine assumptions~\cite{Bracha87}.
|
||||
|
||||
\paragraph{Additional communication primitive.} In addition to reliable point-to-point channels, processes use Reliable Broadcast ($\RB$) with operations $\RBcast(m)$ and $m=\rdeliver()$. We use Bracha's Byzantine RB specification~\cite{Bracha87}: for a fixed sender and broadcast instance, all correct processes that deliver, deliver the same payload, and Byzantine equivocation on that instance is prevented.
|
||||
|
||||
\paragraph{Byzantine behaviour}
|
||||
A Byzantine process may deviate arbitrarily from the algorithm (malformed inputs, selective omission, collusion, inconsistent timing, etc.).
|
||||
|
||||
Byzantine processes are still constrained by the assumed primitives: they cannot violate the safety/liveness guarantees of $\DL$ and cannot break the Integrity, No-duplicates, and Validity guarantees of $\RB$.
|
||||
|
||||
|
||||
\paragraph{Notation.} For any indice $k$ we defined by $\DL[k]$ as the $k$-th DenyList object. For a given $\DL[k]$ and any indice $x$ we defined by $\Pi_x^k$ a subset of $\Pi$. Still for a given $k$ we consider $\Pi_M^k \subseteq \Pi$ and $\Pi_V^k \subseteq \Pi$ two authorization subsets for $\DL[k]$. Indice $i \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec_k$ for the $\DL[k]$ linearization: $x \prec_k y$ means that operation $x$ appears strictly before $y$ in the linearized history of $\DL[k]$. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes).
|
||||
For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked by process $p_i$, and by $F_i^k(...)$ the same operation invoked on the $\DL[k]$ object.
|
||||
|
||||
% ------------------------------------------------------------------------------
|
||||
\subsection{Primitives}
|
||||
|
||||
\subsection{Reliable Broadcast (RB)}
|
||||
|
||||
\RB provides the following properties in this model (cf.~\cite{Bracha87}).
|
||||
\begin{itemize}[leftmargin=*]
|
||||
\item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ m = \rbreceived_i() \Rightarrow \exists p_j:\ \RBcast_j(m)$.
|
||||
\item \textbf{No-duplicates}: No message is received more than once at any process.
|
||||
\item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
|
||||
\end{itemize}
|
||||
|
||||
\subsubsection{t-BFT-DL}
|
||||
|
||||
We consider a t-Byzantine Fault Tolerant DenyList (t-$\BFTDL$) with the following properties.
|
||||
There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD()$ such that :
|
||||
|
||||
\paragraph{Termination.} Every operation $\BFTAPPEND(x)$, $\BFTPROVE(x)$, and $\BFTREAD()$ invoked by a correct process always returns.
|
||||
|
||||
\paragraph{PROVE Validity.} The invocation of $op = \BFTPROVE(x)$ by a correct process is valid iff there exist a set of correct process $C$ such that $\forall c \in C$, $c$ invoke $op_2 = \BFTAPPEND(x)$ with $op_2 \prec op_1$ and $|C| \leq t$
|
||||
|
||||
\paragraph{PROVE Anti-Flickering.} If the invocation of a operation $op = \BFTPROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\BFTPROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
|
||||
|
||||
\paragraph{READ Liveness.} Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, x) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$.
|
||||
|
||||
\paragraph{READ Anti-Flickering.} Let $op_1, op_2$ two $\BFTREAD()$ operations that returns respectively $R_1, R_2$. Iff $op_1 \prec op_2$ then $R_2 \subseteq R_1$. Otherwise $R_1 \subseteq R_2$.
|
||||
|
||||
\paragraph{READ Safety.} Let $op_1, op_2$ respectively a valid $\BFTPROVE(x)$ operation submited by the process $p_i$ and a $\BFTREAD()$ operation submited by any correct process such that $op_1 \prec op_2$. Let $R$ the result of $op_2$ then $R \ni (i, x)$
|
||||
|
||||
\subsection{DL $\Rightarrow$ t-BFT-DL}
|
||||
|
||||
|
||||
Fix $3t < |M|$. Let
|
||||
\[
|
||||
\mathcal{U} = \{\, U \subseteq M \mid |U| = |M| - t \,\}.
|
||||
\]
|
||||
For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose authorization sets are
|
||||
\[
|
||||
\Pi_M(DL_T) = S_T = U
|
||||
\qquad\text{and}\qquad
|
||||
\Pi_V(DL_T) = V.
|
||||
\]
|
||||
|
||||
\[
|
||||
|\mathcal{U}| = \binom{|M|}{|M| - t}.
|
||||
\]
|
||||
|
||||
\begin{algorithm}
|
||||
\caption{t-BFT-DL implementation using multiple DL objects}
|
||||
|
||||
\Fn{$\BFTAPPEND(x)$}{
|
||||
\For{\textbf{each } $U \in \mathcal{U}$ st $i \in U$}{
|
||||
$DL_U.\APPEND(x)$\;
|
||||
}
|
||||
}
|
||||
|
||||
\vspace{1em}
|
||||
|
||||
\Fn{$\BFTPROVE(x)$}{
|
||||
$\state \gets false$\;
|
||||
\For{\textbf{each } $U \in \mathcal{U}$}{
|
||||
$\state \gets \state \textbf{ OR } DL_U.\PROVE(x)$\;\nllabel{code:prove-or}
|
||||
}
|
||||
\Return{$\state$}\;
|
||||
}
|
||||
|
||||
\vspace{1em}
|
||||
|
||||
\Fn{$\BFTREAD()$}{
|
||||
$\results \gets \emptyset$\;
|
||||
\For{\textbf{each } $U \in \mathcal{U}$}{
|
||||
$\results \gets \results \cup DL_U.\READ()$\;
|
||||
}
|
||||
\Return{$\results$}\;
|
||||
}
|
||||
\end{algorithm}
|
||||
|
||||
\paragraph{Algorithm intuition.}
|
||||
In the Byzantine setting, a process identifier $j$ is selected in $\winners[r]$ only when it accumulates at least $t+1$ proofs for round $r$ in $\validated(r)$. A process emits such a proof for $j$ only after receiving $j$'s $\texttt{PROP}$ payload (handler $\rdeliver(\texttt{PROP},\cdot)$). Therefore, if $j$ is a winner, at least one correct process has received $j$'s proposal. By RB agreement/validity, once one correct process receives that proposal for the instance, all correct processes eventually receive the same payload, so winner proposals eventually become available everywhere and can be merged consistently.
|
||||
|
||||
\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$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$. Let $A\subseteq M$ be the set of distinct issuers that invoked $\BFTAPPEND(x)$ before $op$ in $\Seq$.
|
||||
|
||||
\begin{itemize}
|
||||
\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~\ref{code:prove-or} is never becoming true, and $op$ return false.
|
||||
|
||||
\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.
|
||||
\end{itemize}
|
||||
|
||||
\smallskip
|
||||
Combining the cases yields the claimed characterization of invalidity.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[BFT-PROVE Anti-Flickering]\label{lem:bft-prove-anti-flickering}
|
||||
If the invocation of a operation $op = \BFTPROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\BFTPROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$ that is \emph{invalid} in $\Seq$.
|
||||
By BFT-PROVE Validity, this implies that there exist at least $t+1$ \emph{distinct} processes in $M$ that invoked a \emph{valid} $\BFTAPPEND(x)$ before $op$ in $\Seq$. Let $A\subseteq M$ denote that set, with $|A|\ge t+1$.
|
||||
|
||||
Fix any $U\in\mathcal{U}$. We have $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND_j(x)$ triggers a call $DL_U.\APPEND(x)$. Moreover, because $\BFTAPPEND_j(x)\prec op$ in $\Seq$, the induced $DL_U.\APPEND(x)$ appears before the induced $DL_U.\PROVE(x)$ of $op$ in the projection $\Seq_U$.
|
||||
|
||||
Hence, in $\Seq_U$, there exists a \emph{valid} $DL_U.\APPEND(x)$ that appears before the $DL_U.\PROVE(x)$ induced by $op$. By \textbf{PROVE Validity} the base $\DL$ object, the induced $DL_U.\PROVE(x)$ is therefore \emph{invalid} in $\Seq_U$.
|
||||
|
||||
Let $op'=\BFTPROVE(x)$ be any invocation such that $op\prec op'$ in $\Seq$. Fix again any $U\in\mathcal{U}$. Hence, the $DL_U.\PROVE(x)$ induced by $op'$ appears after the $DL_U.\PROVE(x)$ induced by $op$ in $\Seq_U$. Since the induced $DL_U.\PROVE(x)$ of $op$ is invalid, by \textbf{PROVE Anti-Flickering} of $\DL$, \emph{every} subsequent $DL_U.\PROVE(x)$ in $\Seq_U$ is invalid.
|
||||
|
||||
As this holds for every $U\in\mathcal{U}$, there is no component $DL_U$ in which the induced $\PROVE(x)$ of $op'$ is valid.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[BFT-READ Liveness]
|
||||
Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, x) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let $R$ the result of a $READ()$ operation submit by any correct process. $(i, x) \in R$ implie that $\exists U^\star \in \mathcal{U}$ such that $(i, x) \in R^{U^\star}$ with $R^{U^\star}$ the result of $DL_{U^\star}.\READ()$. By \textbf{READ Validity} $(i, x) \in R^{U^\star}$ implie that there exist a valid $DL_{U^\star}.\PROVE_i(x)$. The for loop in the $\BFTPROVE(x)$ implementation return true iff there at least one valid $DL_{U}.\PROVE_i(x)$ for any $U \in \mathcal{U}$.
|
||||
|
||||
Hence because there exist a $U^\star$ such that $DL_{U^\star}.\PROVE_i(x)$, there exist a valid $\BFTPROVE_i(x)$.
|
||||
|
||||
$(i, x) \in R \implies \exists \BFTPROVE_i(x)$
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[BFT-READ Anti-Flickering]\label{lem:bft-read-anti-flickering}
|
||||
Let $op_1, op_2$ two $\BFTREAD()$ operations that returns respectively $R_1, R_2$. Iff $op_1 \prec op_2$ then $R_2 \subseteq R_1$. Otherwise $R_1 \subseteq R_2$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let $R_1, R_2$ respectively the output of two $\BFTREAD()$ operations $op_1, op_2$ such that $op_1 \prec op_2$.
|
||||
By the implementation of $\BFTREAD$, $R_k = \bigcup_{U \in \mathcal{U}} R_k^U$ where $R_k^U$ is the result of $DL_U.\READ()$ during $op_k$.
|
||||
|
||||
Because $op_1 \prec op_2$ for any $U \in \mathcal{U}$, the $DL_U.\READ()$ induced by $op_1$ happen before the $DL_U.\READ()$ induced by $op_2$. Hence we have for all $U, R_2^U \subseteq R_1^U$.
|
||||
Therefore
|
||||
\[
|
||||
\bigcup_U R_2^U \subseteq \bigcup_U R_1^U \implies
|
||||
R_2 \subseteq R_1
|
||||
\]
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[BFT-READ Safety]\label{lem:bft-read-safety}
|
||||
Let $op_1, op_2$ respectively a valid $\BFTPROVE(x)$ operation submited by the process $p_i$ and a $\BFTREAD()$ operation submited by any correct process such that $op_1 \prec op_2$. Let $R$ the result of $op_2$ then $R \ni (i, x)$
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let $op_1 = \BFTPROVE_i(x)$ be a valid operation by a correct process $p_i$ and $op_2 = \BFTREAD()$ be any $\BFTREAD()$ operation such that $op_1 \prec op_2$ in $\Seq$.
|
||||
By BFT-PROVE Validity, there exist at most $t$ distinct processes in $M$ that invoked a valid $\BFTAPPEND(x)$ before $op_1$ in $\Seq$. Let $A\subseteq M$ denote that set, with $|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)$ of $op_1$. Since also $i\in \Pi_V(DL_{U^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{U^\star}.\PROVE_i(x)$ is valid.
|
||||
|
||||
Now, because $op_1 \prec op_2$ in $\Seq$, the induced $DL_{U^\star}.\PROVE_i(x)$ appears before the induced $DL_{U^\star}.\READ()$ of $op_2$ in $\Seq_{U^\star}$. By \textbf{READ Safety} of $\DL$, the result $R^{U^\star}$ of the induced $DL_{U^\star}.\READ()$ contains $(i, x)$.
|
||||
|
||||
Finally, by the implementation of $\BFTREAD()$, we have $R = \bigcup_{U \in \mathcal{U}} R^U$, so $(i, x) \in R$.
|
||||
\end{proof}
|
||||
|
||||
\begin{theorem}
|
||||
For any fixed value $t$ such that $3t < |M|$, multiple DenyList Object can be used to implement a t-Byzantine Fault Tolerant DenyList Object.
|
||||
\end{theorem}
|
||||
|
||||
\begin{proof}
|
||||
Follows directly from the previous lemmas.
|
||||
\end{proof}
|
||||
|
||||
\subsection{Algorithm}
|
||||
|
||||
\begin{algorithm}[H]
|
||||
\caption{t-BFT ARB at process $p_i$}\label{alg:bft-arb}
|
||||
|
||||
\SetKwBlock{LocalVars}{Local Variables:}{}
|
||||
\LocalVars{
|
||||
$\unordered \gets \emptyset$,
|
||||
$\ordered \gets \epsilon$,
|
||||
$\delivered \gets \epsilon$\;
|
||||
$\prop[r][j] \gets \bot, \forall j, r \in \Pi \times \mathbb{N}$\;
|
||||
$\done[r] \gets \emptyset, \forall r \in \mathbb{N}$\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\For{$r = 1, 2, \ldots$}{\nllabel{alg:main-loop}
|
||||
\textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
|
||||
$S \gets \unordered \setminus \ordered$;
|
||||
$\RBcast(\texttt{PROP}, S, \langle i, r \rangle)$\;
|
||||
|
||||
\textbf{wait until} $|\validated(r)| \geq n - t$\;\nllabel{alg:check-validated}
|
||||
|
||||
\BlankLine
|
||||
|
||||
\lForEach{$j \in \Pi$}{
|
||||
$\BFTAPPEND(\langle j, r\rangle)$\nllabel{alg:append}
|
||||
}
|
||||
|
||||
\lForEach{$j \in \Pi$}{
|
||||
$\send(\texttt{DONE}, r)$ \textbf{ to } $p_j$
|
||||
}
|
||||
|
||||
\BlankLine
|
||||
|
||||
\textbf{wait until} $|\done[r]| \geq n - t$\;\nllabel{alg:check-done}
|
||||
\textbf{wait until} $\forall j \in \winners[r],\ \prop[r][j] \neq \bot$ \textbf{ with } $\winners[r] \gets \validated(r)$\;
|
||||
|
||||
\BlankLine
|
||||
|
||||
$M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute}
|
||||
$\ordered \gets \ordered \cdot \order(M)$\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Fn{\validated($r$)}{
|
||||
\Return{$\{j: |\{k: (k, r) \in \BFTREAD()\}| \geq t+1\}$}\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\ABbroadcast(m)$}{
|
||||
$\unordered \gets \unordered \cup \{m\}$\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\rdeliver(\texttt{PROP}, S, \langle j, r \rangle)$ from process $p_j$}{
|
||||
$\unordered \gets \unordered \cup S$;
|
||||
$\prop[r][j] \gets S$\;
|
||||
$\BFTPROVE(\langle j, r\rangle)$\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\receive(\texttt{DONE}, r)$ from process $p_j$}{
|
||||
$\done[r] \gets \done[r] \cup \{j\}$\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\ABdeliver()$}{
|
||||
\lIf{$\ordered \setminus \delivered = \emptyset$}{
|
||||
\Return{$\bot$}
|
||||
}
|
||||
let $m$ be the first message in $(\ordered \setminus \delivered)$\;
|
||||
$\delivered \gets \delivered \cdot \{m\}$\;
|
||||
\Return{$m$}
|
||||
}
|
||||
|
||||
\end{algorithm}
|
||||
|
||||
\paragraph{Algorithm intuition.}
|
||||
The Byzantine-tolerant construction combines threshold evidence and RB agreement to make winner selection robust. A sender $j$ appears in $\validated(r)$ only when at least $t+1$ proofs for $\langle j,r\rangle$ are observed through $\BFTREAD()$, and by \Cref{lem:bft-prove-validity} this threshold means that $j$ cannot be certified without broad enough support from the system. Once a round is closed, the winner set becomes stable by \Cref{lem:winners-stability}, so correct processes stop diverging on who contributes to the round outcome. For each stable winner, the associated proposal payload is unique at correct receivers by \Cref{lem:bft-unique-proposal}, which prevents equivocation from creating distinct local values for the same winner identity. Consequently, when correct processes wait for all winner proposals and compute the union at line~\ref{code:Mcompute}, they obtain the same message set by \Cref{lem:message-content-invariance}. Progress is then ensured by \Cref{lem:bft-eventual-closure}, which guarantees that if new messages remain unordered, a new round eventually closes with at least $n-t$ winners. Finally, once rounds are commonly closed, appending $\order(M)$ at each round yields a common delivery sequence, exactly formalized by \Cref{lem:bft-total-order}.
|
||||
|
||||
% \textbf{Everything below has to be updated}
|
||||
|
||||
% \begin{definition}[BFT Closed round for $k$]
|
||||
% Given $Seq^{k}$ the linearization of the $\BFTDL$ $Y[k]$, a round $r \in \mathcal{R}$ is \emph{closed} in $\Seq$ iff there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND_j(r)$ appears in $\Seq^k$. Let call $\BFTAPPEND(r)^\star$ the $(n-f)^{th}$ $\BFTAPPEND(r)$.
|
||||
% \end{definition}
|
||||
|
||||
% \begin{definition}[BFT Closed round]\label{def:bft-closed-round}
|
||||
% A round $r \in \mathcal{R}$ is \emph{closed} iff for all $\DL[k]$, $r$ is closed in $\Seq^k$.
|
||||
% \end{definition}
|
||||
|
||||
% \subsection{Proof of correctness}
|
||||
|
||||
% \begin{remark}[BFT Stable round closure]\label{rem:bft-stable-round-closure}
|
||||
% If a round $r$ is closed, no more $\BFTPROVE(r)$ can be valid and thus linearized. In other words, once $\BFTAPPEND(r)^\star$ is linearized, no more process can make a proof on round $r$, and the set of valid proofs for round $r$ is fixed. Therefore $\Winners_r$ is fixed.
|
||||
% \end{remark}
|
||||
|
||||
% \begin{proof}
|
||||
% By definition $r$ closed means that for all process $p_i$, there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND_j(r)$ appears in $\Seq^k$. By BFT-PROVE Validity, any subsequent $\BFTPROVE(r)$ is invalid because at least $n - f$ processes already invoked a valid $\BFTAPPEND(r)$ before it. Thus no new valid $\BFTPROVE(r)$ can be linearized after $\BFTAPPEND(r)^\star$. Hence the set of valid proofs for round $r$ is fixed, and so is $\Winners_r$.
|
||||
% \end{proof}
|
||||
|
||||
% \begin{lemma}[BFT Across rounds]\label{lem:bft-across-rounds}
|
||||
% For any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{proof}
|
||||
% Let $r \in \mathcal{R}$. By \cref{def:bft-closed-round}, if $r + 1$ is closed, then for all $\DL[k]$, $r + 1$ is closed in $\Seq^k$. By the implementation, a process can only invoke $\BFTAPPEND(r + 1)$ after observing at least $n - f$ valid $\BFTPROVE(r)$, which means that for all $\DL[k]$, $r$ is closed in $\Seq^k$. Hence by \cref{def:bft-closed-round}, $r$ is closed.
|
||||
|
||||
% Because $r$ is monotonically increasing, we can reccursively apply the same argument to conclude that for any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
|
||||
% \end{proof}
|
||||
|
||||
% \begin{lemma}[BFT Progress]\label{lem:bft_progress}
|
||||
% For any correct process $p_i$ such that
|
||||
% \[
|
||||
% \received \setminus (\delivered \cup (\cup_{r' < r} \cup_{j \in W[r'] \prop[r'][j]})) \neq \emptyset
|
||||
% \]
|
||||
% with $r$ the highest closed round in the $\DL$ linearization. Eventually $r+1$ will be closed.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{lemma}[BFT Winners invariant]\label{lem:bft-winners-invariant}
|
||||
% For any closed round $r$, define
|
||||
% \[
|
||||
% \Winners_r = \{j: \BFTPROVE_j(r) \prec \BFTAPPEND^\star(r)\}
|
||||
% \]
|
||||
% called the unique set of winners of round $r$.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{lemma}[BFT n-f lower-bounded Winners]
|
||||
% Let $r$ a closed round, $|W[r]| \geq n-f$.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{remark}\label{rem:correct-in-winners}
|
||||
% Because we assume $n \geq 2f+ 1$, if $|W[r]| \geq n-f$ at least 1 correct have to be in $W[r]$ to progress.
|
||||
% \end{remark}
|
||||
|
||||
% \begin{lemma}[BFT Winners must purpose]\label{lem:bft-winners-purpose}
|
||||
% Let $r$ a closed round, for all process $p_j$ such that $j \in W[r]$, $p_j$ must have executed $\RBcast(j, PROP, \_, r)$ and hence any correct will eventually set $\prop[r][j]$ to a non-$\bot$ value.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{lemma}[BFT Messages Incariant]\label{lem:bft-messages-invariant}
|
||||
% For any closed round $r$ and any correct process $p_i$ such that $\forall j \in \Winners_r$: $\prop^{(i)}[r][j] \neq \bot$ define
|
||||
% \[
|
||||
% \Messages_r = \cup_{j \in \Winners_r} prop^{(i)}[r][j]
|
||||
% \]
|
||||
% as the set of messages proposed by the winners of round $r$
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{lemma}[BFT EVentual proposal closure]\label{lem:bft-eventual-proposal-closure}
|
||||
% 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}
|
||||
|
||||
% \begin{lemma}[BFT Unique proposal per sender per round]\label{lem:bft-unique-proposal}
|
||||
% For any round $r$ and any process $p_i$, if $p_i$ invokes two $\RBcast$ call for the same round, such that $\RBcast(i, PROP, S, r) \prec \RBcast(i, PROP, S', r)$. Then for any correct process $p_j$, $\prop^{(j)}[r][i] \in \{\bot, S\}$
|
||||
% \end{lemma}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
% \begin{lemma}[BFT $W_r$ as grow only set]\label{lem:bft-wr-grow-only}
|
||||
% For any correct process $p_i$. If $p_i$ computes $W_r$ at two different times $t_1$ and $t_2$ with $t_1 < t_2$, then $W_r^{t_1} \subseteq W_r^{t_2}$.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{proof}
|
||||
% By the implementation, $W_r$ is computed exclusively from the results of $\{j: (j, \PROVEtrace(r)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$.
|
||||
|
||||
% We know by BFT-READ Anti-Flickering that for any two $\BFTREAD()$ operations $op_1, op_2$ such that $op_1 \prec op_2$, the result of $op_2$ is included in the result of $op_1$. Therefore, if $p_i$ computes $W_r$ at two different times $t_1$ and $t_2$ with $t_1 < t_2$, then $W_r^{t_1} \subseteq W_r^{t_2}$.
|
||||
% \end{proof}
|
||||
|
||||
% \begin{lemma}[BFT well defined winners]\label{lem:bft-well-defined-winners}
|
||||
% For any closed round $r$, if a correct process $p_i$ compute $W_r$, then $W_r = \Winners_r$ with $|W_r| \geq n - f$.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{proof}
|
||||
% By \Cref{lem:bft-read-safety}, any correct process $p_i$ computing $W_r$ after round $r$ is closed includes all valid $\BFTPROVE(r)$ in its computation of $W_r$. Therefore $W_r = \Winners_r$.
|
||||
|
||||
% By \Cref{def:bft-closed-round}, at least $n - f$ distinct processes invoked a valid $\BFTAPPEND(r)$ before $\BFTAPPEND(r)^\star$. By the implementation in algorithm D, if a process correct $j$ invoked a valid $\BFTAPPEND(r)$, thats means that he observed at least $n - f$ valid $\BFTPROVE(r)$ submitted by distinct processes. By \Cref{lem:bft-wr-grow-only}, once $p_j$ observed $n - f$ valid $\BFTPROVE(r)$, any correct process computing $W_r$ will eventually observe at least these $n - f$ valid $\BFTPROVE(r)$. By \Cref{lem:bft-stable-round-closure}, no more valid $\BFTPROVE(r)$ can be linearized after round $r$ is closed, so any correct process computing the same fixed set $W_r$ of at least $n - f$ distinct processes.
|
||||
% \end{proof}
|
||||
|
||||
% \begin{lemma}[BFT Non-empty winners proposal]\label{lem:bft-non-empty-winners-proposal}
|
||||
% For every process $p_i$ such as $i \in W_r$, eventually $\prop[r][i] \neq \bot$.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{proof}
|
||||
% By the implementation, if $i \in W_r$, then $(i, \PROVEtrace(r))$ is included in the result of at least one $\BFTREAD()$ operation. Hence there exist a valid $\BFTPROVE(r)$ operation.
|
||||
% By \Cref{lem:bft-prove-validity}, this implies that there exist at least $f + 1$ valid $\PROVE(r)$ operation invoked by processes. At least one of these processes is correct, say $p_j$. By the implementation, $p_j$ invoked $\BFTPROVE(r)$ after receiving a $Rdeliver(j, \texttt{PROP}, S, r)$ message from $p_i$. Therefore, by the reliable broadcast properties, the message will eventually be delivered to every correct process, hence eventually for any correct process $\prop[r][i] \neq \bot$.
|
||||
% \end{proof}
|
||||
|
||||
% \begin{definition}[BFT Message invariant]\label{def:bft-message-invariant}
|
||||
% For any closed round $r$, for any correct process $p_i$, such that $\nexists j \in W_r : \prop[r][j] = \bot$, twe define the set
|
||||
% \[
|
||||
% \Messages_r = \bigcup_{j \in \Winners_r} \prop[r][j]
|
||||
% \]
|
||||
% as the unique set of messages proposed during round $r$.
|
||||
% \end{definition}
|
||||
|
||||
% \begin{lemma}[BFT Proposal convergence]\label{lem:bft-proposal-convergence}
|
||||
% For any closed round $r$, for any correct process $p_i$, that define $M_r$ at line B10, we have $M_r = \Messages_r$.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{proof}
|
||||
% By \Cref{lem:bft-well-defined-winners}, any correct process $p_i$ computing $W_r$ after round $r$ is closed has $W_r = \Winners_r$.
|
||||
% By \Cref{lem:bft-non-empty-winners-proposal}, for any correct process $p_i$, such as $i \in W_r$, eventually $\prop[r][i] \neq \bot$.
|
||||
|
||||
% Therefore, eventually for any correct process $p_i$, at line B10 we have
|
||||
% \[
|
||||
% M_r = \bigcup_{j \in W_r} \prop[r][j] = \bigcup_{j \in \Winners_r} \prop[r][j] = \Messages_r
|
||||
% \]
|
||||
% \end{proof}
|
||||
|
||||
% \begin{lemma}[BFT Inclusion]\label{proof:bft-inclusion}
|
||||
% If a correct process $p_i$ ABroadcasts a message $m$, then eventually any correct process $p_j$ ADelivers $m$.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{proof}
|
||||
% Let $m$ be a message ABroadcast by a correct process $p_i$ and eventually exit the \texttt{ABroadcast} function at line A10.
|
||||
|
||||
% By the implementation, if $p_i$ exits the \texttt{ABroadcast} function at line A10, then there exists a round $r'$ such that $m \in \prop[r'][j]$ for some $j \in W_{r'}$.
|
||||
|
||||
% Since $p_i$ is correct, seeing that $m \in \prop[r'][j]$ for some $j \in W_{r'}$ implies that $p_i$ received a $Rdeliver(j, \texttt{PROP}, S, r')$ message from $p_j$ such that $m \in S$. And because $p_j$ is in $W_{r'}$, at least $n - f$ correct processes invoked a valid $Y[j].\BFTPROVE(r')$ before the round $r'$ were closed. By the reliable broadcast properties, the $Rdeliver(j, \texttt{PROP}, S, r')$ message will eventually be delivered to every correct process, hence eventually for any correct process $m \in \prop[r'][j]$ with $j \in W_{r'}$. Hence $m$ will eventually be included in the set $\Messages_{r'}$ defined in \Cref{def:bft-message-invariant} and thus eventually be ADelivered by any correct process.
|
||||
% \end{proof}
|
||||
|
||||
\subsection{Correctness Lemmas}
|
||||
|
||||
\begin{definition}[Closed Round]
|
||||
A round $r \in \mathcal{R}$ is said to be \emph{closed} for a correct process $p_i$ if at the moment $p_i$ computes $\winners[r]$, it satisfies $|\{k : (k, r) \in \BFTREAD()\}| \geq n - t$.
|
||||
\end{definition}
|
||||
|
||||
\begin{lemma}[Round Monotonicity]\label{lem:round-monotonicity}
|
||||
If a round $r$ is closed, then every round $r_1 < r$ is also closed.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
\textbf{Base:} $r = 0$. Suppose round $1$ is closed, the set $\{r' \in \mathcal{R}: r' < r\}$ is empty, so the claim holds.
|
||||
|
||||
\textbf{Inductive step:} Let $r \geq 1$. Assume that the property holds for all rounds $r' < r$: whenever round $r'$ is closed, all rounds $r_2 < r'$ are also closed. We show that if round $r$ is closed, then all rounds $r_1 < r$ are closed.
|
||||
|
||||
Suppose round $r$ is closed. This means at least one correct process $p_i$ has reached line \ref{alg:check-validated} and satisfied the condition $|\validated(r)| \geq n - t$. Consequently, $p_i$ has invoked $\BFTAPPEND(\langle j, r \rangle)$ for each $j \in \Pi$ at line \ref{alg:append}. Since these operations are invoked by a correct process, and they depend on valid proofs in the byzantine fault tolerant deny list, at least one of these operations must have succeeded in the DL object.
|
||||
|
||||
Moreover, by the algorithm structure, a correct process can only reach the beginning of round $r$ after completing round $r-1$. In particular, process $p_i$ reaches line \ref{alg:main-loop} for round $r$ only after having completed round $r-1$, which requires the process to have observed at least $|\done[r-1]| \geq n - t$ (line \ref{alg:check-done} for round $r-1$). This condition can only be satisfied if round $r-1$ is closed: at least $n - t$ processes must have issued DONE messages, and since $n > 3f$, at least one of these is correct.
|
||||
|
||||
Since $n - t > 2f + 1$, among the $n - t$ processes satisfying the condition for round $r-1$, at least one is correct. A correct process that issued a DONE message for round $r-1$ must have previously completed its execution of lines \ref{alg:append} for round $r-1$, which in turn required observing $|\validated(r-1)| \geq n - t$ from line \ref{alg:check-validated}. Thus, round $r-1$ is closed.
|
||||
|
||||
Now, considering any round $r_1 < r-1$: by the inductive hypothesis applied to round $r-1$, since round $r-1$ is closed and $r_1 < r-1$, we have that $r_1$ is also closed.
|
||||
|
||||
By strong induction, if round $r$ is closed, all rounds $r_1 < r$ are closed.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Uniqueness of Winners' Proposals]\label{lem:bft-unique-proposal}
|
||||
For any closed round $r$ and any process $p_j \in \winners[r]$, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process $p_i$ that has received a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly this set $S_j$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let $r$ be a closed round and $p_j \in \winners[r]$. Since $j \in \winners[r]$, it means that $(j, r) \in \BFTREAD()$, i.e., at least $t+1$ distinct processes have invoked a valid $\BFTPROVE(\langle j, r \rangle)$ before the round $r$ closed.
|
||||
|
||||
By the algorithm, a correct process $p_i$ invokes $\BFTPROVE(\langle j, r \rangle)$ only upon receiving a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ at line \ref{alg:append}. Let $S_j^{(i)}$ denote the set received by $p_i$.
|
||||
|
||||
Since at least $t+1$ distinct processes have performed a valid $\BFTPROVE(\langle j, r \rangle)$, and since $t < n/3$, at least one of these processes is correct. Thus, at least one correct process must have received a reliable broadcast from $p_j$ for round $r$.
|
||||
|
||||
Now, by Bracha's Byzantine Reliable Broadcast specification, for any message broadcast instance by process $p_j$ in round $r$, all correct processes that deliver this broadcast either receive the identical message or none at all. Formally, for all correct processes $p_i, p_i'$ that received a delivery from $p_j$ for round $r$, we have $S_j^{(i)} = S_j^{(i')}$.
|
||||
|
||||
Therefore, there exists a unique set $S_j$ such that every correct process $p_i$ that receives a reliable delivery from $p_j$ for round $r$ receives exactly $S_j$.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Winners Stability]\label{lem:winners-stability}
|
||||
For any closed round $r$, the set $\winners[r]$ is stable.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let $r$ be a closed round. By definition, a closed round $r$ means that at least one correct process $p_i$ has observed $|\{k : (k, r) \in \BFTREAD()\}| \geq n - t$ and computed $\winners[r]$ at line \ref{alg:check-done}.
|
||||
|
||||
When round $r$ becomes closed, this implies that at least $n - t$ distinct processes have invoked $\BFTAPPEND(\langle j, r \rangle)$ for $j \in \Pi$ (by the algorithm structure, since $\done[r]$ contains DONE messages from processes that completed line \ref{alg:append}). Since $n > 3f$, we have $n - t > 2f + 1 > t + 1$.
|
||||
|
||||
Consider a fixed $j \in \Pi$. Since at least $n - t > t + 1$ processes have invoked a valid $\BFTAPPEND(\langle j, r \rangle)$, by \cref{lem:bft-prove-validity}, any subsequent invocation of $\BFTPROVE(\langle j, r \rangle)$ will be invalid.
|
||||
|
||||
By \cref{lem:bft-prove-anti-flickering}, once a $\BFTPROVE(\langle j, r \rangle)$ operation becomes invalid, all subsequent $\BFTPROVE(\langle j, r \rangle)$ operations are also invalid.
|
||||
|
||||
This holds for all $j \in \Pi$. Therefore, after the round $r$ is closed, the set of valid $\BFTPROVE(\langle j, r \rangle)$ operations for each $j$ cannot grow. By \cref{lem:bft-read-anti-flickering}, any subsequent $\BFTREAD()$ invocation will not return any new $(k, r)$ pairs beyond those already returned. Thus, $\winners[r] = \{j : (j, r) \in \BFTREAD()\}$ becomes stable and cannot change.
|
||||
|
||||
Since this reasoning applies to all correct processes that compute $\winners[r]$ after round $r$ is closed, all correct processes will compute the same stable set $\winners[r]$.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Message Content Invariance]\label{lem:message-content-invariance}
|
||||
For any closed round $r$ and any correct process $p_i$, the set $M$ computed at line \ref{code:Mcompute} by $p_i$ is identical to the set computed by any other correct process $p_j$ for the same round $r$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let $r$ be a closed round and let $p_i, p_{i'}$ be two correct processes. By the algorithm, both processes compute $M$ as:
|
||||
\[
|
||||
M^{(i)} = \bigcup_{j \in \winners[r]} \prop^{(i)}[r][j]
|
||||
\]
|
||||
and
|
||||
\[
|
||||
M^{(i')} = \bigcup_{j \in \winners[r]} \prop^{(i')}[r][j]
|
||||
\]
|
||||
at line \ref{code:Mcompute}.
|
||||
|
||||
By \cref{lem:winners-stability}, the set $\winners[r]$ is stable once round $r$ is closed. Therefore, both $p_i$ and $p_{i'}$ compute the same set of winners $\winners[r]$.
|
||||
|
||||
Now, consider any winner $j \in \winners[r]$. By \cref{lem:bft-unique-proposal}, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process that receives a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly $S_j$.
|
||||
|
||||
By the algorithm, each correct process stores this received set in its local variable: $\prop^{(i)}[r][j] = S_j$ and $\prop^{(i')}[r][j] = S_j$.
|
||||
|
||||
Since both processes compute the union over the same set of winners, and each winner's proposal is identical for all correct processes:
|
||||
\[
|
||||
M^{(i)} = \bigcup_{j \in \winners[r]} \prop^{(i)}[r][j] = \bigcup_{j \in \winners[r]} S_j = \bigcup_{j \in \winners[r]} \prop^{(i')}[r][j] = M^{(i')}
|
||||
\]
|
||||
|
||||
Therefore, all correct processes compute the same set $M$ for any closed round $r$.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Inclusion]\label{lem:bft-inclusion}
|
||||
If a correct process $p_i$ invokes $\ABbroadcast(m)$, then there exist a closed round $r$ and a winner $j \in \winners[r]$ such that $p_j$ invoked $\RBcast(j, \texttt{PROP}, S, r)$ with $m \in S$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let $p_i$ be a correct process that invokes $\ABbroadcast(m)$. By the algorithm, $p_i$ adds $m$ to $\unordered$. Consequently, $\unordered \setminus \ordered \neq \emptyset$, and the process enters the main loop and eventually invokes $\RBcast(i, \texttt{PROP}, S_i^{(1)}, r_1)$ for some round $r_1$ where $m \in S_i^{(1)}$.
|
||||
|
||||
We distinguish two cases:
|
||||
|
||||
\textbf{Case 1: $p_i$ becomes a winner in round $r_1$.}
|
||||
If $p_i$ is elected as a winner for round $r_1$ (i.e., $i \in \winners[r_1]$), then the claim holds with $r = r_1$ and $j = i$.
|
||||
|
||||
\textbf{Case 2: $p_i$ does not become a winner in round $r_1$.}
|
||||
If $p_i$ is not elected as a winner, by the properties of Reliable Broadcast (Bracha's specification), at least one correct process $p_{i_1}$ will eventually receive the reliable delivery of the $\texttt{PROP}$ message from $p_i$ for round $r_1$. Process $p_{i_1}$ adds all messages from $S_i^{(1)}$ to its $\unordered$ set at line \ref{alg:append}. In particular, $m$ is now in $p_{i_1}$'s $\unordered$ set.
|
||||
|
||||
In round $r_2 > r_1$ (and any subsequent round), process $p_{i_1}$ computes $S_{i_1}^{(2)} = \unordered \setminus \ordered$ and invokes $\RBcast(i_1, \texttt{PROP}, S_{i_1}^{(2)}, r_2)$ with $m \in S_{i_1}^{(2)}$.
|
||||
|
||||
This process repeats: either $p_{i_1}$ becomes a winner and the claim holds, or another correct process receives $p_{i_1}$'s proposal and includes $m$ in its own proposal.
|
||||
|
||||
Since $n > 3f$, we have $n - t > t + 1 > f$. By the pigeonhole principle, there eventually exists a round $r$ where at least $n - t$ distinct processes have proposed sets containing $m$. Since more than $2f$ processes have proposed $m$, at least one of them must be correct and be elected as a winner. Therefore, there exist a round $r$ and a winner $j \in \winners[r]$ such that $m \in S_j$ was broadcast by $p_j$.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Eventual Closure]\label{lem:bft-eventual-closure}
|
||||
For any correct process $p_i$, if $\unordered \setminus \ordered \neq \emptyset$ and if $r$ is the highest closed round observed by $p_i$, then eventually round $r+1$ will be closed with $|\winners[r+1]| \geq n - t$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let $p_i$ be a correct process such that $\unordered \setminus \ordered \neq \emptyset$ after round $r$ is the highest closed round it observed. By the main loop of Algorithm~\ref{alg:bft-arb}, $p_i$ eventually enters round $r+1$, computes $S=\unordered\setminus\ordered$, and invokes $\RBcast(\texttt{PROP},S,\langle i,r+1\rangle)$.
|
||||
|
||||
By RB Validity, every correct process eventually $\rdeliver(\texttt{PROP},S,\langle i,r+1\rangle)$. Upon this delivery, each correct process executes $\BFTPROVE(\langle i,r+1\rangle)$. Hence at least $n-t$ correct processes issue a proof for candidate $i$ in round $r+1$, and in particular the threshold $t+1$ used in $\validated(r+1)$ is eventually met for that candidate.
|
||||
|
||||
The same argument applies to each correct process that broadcasts in round $r+1$: once its proposal is RB-delivered, at least $n-t$ correct processes issue the corresponding proofs, so that sender is eventually included in $\validated(r+1)$. Since there are at least $n-t$ correct processes, eventually $|\validated(r+1)| \geq n-t$, and the wait at line~\ref{alg:check-validated} is eventually released for every correct process in that round.
|
||||
|
||||
After this point, each correct process executes the $\BFTAPPEND$ loop (line~\ref{alg:append}) and sends $\texttt{DONE}$ to all processes. By reliability of point-to-point channels, every correct process eventually receives at least $n-t$ DONE messages, so the wait at line~\ref{alg:check-done} is also eventually released. At that moment, the process computes $\winners[r+1] \gets \validated(r+1)$, and by the previous bound we have $|\winners[r+1]| \geq n-t$.
|
||||
|
||||
Therefore round $r+1$ eventually becomes closed with at least $n-t$ winners.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Total Order]\label{lem:bft-total-order}
|
||||
For any two correct processes $p_i$ and $p_j$, the sequence $\ordered$ maintained locally by $p_i$ and the sequence maintained by $p_j$ contain the same messages in the same order, provided that both have reached the same set of closed rounds.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
We prove the claim by induction on the number of closed rounds completed by both processes.
|
||||
|
||||
\textbf{Base case.} Before any closed round is completed, both local sequences are initialized to $\epsilon$, hence identical.
|
||||
|
||||
\textbf{Induction step.} Assume that after all closed rounds up to $r-1$, processes $p_i$ and $p_j$ have identical $\ordered$ prefixes. Consider round $r$.
|
||||
|
||||
By \Cref{lem:winners-stability}, once round $r$ is closed, both processes use the same stable winner set $\winners[r]$. By \Cref{lem:message-content-invariance}, the set $M$ computed at line~\ref{code:Mcompute} is identical at all correct processes for that round. Both processes then apply the same deterministic ordering function $\order(M)$ and append that same ordered block to their current sequence.
|
||||
|
||||
Since they started round $r$ from identical prefixes and append the same ordered suffix for round $r$, their resulting sequences after round $r$ are identical. The induction concludes that for any common set of closed rounds, both correct processes maintain the same messages in the same order.
|
||||
\end{proof}
|
||||
|
||||
\begin{theorem}
|
||||
The algorithm implements a BFT Atomic Reliable Broadcast.
|
||||
\end{theorem}
|
||||
@@ -1,280 +0,0 @@
|
||||
|
||||
\subsection{Model extension}
|
||||
We consider a static set of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable.
|
||||
|
||||
\paragraph{Synchrony.} The network is asynchronous. Processes may crash or be byzantine; at most $f = \frac{n}{2} - 1$ processes can be faulty.
|
||||
|
||||
\paragraph{Communication.} Processes can exchange through a Reliable Broadcast (\RB) primitive (defined below) which's invoked with the functions \RBcast$(m)$ and \RBreceived$(m)$. There exists a shared object called DenyList (\DL) (defined below) that is interfaced with the functions \APPEND$(x)$, \PROVE$(x)$ and \READ$()$.
|
||||
|
||||
\paragraph{Byzantine behaviour}
|
||||
A process exhibits Byzantine behavior if it deviates arbitrarily from the specified algorithm. This includes, but is not limited to, the following actions:
|
||||
|
||||
\begin{itemize}
|
||||
\item Invoking primitives (\RBcast, \APPEND, \PROVE, etc.) with invalid or maliciously crafted inputs.
|
||||
\item Colluding with other Byzantine processes to manipulate the system's state or violate its guarantees.
|
||||
\item Delaying or accelerating message delivery to specific nodes to disrupt the expected timing of operations.
|
||||
\item Withholding messages or responses to create inconsistencies in the system's state.
|
||||
\end{itemize}
|
||||
|
||||
Byzantine processes are constrained by the following:
|
||||
\begin{itemize}
|
||||
\item They cannot forge valid cryptographic signatures or threshold shares without the corresponding private keys.
|
||||
\item They cannot violate the termination, validity, or anti-flickering properties of the \DL{} object.
|
||||
\item They cannot break the integrity, no-duplicates, or validity properties of the \RB{} primitive.
|
||||
\end{itemize}
|
||||
|
||||
\paragraph{Notation.} Let $\Pi$ be the finite set of process identifiers and let $n \triangleq |\Pi|$. Two authorization subsets are $M \subseteq \Pi$ (processes allowed to issue \APPEND) and $V \subseteq \Pi$ (processes allowed to issue \PROVE). Indices $i,j \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec$ for the \DL{} linearization: $x \prec y$ means that operation $x$ appears strictly before $y$ in the linearized history of \DL. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes). For any round $r \in \mathcal{R}$, define $\Winners_r \triangleq \{\, j \in \Pi \mid (j,\PROVEtrace(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization.
|
||||
We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$.
|
||||
|
||||
% ------------------------------------------------------------------------------
|
||||
\subsection{Primitives}
|
||||
|
||||
\subsubsection{t-BFT-DL}
|
||||
|
||||
We consider a t-Byzantine Fault Tolerant DenyList (t-$\BFTDL$) with the following properties.
|
||||
There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that :
|
||||
|
||||
\paragraph{Termination.} Every operation $\BFTAPPEND(x)$, $\BFTPROVE(x)$, and $\BFTREAD()$ invoked by a correct process always returns.
|
||||
|
||||
% \paragraph{APPEND Validity.} The invocation of $\BFTAPPEND(x)$ by a correct process $p_i$ is valid iff $i \in \Pi_M$. Otherwise the operation is invalid.
|
||||
|
||||
\paragraph{PROVE Validity.} The invocation of $op = \BFTPROVE(x)$ by a correct process is valid iff there exist a set of correct process $C$ such that $\forall c \in C$, $c$ invoke $op_2 = \BFTAPPEND(x)$ with $op_2 \prec op_1$ and $|C| \leq t$
|
||||
|
||||
\paragraph{PROVE Anti-Flickering.} If the invocation of a operation $op = \BFTPROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\BFTPROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
|
||||
|
||||
\paragraph{READ Validity.} The invocation of $op = \BFTREAD()$ by a process $p$ returns the list of valid invocations of $\BFTPROVE$ that appears before $op$ in $\Seq$ along with the names of the processes that invoked each operation.
|
||||
|
||||
\paragraph{Local consistency.} For all correct process $p_i$ such that $p_i$ invoke an valid $\BFTPROVE(x)$ before a $P \gets \BFTREAD()$ operation in his local execution. Then the set of valid $\BFTPROVE(x)$ in $P$ must contain the previous valid $\BFTPROVE(x)$.
|
||||
|
||||
\paragraph{Liveness} For all correct process $p_i$ such that $p_i$ invoke an invalid $\BFTPROVE(x)$ before a $P \gets \BFTREAD()$ operation in his local execution. Then the set of valid $\BFTPROVE(x)$ in $P$ must be the same for any $p_i$.
|
||||
|
||||
% \subsubsection{t-BFT-GE}
|
||||
|
||||
% We consider a t-Byzantine Fault Tolerant Group Election Object (t-$\BFTGE[r]$) per round $r \in \mathcal{R}$ with the following properties.
|
||||
|
||||
% There are three operations: $\BFTVOTE(j, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$.
|
||||
|
||||
% \paragraph{Termination.} Every operation $\BFTVOTE(i, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$ invoked by a correct process always returns.
|
||||
|
||||
% \paragraph{Stability.} If there exist at least $n-f$ invocations of $\BFTCOMMIT(r)$ by distincts processes and let call $\BFTCOMMIT(r)^\star$ the $(n-f)^{th}$ such invocation in the linearization of $\Seq$. Then any invocation of $\BFTRESULT(r)$ that appears after $\BFTCOMMIT(r)^\star$ in $\Seq$ returns the same set of processes $W_r$.
|
||||
|
||||
% \paragraph{VOTE-Validity.} The invocation of $\BFTVOTE(j, r)$ by a correct process is not valid if $\BFTCOMMIT(r)^\star$ appears before in $\Seq$. Otherwise, the operation is valid.
|
||||
|
||||
% \paragraph{Election.} If at least $f+1$ correct processes invoked a valid $\BFTVOTE(j, r)$ for the same process $j$ then $j$ will be enventually included in the set $W_r$ returned by $\BFTRESULT(r)$.
|
||||
|
||||
\subsection{DL $\Rightarrow$ t-BFT-DL}
|
||||
|
||||
\begin{lemma}
|
||||
For any fixed value $t$ such that $3t < |M|$, multiple DenyList Object can be used to implement a t-Byzantine Fault Tolerant DenyList Object.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Fix $3t < |M|$. Let
|
||||
\[
|
||||
\mathcal{U} = \{\, U \subseteq M \mid |U| = |M| - t \,\}.
|
||||
\]
|
||||
For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose authorization sets are
|
||||
\[
|
||||
\Pi_M(DL_T) = S_T = U
|
||||
\qquad\text{and}\qquad
|
||||
\Pi_V(DL_T) = V.
|
||||
\]
|
||||
Let
|
||||
\[
|
||||
K = \{\, DL_U \mid U \in \mathcal{U} \,\},
|
||||
\qquad\text{so that}\qquad
|
||||
|U| = \binom{|M|}{|M| - t}.
|
||||
\]
|
||||
|
||||
\begin{algorithmic}[1]
|
||||
% \State $K \gets \{DL_T : T \subseteq M, |T|=t\}$
|
||||
|
||||
\renewcommand{\algletter}{DL}
|
||||
\begin{algorithm}[H]
|
||||
\caption{\BFTAPPEND}
|
||||
\Function{$\BFTAPPEND$}{x}
|
||||
\For{\textbf{each } $DL_U \in K$ such that $p_i \in U$}
|
||||
\State $DL_U.\APPEND(x)$
|
||||
\EndFor
|
||||
\EndFunction
|
||||
\end{algorithm}
|
||||
|
||||
% \renewcommand{\algletter}{B}
|
||||
\begin{algorithm}[H]
|
||||
\caption{\BFTPROVE}
|
||||
\Function{$\BFTPROVE$}{x}
|
||||
\State $state \gets false$
|
||||
\For{\textbf{each } $DL_U \in K$}
|
||||
\State $state \gets state \textbf{ OR } DL_U.\PROVE(x)$
|
||||
\EndFor
|
||||
\State \Return $state$
|
||||
\EndFunction
|
||||
\end{algorithm}
|
||||
|
||||
% \renewcommand{\algletter}{C}
|
||||
\begin{algorithm}[H]
|
||||
\caption{\BFTREAD}
|
||||
\Function{$\BFTREAD$}{$\bot$}
|
||||
\State $results \gets \emptyset$
|
||||
\For{\textbf{each } $DL_U \in K$}
|
||||
\State $results \gets results \cup DL_U.\READ()$
|
||||
\EndFor
|
||||
\State \Return $results$
|
||||
\EndFunction
|
||||
\end{algorithm}
|
||||
\end{algorithmic}
|
||||
|
||||
% \paragraph{BFT-APPEND Validity.} Let $A\subseteq M$ be the set of distinct issuers that invoked a valid $\BFTAPPEND(x)$ Suppose by contradiction that there exists $T\in\mathcal{T}$ with $A\cap S_T=\emptyset$. Since $S_T=M\setminus T$, this implies $A\subseteq T$, hence $|A|\le |T|=t$, contradicting $|A|\ge t+1$.
|
||||
|
||||
\paragraph{BFT-PROVE Validity.} Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$. Let $A\subseteq M$ be the set of distinct issuers that invoked a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$.
|
||||
|
||||
\begin{itemize}
|
||||
% \item \textbf{Case (i): $i\notin V$.}
|
||||
% For every $T\in\mathcal{T}$, we configured $\Pi_V(DL_T)=V$, hence the induced operation $DL_T.\PROVE(x)$ is invalid by \textbf{PROVE Validity} of $\DL$. Therefore $op$ is invalid.
|
||||
|
||||
\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 \textbf{PROVE Validity} of $\DL$, the induced $DL_U.\PROVE(x)$ is invalid. As this holds for every $T\in\mathcal{T}$, there is \emph{no} component $DL_U$ where $\PROVE(x)$ is valid, so $op$ is invalid.
|
||||
|
||||
\item \textbf{Case (ii): $|A|\le t$.}
|
||||
Fix any $U\in\mathcal{U}$, 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 V=\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 by the lifting convention $op$ is valid.
|
||||
\end{itemize}
|
||||
|
||||
\smallskip
|
||||
Combining the cases yields the claimed characterization of invalidity.
|
||||
|
||||
\paragraph{BFT-PROVE Anti-Flickering.} Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i\in V$ that is \emph{invalid} in $\Seq$.
|
||||
By BFT-PROVE Validity, this implies that there exist at least $t+1$ \emph{distinct} processes in $M$ that invoked a \emph{valid} $\BFTAPPEND(x)$ before $op$ in $\Seq$. Let $A\subseteq M$ denote that set, with $|A|\ge t+1$.
|
||||
|
||||
Fix any $U\in\mathcal{U}$. We have $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND^{(j)}(x)$ triggers a call $DL_U.\APPEND(x)$. Moreover, because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, the induced $DL_U.\APPEND(x)$ appears before the induced $DL_U.\PROVE(x)$ of $op$ in the projection $\Seq_U$.
|
||||
|
||||
Hence, in $\Seq_U$, there exists a \emph{valid} $DL_U.\APPEND(x)$ that appears before the $DL_U.\PROVE(x)$ induced by $op$. By \textbf{PROVE Validity} the base $\DL$ object, the induced $DL_U.\PROVE(x)$ is therefore \emph{invalid} in $\Seq_U$.
|
||||
|
||||
Now let $op'=\BFTPROVE(x)$ be any invocation such that $op\prec op'$ in $\Seq$. Fix again any $U\in\mathcal{U}$. Hence, the $DL_U.\PROVE(x)$ induced by $op'$ appears after the $DL_U.\PROVE(x)$ induced by $op$ in $\Seq_U$. Since the induced $DL_U.\PROVE(x)$ of $op$ is invalid, by \textbf{PROVE Anti-Flickering} of $\DL$, \emph{every} subsequent $DL_U.\PROVE(x)$ in $\Seq_U$ is invalid.
|
||||
|
||||
As this holds for every $U\in\mathcal{U}$, there is no component $DL_U$ in which the induced $\PROVE(x)$ of $op'$ is valid.
|
||||
|
||||
|
||||
\paragraph{Local consistency.}
|
||||
|
||||
\paragraph{Liveness.}
|
||||
|
||||
\end{proof}
|
||||
|
||||
|
||||
\subsection{t-BFT-DL $\Rightarrow$ t-BFT-GE}
|
||||
|
||||
\begin{lemma}
|
||||
For any fixed value $r \in S$, multiple BFT-DenyList Object can be used to implement a BFT-Group Election Object.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
\begin{algorithmic}
|
||||
\State $Y[i]$ \Comment{Is a set of $n$ $\BFTDL$ with $\Pi_M = \Pi_V = \Pi$}
|
||||
|
||||
\vspace{1em}
|
||||
|
||||
\Function{BFTVOTE}{j, r}
|
||||
|
||||
\EndFunction
|
||||
\vspace{1em}
|
||||
|
||||
\Function{BFTCOMMIT}{r}
|
||||
\EndFunction
|
||||
\vspace{1em}
|
||||
\Function{BFTRESULT}{r}
|
||||
\State $Z \gets \emptyset$
|
||||
\For{\textbf{each } $j \in \Pi$}
|
||||
\If{$|\{(\_, \PROVEtrace(\_, r)) \in Y[j].\BFTREAD(r)\}| \geq n-f$}
|
||||
\State $P \gets \BFTREAD()$
|
||||
\State \Return $\{j : (j, \PROVEtrace), \}$
|
||||
\EndIf
|
||||
\EndFor
|
||||
\EndFunction
|
||||
\vspace{1em}
|
||||
\end{algorithmic}
|
||||
\end{proof}
|
||||
|
||||
\subsection{Algorithm}
|
||||
|
||||
\subsubsection{Variables}
|
||||
Each process $p_i$ maintains the following local variables:
|
||||
\begin{algorithmic}
|
||||
\State $\current \gets 0$
|
||||
\State $\received \gets \emptyset$
|
||||
\State $\delivered \gets \emptyset$
|
||||
\State $\prop[r][j] \gets \bot, \forall r, j$
|
||||
% \State $X_r \gets \bot, \forall r$
|
||||
\State $W_r \gets \bot, \forall r$
|
||||
\State $\resolved[r] \gets \bot, \forall r$
|
||||
\end{algorithmic}
|
||||
|
||||
\renewcommand{\algletter}{A}
|
||||
\begin{algorithm}[H]
|
||||
\caption{ABroadcast$(m)$}
|
||||
\begin{algorithmic}[1]
|
||||
\Function{ABroadcast}{$m$}
|
||||
\State $r \gets \current$
|
||||
\State $S \gets (\received \cup \{m\}$)
|
||||
\For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$}
|
||||
\State $\RBcast(i, PROP, S, r)$
|
||||
\State \textbf{wait} until $|W_r| \geq n - f$ where $W_r = \BFTRESULT[r]$
|
||||
\State $\BFTCOMMIT(r)$
|
||||
\State \textbf{wait} until $|\resolved[r]| \geq n - f$
|
||||
\State $W_r \gets \BFTRESULT[r]$
|
||||
\If{$i \in W_r \vee (\exists j, r': j \in W_r \wedge \prop[r'][j] \ni m)$}
|
||||
\State \textbf{break}
|
||||
\EndIf
|
||||
\EndFor
|
||||
\EndFunction
|
||||
\end{algorithmic}
|
||||
\end{algorithm}
|
||||
|
||||
\renewcommand{\algletter}{B}
|
||||
\begin{algorithm}[H]
|
||||
\caption{ADeliver$(m)$}
|
||||
\begin{algorithmic}[1]
|
||||
\Function{ADeliver}{m}
|
||||
\State $r \gets \current$
|
||||
\If{$|\resolved[r]| < n - f$}
|
||||
\State \Return $\bot$
|
||||
\EndIf
|
||||
\State $W_r \gets \BFTRESULT[r]$
|
||||
\If{$\exists j \in W_r,\ \prop[r][j] = \bot$}
|
||||
\State \Return $\bot$
|
||||
\EndIf
|
||||
\State $M_r \gets \bigcup_{j \in W_r} \prop[r][j]$
|
||||
\State $m \gets \ordered(M_r \setminus \delivered)[0]$ \Comment{Set $m$ as the smaller message not already delivered}
|
||||
\State $\delivered \leftarrow \delivered \cup \{m\}$
|
||||
\If{$M_r \setminus \delivered = \emptyset$} \Comment{Check if all messages from round $r$ have been delivered}
|
||||
\State $\current \leftarrow \current + 1$
|
||||
\EndIf
|
||||
\State \textbf{return} $m$
|
||||
\EndFunction
|
||||
\end{algorithmic}
|
||||
\end{algorithm}
|
||||
|
||||
\renewcommand{\algletter}{C}
|
||||
\begin{algorithm}[H]
|
||||
\caption{RB handlers}
|
||||
\begin{algorithmic}[1]
|
||||
\Function{Rreceived}{j, PROP, S, r}
|
||||
\State $\received \gets \received \cup \{S\}$
|
||||
\State $\prop[r][j] \gets S$
|
||||
\State $\BFTVOTE(j, r)$
|
||||
\EndFunction
|
||||
|
||||
\vspace{1em}
|
||||
|
||||
\Function{Rreceived}{j, COMMIT, r}
|
||||
\State $\received[r] \cup \{j\}$
|
||||
\EndFunction
|
||||
\end{algorithmic}
|
||||
\end{algorithm}
|
||||
|
||||
% \subsection{Example execution}
|
||||
|
||||
% \begin{figure}[H]
|
||||
% \centering
|
||||
% \input{diagrams/classic_seq.tex}
|
||||
% \caption{Expected Executions of P1 willing to send a message at round r}
|
||||
% \end{figure}
|
||||
BIN
Recherche/BFT-ARBover/dlarb.pdf
Normal file
BIN
Recherche/BFT-ARBover/dlarb.pdf
Normal file
Binary file not shown.
Binary file not shown.
@@ -11,13 +11,14 @@
|
||||
\usepackage{csquotes}
|
||||
\usepackage[hidelinks]{hyperref}
|
||||
\usepackage[nameinlink,noabbrev]{cleveref}
|
||||
\usepackage{algorithm}
|
||||
\usepackage{algpseudocode}
|
||||
\usepackage[ruled, vlined, linesnumbered, algonl, titlenumbered]{algorithm2e}
|
||||
\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}
|
||||
|
||||
\SetKwProg{Fn}{Function}{}{EndFunction}
|
||||
\SetKwFunction{Wait}{Wait Until}
|
||||
\SetKwProg{Upon}{Upon}{}{EndUpon}
|
||||
\SetKwComment{Comment}{}{}
|
||||
|
||||
\usepackage{tikz}
|
||||
\graphicspath{{diagrams/out}}
|
||||
\usepackage{xspace}
|
||||
@@ -43,720 +44,281 @@
|
||||
\newtheorem{remark}{Remark}
|
||||
|
||||
\newcommand{\RB}{\textsf{RB}\xspace}
|
||||
\newcommand{\res}{\mathsf{res}}
|
||||
\newcommand{\ARB}{\textsf{ARB}\xspace}
|
||||
\newcommand{\DL}{\textsf{DL}\xspace}
|
||||
\newcommand{\APPEND}{\textsf{APPEND}}
|
||||
\newcommand{\PROVE}{\textsf{PROVE}}
|
||||
\newcommand{\PROVEtrace}{\textsf{prove}}
|
||||
\newcommand{\READ}{\textsf{READ}}
|
||||
\newcommand{\DL}{\textsf{DL}}
|
||||
\newcommand{\append}{\ensuremath{\mathsf{append}}}
|
||||
\newcommand{\prove}{\ensuremath{\mathsf{prove}}}
|
||||
% \newcommand{\PROVEtrace}{\ensuremath{\mathsf{prove}}}
|
||||
\newcommand{\readop}{\ensuremath{\mathsf{read}}}
|
||||
|
||||
\newcommand{\BFTAPPEND}{\textsf{BFT\text{-}APPEND}}
|
||||
\newcommand{\BFTPROVE}{\textsf{BFT\text{-}PROVE}}
|
||||
\newcommand{\BFTREAD}{\textsf{BFT\text{-}READ}}
|
||||
% Backward compatibility aliases
|
||||
\newcommand{\APPEND}{\append}
|
||||
\newcommand{\PROVE}{\prove}
|
||||
\newcommand{\READ}{\readop}
|
||||
|
||||
\newcommand{\BFTAPPEND}{\textsc{bft-append}}
|
||||
\newcommand{\BFTPROVE}{\textsc{bft-prove}}
|
||||
\newcommand{\BFTREAD}{\textsc{bft-read}}
|
||||
|
||||
\newcommand{\ABbroadcast}{\textsf{AB-broadcast}}
|
||||
\newcommand{\ABdeliver}{\textsf{AB-deliver}}
|
||||
\newcommand{\RBcast}{\textsf{RB-cast}}
|
||||
\newcommand{\RBreceived}{\textsf{RB-received}}
|
||||
\newcommand{\ordered}{\textsf{ordered}}
|
||||
\newcommand{\ABbroadcast}{\textsc{abroadcast}}
|
||||
\newcommand{\ABdeliver}{\textsc{adeliver}}
|
||||
\newcommand{\validated}{\ensuremath{\textsc{validated}}}
|
||||
\newcommand{\rbcast}{\ensuremath{\mathsf{rbcast}}}
|
||||
\newcommand{\rbreceived}{\ensuremath{\mathsf{rreceived}}}
|
||||
\newcommand{\order}{\ensuremath{\mathsf{order}}}
|
||||
|
||||
% Backward compatibility aliases
|
||||
\newcommand{\RBcast}{\rbcast}
|
||||
|
||||
\newcommand{\rdeliver}{\ensuremath{\mathsf{rdeliver}}}
|
||||
\newcommand{\send}{\ensuremath{\mathsf{send}}}
|
||||
\newcommand{\receive}{\ensuremath{\mathsf{receive}}}
|
||||
|
||||
% Local variables
|
||||
\newcommand{\unordered}{\ensuremath{\mathit{unordered}}}
|
||||
\newcommand{\ordered}{\ensuremath{\mathit{ordered}}}
|
||||
\newcommand{\delivered}{\ensuremath{\mathit{delivered}}}
|
||||
\newcommand{\prop}{\ensuremath{\mathit{prop}}}
|
||||
\newcommand{\winners}{\ensuremath{\mathit{winners}}}
|
||||
\newcommand{\done}{\ensuremath{\mathit{done}}}
|
||||
\newcommand{\res}{\ensuremath{\mathit{res}}}
|
||||
\newcommand{\flag}{\ensuremath{\mathit{flag}}}
|
||||
|
||||
%% Used in BFT-DL implementation
|
||||
\newcommand{\state}{\ensuremath{\mathit{state}}}
|
||||
\newcommand{\results}{\ensuremath{\mathit{results}}}
|
||||
|
||||
% Invariant/concept names (used in proofs)
|
||||
\newcommand{\Winners}{\mathsf{Winners}}
|
||||
\newcommand{\Messages}{\mathsf{Messages}}
|
||||
\newcommand{\ABlisten}{\textsf{AB-listen}}
|
||||
|
||||
\newcommand{\CANDIDATE}{\textsf{VOTE}}
|
||||
\newcommand{\CLOSE}{\textsf{COMMIT}}
|
||||
\newcommand{\READGE}{\textsf{RESULT}}
|
||||
|
||||
\newcommand{\SHARE}{\mathsf{SHARE}}
|
||||
\newcommand{\COMBINE}{\mathsf{COMBINE}}
|
||||
\newcommand{\VERIFY}{\mathsf{VERIFY}}
|
||||
|
||||
\newcommand{\RETRIEVE}{\mathsf{RETRIEVE}}
|
||||
\newcommand{\SUBMIT}{\mathsf{SUBMIT}}
|
||||
|
||||
\newcommand{\delivered}{\mathsf{delivered}}
|
||||
\newcommand{\received}{\mathsf{received}}
|
||||
\newcommand{\prop}{\mathsf{prop}}
|
||||
\newcommand{\resolved}{\mathsf{resolved}}
|
||||
\newcommand{\current}{\mathsf{current}}
|
||||
\newcommand{\received}{\ensuremath{\mathsf{received}}}
|
||||
\newcommand{\current}{\ensuremath{\mathsf{current}}}
|
||||
|
||||
\newcommand{\Seq}{\mathsf{Seq}}
|
||||
\newcommand{\GE}{\mathsf{GE}}
|
||||
\newcommand{\BFTDL}{\textsf{BFT\text{-}DL}}
|
||||
|
||||
\newcommand{\BFTGE}{\textsf{BFT\text{-}GE}}
|
||||
\newcommand{\BFTVOTE}{\textsf{BFT\text{-}VOTE}}
|
||||
\newcommand{\BFTCOMMIT}{\textsf{BFT\text{-}COMMIT}}
|
||||
\newcommand{\BFTRESULT}{\textsf{BFT\text{-}RESULT}}
|
||||
|
||||
|
||||
\crefname{theorem}{Theorem}{Theorems}
|
||||
\crefname{lemma}{Lemma}{Lemmas}
|
||||
\crefname{definition}{Definition}{Definitions}
|
||||
\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
|
||||
|
||||
\begin{document}
|
||||
|
||||
\section{Model}
|
||||
We consider a static set of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable.
|
||||
\section{Model 1: Crash}
|
||||
We consider a static set $\Pi$ of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable. At most $f$ processes can crash, with $n \geq f$, in the standard asynchronous crash-failure message-passing model~\cite{ChandraToueg96}.
|
||||
|
||||
\paragraph{Synchrony.} The network is asynchronous. Processes may crash; at most $f$ crashes occur.
|
||||
\paragraph{Synchrony.} The network is asynchronous.
|
||||
|
||||
\paragraph{Communication.} Processes can exchange through a Reliable Broadcast (\RB) primitive (defined below) which's invoked with the functions \RBcast$(m)$ and \RBreceived$(m)$. There exists a shared object called DenyList (\DL) (defined below) that is interfaced with the functions \APPEND$(x)$, \PROVE$(x)$ and \READ$()$.
|
||||
\paragraph{Communication.} Processes communicate through reliable, error-free point-to-point channels. Messages sent by a correct process to another correct process are eventually delivered without loss or corruption. There exists a shared object called DenyList ($\DL$) (defined below) that is interfaced with a set $O$ of operations. There exist three types of these operations: $\APPEND(x)$, $\PROVE(x)$ and $\READ()$.
|
||||
|
||||
\paragraph{Notation.} Let $\Pi$ be the finite set of process identifiers and let $n \triangleq |\Pi|$. Two authorization subsets are $\Pi_M \subseteq \Pi$ (processes allowed to issue \APPEND) and $\Pi_V \subseteq \Pi$ (processes allowed to issue \PROVE). Indices $i,j \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec$ for the \DL{} linearization: $x \prec y$ means that operation $x$ appears strictly before $y$ in the linearized history of \DL. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes). For any round $r \in \mathcal{R}$, define $\Winners_r \triangleq \{\, j \in \Pi \mid (j,\PROVEtrace(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization.
|
||||
We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$.
|
||||
\paragraph{Notation.} For any indice $x$ we defined by $\Pi_x$ a subset of $\Pi$. We consider two subsets $\Pi_M$ and $\Pi_V$ two authorization subsets. Indices $i \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec$ for the \DL{} linearization: $x \prec y$ means that operation $x$ appears strictly before $y$ in the linearized history of \DL. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes).
|
||||
For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked by process $p_i$.
|
||||
%For any round $r \in \mathcal{R}$, define $\Winners_r \triangleq \{\, j \in \Pi \mid (j,\PROVEtrace(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization.
|
||||
%We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$.
|
||||
|
||||
% ------------------------------------------------------------------------------
|
||||
\section{Primitives}
|
||||
|
||||
\input{2_Primitives/index.tex}
|
||||
|
||||
\section{Atomic Reliable Broadcast (ARB)}
|
||||
|
||||
\section{Group Election Object Consensus Number}
|
||||
\input{3_ARB_Def/index.tex}
|
||||
|
||||
\input{3_GEO_CS/index.tex}
|
||||
\section{ARB using DL}
|
||||
|
||||
% ------------------------------------------------------------------------------
|
||||
\section{Target Abstraction: Atomic Reliable Broadcast (ARB)}
|
||||
|
||||
\input{4_ARB_Def/index.tex}
|
||||
|
||||
|
||||
\section{ARB over RB and DL}
|
||||
|
||||
\input{5_ARB_with_RB_DL/index.tex}
|
||||
% ------------------------------------------------------------------------------
|
||||
\input{4_ARB_with_RB_DL/index.tex}
|
||||
|
||||
\section{BFT-ARB over RB and DL}
|
||||
|
||||
\input{6_BFT_ARB/index.tex}
|
||||
|
||||
\section{Example of implementation of ARB with DL and RB}
|
||||
|
||||
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.
|
||||
|
||||
\subsection{Algorithm}
|
||||
% granularité diff commentaire de code et paragraphe pre algo
|
||||
|
||||
\begin{definition}[Closed round]\label{def:closed-round}
|
||||
Given a \DL{} linearization $H$, a round $r\in\mathcal{R}$ is \emph{closed} in $H$ iff $H$ contains an operation $\APPEND(r)$.
|
||||
Equivalently, there exists a time after which every $\PROVE(r)$ is invalid in $H$.
|
||||
\end{definition}
|
||||
|
||||
\subsubsection{Variables}
|
||||
Each process $p_i$ maintains:
|
||||
|
||||
%on met toutes les variables locales ici
|
||||
\begin{algorithmic}
|
||||
\State $\received \gets \emptyset$ \Comment{Messages received via \RB but not yet delivered}
|
||||
\State $\delivered \gets \emptyset$ \Comment{Messages already delivered}
|
||||
\State $\prop[r][j] \gets \bot,\ \forall r,j$ \Comment{Proposal from process $j$ for round $r$}
|
||||
\State $\current \gets 0$
|
||||
\end{algorithmic}
|
||||
|
||||
\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}
|
||||
|
||||
\renewcommand{\algletter}{A}
|
||||
\begin{algorithm}[H]
|
||||
\caption{\RB handler (at process $p_i$)}\label{alg:rb-handler}
|
||||
\begin{algorithmic}[1]
|
||||
\Function{RBreceived}{$S, r, j$}
|
||||
% \State \textbf{on} $\RBreceived(S, r, j)$ \textbf{do}
|
||||
\State $\received \leftarrow \received \cup \{S\}$
|
||||
\State $\prop[r][j] \leftarrow S$ \Comment{Record sender $j$'s proposal $S$ for round $r$}
|
||||
\EndFunction
|
||||
\end{algorithmic}
|
||||
\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.
|
||||
|
||||
\renewcommand{\algletter}{B}
|
||||
\begin{algorithm}[H]
|
||||
\caption{\ABbroadcast$(m)$ (at process $p_i$)}\label{alg:ab-bcast}
|
||||
\begin{algorithmic}[1]
|
||||
\Function{ABbroadcast}{$m$}
|
||||
\State $P \leftarrow \READ()$ \Comment{Fetch latest \DL state to learn recent $\PROVE$ operations}
|
||||
\State $r_{max} \leftarrow \max(\{ r' : \exists j,\ (j,\PROVE(r')) \in P \})$ \Comment{Pick current open round}
|
||||
\State $S \leftarrow (\received \setminus \delivered) \cup \{m\}$ \Comment{Propose all pending messages plus the new $m$}
|
||||
|
||||
\vspace{1em}
|
||||
|
||||
\For{\textbf{each}\ $r \in \{r_{max}, r_{max}+1, \cdots \}$}
|
||||
\State $\RBcast(S, r, i)$; $\PROVE(r)$; $\APPEND(r)$;
|
||||
\State $P \leftarrow \READ()$ \Comment{Refresh local view of \DL}
|
||||
\If{($\big((i, \PROVEtrace(r)) \in P\ \vee\ (\exists j, r': (j, \PROVEtrace(r')) \in P \wedge \ m \in \prop[r'][j]))$)}
|
||||
\State \textbf{break} \Comment{Exit loop once $m$ is included in some closed round}
|
||||
\EndIf
|
||||
\EndFor
|
||||
\EndFunction
|
||||
\end{algorithmic}
|
||||
\end{algorithm}
|
||||
|
||||
\renewcommand{\algletter}{C}
|
||||
\begin{algorithm}[H]
|
||||
\caption{\ABdeliver() at process $p_i$}\label{alg:delivery}
|
||||
\begin{algorithmic}[1]
|
||||
\Function{ABdeliver}{}
|
||||
\State $r \gets \current$
|
||||
\State $P \gets \READ()$
|
||||
\If{$\forall j : (j, \PROVEtrace(r)) \not\in P$}
|
||||
\State \Return $\bot$
|
||||
\EndIf
|
||||
\State $\APPEND(r)$; $P \gets \READ()$
|
||||
\State $W_r \gets \{ j : (j, \PROVEtrace(r)) \in P \}$
|
||||
\If{$\exists j \in W_r,\ \prop[r][j] = \bot$}
|
||||
\State \Return $\bot$
|
||||
\EndIf
|
||||
\State $M_r \gets \bigcup_{j \in W_r} \prop[r][j]$
|
||||
\State $m \gets \ordered(M_r \setminus \delivered)[0]$ \Comment{Set $m$ as the smaller message not already delivered}
|
||||
\State $\delivered \leftarrow \delivered \cup \{m\}$
|
||||
\If{$M_r \setminus \delivered = \emptyset$} \Comment{Check if all messages from round $r$ have been delivered}
|
||||
\State $\current \leftarrow \current + 1$
|
||||
\EndIf
|
||||
\State \textbf{return} $m$
|
||||
\EndFunction
|
||||
\end{algorithmic}
|
||||
\end{algorithm}
|
||||
|
||||
% ------------------------------------------------------------------------------
|
||||
\subsection{Correctness}
|
||||
|
||||
\begin{lemma}[Stable round closure]\label{lem:closure-stable}
|
||||
If a round $r$ is closed, then there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid.
|
||||
Once closed, a round never becomes open again.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the linearization $H$. \\
|
||||
$H$ is a total order of operations, the set of $\APPEND(r)$ operations is totally ordered, and hence there exists a smallest $\APPEND(r)$ in $H$. We denote this operation $\APPEND^{(\star)}(r)$ and $t_0$ its linearization point. \\
|
||||
By the validity property of \DL, a $\PROVE(r)$ is valid iff $\PROVE(r) \prec \APPEND^{(\star)}(r)$. Thus, after $t_0$, no $\PROVE(r)$ can be valid. \\
|
||||
$H$ is a immutable grow-only history, and hence once closed, a round never becomes open again. \\
|
||||
Hence there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid and the closure is stable.
|
||||
\end{proof}
|
||||
|
||||
\begin{definition}[First APPEND]\label{def:first-append}
|
||||
Given a \DL{} linearization $H$, for any closed round $r\in\mathcal{R}$, we denote by $\APPEND^{(\star)}(r)$ the earliest $\APPEND(r)$ in $H$.
|
||||
\end{definition}
|
||||
|
||||
\begin{lemma}[Across rounds]\label{lem:across}
|
||||
If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$, r' is also closed.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
\emph{Base.} For a closed round $k=0$, the set $\{k' \in \mathcal{R},\ k' < k\}$ is empty, hence the lemma is true.
|
||||
|
||||
\emph{Induction.} Assume the lemma is true for round $k\geq 0$, we prove it for round $k+1$.
|
||||
|
||||
\smallskip
|
||||
Assume $k+1$ is closed and let $\APPEND^{(\star)}(k+1)$ be the earliest $\APPEND(k+1)$ in the DL linearization $H$.
|
||||
By Lemma 1, after an $\APPEND(k)$ is in $H$, any later $\PROVE(k)$ is rejected also, a process’s program order is preserved in $H$.
|
||||
|
||||
There are two possibilities for where $\APPEND^{(\star)}(k+1)$ is invoked.
|
||||
|
||||
\begin{itemize}
|
||||
\item \textbf{Case (B6) :}
|
||||
Some process $p^\star$ executes the loop (lines B5–B11) and invokes $\APPEND^{(\star)}(k+1)$ at line B6.
|
||||
Immediately before line B6, line B5 sets $r\leftarrow r+1$, so the previous loop iteration (if any) targeted $k$. We consider two sub-cases.
|
||||
|
||||
\begin{itemize}
|
||||
\item \emph{(i) $p^\star$ is not in its first loop iteration.}
|
||||
In the previous iteration, $p^\star$ executed $\PROVE^{(\star)}(k)$ at B6, followed (in program order) by $\APPEND^{(\star)}(k)$.
|
||||
If round $k$ wasn't closed when $p^\star$ execute $\PROVE^{(\star)}(k)$ at B9, then the condition at B8 would be true hence the tuple $(p^\star, \PROVEtrace(k))$ should be visible in P which implies that $p^\star$ should leave the loop at round $k$, contradicting the assumption that $p^\star$ is now executing another iteration.
|
||||
Since the tuple is not visible, the $\PROVE^{(\star)}(k)$ was rejected by the DL which implies by definition an $\APPEND(k)$ already exists in $H$. Thus in this case $k$ is closed.
|
||||
|
||||
\item \emph{(ii) $p^\star$ is in its first loop iteration.}
|
||||
To compute the value $r_{max}$, $p^\star$ must have observed one or many $(\_ , \PROVEtrace(k+1))$ in $P$ at B2/B3, issued by some processes (possibly different from $p^\star$). Let's call $p_1$ the issuer of the first $\PROVE^{(1)}(k+1)$ in the linearization $H$. \\
|
||||
When $p_1$ executed $P \gets \READ()$ at B2 and compute $r_{max}$ at B3, he observed no tuple $(\_,\PROVEtrace(k+1))$ in $P$ because he's the issuer of the first one. So when $p_1$ executed the loop (B5–B11), he run it for the round $k$, didn't seen any $(1,\PROVEtrace(k))$ in $P$ at B8, and then executed the first $\PROVE^{(1)}(k+1)$ at B6 in a second iteration. \\
|
||||
If round $k$ wasn't closed when $p_1$ execute $\PROVE^{(1)}(k)$ at B6, then the condition at B8 should be true which implies that $p_1$ sould leave the loop at round $k$, contradicting the assumption that $p_1$ is now executing $\PROVE^{(1)}(r+1)$. In this case $k$ is closed.
|
||||
\end{itemize}
|
||||
|
||||
\item \textbf{Case (C8) :}
|
||||
Some process invokes $\APPEND(k+1)$ at C8.
|
||||
Line C8 is guarded by the presence of $\PROVE(\textit{next})$ in $P$ with $\textit{next}=k+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}=k+1$ it implies that he has completed round $k$, which includes closing $k$ at C8 when $\PROVE(k)$ is observed.
|
||||
Hence $\APPEND^\star(k+1)$ implies a prior $\APPEND(k)$ in $H$, so $k$ is closed.
|
||||
\end{itemize}
|
||||
|
||||
\smallskip
|
||||
In all cases, $k+1$ closed implie $k$ closed. By induction on $k$, if the lemme is true for a closed $k$ then it is true for a closed $k+1$.
|
||||
Therefore, the lemma is true for all closed rounds $r$.
|
||||
\end{proof}
|
||||
|
||||
\begin{definition}[Winner Invariant]\label{def:winner-invariant}
|
||||
For any closed round $r$, define
|
||||
\[
|
||||
\Winners_r \triangleq \{ j : \PROVE^{(j)}(r) \prec \APPEND^\star(r) \}
|
||||
\]
|
||||
as the unique set of winners of round $r$.
|
||||
\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.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let's take a closed round $r$. By \Cref{def:first-append}, there exists a unique earliest $\APPEND(r)$ in the DL linearization, denoted $\APPEND^\star(r)$.
|
||||
|
||||
Consider any correct process $p$ 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 $(\_,\PROVEtrace(r))$ observed by any correct process 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.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Well-defined winners]\label{lem:winners}
|
||||
For any correct process and round $r$, if the process computes $W_r$ at line C9, then :
|
||||
\begin{itemize}
|
||||
\item $\Winners_r$ is defined;
|
||||
\item the computed $W_r$ is exactly $\Winners_r$.
|
||||
\end{itemize}
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let take a correct process $p_i$ that reach line C9 to compute $W_r$. \\
|
||||
By program order, $p_i$ must have executed $\APPEND^{(i)}(r)$ at C8 before, which implies by \Cref{def:closed-round} that round $r$ is closed. 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 $(\_,\PROVEtrace(r))$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at C8 after the $\APPEND^{(i)}(r)$, it observes a set $P$ that includes all valid tuples $(\_,\PROVEtrace(r))$ such that
|
||||
\[
|
||||
W_r = \{ j : (j,\PROVEtrace(r)) \in P \} = \{j : \PROVE^{(j)}(r) \prec \APPEND^\star(r) \} = \Winners_r
|
||||
\]
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[No APPEND without PROVE]\label{lem:append-prove}
|
||||
If some process invokes $\APPEND(r)$, then at least a process must have previously invoked $\PROVE(r)$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}[Proof]
|
||||
Consider the round $r$ such that some process invokes $\APPEND(r)$. There are two possible cases
|
||||
|
||||
\begin{itemize}
|
||||
\item \textbf{Case (B6) :}
|
||||
There exists a process $p^\star$ who's the issuer of the earliest $\APPEND^{(\star)}(r)$ in the DL linearization $H$. By program order, $p^\star$ must have previously invoked $\PROVE^{(\star)}(r)$ before invoking $\APPEND^{(\star)}(r)$ at B6. 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) :}
|
||||
There exist a process $p^\star$ invokes $\APPEND^{(\star)}(r)$ at C8. Line C8 is guarded by the condition at C5, which ensures that $p$ observed some $(\_,\PROVEtrace(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}
|
||||
|
||||
In both cases, if some process invokes $\APPEND(r)$, then some process must have previously invoked $\PROVE(r)$.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[No empty winners]\label{lem:nonempty}
|
||||
Let $r$ be a round, if $\Winners_r$ is defined, then $\Winners_r \neq \emptyset$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}[Proof]
|
||||
If $\Winners_r$ is defined, then by \Cref{def:winner-invariant}, round $r$ is closed. By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the DL linearization. \\
|
||||
By \Cref{lem:append-prove}, at least a process must have invoked a valid $\PROVE(r)$ before $\APPEND^{(\star)}(r)$. Hence, there exists at least one $j$ such that $\{j: \PROVE^{(j)}(r) \prec \APPEND^\star(r)\}$, so $\Winners_r \neq \emptyset$.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Winners must propose]\label{lem:winners-propose}
|
||||
For any closed round $r$, $\forall j \in \Winners_r$, process $j$ must have invoked a $\RBcast(S^{(j)}, r, j)$
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}[Proof]
|
||||
Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $j \in \Winners_r$, there exist a valid $\PROVE^{(j)}(r)$ such that $\PROVE^{(j)}(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order, if $j$ invoked a valid $\PROVE^{(j)}(r)$ at line B6 he must have invoked $\RBcast(S^{(j)}, r, j)$ directly before.
|
||||
\end{proof}
|
||||
|
||||
\begin{definition}[Messages invariant]\label{def:messages-invariant}
|
||||
For any closed round $r$ and any correct process $p_i$ such that $\nexists j \in \Winners_r : prop^{[i)}[r][j] = \bot$, define
|
||||
\[
|
||||
\Messages_r \triangleq \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]
|
||||
\]
|
||||
as the unique set of messages proposed by the winners of round $r$.
|
||||
\end{definition}
|
||||
|
||||
\begin{lemma}[Non-empty winners proposal]\label{lem:winner-propose-nonbot}
|
||||
For any closed round $r$, $\forall j \in \Winners_r$, for any correct process $p_i$, eventually $\prop^{(i)}[r][j] \neq \bot$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}[Proof]
|
||||
Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $j \in \Winners_r$, there exist a valid $\PROVE^{(j)}(r)$ such that $\PROVE^{(j)}(r) \prec \APPEND^\star(r)$ in the DL linearization. By \Cref{lem:winners-propose}, $j$ must have invoked $\RBcast(S^{(j)}, r, j)$.
|
||||
|
||||
Let take a process $p_i$, by \RB \emph{Validity}, every correct process eventually receives $j$'s \RB message for round $r$, which sets $\prop[r][j]$ to a non-$\bot$ value at line A3.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Eventual proposal closure]\label{lem:eventual-closure}
|
||||
If a correct process $p_i$ define $M_r$ at line C13, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}[Proof]
|
||||
Let take a correct process $p_i$ that computes $M_r$ at line C13. By \Cref{lem:winners}, $p_i$ computes the unique winner set $\Winners_r$.
|
||||
|
||||
By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line C13 where $p_i$ computes $M_r$ is guarded by the condition at C10, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, when $p_i$ computes $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}
|
||||
|
||||
\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(S, r, i)$.
|
||||
\end{lemma}
|
||||
|
||||
\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$.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Proposal convergence]\label{lem:convergence}
|
||||
For any round $r$, for any correct processes $p_i$ that define $M_r$ at line C13, we have
|
||||
\[
|
||||
M_r^{(i)} = \Messages_r
|
||||
\]
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}[Proof]
|
||||
Let take a correct process $p_i$ that define $M_r$ at line C13. That implies that $p_i$ has defined $W_r$ at line C9. 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
|
||||
\[
|
||||
M_r^{(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(S, r, j)\quad\text{with}\quad m\in S.
|
||||
\]
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Fix a correct process $p_i$ that invokes $\ABbroadcast(m)$ and eventually exits the loop (B5–B11) at some round $r$. There are two possible cases.
|
||||
|
||||
\begin{itemize}
|
||||
\item \textbf{Case 1:} $p_i$ exits the loop because $(i, \PROVEtrace(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 B6 before invoking $\PROVE^{(i)}(r)$ at B7. By line B4, $m \in S$. Hence there exist a closed round $r$ and a correct process $j=i\in\Winners_r$ such that $j$ invokes $\RBcast(S, r, j)$ with $m\in S$.
|
||||
|
||||
\item \textbf{Case 2:} $p_i$ exits the loop because $\exists j, r': (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$. In this case, by \Cref{lem:winners-propose} and \Cref{lem:unique-proposal} $j$ must have invoked a unique $\RBcast(S, r', j)$. Which set $\prop^{(i)}[r'][j] = S$ with $m \in S$.
|
||||
\end{itemize}
|
||||
|
||||
In both cases, if some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a correct process $j\in\Winners_r$ such that $j$ invokes
|
||||
\[
|
||||
\RBcast(S, r, j)\quad\text{with}\quad m\in S.
|
||||
\]
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Broadcast Termination]\label{lem:bcast-termination}
|
||||
If a correct process invokes $\ABbroadcast(m)$, then he eventually exit the function and returns.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}[Proof]
|
||||
Let a correct process $p_i$ that invokes $\ABbroadcast(m)$. The lemma is true if $\exists r_1$ such that $r_1 \geq r_{max}$ and if $(i, \PROVEtrace(r_1)) \in P$; or if $\exists r_2$ such that $r_2 \geq r_{max}$ and if $\exists j: (j, \PROVEtrace(r_2)) \in P \wedge m \in \prop[r_2][j]$ (like guarded at B8).
|
||||
|
||||
Let admit 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).\\
|
||||
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 a correct 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$ execute \Cref{alg:rb-handler} and do $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line A2).
|
||||
For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \Cref{alg:rb-handler}, $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:winner-propose-nonbot}, 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 cover the condition $(i, \PROVEtrace(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}
|
||||
|
||||
\begin{lemma}[Validity]\label{lem:validity}
|
||||
If a correct process $p$ invokes $\ABbroadcast(m)$, then every correct process that invokes a infinitely often times $\ABdeliver()$ eventually delivers $m$.
|
||||
\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(S, r, j)\quad\text{with}\quad m\in S.
|
||||
\]
|
||||
|
||||
By \Cref{lem:eventual-closure}, when $p_q$ computes $M_r$ at line C13, $\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],
|
||||
\]
|
||||
we have $m \in \prop[r][j] = S$, so $m \in M_r$. By \Cref{lem:convergence}, $M_r$ is invariant so each computation of $M_r$ by any correct process that defines it includes $m$. At each invocation of $\ABdeliver()$ which deliver $m'$, $m'$ is add to $\delivered$ until $M_r \subseteq \delivered$. Once this append we're assured that there exist an invocation of $\ABdeliver()$ which return $m$. Hence $m$ is well delivered.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[No duplication]\label{lem:no-duplication}
|
||||
No correct process delivers the same message more than once.
|
||||
\end{lemma}
|
||||
|
||||
\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)}()$.
|
||||
|
||||
When $\ABdeliver^{(A)}()$ occur, by program order and because it reach line C19 to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reach line C14 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 deliver $m$ can't occur.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Total order]\label{lem:total-order}
|
||||
For any two messages $m_1$ and $m_2$ delivered by correct processes, if a correct process $p_i$ delivers $m_1$ before $m_2$, then any correct process $p_j$ that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Consider any correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exist 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(S_1, r'_1, k_1)\quad\text{with}\quad m_1\in S_1,
|
||||
\]
|
||||
\[
|
||||
\RBcast(S_2, r'_2, k_2)\quad\text{with}\quad m_2\in S_2.
|
||||
\]
|
||||
|
||||
Let consider three cases :
|
||||
\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 $\ABdeliver()$ that returns $m_2$. 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 C13 computes the same set of messages $\Messages_{r_1}$. By line C14 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}
|
||||
|
||||
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.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}[Fifo Order]\label{lem:fifo-order}
|
||||
For any two messages $m_1$ and $m_2$ broadcast by the same correct process $p_i$, if $p_i$ invokes $\ABbroadcast(m_1)$ before $\ABbroadcast(m_2)$, then any correct process $p_j$ that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let take two messages $m_1$ and $m_2$ broadcast by the same correct process $p_i$, with $p_i$ invoking $\ABbroadcast(m_1)$ before $\ABbroadcast(m_2)$. By \Cref{lem:validity}, there exist 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(S_1, r_1, k_1)\quad\text{with}\quad m_1\in S_1,
|
||||
\]
|
||||
\[
|
||||
\RBcast(S_2, r_2, k_2)\quad\text{with}\quad m_2\in S_2.
|
||||
\]
|
||||
|
||||
By program order, $p_i$ must have invoked $\RBcast(S_1, r_1, i)$ before $\RBcast(S_2, r_2, i)$. By \Cref{lem:unique-proposal}, any process invokes at most one $\RBcast(S, r, i)$ per round, hence $r_1 < r_2$. By \Cref{lem:total-order}, any correct process that delivers both $m_1$ and $m_2$ delivers them in a deterministic order.
|
||||
|
||||
In all possible cases, any correct process that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
|
||||
\end{proof}
|
||||
|
||||
\begin{theorem}[FIFO-\ARB]
|
||||
Under the assumed \DL synchrony and \RB reliability, the algorithm implements FIFO Atomic Reliable Broadcast.
|
||||
\end{theorem}
|
||||
|
||||
\begin{proof}
|
||||
We show that the algorithm satisfies the properties of FIFO Atomic Reliable Broadcast under the assumed \DL synchrony and \RB reliability.
|
||||
|
||||
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.
|
||||
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.
|
||||
Furthermore, \Cref{lem:fifo-order} states that for any two messages $m_1$ and $m_2$ broadcast by the same correct process, any correct process that delivers both messages delivers $m_1$ before $m_2$ whenever $m_1$ was broadcast before $m_2$.
|
||||
Thus the global total order extends the per-sender FIFO order of \ABbroadcast.
|
||||
|
||||
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.
|
||||
Therefore, under these assumptions, the algorithm satisfies Validity, Integrity/No-duplicates, total order and per-sender FIFO order, and hence implements FIFO 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 (ignoring the
|
||||
anonymity property).
|
||||
|
||||
\paragraph{DenyList as a deterministic state machine.}
|
||||
Without anonymity, the \DL specification defines a
|
||||
deterministic abstract object: given a sequence $\Seq$ of operations
|
||||
$\APPEND(x)$, $\PROVE(x)$, and $\READ()$, the resulting sequence of return
|
||||
values and the evolution of the abstract state (set of appended elements,
|
||||
history of operations) are uniquely determined.
|
||||
|
||||
\paragraph{State machine replication over \ARB.}
|
||||
Assume a system that exports a FIFO-\ARB primitive with the guarantees that if a correct process invokes $\ABbroadcast(m)$, then every correct process eventually $\ABdeliver(m)$ and the invocation eventually returns.
|
||||
Following the classical \emph{state machine replication} approach
|
||||
such as described in Schneider~\cite{Schneider90}, we can implement a fault-tolerant service by ensuring the following properties:
|
||||
\begin{quote}
|
||||
\textbf{Agreement.} Every nonfaulty state machine replica receives every request. \\
|
||||
\textbf{Order.} Every nonfaulty state machine replica processes the requests it receives in
|
||||
the same relative order.
|
||||
\end{quote}
|
||||
|
||||
Which are cover by our FIFO-\ARB specification.
|
||||
|
||||
\paragraph{Correctness.}
|
||||
|
||||
|
||||
\begin{theorem}[From \ARB to synchronous \DL]\label{thm:arb-to-dl}
|
||||
In an asynchronous message-passing system with crash failures, assume a
|
||||
FIFO Atomic Reliable Broadcast primitive with Integrity, No-duplicates,
|
||||
Validity, and the liveness of $\ABbroadcast$. Then, ignoring anonymity, there
|
||||
exists an implementation of a synchronous DenyList object that satisfies the
|
||||
Termination, Validity, and Anti-flickering properties.
|
||||
\end{theorem}
|
||||
|
||||
\begin{proof}
|
||||
Because the \DL object is deterministic, all correct processes see the same
|
||||
sequence of operations and compute the same sequence of states and return
|
||||
values. We obtain:
|
||||
|
||||
\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.
|
||||
\end{itemize}
|
||||
|
||||
Formally, we can describe the \DL object with the state machine approach for
|
||||
crash-fault, asynchronous message-passing systems with a total order broadcast
|
||||
layer~\cite{Schneider90}.
|
||||
\end{proof}
|
||||
|
||||
\subsubsection{Example executions}
|
||||
|
||||
\begin{figure}[H]
|
||||
\centering
|
||||
\resizebox{0.4\textwidth}{!}{
|
||||
\input{diagrams/nonBFT_behaviour.tex}
|
||||
}
|
||||
\caption{Example execution of the ARB algorithm in a non-BFT setting}
|
||||
\end{figure}
|
||||
|
||||
|
||||
\begin{figure}
|
||||
\centering
|
||||
\resizebox{0.4\textwidth}{!}{
|
||||
\input{diagrams/BFT_behaviour.tex}
|
||||
}
|
||||
\caption{Example execution of the ARB algorithm with a byzantine process}
|
||||
\end{figure}
|
||||
|
||||
|
||||
\section{Implementation of BFT-DenyList and Threshold Cryptography}
|
||||
|
||||
\subsection{DenyList}
|
||||
|
||||
\paragraph{BFT-DenyList}
|
||||
In our algorithm we use multiple DenyList as follows:
|
||||
|
||||
\begin{itemize}
|
||||
\item Let $\mathcal{DL} = \{DL_1, \dots, DL_k\}$ be the set of DenyList used by the algorithm.
|
||||
\item We set $k = \binom{n}{f}$.
|
||||
\item For each $i \in \{1,\dots,k\}$, let $M_i$ be the set of moderators associated with $DL_i$ according to the DenyList definition, so that $|M_i| = n-f$.
|
||||
\item Let $\mathcal{M} = \{M_1, \dots, M_k\}$. We require that the $M_i$ are pairwise distinct:
|
||||
\[
|
||||
\forall i,j \in \{1,\dots,k\},\ i \neq j \implies M_i \neq M_j.
|
||||
\]
|
||||
\end{itemize}
|
||||
|
||||
|
||||
\begin{lemma}
|
||||
$\exists M_i \in M : \forall p \in M_i$ $p$ is correct.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let consider the set $F$ of faulty processes, with $|F| = f$. We can construct the set $M_i = \Pi \setminus F$ such that $|M_i| = n - |F| = n - f$. By construction, $\forall p \in M_i$ $p$ is correct.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}
|
||||
$\forall M_i \in M, \exists p \in M_i$ such that $p$ is correct.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
$\forall i \in \{1, \dots, k\}, |M_i| = n-f$ with $n \geq 2f+1$. We can say that $|M_i| \geq 2f+1-f = f+1 > f$
|
||||
\end{proof}
|
||||
|
||||
Each process can invoke the following functions :
|
||||
|
||||
\begin{itemize}
|
||||
\item $\READ' : () \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$
|
||||
\item $\APPEND' : \mathbb{R} \rightarrow ()$
|
||||
\item $\PROVE' : \mathbb{R} \rightarrow \{0, 1\}$
|
||||
\end{itemize}
|
||||
|
||||
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}
|
||||
|
||||
\subsection{Threshold Cryptography}
|
||||
|
||||
We are using the Boneh-Lynn-Shacham scheme as cryptography primitive to our threshold signature scheme.
|
||||
With :
|
||||
|
||||
\begin{itemize}
|
||||
\item $G : \mathbb{R} \rightarrow \mathbb{R} \times \mathbb{R} $
|
||||
\item $S : \mathbb{R} \times \mathcal{R} \rightarrow \mathbb{R} $
|
||||
\item $V : \mathbb{R} \times \mathcal{R} \times \mathbb{R} \rightarrow \{0, 1\} $
|
||||
\end{itemize}
|
||||
|
||||
Such that :
|
||||
|
||||
\begin{itemize}
|
||||
\item $G(x) \rightarrow (pk, sk)$ : where $x$ is a random value such that $\nexists x_1, x_2: x_1 \neq x_2, G(x_1) = G(x_2)$
|
||||
\item $S(sk, m) \rightarrow \sigma_m$
|
||||
\item $V(pk, m_1, \sigma_{m_2}) \rightarrow k$ : with $k = 1$ iff $m_1 == m_2$ and $\exists x \in \mathbb{R}$ such that $G(x) \rightarrow (pk, sk)$; otherwise $k = 0$
|
||||
\end{itemize}
|
||||
|
||||
\paragraph{threshold Scheme}
|
||||
|
||||
In our algorithm we are only using the following functions :
|
||||
|
||||
\begin{itemize}
|
||||
\item $G' : \mathbb{R} \times \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{R} \times (\mathbb{R} \times \mathbb{R})^n$ : with $n \triangleq |\Pi|$
|
||||
\item $S' : \mathbb{R} \times \mathcal{R} \rightarrow \mathbb{R}$
|
||||
\item $C' : \mathbb{R}^n \times \mathcal{R} \times \mathbb{R} \times \mathbb{R}^t \rightarrow \{\mathbb{R}, \bot\}$ : with $t \leq n$
|
||||
\item $V' : \mathbb{R} \times \mathcal{R} \times \mathbb{R} \rightarrow \{0, 1\}$
|
||||
\end{itemize}
|
||||
|
||||
Such that :
|
||||
|
||||
\begin{itemize}
|
||||
\item $G'(x, n, t) \rightarrow (pk, pk_1, sk_1, \dots, pk_n, sk_n)$ : let define $pkc = {pk_1, \dots, pk_n}$
|
||||
\item $S'(sk_i, m) \rightarrow \sigma_m^i$
|
||||
\item $C'(pkc, m_1, J, \{\sigma_{m_2}^j\}_{j \in J}) \rightarrow \sigma$ : with $J \subseteq \Pi$; and $\sigma = \sigma_{m_1}$ iff $|J| \geq t, \forall j \in J: V(pk_j, m_1, \sigma_{m_2}^j) == 1$; otherwise $\sigma = \bot$.
|
||||
\item $V'(pk, m_1, \sigma_{m_2}) \rightarrow V(pk, m_1, \sigma_{m_2})$
|
||||
\end{itemize}
|
||||
\input{5_BFT_ARB/index.tex}
|
||||
|
||||
|
||||
|
||||
|
||||
% \section{Implementation of BFT-DenyList and Threshold Cryptography}
|
||||
|
||||
% \subsection{DenyList}
|
||||
|
||||
% \paragraph{BFT-DenyList}
|
||||
% In our algorithm we use multiple DenyList as follows:
|
||||
|
||||
% \begin{itemize}
|
||||
% \item Let $\mathcal{DL} = \{DL_1, \dots, DL_k\}$ be the set of DenyList used by the algorithm.
|
||||
% \item We set $k = \binom{n}{f}$.
|
||||
% \item For each $i \in \{1,\dots,k\}$, let $M_i$ be the set of moderators associated with $DL_i$ according to the DenyList definition, so that $|M_i| = n-f$.
|
||||
% \item Let $\mathcal{M} = \{M_1, \dots, M_k\}$. We require that the $M_i$ are pairwise distinct:
|
||||
% \[
|
||||
% \forall i,j \in \{1,\dots,k\},\ i \neq j \implies M_i \neq M_j.
|
||||
% \]
|
||||
% \end{itemize}
|
||||
|
||||
|
||||
% \begin{lemma}
|
||||
% $\exists M_i \in M : \forall p \in M_i$ $p$ is correct.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{proof}
|
||||
% Let consider the set $F$ of faulty processes, with $|F| = f$. We can construct the set $M_i = \Pi \setminus F$ such that $|M_i| = n - |F| = n - f$. By construction, $\forall p \in M_i$ $p$ is correct.
|
||||
% \end{proof}
|
||||
|
||||
% \begin{lemma}
|
||||
% $\forall M_i \in M, \exists p \in M_i$ such that $p$ is correct.
|
||||
% \end{lemma}
|
||||
|
||||
% \begin{proof}
|
||||
% $\forall i \in \{1, \dots, k\}, |M_i| = n-f$ with $n \geq 2f+1$. We can say that $|M_i| \geq 2f+1-f = f+1 > f$
|
||||
% \end{proof}
|
||||
|
||||
% Each process can invoke the following functions :
|
||||
|
||||
% \begin{itemize}
|
||||
% \item $\READ' : () \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$
|
||||
% \item $\APPEND' : \mathbb{R} \rightarrow ()$
|
||||
% \item $\PROVE' : \mathbb{R} \rightarrow \{0, 1\}$
|
||||
% \end{itemize}
|
||||
|
||||
% 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]
|
||||
% \caption{$\READ'() \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$}
|
||||
% $j \gets$ the process invoking $\READ'()$\;
|
||||
% $\res \gets \emptyset$\;
|
||||
% \ForAll{$i \in \{1, \dots, k\}$}{
|
||||
% $\res \gets \res \cup DL_i.\READ()$\;
|
||||
% }
|
||||
% \Return{$\res$}\;
|
||||
% \end{algorithm}
|
||||
|
||||
% \begin{algorithm}[H]
|
||||
% \caption{$\APPEND'(\sigma) \rightarrow ()$}
|
||||
% $j \gets$ the process invoking $\APPEND'(\sigma)$\;
|
||||
% \ForAll{$M_i \in \{M_k \in M : j \in M_k\}$}{
|
||||
% $DL_i.\APPEND(\sigma)$\;
|
||||
% }
|
||||
% \end{algorithm}
|
||||
|
||||
% \begin{algorithm}[H]
|
||||
% \caption{$\PROVE'(\sigma) \rightarrow \{0, 1\}$}
|
||||
% $j \gets$ the process invoking $\PROVE'(\sigma)$\;
|
||||
% $\flag \gets false$\;
|
||||
% \ForAll{$i \in \{1, \dots, k\}$}{
|
||||
% $\flag \gets \flag$ OR $DL_i.\PROVE(\sigma)$\;
|
||||
% }
|
||||
% \Return{$\flag$}\;
|
||||
% \end{algorithm}
|
||||
|
||||
% \subsection{Threshold Cryptography}
|
||||
|
||||
% We are using the Boneh-Lynn-Shacham scheme as cryptography primitive to our threshold signature scheme.
|
||||
% With :
|
||||
|
||||
% \begin{itemize}
|
||||
% \item $G : \mathbb{R} \rightarrow \mathbb{R} \times \mathbb{R} $
|
||||
% \item $S : \mathbb{R} \times \mathcal{R} \rightarrow \mathbb{R} $
|
||||
% \item $V : \mathbb{R} \times \mathcal{R} \times \mathbb{R} \rightarrow \{0, 1\} $
|
||||
% \end{itemize}
|
||||
|
||||
% Such that :
|
||||
|
||||
% \begin{itemize}
|
||||
% \item $G(x) \rightarrow (pk, sk)$ : where $x$ is a random value such that $\nexists x_1, x_2: x_1 \neq x_2, G(x_1) = G(x_2)$
|
||||
% \item $S(sk, m) \rightarrow \sigma_m$
|
||||
% \item $V(pk, m_1, \sigma_{m_2}) \rightarrow k$ : with $k = 1$ iff $m_1 == m_2$ and $\exists x \in \mathbb{R}$ such that $G(x) \rightarrow (pk, sk)$; otherwise $k = 0$
|
||||
% \end{itemize}
|
||||
|
||||
% \paragraph{threshold Scheme}
|
||||
|
||||
% In our algorithm we are only using the following functions :
|
||||
|
||||
% \begin{itemize}
|
||||
% \item $G' : \mathbb{R} \times \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{R} \times (\mathbb{R} \times \mathbb{R})^n$ : with $n \triangleq |\Pi|$
|
||||
% \item $S' : \mathbb{R} \times \mathcal{R} \rightarrow \mathbb{R}$
|
||||
% \item $C' : \mathbb{R}^n \times \mathcal{R} \times \mathbb{R} \times \mathbb{R}^t \rightarrow \{\mathbb{R}, \bot\}$ : with $t \leq n$
|
||||
% \item $V' : \mathbb{R} \times \mathcal{R} \times \mathbb{R} \rightarrow \{0, 1\}$
|
||||
% \end{itemize}
|
||||
|
||||
% Such that :
|
||||
|
||||
% \begin{itemize}
|
||||
% \item $G'(x, n, t) \rightarrow (pk, pk_1, sk_1, \dots, pk_n, sk_n)$ : let define $pkc = {pk_1, \dots, pk_n}$
|
||||
% \item $S'(sk_i, m) \rightarrow \sigma_m^i$
|
||||
% \item $C'(pkc, m_1, J, \{\sigma_{m_2}^j\}_{j \in J}) \rightarrow \sigma$ : with $J \subseteq \Pi$; and $\sigma = \sigma_{m_1}$ iff $|J| \geq t, \forall j \in J: V(pk_j, m_1, \sigma_{m_2}^j) == 1$; otherwise $\sigma = \bot$.
|
||||
% \item $V'(pk, m_1, \sigma_{m_2}) \rightarrow V(pk, m_1, \sigma_{m_2})$
|
||||
% \end{itemize}
|
||||
|
||||
|
||||
\bibliographystyle{plain}
|
||||
\begin{thebibliography}{9}
|
||||
% (left intentionally blank)
|
||||
\bibitem{frey:disc23}
|
||||
Davide Frey, Mathieu Gestin, and Michel Raynal.
|
||||
\newblock The synchronization power (consensus number) of access-control objects: The case of allowlist and denylist.
|
||||
\newblock {\em LIPIcs, DISC 2023}, 281:21:1--21:23, 2023.
|
||||
\newblock doi:10.4230/LIPIcs.DISC.2023.21.
|
||||
|
||||
\bibitem{Bracha87}
|
||||
Gabriel Bracha.
|
||||
\newblock Asynchronous byzantine agreement protocols.
|
||||
\newblock {\em Information and Computation}, 75(2):130--143, 1987.
|
||||
|
||||
\bibitem{Defago2004}
|
||||
Xavier Defago, Andre Schiper, and Peter Urban.
|
||||
\newblock Total order broadcast and multicast algorithms: Taxonomy and survey.
|
||||
\newblock {\em ACM Computing Surveys}, 36(4):372--421, 2004.
|
||||
|
||||
\bibitem{ChandraToueg96}
|
||||
Tushar Deepak Chandra and Sam Toueg.
|
||||
\newblock Unreliable failure detectors for reliable distributed systems.
|
||||
\newblock {\em Journal of the ACM}, 43(2):225--267, 1996.
|
||||
|
||||
\bibitem{Schneider90}
|
||||
Fred B.~Schneider.
|
||||
\newblock Implementing fault-tolerant services using the state machine
|
||||
|
||||
1006
Recherche/Ma bibliothèque.bib
Normal file
1006
Recherche/Ma bibliothèque.bib
Normal file
File diff suppressed because it is too large
Load Diff
Reference in New Issue
Block a user