update

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 $p \not\in \Pi_V$; \textbf{or}
-  \item $x \in S$, where $S$ is a predefined set.
+  \item At least $t+1$ valid $\BFTAPPEND(x)$ appears before $op$ in $\Seq$.
-\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$.
 \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,127 @@ 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} = \{\, 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) = S_T = M \setminus T
+    \qquad\text{and}\qquad
+    \Pi_V(DL_T) = V.
+    \]
+    Let
+    \[
+    K = \{\, DL_T \mid T \in \mathcal{T} \,\},
+    \qquad\text{so that}\qquad
+    |K| = \binom{|M|}{t}.
+    \]
+
+    \begin{algorithmic}
+        \State $K \gets \{DL_T : T \subseteq M, |T|=t\}$
+
+        \Function{BFTAPPEND}{x}
+            \If{$p_i \notin M$}
+                \State \Return \textbf{false}
+            \EndIf
+            \For{\textbf{each } $DL_T \in K$} 
+                \State $DL_T.\APPEND(x)$
+            \EndFor
+            \State \Return \textbf{true}
+        \EndFunction
+        
+        \Function{BFTPROVE}{x}
+            \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
+        
+        \Function{BFTREAD}{}
+            \State $results \gets \emptyset$
+            \For{\textbf{each } $DL_T \in K$}
+                \State $results \gets results \cup DL_T.\READ()$
+            \EndFor
+            \State \Return $results$
+        \EndFunction
+    \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$.
+
+    \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$.
+
+    \smallskip
+    \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
+    \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}
+
+
+\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 +194,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$
+        \Function{ABroadcast}{$m$}
-        \For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$}
+            \State $r \gets \current$
-            \State $\RBcast(i, PROP, m, r)$
+            \State $S \gets (\received \cup \{m\}$)
-            \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r = \BFTRESULT[r]$
+            \For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$}
-            \State $\BFTCOMMIT(r)$
+                \State $\RBcast(i, PROP, S, r)$
-            \State \textbf{wait} until $|\resolved[r]| \geq n - f$
+                \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r = \BFTRESULT[r]$
-            \State $W \gets \BFTRESULT[r]$
+                \State $\BFTCOMMIT(r)$
-            \If{$i \in W_r \vee (\exists j, r': j \in W_r \wedge \prop[r'][j] \ni m)$}
+                \State \textbf{wait} until $|\resolved[r]| \geq n - f$
-                \State \textbf{break}
+                \State $W_r \gets \BFTRESULT[r]$
-            \EndIf
+                \If{$i \in W_r \vee (\exists j, r': j \in W_r \wedge \prop[r'][j] \ni m)$}
-        \EndFor
+                    \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}
 

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{\CANDIDATE}{\textsf{VOTE}}
-\newcommand{\CLOSE}{\mathsf{CLOSE}}
+\newcommand{\CLOSE}{\textsf{COMMIT}}
-\newcommand{\READGE}{\mathsf{READGE}}
+\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{\BFTGE}{\textsf{BFT\text{-}GE}}
-\newcommand{\BFTVOTE}{\mathsf{BFT\text{-}VOTE}}
+\newcommand{\BFTVOTE}{\textsf{BFT\text{-}VOTE}}
-\newcommand{\BFTCOMMIT}{\mathsf{BFT\text{-}COMMIT}}
+\newcommand{\BFTCOMMIT}{\textsf{BFT\text{-}COMMIT}}
-\newcommand{\BFTRESULT}{\mathsf{BFT\text{-}RESULT}}
+\newcommand{\BFTRESULT}{\textsf{BFT\text{-}RESULT}}
 
 
 \crefname{theorem}{Theorem}{Theorems}