redaction des lemmes + preuve

Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex

@@ -57,7 +57,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
     \If{$\ordered \setminus \delivered = \emptyset$}{
       \Return{$\bot$}
     }
-    let $m$ be the first element in $\ordered \setminus \delivered$\;\nllabel{code:adeliver-extract}
+    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$}
   }
@@ -160,7 +160,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 \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
+  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]
   \]
@@ -227,18 +227,11 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 \end{proof}
 
 \begin{lemma}[Broadcast Termination]\label{lem:bcast-termination}
-  A correct process which invokes $\ABbroadcast(m)$, eventually exits the function and returns.
+  A correct process which invokes $\ABbroadcast(m)$ eventually exits the function and returns.
 \end{lemma}
 
 \begin{proof}[Proof]
-  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).
-
-  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(PROP, S, \langle \_, i \rangle)$ 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: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)$.
+  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}
@@ -273,15 +266,15 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 \end{lemma}
 
 \begin{proof}
-  Consider a correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exists a closed rounds $r'_1$ and $r'_2$ and correct processes $k_1 \in \Winners_{r'_1}$ and $k_2 \in \Winners_{r'_2}$ such that
+  Consider a correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exists a closed rounds $r_1$ and $r_2$ and correct processes $k_1 \in \Winners_{r_1}$ and $k_2 \in \Winners_{r_2}$ such that
   \[
-    \RBcast(PROP, S_1, \langle r'_1, k_1 \rangle)\quad\text{with}\quad m_1\in S_1,
+    \RBcast(PROP, S_1, \langle r_1, k_1 \rangle)\quad\text{with}\quad m_1\in S_1,
   \]
   \[
-    \RBcast(PROP, S_2, \langle r'_2, k_2 \rangle)\quad\text{with}\quad m_2\in S_2.
+    \RBcast(PROP, S_2, \langle r_2, k_2 \rangle)\quad\text{with}\quad m_2\in S_2.
   \]
 
-  Let consider three cases :
+  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$.
     
@@ -291,30 +284,12 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
   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 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 $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(PROP, S_1, \langle r_1, k_1 \rangle)\quad\text{with}\quad m_1\in S_1,
-  \]
-  \[
-    \RBcast(PROP, S_2, \langle r_2, k_2 \rangle)\quad\text{with}\quad m_2\in S_2.
-  \]
-
-  By program order, $p_i$ must have invoked $\RBcast(PROP, S_1, \langle r_1, i \rangle)$ before $\RBcast(PROP, S_2, \langle r_2, i \rangle)$. By \Cref{lem:unique-proposal}, any process invokes at most one $\RBcast(PROP, S, \langle r, i \rangle)$ 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.
+\begin{theorem}[\ARB]
+Under the assumed $\DL$ synchrony and $\RB$ reliability, the algorithm implements 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 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$.
@@ -327,11 +302,9 @@ Under the assumed $\DL$ synchrony and $\RB$ reliability, the algorithm implement
 
   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.
+  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}