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

refactoring

Browse Source
This commit is contained in:
Amaury JOLY
2026-03-04 18:38:08 +00:00
parent e4e3abad91
commit 61282a0737
5 changed files with 109 additions and 104 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -17,48 +17,48 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\SetKwBlock{LocalVars}{Local Variables:}{}
\LocalVars{
$\mathit{unordered} \gets \emptyset$,
$\mathit{ordered} \gets \epsilon$,
$\mathit{delivered} \gets \epsilon$\;
$\mathit{prop}[r][j] \gets \bot,\ \forall r,j$\;
$\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} $\mathit{unordered} \setminus \mathit{ordered} \neq \emptyset$\;
$S \leftarrow (\mathit{unordered} \setminus \mathit{ordered})$\;\nllabel{code:Sconstruction}
\textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
$S \leftarrow (\unordered \setminus \ordered)$\;\nllabel{code:Sconstruction}
$\RBcast(\texttt{PROP}, S, \langle r, i \rangle)$; $\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition}
$\mathit{winners}_r \gets \{ j : (j, r) \in \READ() \}$\;\nllabel{code:Wcompute}
$\winners[r] \gets \{ j : (j, r) \in \READ() \}$\;\nllabel{code:Wcompute}
\textbf{wait until} $\forall j \in \mathit{winners}_r,\ \mathit{prop}[r][j] \neq \bot$\;\nllabel{code:check-winners-ack}
\textbf{wait until} $\forall j \in \winners[r],\ \prop[r][j] \neq \bot$\;\nllabel{code:check-winners-ack}
$M \gets \bigcup_{j \in \mathit{winners}_r} \mathit{prop}[r][j]$\;\nllabel{code:Mcompute-dl}
$\mathit{ordered} \leftarrow \mathit{ordered} \cdot \ordered(M)$\;\nllabel{code:next-msg-extraction}
$M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute-dl}
$\ordered \leftarrow \ordered \cdot \ordered(M)$\;\nllabel{code:next-msg-extraction}
}
\vspace{0.3em}
\Upon{$\ABbroadcast(m)$}{
$\mathit{unordered} \gets \mathit{unordered} \cup \{m\}$\;\nllabel{code:abbroadcast-add}
$\unordered \gets \unordered \cup \{m\}$\;\nllabel{code:abbroadcast-add}
}
\vspace{0.3em}
\Upon{$\textsf{rdeliver}(\texttt{PROP}, S, \langle r, j \rangle)$ from process $p_j$}{
$\mathit{unordered} \leftarrow \mathit{unordered} \cup \{S\}$\;\nllabel{code:receivedConstruction}
$\mathit{prop}[r][j] \leftarrow S$\;\nllabel{code:prop-set}
\Upon{$\rdeliver(\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()$}{
\If{$\mathit{ordered} \setminus \mathit{delivered} = \emptyset$}{
\If{$\ordered \setminus \delivered = \emptyset$}{
\Return{$\bot$}
}
let $m$ be the first element in $\mathit{ordered} \setminus \mathit{delivered}$\;\nllabel{code:adeliver-extract}
$\mathit{delivered} \gets \mathit{delivered} \cdot m$\;\nllabel{code:adeliver-mark}
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$}
}
@@ -121,19 +121,19 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\end{proof}
\begin{lemma}[Well-defined winners]\label{lem:winners}
For any correct process $p_i$ and round $r$, if $p_i$ computes $\mathit{winners}_r$ at line~\ref{code:Wcompute}, then :
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 $\mathit{winners}_r$ is exactly $\Winners_r$.
\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 $\mathit{winners}_r$. \\
Lets consider a correct process $p_i$ that reach line~\ref{code:Wcompute} to compute $\winners[r]$. \\
By program order, $p_i$ must have executed $\APPEND_i(r)$ at line~\ref{code:submit-proposition} before, which implies by \Cref{def:closed-round} that round $r$ is closed at that point. So by \Cref{def:winner-invariant}, $\Winners_r$ is defined. \\
By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\_,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at line~\ref{code:Wcompute} after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\_,r)$ such that
\[
\mathit{winners}_r = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r
\winners[r] = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r
\]
\end{proof}
@@ -195,7 +195,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\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 $\mathit{winners}_r$ at line~\ref{code:Wcompute}. It implies that, by \Cref{lem:winners}, $r$ is closed and $\mathit{winners}_r = \Winners_r$. \\
Let take a correct process $p_i$ that compute $M$ at line~\ref{code:Mcompute-dl}. That implies that $p_i$ has defined $\winners r$ at line~\ref{code:Wcompute}. It implies that, by \Cref{lem:winners}, $r$ is closed and $\winners_r = \Winners_r$. \\
By \Cref{lem:eventual-closure}, for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. By \Cref{lem:unique-proposal}, each winner $j$ invokes at most one $\RBcast(PROP, S^{(j)}, \langle r, j \rangle)$, so $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined. Hence, when $p_i$ computes
\[
M^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r.
@@ -210,17 +210,17 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\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 $\mathit{unordered}$. Since $p_i$ is correct, it continues executing the main loop.
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 (\mathit{unordered} \setminus \mathit{ordered})$. At that iteration, for some round $r$, process $p_i$ constructs $S$ containing $m$ and invokes $\RBcast(PROP, S, \langle r, i \rangle)$ at line~\ref{code:submit-proposition}.
Consider any iteration of the loop where $p_i$ executes line~\ref{code:Sconstruction} while $m \in (\unordered \setminus \ordered)$. At that iteration, for some round $r$, process $p_i$ constructs $S$ containing $m$ and invokes $\RBcast(PROP, S, \langle r, i \rangle)$ at line~\ref{code:submit-proposition}.
We distinguish two cases:
\begin{itemize}
\item \textbf{Case 1: $p_i$ is a winner.} If $p_i \in \Winners_r$ for this round $r$, then by \Cref{def:winner-invariant} and program order, $p_i$ has invoked $\RBcast(PROP, S, \langle r, i \rangle)$ with $m \in S$, and the lemma holds with $j = i$.
\item \textbf{Case 2: $p_i$ is not a winner.} If $p_i \notin \Winners_r$, then by the \RB \emph{Validity} property, all correct processes eventually \textsf{rdeliver} $p_i$'s message. By line~\ref{code:receivedConstruction}, each correct process $p_k$ adds $m$ to its own $\mathit{unordered}$ set. Hence every correct process will eventually attempt to broadcast $m$ in some subsequent round.
\item \textbf{Case 2: $p_i$ is not a winner.} If $p_i \notin \Winners_r$, then by the \RB \emph{Validity} property, all correct processes eventually \rdeliver $p_i$'s message. By line~\ref{code:receivedConstruction}, each correct process $p_k$ adds $m$ to its own $\unordered$ set. Hence every correct process will eventually attempt to broadcast $m$ in some subsequent round.
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 (\mathit{unordered} \setminus \mathit{ordered})$ when $p_j$ constructs its proposal $S$ at line~\ref{code:Sconstruction} for round $r'$. Hence $p_j$ invokes $\RBcast(PROP, S, \langle r', j \rangle)$ with $m \in S$.
Since there are infinitely many rounds and finitely many processes, and by \Cref{lem:nonempty} every closed round has at least one winner, there must exist a round $r'$ and a correct process $p_j \in \Winners_{r'}$ such that $m \in (\unordered \setminus \ordered)$ when $p_j$ constructs its proposal $S$ at line~\ref{code:Sconstruction} for round $r'$. Hence $p_j$ invokes $\RBcast(PROP, S, \langle r', j \rangle)$ with $m \in S$.
\end{itemize}
In both cases, there exists a round and a winner whose proposal includes $m$.
@@ -265,7 +265,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\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 (\mathit{ordered} \setminus \mathit{delivered})$. So a $\ABdeliver^{(B)}()$ which delivers $m$ can't occur.
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}