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

typo et quelques lemmes

Browse Source
This commit is contained in:
Amaury JOLY
2026-02-17 14:30:31 +01:00
parent 921dd502e3
commit 268c30a112
8 changed files with 266 additions and 234 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -4,7 +4,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
% 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)$.
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}
@@ -19,7 +19,7 @@ Each process $p_i$ maintains:
\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).
% \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}
@@ -28,7 +28,6 @@ Each process $p_i$ maintains:
\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
@@ -43,18 +42,17 @@ Each process $p_i$ maintains:
\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 $r_{max} \leftarrow \max(\{ r' : \exists j,\ (j,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 $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]))$}
\State $r \gets r + 1$
\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
\EndWhile
\EndFunction
\end{algorithmic}
\end{algorithm}
@@ -65,8 +63,8 @@ Each process $p_i$ maintains:
\begin{algorithmic}[1]
\Function{ABdeliver}{}
\State $r \gets \current$
\State $P \gets \READ()$
\If{$\forall j : (j, \PROVEtrace(r)) \not\in P$}
\State $P_r \gets \{(j,r): (j,r) \in \READ()\}$
\If{$P_r = \emptyset$}
\State \Return $\bot$
\EndIf
\State $\APPEND(r)$; $P \gets \READ()$
@@ -88,10 +86,14 @@ Each process $p_i$ maintains:
% ------------------------------------------------------------------------------
\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{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$. \\
@@ -101,60 +103,58 @@ 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.
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{Base.} For a closed round $r=0$, the set $\{r' \in \mathcal{R},\ r' < r\}$ 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$.
\emph{Induction.} Assume the lemma is true for round $r\geq 0$, we prove it for round $r+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$.
Assume $r+1$ is closed and by \cref{def:first-append} $\APPEND^{(\star)}(r+1)$ be the earliest $\APPEND(r+1)$ in the DL linearization $H$.
By Lemma 1, after an $\APPEND(r)$ were in $H$, any later $\PROVE(r)$ will be invalid also, a process’s program order is preserved in $H$.
There are two possibilities for where $\APPEND^{(\star)}(k+1)$ is invoked.
There are two possibilities for where $\APPEND^{(\star)}(r+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.
\item \textbf{Case Algorithm B :}
Some process executes the loop (lines B6-10) and invokes $\PROVE(r+1);\APPEND^{(\star)}(r+1)$ at line B8. Let $p_i$ be this process.
Immediately before line B8, line B7 sets $r\leftarrow r+1$, so the previous loop iteration targeted $r$. 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{(i) $p_i$ is not in its first loop iteration.}
In the previous iteration, $p_i$ executed $\PROVE_i(r)$ at B8, followed (in program order) by $\APPEND_i(r)$.
If round $r$ wasn't closed when $p_i$ execute $\PROVE_i(r)$ at B8, then the condition at B6 would be true hence the tuple $(i, r)$ should be visible in P which implies that $p_i$ should leave the loop at round $r$, contradicting the assumption that $p_i$ is now executing another iteration.
Since the tuple is not visible, the $\PROVE_i(r)$ was invalid which implies by definition that an $\APPEND(r)$ already exists in $H$. Thus in this case $r$ 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.
\item \emph{(ii) $p_i$ is in its first loop iteration.}
To compute the value $r_{max}$, $p_i$ must have observed one or many $(\_ , r+1)$ in $P$ at B2/B3, issued by some processes (possibly different from $p_i$). Let's call $p_j$ the issuer of the first $\PROVE_j(r+1)$ in the linearization $H$. \\
When $p_j$ executed $P \gets \READ()$ at B2 and compute $r_{max}$ at B3, he observed no tuple $(\_,r+1)$ in $P$ because he's the issuer of the first one. So when $p_j$ executed the loop (B6–B10), he run it for the round $r$, didn't seen any $(j,r)$ in $P$ at B6, and then executed the first $\PROVE_j(r+1)$ at B8 in a second iteration. \\
If round $r$ wasn't closed when $p_j$ execute $\PROVE_j(r)$ at B8, then the $(j, r)$ will be in $P$ and the condition at B6 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 (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.
\item \textbf{Case Algorithm C :}
Some process invokes $\APPEND(r+1)$ at C7. Let $p_i$ be this process.
Line C7 is guarded by the condition at C5, 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 B8, he observed no tuple $(\_,r+1)$ in $P$ at B6 because he's the issuer of the first one. By the same reasoning as in the Case Algorithm B (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.
\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$.
In all cases, $r+1$ closed implies $r$ closed. By induction on $r$, if the lemma is true for a closed $r$ then it is true for a closed $r+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) \}
\Winners_r \triangleq \{ j : \PROVE_j(r) \prec \APPEND^\star(r) \}
\]
as the unique set of winners of round $r$.
called the unique set of winners of round $r$.
\end{definition}
\begin{lemma}[Invariant view of closure]\label{lem:closure-view}
@@ -162,15 +162,15 @@ If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$,
\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)$.
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$ 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.
Consider any correct process $p_i$ that invokes $\READ()$ after $\APPEND^\star(r)$ in the DL linearization. Since $\APPEND^\star(r)$ invalidates all subsequent $\PROVE(r)$, the set of valid tuples $(\_,r)$ retrieved by a $\READ()$ after $\APPEND^\star(r)$ is fixed and identical across all correct processes.
Therefore, for any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\_,\PROVEtrace(r))$ in their \DL view.
\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 :
For any correct process $p_i$ and round $r$, if $p_i$ computes $W_r$ at line C8, then :
\begin{itemize}
\item $\Winners_r$ is defined;
\item the computed $W_r$ is exactly $\Winners_r$.
@@ -178,11 +178,11 @@ If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$,
\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
Lets consider a correct process $p_i$ that reach line C8 to compute $W_r$. \\
By program order, $p_i$ must have executed $\APPEND_i(r)$ at C7 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 C7 after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\_,r)$ such that
\[
W_r = \{ j : (j,\PROVEtrace(r)) \in P \} = \{j : \PROVE^{(j)}(r) \prec \APPEND^\star(r) \} = \Winners_r
W_r = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r
\]
\end{proof}
@@ -195,58 +195,50 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\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)$.
There exists a process $p_i$ who's the issuer of the earliest $\APPEND^{(\star)}(r)$ in the DL linearization $H$. By program order, $p_i$ must have previously invoked $\PROVE_i(r)$ before invoking $\APPEND^{(\star)}(r)$ at B8. 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)$.
There exists a process $p_i$ that invoked $\APPEND^{(\star)}(r)$ at C7. Line C7 is guarded by the condition at C4, which ensures that $p$ observed some $(\_,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$.
Let $r$ be a closed round, 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$.
By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the DL linearization. \\
By \Cref{lem:append-prove}, at least one process must have invoked a valid $\PROVE(r)$ before $\APPEND^{(\star)}(r)$. Hence, there exists at least one $p_j$ such that $p_j$ invoked $\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)$
For any closed round $r$, $\forall i \in \Winners_r$, process $p_i$ must have invoked a $\RBcast(S^{(i)}, r, i)$ and hence any correct will eventually 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 $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.
Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $i \in \Winners_r$, there exist a valid $\PROVE_i(r)$ such that $\PROVE_i(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order, if $i$ invoked a valid $\PROVE_i(r)$ at line B8 he must have invoked $\RBcast(S^{(i)}, r, i)$ directly before.
Let take a correct process $p_j$, by \RB \emph{Validity}, every correct process eventually receives $i$'s \RB message for round $r$, which sets $\prop[r][i]$ to a non-$\bot$ value at line A3.
\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
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 unique set of messages proposed by the winners of round $r$.
as the 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$.
If a correct process $p_i$ define $M_r$ at line C12, 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$.
Let take a correct process $p_i$ that computes $M_r$ at line C12. 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 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$.
By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line C12 where $p_i$ computes $M_r$ is guarded by the condition at C9, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, $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}
@@ -258,14 +250,14 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\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
For any round $r$, for any correct processes $p_i$ that execute C12, 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$. \\
Let take a correct process $p_i$ that compute $M_r$ at line C12. That implies that $p_i$ has defined $W_r$ at line C8. 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.
@@ -275,17 +267,17 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\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.
\RBcast(S, r, j)\quad\text{for same S 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.
Fix a correct process $p_i$ that invokes $\ABbroadcast(m)$ and eventually exits the loop (B6–B10) 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 1:} $p_i$ exits the loop because $(i, 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 B8 before invoking $\PROVE_i(r)$. By line B4, $m \in S$. Hence there exist a closed round $r$ and $p_i$ is a correct process such that $i\in\Winners_r$. Hence, $i$ invokes $\RBcast(S, r, i)$ 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$.
\item \textbf{Case 2:} $p_i$ exits the loop because $\exists j, r': (j, r') \in P \wedge m \in \prop[r'][j]$. In this case, by \Cref{lem:winners-propose} and \Cref{lem:unique-proposal} $p_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
@@ -295,22 +287,22 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\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.
A correct process which invokes $\ABbroadcast(m)$, eventually exits 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).
Consider a correct process $p_i$ that invokes $\ABbroadcast(m)$. The statement is true if $\exists r_1$ such that $r_1 \geq r_{max}$ and if $(i, r_1) \in P$; or if $\exists r_2$ such that $r_2 \geq r_{max}$ and if $\exists j: (j, 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}$.
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 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 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 \Cref{alg:rb-handler} and sets $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line A2).
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 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: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 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)$.
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)$.
\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$.
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]
@@ -319,11 +311,11 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\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
By \Cref{lem:eventual-closure}, when $p_q$ computes $M_r$ at line C12, $\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.
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 a correct process includes $m$. At each invocation of $m' = \ABdeliver()$, $m'$ is added to $\delivered$ until $M_r \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}
@@ -333,7 +325,7 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\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.
When $\ABdeliver^{(A)}()$ occurs, by program order and because it reached line C18 to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reached line C13 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 delivers $m$ can't occur.
\end{proof}
\begin{lemma}[Total order]\label{lem:total-order}
@@ -341,7 +333,7 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\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
Consider a correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exists a closed rounds $r'_1$ and $r'_2$ and correct processes $k_1 \in \Winners_{r'_1}$ and $k_2 \in \Winners_{r'_2}$ such that
\[
\RBcast(S_1, r'_1, k_1)\quad\text{with}\quad m_1\in S_1,
\]
@@ -351,20 +343,20 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
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 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 $ 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_{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(\_)$.
\item \textbf{Case 2:} $r_1 = r_2$. By \Cref{lem:convergence}, any correct process that computes $M_{r_1}$ at line C12 computes the same set of messages $\Messages_{r_1}$. By line C13 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$.
For any two distints 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
Let take $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$ such that $r_1 \leq 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,
\]
@@ -378,38 +370,36 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\end{proof}
\begin{theorem}[FIFO-\ARB]
Under the assumed \DL synchrony and \RB reliability, the algorithm implements FIFO Atomic Reliable Broadcast.
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.
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.
First, by \Cref{lem:bcast-termination}, if a correct process invokes $\ABbroadcast(m)$, then it eventually returns from this invocation.
Moreover, \Cref{lem:validity} states that if a correct process invokes $\ABbroadcast(m)$, then every correct process that invokes $\ABdeliver()$ infinitely often eventually delivers $m$.
This gives the usual Validity property of $\ARB$.
Concerning Integrity and No-duplicates, the construction only ever delivers messages that have been obtained from the underlying \RB primitive.
By the Integrity property of \RB, every such message was previously \RBcast by some process, so no spurious messages are delivered.
Concerning Integrity and No-duplicates, the construction only ever delivers messages that have been obtained from 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.
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.
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.
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).
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.
\xspace
\paragraph{DenyList as a deterministic state machine.}
Without anonymity, the \DL specification defines a
@@ -434,36 +424,16 @@ Which are cover by our FIFO-\ARB specification.
\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.
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 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:
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.
\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