diff --git a/Recherche/BFT-ARBover/6_BFT_ARB/index.tex b/Recherche/BFT-ARBover/6_BFT_ARB/index.tex index e46df61..3543f1e 100644 --- a/Recherche/BFT-ARBover/6_BFT_ARB/index.tex +++ b/Recherche/BFT-ARBover/6_BFT_ARB/index.tex @@ -21,7 +21,7 @@ We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ \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 : +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. @@ -29,7 +29,7 @@ There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that : \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, \PROVEtrace(x)) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$. +\paragraph{READ Liveness.} Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, \PROVEtrace(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$. @@ -54,20 +54,20 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au \] \begin{algorithmic}[1] - + % \renewcommand{\algletter}{} \begin{algorithm}[H] \caption{t-BFT-DL implementation using multiple DL objects} % \caption{\BFTAPPEND} \Function{$\BFTAPPEND$}{x} - \For{\textbf{each } $U \in \mathcal{U}$ st $i \in U$} + \For{\textbf{each } $U \in \mathcal{U}$ st $i \in U$} \State $DL_U.\APPEND(x)$ \EndFor \EndFunction \vspace{1em} - + % \caption{\BFTPROVE} \Function{$\BFTPROVE$}{x} \State $state \gets false$ @@ -78,7 +78,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au \EndFunction \vspace{1em} - + % \caption{\BFTREAD} \Function{$\BFTREAD$}{$\bot$} \State $results \gets \emptyset$ @@ -90,7 +90,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au \end{algorithm} \end{algorithmic} -\begin{lemma}[BFT-PROVE Validity] +\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} @@ -98,13 +98,13 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au 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$.} + \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 DL9 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} @@ -126,19 +126,19 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au 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}[READ Liveness] - Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, \PROVEtrace(x)) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$. +\begin{lemma}[BFT-READ Liveness] + Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, \PROVEtrace(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, \PROVEtrace(x)) \in R$ implie that $\exists U^\star \in \mathcal{U}$ such that $(i, \PROVEtrace(x)) \in R^{U^\star}$ with $R^{U^\star}$ the result of $DL_{U^\star}.\READ()$. By \textbf{READ Validity} $(i, \PROVEtrace(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, \PROVEtrace(x)) \in R \implies \exists \BFTPROVE^{(i)}(x)$ \end{proof} -\begin{lemma}[READ Anti-Flickering] +\begin{lemma}[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} @@ -147,14 +147,14 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au 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 + Therefore \[ \bigcup_U R_2^U \subseteq \bigcup_U R_1^U \implies R_2 \subseteq R_1 \] \end{proof} -\begin{lemma}[READ Safety] +\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, \PROVEtrace(x))$ \end{lemma} @@ -191,9 +191,9 @@ Each process $p_i$ maintains the following local variables: \State $Y[j]$ \Comment{Set of $n$ \BFTDL{}} \end{algorithmic} -\renewcommand{\algletter}{D} +\renewcommand{\algletter}{A} \begin{algorithm}[H] - \caption{ABroadcast$(m)$} + % \caption{ABroadcast$(m)$} \begin{algorithmic}[1] \Function{ABroadcast}{$m$} % \State $r \gets \current$ @@ -201,13 +201,13 @@ Each process $p_i$ maintains the following local variables: \For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$} \Statex \Comment{PROPOSAL PHASE} \State $\RBcast(i, \texttt{PROP}, S, r)$ - \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r \gets \{j: (j, \PROVEtrace(x)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$ + \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r \gets \{j: (j, \PROVEtrace(r)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$ \Statex \Comment{COMMIT PHASE} \State \textbf{for each} $j \in W_r$ \textbf{do} $Y[j].\BFTAPPEND(r)$ \State $\RBcast(i, \texttt{COMMIT}, r)$ \State \textbf{wait} until $|\resolved[r]| \geq n - f$ \Statex \Comment{X PHASE} - \State $W_r \gets \{j: (j, \PROVEtrace(x)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$ + \State $W_r \gets \{j: (j, \PROVEtrace(r)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$ \If{$\exists r' \in \mathcal{R}, j \in W_{r'} : m \in \prop[r'][j]$} \Comment{any process $j$ submited $m$ in any round $r'$} \State \textbf{break} \EndIf @@ -216,17 +216,17 @@ Each process $p_i$ maintains the following local variables: \end{algorithmic} \end{algorithm} -\renewcommand{\algletter}{C} +\renewcommand{\algletter}{B} \begin{algorithm}[H] - \caption{ADeliver$(m)$} + % \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 \{j: (j, \PROVEtrace(x)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$ - \If{$\exists j \in W_r,\ \prop[r][j] = \bot$} + \State $W_r \gets \{j: (j, \PROVEtrace(r)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$ + \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]$ @@ -240,9 +240,9 @@ Each process $p_i$ maintains the following local variables: \end{algorithmic} \end{algorithm} -\renewcommand{\algletter}{E} +\renewcommand{\algletter}{C} \begin{algorithm}[H] - \caption{RB handlers} + % \caption*{RB handlers} \begin{algorithmic}[1] \Upon{$Rdeliver(j, \texttt{PROP}, S, r)$} \State $\received \gets \received \cup \{S\}$ @@ -251,7 +251,7 @@ Each process $p_i$ maintains the following local variables: \EndUpon \vspace{1em} - + \Upon{$Rdeliver(j, \texttt{COMMIT}, r)}$ \State $\resolved[r] \gets \resolved[r] \cup \{j\}$ \EndUpon @@ -259,19 +259,86 @@ Each process $p_i$ maintains the following local variables: \end{algorithm} \begin{definition}[BFT Closed round for $i$] - Given $Seq^{(i)}$ the linearization of the $\BFTDL$ $Y[i]$, 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^{(i)}$. + Given $Seq^{(i)}$ the linearization of the $\BFTDL$ $Y[i]$, 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^{(i)}$. Let call $\BFTAPPEND(r)^\star$ the $(n-f)^{th}$ $\BFTAPPEND(r)$. \end{definition} -\begin{definition}[BFT Closed round] +\begin{definition}[BFT Closed round]\label{def:bft-closed-round} A round $r \in \mathcal{R}$ is \emph{closed} iff for all process $p_i$, $r$ is closed in $\Seq^{(i)}$. \end{definition} \subsection{Proof of correctness} -\begin{lemma}[BFT Stable round closure] - % If a round $r$ is closed by a correct process, +\begin{lemma}[BFT Stable round closure]\label{lem: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{lemma} +\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^{(i)}$. 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 $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} + \begin{theorem} The algorithm implements a BFT Atomic Reliable Broadcast. \end{theorem} diff --git a/Recherche/BFT-ARBover/main.pdf b/Recherche/BFT-ARBover/main.pdf index e5495b5..6ee776c 100644 Binary files a/Recherche/BFT-ARBover/main.pdf and b/Recherche/BFT-ARBover/main.pdf differ