diff --git a/Recherche/BFT-ARBover/6_BFT_ARB/index.tex b/Recherche/BFT-ARBover/6_BFT_ARB/index.tex index 414a26a..4cf662c 100644 --- a/Recherche/BFT-ARBover/6_BFT_ARB/index.tex +++ b/Recherche/BFT-ARBover/6_BFT_ARB/index.tex @@ -72,143 +72,82 @@ There are three operations: $\BFTVOTE(j, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r \begin{proof} Fix $t < |M|$. Let \[ - \mathcal{T} \triangleq \{\, T \subseteq M \mid |T| = t \,\}. + \mathcal{T} = \{\, 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 + \Pi_M(DL_T) = S_T = M \setminus T \qquad\text{and}\qquad - \Pi_V(DL_T) \triangleq V. + \Pi_V(DL_T) = V. \] Let \[ - K \triangleq \{\, DL_T \mid T \in \mathcal{T} \,\}, + K = \{\, 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} + \State $K \gets \{DL_T : T \subseteq M, |T|=t\}$ + \Function{BFTAPPEND}{x} - \If{$p_i \not\in \Pi_M$} + \If{$p_i \notin 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)$ + \For{\textbf{each } $DL_T \in K$} + \State $DL_T.\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$ + \If{$p_i \notin V$} + \State \Return $\bot$ + \EndIf + \State $state \gets false$ + \For{\textbf{each } $DL_T \in K$} + \State $state \gets state \textbf{ OR } DL_T.\PROVE(x)$ \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$ + \For{\textbf{each } $DL_T \in K$} + \State $results \gets results \cup DL_T.\READ()$ \EndFor \State \Return $results$ \EndFunction - \vspace{1em} - \end{algorithmic} + \end{algorithmic} + + \paragraph{BFT-APPEND Validity.} Let $A\subseteq M$ be the set of distinct issuers that invoked a valid $\BFTAPPEND(x)$ Suppose by contradiction that there exists $T\in\mathcal{T}$ with $A\cap S_T=\emptyset$. Since $S_T=M\setminus T$, this implies $A\subseteq T$, hence $|A|\le |T|=t$, contradicting $|A|\ge t+1$. - \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. + \paragraph{BFT-PROVE Validity.} 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 a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$. - \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$. - + \noindent\textbf{Case (i): $i\notin V$.} + For every $T\in\mathcal{T}$, we configured $\Pi_V(DL_T)=V$, hence the induced operation $DL_T.\PROVE(x)$ is invalid by \textbf{PROVE Validity} of $\DL$. Therefore $op$ is invalid. + \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. + \noindent\textbf{Case (ii): $|A|\ge t+1$ and $i\in V$.} Fix any $T\in\mathcal{T}$. By BFT-APPEND Validity, $A\cap S_T\neq\emptyset$. Pick $j\in A\cap S_T$. Since $j\in S_T$, the call $\BFTAPPEND^{(j)}(x)$ triggers $DL_T.\APPEND(x)$, and because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, this induces a valid $DL_T.\APPEND(x)$ that appears before the induced $DL_T.\PROVE(x)$. By \textbf{PROVE Validity} of $\DL$, the induced $DL_T.\PROVE(x)$ is invalid. As this holds for every $T\in\mathcal{T}$, there is \emph{no} component $DL_T$ where $\PROVE(x)$ is valid, so $op$ is invalid. + + \smallskip + \noindent\textbf{Case (iii): $|A|\le t$ and $i\in V$.} + By BFT-APPEND Validity, there exists $T^\star\in\mathcal{T}$ such that $A\cap S_{T^\star}=\emptyset$, i.e., $A\subseteq T^\star$. For any $j\in A$, we have $j\notin S_{T^\star}$, so $\BFTAPPEND^{(j)}(x)$ does \emph{not} call $DL_{T^\star}.\APPEND(x)$. Hence no valid $DL_{T^\star}.\APPEND(x)$ appears before the induced $DL_{T^\star}.\PROVE(x)$. Since also $i\in V=\Pi_V(DL_{T^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{T^\star}.\PROVE(x)$ is valid. Therefore, there exists a component with a valid $\PROVE(x)$, so by the lifting convention $op$ is valid. + + \smallskip + Combining the cases yields the claimed characterization of invalidity. + + \paragraph{BFT-PROVE Anti-Flickering.} Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i\in V$ that is \emph{invalid} in $\Seq$. + By BFT-PROVE Validity, since $i\in V$, this implies that there exist at least $t+1$ \emph{distinct} processes in $M$ that invoked a \emph{valid} $\BFTAPPEND(x)$ before $op$ in $\Seq$. Let $A\subseteq M$ denote that set, with $|A|\ge t+1$. + + Fix any $T\in\mathcal{T}$ and $DL_T$ with $\Pi_M(DL_T)=S_T=M\setminus T$. By BFT-APPEND Validity, we have $A\cap S_T\neq\emptyset$. Pick $j\in A\cap S_T$. Since $j\in S_T$, the call $\BFTAPPEND^{(j)}(x)$ triggers a call $DL_T.\APPEND(x)$. Moreover, because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, the induced $DL_T.\APPEND(x)$ appears before the induced $DL_T.\PROVE(x)$ of $op$ in the projection $\Seq_T$. + + Hence, in $\Seq_T$, there exists a \emph{valid} $DL_T.\APPEND(x)$ that appears before the $DL_T.\PROVE(x)$ induced by $op$. By \textbf{PROVE Validity} the base $\DL$ object, the induced $DL_T.\PROVE(x)$ is therefore \emph{invalid} in $\Seq_T$. + + Now let $op'=\BFTPROVE(x)$ be any invocation such that $op\prec op'$ in $\Seq$. Fix again any $T\in\mathcal{T}$. Hence, the $DL_T.\PROVE(x)$ induced by $op'$ appears after the $DL_T.\PROVE(x)$ induced by $op$ in $\Seq_T$. Since the induced $DL_T.\PROVE(x)$ of $op$ is invalid, by \textbf{PROVE Anti-Flickering} of $\DL$, \emph{every} subsequent $DL_T.\PROVE(x)$ in $\Seq_T$ is invalid. + + As this holds for every $T\in\mathcal{T}$, there is no component $DL_T$ in which the induced $\PROVE(x)$ of $op'$ is valid. \end{proof} diff --git a/Recherche/BFT-ARBover/main.pdf b/Recherche/BFT-ARBover/main.pdf index c3c2995..14f5972 100644 Binary files a/Recherche/BFT-ARBover/main.pdf and b/Recherche/BFT-ARBover/main.pdf differ