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

refacto algo crash (todo preuve)

Browse Source
This commit is contained in:
Amaury JOLY
2026-03-02 15:10:18 +00:00
parent d9848967b8
commit 55fa76a272
4 changed files with 111 additions and 108 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -8,76 +8,66 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
Equivalently, there exists a time after which every $\PROVE(r)$ is invalid in $H$.
\end{definition}
\subsubsection{Variables}
Each process $p_i$ maintains:
\LinesNotNumbered
\begin{algorithm}
$\received \gets \emptyset$\; %\Comment{Messages received via \RB but not yet delivered}
$\delivered \gets \emptyset$\; %\Comment{Messages already delivered}
$\prop[r][j] \gets \bot,\ \forall r,j$\; %\Comment{Proposal from process $j$ for round $r$}
$\current \gets 0$\;
\end{algorithm}
% \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}
\LinesNumbered
\begin{algorithm}[H]
\caption{\RB handler (at process $p_i$)}\label{alg:rb-handler}
\Fn{RBreceived($S, r, j$)}{
$\received \leftarrow \received \cup \{S\}$\;\nllabel{code:receivedConstruction}
$\prop[r][j] \leftarrow S$\;\nllabel{code:prop-set} % \Comment{Record sender $j$'s proposal $S$ for round $r$}
\caption{ARB at process $p_i$}\label{alg:arb-crash}
% \SetAlgoLined
\SetKwBlock{LocalVars}{Local Variables:}{}
\LocalVars{
$\mathit{unordered} \gets \emptyset$,
$\mathit{ordered} \gets \epsilon$,
$\mathit{delivered} \gets \epsilon$\;
$\mathit{prop}[r][j] \gets \bot,\ \forall r,j$\;
}
\end{algorithm}
% \paragraph{} An \ABbroadcast$(m)$ chooses the next open round from the \DL view, proposes all pending messages together with the new $m$, disseminates this proposal via \RB, then executes $\PROVE(r)$ followed by $\APPEND(r)$ to freeze the winners of the round. The loop polls \DL until (i) some winner’s proposal includes $m$ in a \emph{closed} round and (ii) all winners' proposals for closed rounds are known locally, ensuring eventual inclusion and delivery.
\vspace{0.3em}
\begin{algorithm}[H]\label{alg:ABroadcast}
\caption{\ABbroadcast$(m)$ (at process $p_i$)}\label{alg:ab-bcast}
\Fn{ABbroadcast($m$)}{
$P \leftarrow \READ()$\;\nllabel{code:set-up-read} %\Comment{Fetch latest \DL state to learn recent $\PROVE$ operations}
$r_{max} \leftarrow \max(\{ r' : \exists j,\ (j,r') \in P \})$\;\nllabel{code:rmax-compute} %\Comment{Pick current open round}
$S \leftarrow (\received \setminus \delivered) \cup \{m\}$\;\nllabel{code:Sconstruction}
%\Comment{Propose all pending messages plus the new $m$}
\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}
$\RBcast(S, r, i)$; $\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition}
\vspace{1em}
$\mathit{winners}_r \gets \{(j,r): (j,r) \in \READ()\}$\;
\textbf{wait until} $\mathit{winners}_r \neq \emptyset$\;\nllabel{code:check-if-winners}
$r \gets r_{max} - 1$\;
\While{$((i, r) \not\in P\ \wedge (\nexists j, r': (j, r') \in P \wedge m \in \prop[r'][j]))$}{\nllabel{code:sumbited-check-loop}
$r \gets r + 1$\;\nllabel{code:round-increment}
$\RBcast(S, r, i)$; $\PROVE(r)$; $\APPEND(r)$;\;\nllabel{code:submit-proposition}
$P \leftarrow \READ()$\; % \Comment{Refresh local view of \DL}
$\APPEND(r)$\;\nllabel{code:append-read}
$W_r \gets \{ j : (j, r) \in \READ() \}$\;\nllabel{code:Wcompute}
\textbf{wait until} $\forall j \in W_r,\ \mathit{prop}[r][j] \neq \bot$\;\nllabel{code:check-winners-ack}
$M_r \gets \bigcup_{j \in W_r} \mathit{prop}[r][j]$\;\nllabel{code:Mcompute}
$\mathit{ordered} \leftarrow \mathit{ordered} \cdot \ordered(M_r)$\;\nllabel{code:next-msg-extraction}
}
}
\end{algorithm}
\begin{algorithm}[H]\label{alg:ADeliver}
\caption{\ABdeliver() at process $p_i$}\label{alg:delivery}
\Fn{ABdeliver($\bot$)}{
$r \gets \current$\;
$P_r \gets \{(j,r): (j,r) \in \READ()\}$ \;
\If{$P_r = \emptyset$}{\nllabel{code:check-if-winners}
\vspace{0.3em}
\Upon{$\ABbroadcast(m)$}{
$\mathit{unordered} \gets \mathit{unordered} \cup \{m\}$\;
}
\vspace{0.3em}
\Upon{$\textsf{rdeliver}(S, r, j)$ from process $p_j$}{
$\mathit{unordered} \leftarrow \mathit{unordered} \cup \{S\}$\;\nllabel{code:receivedConstruction}
$\mathit{prop}[r][j] \leftarrow S$\;\nllabel{code:prop-set}
}
\vspace{0.3em}
\Upon{$\ABdeliver()$}{
\If{$\mathit{ordered} \setminus \mathit{delivered} = \emptyset$}{
\Return{$\bot$}
}
$\APPEND(r)$; $P \gets \READ()$\; \nllabel{code:append-read}
$W_r \gets \{ j : (j, \PROVEtrace(r)) \in P \}$\;\nllabel{code:Wcompute}
\If{$\exists j \in W_r,\ \prop[r][j] = \bot$}{ \nllabel{code:check-winners-ack}
\Return{$\bot$}
}
$M_r \gets \bigcup_{j \in W_r} \prop[r][j]$\;\nllabel{code:Mcompute}
$m \gets \ordered(M_r \setminus \delivered)[0]$\;\nllabel{code:next-msg-extraction}
%\Comment{Set $m$ as the smaller message not already delivered}
$\delivered \leftarrow \delivered \cup \{m\}$\;
\If{$M_r \setminus \delivered = \emptyset$}{ %\Comment{Check if all messages from round $r$ have been delivered}
$\current \leftarrow \current + 1$
}
$m \gets (\mathit{ordered} \setminus \mathit{delivered})[0]$\;\nllabel{code:adeliver-extract}
$\mathit{delivered} \gets \mathit{delivered} \cdot m$\;
\Return{$m$}
}
\end{algorithm}
% ------------------------------------------------------------------------------
\end{algorithm}
\subsection{Correctness}
\begin{definition}[First APPEND]\label{def:first-append}
@@ -113,7 +103,7 @@ Each process $p_i$ maintains:
There are two possibilities for where $\APPEND^{(\star)}(r+1)$ is invoked.
\begin{itemize}
\item \textbf{Case Algorithm \ref{alg:ABroadcast} :}
\item \textbf{Case Algorithm \ref{alg:arb-crash} :}
Some process executes the loop at \ref{code:sumbited-check-loop} and invokes $\PROVE(r+1);\APPEND^{(\star)}(r+1)$ at line~\ref{code:submit-proposition}. Let $p_i$ be this process.
Immediately before line~\ref{code:submit-proposition}, line~\ref{code:round-increment} sets $r\leftarrow r+1$, so the previous loop iteration targeted $r$. We consider two sub-cases.
@@ -129,10 +119,10 @@ Each process $p_i$ maintains:
If round $r$ wasn't closed when $p_j$ execute $\PROVE_j(r)$ at \ref{code:submit-proposition}, then the $(j, r)$ will be in $P$ and the condition at \ref{code:sumbited-check-loop} should be true which implies that $p_j$ sould leave the loop at round $r$, contradicting the assumption that $p_j$ is now executing $\PROVE_j(r+1)$. In this case $r$ is closed.
\end{itemize}
\item \textbf{Case Algorithm \ref{alg:ADeliver} :}
\item \textbf{Case Algorithm \ref{alg:arb-crash} :}
Some process invokes $\APPEND(r+1)$ at \ref{code:append-read}. Let $p_i$ be this process.
Line~\ref{code:append-read} is guarded by the condition at \ref{code:check-if-winners}, which ensures that $p_i$ observed some $(\_,r+1)$ in $P$. Let $p_j$ be the issuer of the first $\PROVE_j(r+1)$ in the linearization $H$.
When $p_j$ executed $\PROVE_j(r+1)$ at \ref{code:submit-proposition}, he observed no tuple $(\_,r+1)$ in $P$ at \ref{code:check-if-winners} because he's the issuer of the first one. By the same reasoning as in the Case Algorithm \ref{alg:ABroadcast} (ii), $p_j$ must have observed that the round $r$ was closed.
When $p_j$ executed $\PROVE_j(r+1)$ at \ref{code:submit-proposition}, he observed no tuple $(\_,r+1)$ in $P$ at \ref{code:check-if-winners} because he's the issuer of the first one. By the same reasoning as in the Case Algorithm \ref{alg:arb-crash} (ii), $p_j$ must have observed that the round $r$ was closed.
% Line C7 is guarded by the presence of $\PROVE(r)$ in $P$ with $r=r+1$ (C5).
% Moreover, the local pointer $\textit{next}$ grow by increment of 1 and only advances after finishing the current round (C17), so if a process can reach $\textit{next}=r+1$ it implies that he has completed round $r$, which includes closing $r$ at C8 when $\PROVE(r)$ is observed.
% Hence $\APPEND^\star(r+1)$ implies a prior $\APPEND(r)$ in $H$, so $r$ is closed.
@@ -289,7 +279,7 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
Consider that there exists no round $r_1$ such that $p_i$ invokes a valid $\PROVE(r_1)$. In this case $p_i$ invokes infinitely many $\RBcast(S, \_, i)$ at line~\ref{code:submit-proposition} with $m \in S$ (line~\ref{code:Sconstruction}).\\
The assumption that no $\PROVE(r_1)$ invoked by $p$ is valid implies by \DL \emph{Validity} that for every round $r' \geq r_{max}$, there exists at least one $\APPEND(r')$ in the DL linearization, hence by \Cref{lem:nonempty} for every possible round $r'$ there at least a winner. Because there is an infinite number of rounds, and a finite number of processes, there exists at least one process $p_k$ that invokes infinitely many valid $\PROVE(r')$ and by extension infinitely many $\ABbroadcast(\_)$. By \RB \emph{Validity}, $p_k$ eventually receives $p_i$ 's \RB messages. Let call $t_0$ the time when $p_k$ receives $p_i$ 's \RB message. \\
At $t_0$, $p_k$ executes Algorithm \ref{alg:rb-handler} and sets $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line~\ref{code:receivedConstruction}).
At $t_0$, $p_k$ executes Algorithm \ref{alg:arb-crash} and sets $\mathit{received} \leftarrow \mathit{received} \cup \{S\}$ with $m \in S$ (line~\ref{code:receivedConstruction}).
For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \texttt{RReceived()}, $p_k$ must include $m$ in his proposal $S$ at line~\ref{code:Sconstruction} (because $m$ is pending in $j$'s $\received \setminus \delivered$ set). There exists a minimum round $r_2$ such that $p_k \in \Winners_{r_2}$ after $t_0$. By \Cref{lem:winners-propose}, eventually $\prop^{(i)}[r_2][k] \neq \bot$. By \Cref{lem:unique-proposal}, $\prop^{(i)}[r_2][k]$ is uniquely defined as the set $S$ proposed by $p_k$ at B6, which by \Cref{lem:inclusion} includes $m$. Hence eventually $m \in \prop^{(i)}[r_2][k]$ and $k \in \Winners_{r_2}$.
So if $p_i$ is a winner he satisfies the condition $(i, r_1) \in P$. And we show that if the first condition is never satisfied, the second one will eventually be satisfied. Hence either the first or the second condition will eventually be satisfied, and $p_i$ eventually exits the loop and returns from $\ABbroadcast(m)$.
@@ -437,19 +427,25 @@ Which are cover by our FIFO-\ARB specification.
\subsubsection{Example executions}
\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/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}
% \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

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

@@ -177,65 +177,72 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
\SetKwBlock{LocalVars}{Local Variables:}{}
\LocalVars{
$\texttt{unordered} \gets \emptyset$,
$\texttt{ordered} \gets \emptyset$,
$\texttt{delivered} \gets \emptyset$\;
$\prop[r][j] \gets \bot, \forall r, j \in \pi \times \mathbb{N}$\;
$\texttt{done}[r] \gets \emptyset,$
$\texttt{validate}[r] \gets \emptyset, \forall r \in \mathbb{N}$\;
% $\texttt{winners}[r] \gets \emptyset, \forall r$\;
$\mathit{unordered} \gets \emptyset$,
$\mathit{ordered} \gets \epsilon$,
$\mathit{delivered} \gets \epsilon$\;
$\mathit{prop}[r][j] \gets \bot, \forall j, r \in \Pi \times \mathbb{N}$\;
$\mathit{done}[r] \gets \emptyset, \forall r \in \mathbb{N}$\;
}
\vspace{1em}
\vspace{0.3em}
\For{$r = 1, 2, \ldots$}{
\textbf{wait until} $\texttt{unordered} \setminus \texttt{ordered} \neq \emptyset$\;
$S \gets \texttt{unordered} \setminus \texttt{ordered}$\;
\textbf{wait until} $\mathit{unordered} \setminus \mathit{ordered} \neq \emptyset$\;
$S \gets \mathit{unordered} \setminus \mathit{ordered}$;
$\RBcast(i, \texttt{PROP}, S, r)$\;
\textbf{wait until} $|\texttt{validate}(r)| > n - t$\;
$\texttt{validate}[r] \gets \texttt{validate}(r)$\;
\textbf{wait until} $|\textsf{validated}(r)| \geq n - t$\;
\ForEach{$j \in \Pi$}{
$\BFTAPPEND(\langle j, r\rangle)$\;
}
\ForEach{$j \in \Pi$}{
$\texttt{send}(j, \texttt{DONE}, r)$\;
$\textsf{send}(j, \texttt{DONE}, r)$\;
}
\textbf{wait until} $|\texttt{done}[r]| > n - t$\;
\textbf{wait until} $|\mathit{done}[r]| \geq n - t$\;
$\texttt{winners}[r] \gets \texttt{validate}(r)$\;
$\mathit{winners}[r] \gets \textsf{validated}(r)$\;
\textbf{wait until} $\forall j \in \texttt{winners}[r],\ \prop[r][j] \neq \bot$\;
$M \gets \bigcup_{j \in \texttt{winners}[r]} \prop[r][j]$\;\nllabel{code:Mcompute}
$\texttt{ordered} \gets \texttt{ordered} \cup \ordered(M)$\;
\textbf{wait until} $\forall j \in \mathit{winners}[r],\ \mathit{prop}[r][j] \neq \bot$\;
$M \gets \bigcup_{j \in \mathit{winners}[r]} \mathit{prop}[r][j]$\;\nllabel{code:Mcompute}
$\mathit{ordered} \gets \mathit{ordered} \cdot \ordered(M)$\;
}
\Fn{\texttt{validate}($r$)}{
\Return{$\{j: |\{k: (k, \PROVEtrace(r)) \in \BFTREAD()\}| \geq t+1\}$}\;
\vspace{0.3em}
\Fn{\textsf{validated}($r$)}{
\Return{$\{j: |\{k: (k, r) \in \BFTREAD()\}| \geq t+1\}$}\;
}
\Upon{$\textbf{ABCAST}(m)$}{
$\texttt{unordered} \gets \texttt{unordered} \cup \{m\}$\;
\vspace{0.3em}
\Upon{$\ABbroadcast(m)$}{
$\mathit{unordered} \gets \mathit{unordered} \cup \{m\}$\;
}
\Upon{$\texttt{rdeliver}(\texttt{PROP}, S, \langle j, r \rangle)$ from process $p_j$}{
$\texttt{unordered} \gets \texttt{unordered} \cup S$\;
$\prop[r][j] \gets S$\;
$\BFTPROVE(r)$\;
\vspace{0.3em}
\Upon{$\textsf{rdeliver}(\texttt{PROP}, S, \langle j, r \rangle)$ from process $p_j$}{
$\mathit{unordered} \gets \mathit{unordered} \cup S$;
$\mathit{prop}[r][j] \gets S$\;
$\BFTPROVE(\langle j, r\rangle)$\;
}
\Upon{$\texttt{receive}(\texttt{DONE}, r)$ from process $p_j$}{
$\texttt{done}[r] \gets \texttt{done}[r] \cup \{j\}$\;
\vspace{0.3em}
\Upon{$\textsf{receive}(\texttt{DONE}, r)$ from process $p_j$}{
$\mathit{done}[r] \gets \mathit{done}[r] \cup \{j\}$\;
}
\Upon{$\textbf{ADELIVER}()$}{
\If{$\texttt{ordered} \setminus \texttt{delivered} = \emptyset$}{
\vspace{0.3em}
\Upon{$\ABdeliver()$}{
\If{$\mathit{ordered} \setminus \mathit{delivered} = \emptyset$}{
\Return{$\bot$}
}
$m \gets \ordered(\texttt{ordered} \setminus \texttt{delivered})[0]$\;
$\texttt{delivered} \gets \texttt{delivered} \cup \{m\}$\;
let $m$ be the first message in $\mathit{ordered} \setminus \mathit{delivered}$\;
$\mathit{delivered} \gets \mathit{delivered} \cdot \{m\}$\;
\Return{$m$}
}

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

Binary file not shown.

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

@@ -61,7 +61,7 @@
\newcommand{\ABdeliver}{\textsf{ADeliver}}
\newcommand{\RBcast}{\textsf{RBroadcast}}
\newcommand{\RBreceived}{\textsf{RReceived}}
\newcommand{\ordered}{\textsf{ordered}}
\newcommand{\ordered}{\textsf{order}}
\newcommand{\Winners}{\mathsf{Winners}}
\newcommand{\Messages}{\mathsf{Messages}}
\newcommand{\ABlisten}{\textsf{AB-listen}}