diff --git a/Recherche/BFT-ARBover/6_BFT_ARB/index.tex b/Recherche/BFT-ARBover/6_BFT_ARB/index.tex index f517efa..414a26a 100644 --- a/Recherche/BFT-ARBover/6_BFT_ARB/index.tex +++ b/Recherche/BFT-ARBover/6_BFT_ARB/index.tex @@ -32,27 +32,22 @@ 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 : $\PROVE(x), \APPEND(x), \READ(x)$ such that : +There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that : -\paragraph{Termination.} Every operation $\APPEND(x)$, $\PROVE(x)$, and $\READ()$ invoked by a correct process always returns. +\paragraph{Termination.} Every operation $\BFTAPPEND(x)$, $\BFTPROVE(x)$, and $\BFTREAD()$ invoked by a correct process always returns. -\paragraph{APPEND Validity.} The invocation of $\APPEND(x)$ by a process $p$ is valid if: +\paragraph{APPEND Validity.} The invocation of $\BFTAPPEND(x)$ by a correct process $p_i$ is valid iff $i \in \Pi_M$. Otherwise the operation is invalid. + +\paragraph{PROVE Validity.} If the invocation of a $op = \BFTPROVE(x)$ by a correct process $p$ is not valid, then: \begin{itemize} - \item $p \in \Pi_M \subseteq \Pi$; \textbf{and} - \item $x \in S$, where $S$ is a predefined set. -\end{itemize} -Otherwise, the operation is invalid. - -\paragraph{PROVE Validity.} If the invocation of a $op = \PROVE(x)$ by a correct process $p$ is not valid, then: -\begin{itemize} - \item $p \not\in \Pi_V \subseteq \Pi$; \textbf{or} - \item At least $t+1$ valid $\APPEND(x)$ appears before $op$ in $\Seq$. + \item $p \not\in \Pi_V$; \textbf{or} + \item At least $t+1$ valid $\BFTAPPEND(x)$ appears before $op$ in $\Seq$. \end{itemize} Otherwise, the operation is valid. -\paragraph{PROVE Anti-Flickering.} If the invocation of a operation $op = \PROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\PROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid. +\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 Validity.} The invocation of $op = \READ()$ by a process $p$ returns the list of valid invocations of $\PROVE$ that appears before $op$ in $\Seq$ along with the names of the processes that invoked each operation. +\paragraph{READ Validity.} The invocation of $op = \BFTREAD()$ by a process $p$ returns the list of valid invocations of $\BFTPROVE$ that appears before $op$ in $\Seq$ along with the names of the processes that invoked each operation. \subsubsection{t-BFT-GE} @@ -68,6 +63,188 @@ There are three operations: $\BFTVOTE(j, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r \paragraph{Election.} If at least $f+1$ correct processes invoked a valid $\BFTVOTE(j, r)$ for the same process $j$ then $j$ will be enventually included in the set $W_r$ returned by $\BFTRESULT(r)$. +\subsection{DL $\Rightarrow$ t-BFT-DL} + +\begin{lemma} + For any fixed value $t < |M|$, multiple DenyList Object can be used to implement a t-Byzantine Fault Tolerant DenyList Object. +\end{lemma} + +\begin{proof} + Fix $t < |M|$. Let + \[ + \mathcal{T} \triangleq \{\, T \subseteq M \mid |T| = t \,\}. + \] + For each $T \in \mathcal{T}$, we instantiate one DenyList object $DL_T$ whose authorization sets are + \[ + \Pi_M(DL_T) \triangleq S_T \triangleq M \setminus T + \qquad\text{and}\qquad + \Pi_V(DL_T) \triangleq V. + \] + Let + \[ + K \triangleq \{\, DL_T \mid T \in \mathcal{T} \,\}, + \qquad\text{so that}\qquad + |K| = \binom{|M|}{t}. + \] + + + % The system consists of a set of $\Pi$ processes, we define a subset of processes $M \subseteq \Pi$ which are authorized to invoke the $\BFTAPPEND$ operation and a subset of processes $V \subseteq \Pi$ which are authorized to invoke the $\BFTPROVE$ operation. + + % There exist $K$ a set of $\binom{|M|}{t+1}$ DenyList objects denoted by $DL_1, DL_2, \dots, DL_{|K|}$ such that each DenyList $DL_k$ is associated with a unique subset of processes $S_k \subseteq M$ of size $t+1$. + + \begin{algorithmic} + \State $K \gets \{DL_1, DL_2, \dots, DL_{|K|}\}$ \Comment{Set of DenyList objects} + \vspace{1em} + \Function{BFTAPPEND}{x} + \If{$p_i \not\in \Pi_M$} + \State \Return \textbf{false} + \EndIf + \For{\textbf{each } $DL_k \in K$ \textbf{such that} $p_i \in S_k$} + \State $DL_k.\APPEND(x)$ + \EndFor + \State \Return \textbf{true} + \EndFunction + \vspace{1em} + \Function{BFTPROVE}{x} + \For{\textbf{each } $DL_k \in K$} + \State $state \gets DL_k.\PROVE(x) || state$ + \EndFor + \State \Return $state$ + \EndFunction + \vspace{1em} + \Function{BFTREAD}{} + \State $results \gets \emptyset$ + \For{\textbf{each } $DL_k \in K$} + \State $res \gets DL_k.\READ()$ + \State $results \gets results \cup res$ + \EndFor + \State \Return $results$ + \EndFunction + \vspace{1em} + \end{algorithmic} + + \textbf{APPEND Validity.} A process $p_i$ not in $\Pi_M$ who invokes $\BFTAPPEND(x)$ will never be able to submit a valid $\APPEND(x)$ to any DenyList $DL_k$ since each DenyList $DL_k$ is associated with a unique subset of processes $S_k \subseteq M$. Otherwise, if $p_i \in \Pi_M$, then any invocation of $\BFTAPPEND(x)$ are valid. + + \textbf{PROVE Validity.} + Let set $op$ a particular invocation of $\BFTPROVE(x)$ by $p_i$. + \begin{itemize} + \item Case 1: If $p_i \not\in \Pi_V$, then $op$ is invalid since $p_i$ is not authorized to invoke $\PROVE$ operation in any DL. + \item Case 2: If at least $t+1$ valid $\BFTAPPEND(x)$ submitted by $t+1$ distincts processus appears before $op$ in $\Seq$, then for any set $S_k$ there is at least one process in $S_k$ who submitted a valid $\APPEND(x)$ before $op$. Therefore, $op$ will be invalid since all $DLs$ will be locked on the value $x$ by the PROVE Validity of DL Object. + \end{itemize} + Otherwise $op$ is always valid. + + \textbf{PROVE Anti-Flickering.} + Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i \in \Pi_V$ that is \emph{invalid} in $\Seq$. + By the \textbf{PROVE Validity} of t-$\BFTDL$, this implies that there exist at least $t+1$ \emph{valid} + invocations of $\BFTAPPEND(x)$ by $t+1$ distinct processes that appear before $op$ in $\Seq$. + Let $A \subseteq \Pi_M$ be the set of these (distinct) issuers, with $|A|\ge t+1$. + + Consider any DenyList object $DL_k \in K$, associated with a subset $S_k \subseteq M$ of size $|S_k|=t+1$. + Since $K$ contains \emph{all} $(t+1)$-subsets of $M$ and $|A|\ge t+1$, we have + \[ + S_k \cap A \neq \emptyset. + \] + Let $p_j \in S_k \cap A$. By construction of $\BFTAPPEND$, the invocation $\BFTAPPEND^{(j)}(x)$ triggers + the operation $DL_k.\APPEND(x)$ (because $p_j \in S_k$), and since $\BFTAPPEND^{(j)}(x) \prec op$ in $\Seq$, + this $DL_k.\APPEND(x)$ appears before the operation $DL_k.\PROVE(x)$ induced by $op$ in the linearization $\Seq_k$ + of $DL_k$. + + Therefore, in $\Seq_k$ there exists a valid $\APPEND(x)$ before the invocation $DL_k.\PROVE(x)$ induced by $op$. + By the \textbf{PROVE Validity} property of $\DL$, this implies that the invocation $DL_k.\PROVE(x)$ induced by $op$ + is \emph{invalid}. Since this holds for every $k \in K$, all component $\PROVE$ operations of $op$ are invalid. + + Now consider any invocation $op'=\BFTPROVE(x)$ that appears after $op$ in $\Seq$. + For each $k$, the invocation of $DL_k.\PROVE(x)$ induced by $op'$ appears after the one induced by $op$ in $\Seq_k$. + By the \textbf{PROVE Anti-Flickering} property of $\DL$, once a $\PROVE(x)$ is invalid in $\Seq_k$, + all subsequent $\PROVE(x)$ in $\Seq_k$ are invalid. Hence, for all $k$, the $\PROVE(x)$ induced by $op'$ is invalid, + which implies that $op'$ is invalid at the t-$\BFTDL$ level. + This proves the \textbf{PROVE Anti-Flickering} property for the construction. + + \medskip + \textbf{READ Validity.} + Let $op=\BFTREAD()$ be an invocation by a correct process $p$. + The algorithm executes, for each $DL_k \in K$, a read $res_k \gets DL_k.\READ()$ and returns + \[ + results \;=\; \bigcup_{k\in K} res_k. + \] + By \textbf{READ Validity} of each $\DL$, $res_k$ contains exactly the valid invocations of $\PROVE$ + that appear before $DL_k.\READ()$ in $\Seq_k$, together with the identities of their issuers. + + We show that $results$ is exactly the set of valid invocations of $\BFTPROVE$ that appear before $op$ in $\Seq$. + + \smallskip + \emph{(i) Soundness (no false positives).} + Take any entry $(j,\PROVE(x)) \in results$. Then $(j,\PROVE(x)) \in res_k$ for some $k$, + hence the invocation $DL_k.\PROVE(x)$ by $p_j$ is valid and appears before $DL_k.\READ()$ in $\Seq_k$. + In particular, there is no valid $DL_k.\APPEND(x)$ before that $DL_k.\PROVE(x)$ in $\Seq_k$ + (otherwise $DL_k.\PROVE(x)$ would be invalid by \textbf{PROVE Validity} of $\DL$). + + Assume by contradiction that the corresponding invocation $\BFTPROVE^{(j)}(x)$ is invalid in $\Seq$. + Then, by \textbf{PROVE Validity} of t-$\BFTDL$, there exist at least $t+1$ valid invocations of $\BFTAPPEND(x)$ + by $t+1$ distinct processes before $\BFTPROVE^{(j)}(x)$ in $\Seq$. + As in the argument used for \textbf{PROVE Anti-Flickering}, this implies that for every $DL_{k'} \in K$, + there exists a valid $DL_{k'}.\APPEND(x)$ before the $DL_{k'}.\PROVE(x)$ induced by $\BFTPROVE^{(j)}(x)$. + Therefore the induced $DL_k.\PROVE(x)$ would be invalid, contradicting $(j,\PROVE(x)) \in res_k$. + Hence $\BFTPROVE^{(j)}(x)$ is valid and appears before $op$ in $\Seq$. + + \smallskip + \emph{(ii) Completeness (no omissions).} + Consider a valid invocation $\BFTPROVE^{(j)}(x)$ that appears before $op=\BFTREAD()$ in $\Seq$. + Let $A$ be the set of distinct processes that invoked a valid $\BFTAPPEND(x)$ before $\BFTPROVE^{(j)}(x)$ in $\Seq$. + Since $\BFTPROVE^{(j)}(x)$ is valid in t-$\BFTDL$, we have $|A| \le t$. + + Because $K$ contains all subsets $S_k \subseteq M$ of size $t+1$ and $t<|M|$, + there exists some $S_k$ such that + \[ + S_k \cap A = \emptyset. + \] + For this $DL_k$, none of the $\BFTAPPEND(x)$ invocations issued by processes in $A$ + triggers $DL_k.\APPEND(x)$ (since $\BFTAPPEND$ calls $DL_k.\APPEND(x)$ only for $k$ with issuer in $S_k$). + Thus, there is no valid $DL_k.\APPEND(x)$ before the invocation $DL_k.\PROVE(x)$ induced by $\BFTPROVE^{(j)}(x)$. + By \textbf{PROVE Validity} of $\DL$, the induced $DL_k.\PROVE(x)$ is valid. + Moreover, since $\BFTPROVE^{(j)}(x) \prec \BFTREAD()$ in $\Seq$, this induced $\PROVE(x)$ appears before + $DL_k.\READ()$ in $\Seq_k$, and therefore it is included in $res_k$. + Hence $(j,\PROVE(x)) \in results$. + + Combining (i) and (ii), $results$ contains exactly the valid invocations of $\BFTPROVE$ + that appear before $op$ in $\Seq$, together with the identities of their issuers. + This proves the \textbf{READ Validity} property. + +\end{proof} + + +\subsection{t-BFT-DL $\Rightarrow$ t-BFT-GE} + +\begin{lemma} + For any fixed value $r \in S$, multiple BFT-DenyList Object can be used to implement a BFT-Group Election Object. +\end{lemma} + +\begin{proof} + \begin{algorithmic} + \State $Y[i]$ \Comment{Is a set of $n$ $\BFTDL$ with $\Pi_M = \Pi_V = \Pi$} + + \vspace{1em} + + \Function{BFTVOTE}{j, r} + + \EndFunction + \vspace{1em} + + \Function{BFTCOMMIT}{r} + \EndFunction + \vspace{1em} + \Function{BFTRESULT}{r} + \State $Z \gets \emptyset$ + \For{\textbf{each } $j \in \Pi$} + \If{$|\{(\_, \PROVEtrace(\_, r)) \in Y[j].\BFTREAD(r)\}| \geq n-f$} + \State $P \gets \BFTREAD()$ + \State \Return $\{j : (j, \PROVEtrace), \}$ + \EndIf + \EndFor + \EndFunction + \vspace{1em} + \end{algorithmic} +\end{proof} \subsection{Algorithm} @@ -78,29 +255,73 @@ Each process $p_i$ maintains the following local variables: \State $\received \gets \emptyset$ \State $\delivered \gets \emptyset$ \State $\prop[r][j] \gets \bot, \forall r, j$ - \State $X_r \gets \bot, \forall r$ +% \State $X_r \gets \bot, \forall r$ \State $W_r \gets \bot, \forall r$ \State $\resolved[r] \gets \bot, \forall r$ \end{algorithmic} \renewcommand{\algletter}{A} \begin{algorithm}[H] - \caption{ABbroadcast$(m)$} + \caption{ABroadcast$(m)$} \begin{algorithmic}[1] - \State $r \gets \current$ - \For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$} - \State $\RBcast(i, PROP, m, r)$ - \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r = \BFTRESULT[r]$ - \State $\BFTCOMMIT(r)$ - \State \textbf{wait} until $|\resolved[r]| \geq n - f$ - \State $W \gets \BFTRESULT[r]$ - \If{$i \in W_r \vee (\exists j, r': j \in W_r \wedge \prop[r'][j] \ni m)$} - \State \textbf{break} - \EndIf - \EndFor + \Function{ABroadcast}{$m$} + \State $r \gets \current$ + \State $S \gets (\received \cup \{m\}$) + \For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$} + \State $\RBcast(i, PROP, S, r)$ + \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r = \BFTRESULT[r]$ + \State $\BFTCOMMIT(r)$ + \State \textbf{wait} until $|\resolved[r]| \geq n - f$ + \State $W_r \gets \BFTRESULT[r]$ + \If{$i \in W_r \vee (\exists j, r': j \in W_r \wedge \prop[r'][j] \ni m)$} + \State \textbf{break} + \EndIf + \EndFor + \EndFunction \end{algorithmic} \end{algorithm} +\renewcommand{\algletter}{B} +\begin{algorithm}[H] + \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 \BFTRESULT[r]$ + \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]$ + \State $m \gets \ordered(M_r \setminus \delivered)[0]$ \Comment{Set $m$ as the smaller message not already delivered} + \State $\delivered \leftarrow \delivered \cup \{m\}$ + \If{$M_r \setminus \delivered = \emptyset$} \Comment{Check if all messages from round $r$ have been delivered} + \State $\current \leftarrow \current + 1$ + \EndIf + \State \textbf{return} $m$ + \EndFunction + \end{algorithmic} +\end{algorithm} + +\renewcommand{\algletter}{C} +\begin{algorithm}[H] + \caption{RB handlers} + \begin{algorithmic}[1] + \Function{Rreceived}{j, PROP, S, r} + \State $\received \gets \received \cup \{S\}$ + \State $\prop[r][j] \gets S$ + \State $\BFTVOTE(j, r)$ + \EndFunction + + \vspace{1em} + + \Function{Rreceived}{j, COMMIT, r} + \State $\received[r] \cup \{j\}$ + \EndFunction + \end{algorithmic} +\end{algorithm} % \subsection{Example execution} diff --git a/Recherche/BFT-ARBover/main.pdf b/Recherche/BFT-ARBover/main.pdf index 9e4758a..c3c2995 100644 Binary files a/Recherche/BFT-ARBover/main.pdf and b/Recherche/BFT-ARBover/main.pdf differ diff --git a/Recherche/BFT-ARBover/main.tex b/Recherche/BFT-ARBover/main.tex index 1e868c9..3b2650d 100644 --- a/Recherche/BFT-ARBover/main.tex +++ b/Recherche/BFT-ARBover/main.tex @@ -50,6 +50,12 @@ \newcommand{\PROVE}{\textsf{PROVE}} \newcommand{\PROVEtrace}{\textsf{prove}} \newcommand{\READ}{\textsf{READ}} + +\newcommand{\BFTAPPEND}{\textsf{BFT\text{-}APPEND}} +\newcommand{\BFTPROVE}{\textsf{BFT\text{-}PROVE}} +\newcommand{\BFTREAD}{\textsf{BFT\text{-}READ}} + + \newcommand{\ABbroadcast}{\textsf{AB-broadcast}} \newcommand{\ABdeliver}{\textsf{AB-deliver}} \newcommand{\RBcast}{\textsf{RB-cast}} @@ -59,9 +65,9 @@ \newcommand{\Messages}{\mathsf{Messages}} \newcommand{\ABlisten}{\textsf{AB-listen}} -\newcommand{\CANDIDATE}{\mathsf{CANDIDATE}} -\newcommand{\CLOSE}{\mathsf{CLOSE}} -\newcommand{\READGE}{\mathsf{READGE}} +\newcommand{\CANDIDATE}{\textsf{VOTE}} +\newcommand{\CLOSE}{\textsf{COMMIT}} +\newcommand{\READGE}{\textsf{RESULT}} \newcommand{\SHARE}{\mathsf{SHARE}} \newcommand{\COMBINE}{\mathsf{COMBINE}} @@ -78,12 +84,12 @@ \newcommand{\Seq}{\mathsf{Seq}} \newcommand{\GE}{\mathsf{GE}} -\newcommand{\BFTDL}{\mathsf{BFT\text{-}DL}} +\newcommand{\BFTDL}{\textsf{BFT\text{-}DL}} -\newcommand{\BFTGE}{\mathsf{BFT\text{-}GE}} -\newcommand{\BFTVOTE}{\mathsf{BFT\text{-}VOTE}} -\newcommand{\BFTCOMMIT}{\mathsf{BFT\text{-}COMMIT}} -\newcommand{\BFTRESULT}{\mathsf{BFT\text{-}RESULT}} +\newcommand{\BFTGE}{\textsf{BFT\text{-}GE}} +\newcommand{\BFTVOTE}{\textsf{BFT\text{-}VOTE}} +\newcommand{\BFTCOMMIT}{\textsf{BFT\text{-}COMMIT}} +\newcommand{\BFTRESULT}{\textsf{BFT\text{-}RESULT}} \crefname{theorem}{Theorem}{Theorems}