update de la spéc de BFT-DL + preuve READ Liveness

Recherche/BFT-ARBover/6_BFT_ARB/index.tex

@@ -36,31 +36,15 @@ 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.
 
-% \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.} The invocation of $op = \BFTPROVE(x)$ by a correct process is valid iff there exist a set of correct process $C$ such that $\forall c \in C$, $c$ invoke $op_2 = \BFTAPPEND(x)$ with $op_2 \prec op_1$ and $|C| \leq t$
 
 \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 = \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.
+\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{Local consistency.} For all correct process $p_i$ such that $p_i$ invoke an valid $\BFTPROVE(x)$ before a $P \gets \BFTREAD()$ operation in his local execution. Then the set of valid $\BFTPROVE(x)$ in $P$ must contain the previous valid $\BFTPROVE(x)$.
+\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$.
 
-\paragraph{Liveness} For all correct process $p_i$ such that $p_i$ invoke an invalid $\BFTPROVE(x)$ before a $P \gets \BFTREAD()$ operation in his local execution. Then the set of valid $\BFTPROVE(x)$ in $P$ must be the same for any $p_i$.
+\paragraph{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))$
-
-% \subsubsection{t-BFT-GE}
-
-% We consider a t-Byzantine Fault Tolerant Group Election Object (t-$\BFTGE[r]$) per round $r \in \mathcal{R}$ with the following properties.
-
-% There are three operations: $\BFTVOTE(j, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$.
-
-% \paragraph{Termination.} Every operation $\BFTVOTE(i, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$ invoked by a correct process always returns.
-
-% \paragraph{Stability.} If there exist at least $n-f$ invocations of $\BFTCOMMIT(r)$ by distincts processes and let call $\BFTCOMMIT(r)^\star$ the $(n-f)^{th}$ such invocation in the linearization of $\Seq$. Then any invocation of $\BFTRESULT(r)$ that appears after $\BFTCOMMIT(r)^\star$ in $\Seq$ returns the same set of processes $W_r$.
-
-% \paragraph{VOTE-Validity.} The invocation of $\BFTVOTE(j, r)$ by a correct process is not valid if $\BFTCOMMIT(r)^\star$ appears before in $\Seq$. Otherwise, the operation is valid.
-
-% \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}
 
@@ -79,44 +63,39 @@ There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that :
     \qquad\text{and}\qquad
     \Pi_V(DL_T) = V.
     \]
-    Let
+    
     \[
-    K = \{\, DL_U \mid U \in \mathcal{U} \,\},
+    |\mathcal{U}| = \binom{|M|}{|M| - t}.
-    \qquad\text{so that}\qquad
-    |U| = \binom{|M|}{|M| - t}.
     \]
 
     \begin{algorithmic}[1]
-        % \State $K \gets \{DL_T : T \subseteq M, |T|=t\}$
 
         \renewcommand{\algletter}{DL}
         \begin{algorithm}[H]
             \caption{\BFTAPPEND}
             \Function{$\BFTAPPEND$}{x}
-                \For{\textbf{each } $DL_U \in K$ such that $p_i \in U$} 
+                \For{\textbf{each } $U \in \mathcal{U}$ st $i \in U$} 
                 \State $DL_U.\APPEND(x)$
                 \EndFor
             \EndFunction
         \end{algorithm}
         
-        % \renewcommand{\algletter}{B}    
         \begin{algorithm}[H]
             \caption{\BFTPROVE}
             \Function{$\BFTPROVE$}{x}
                 \State $state \gets false$
-                \For{\textbf{each } $DL_U \in K$}
+                \For{\textbf{each } $U \in \mathcal{U}$}
                     \State $state \gets state \textbf{ OR } DL_U.\PROVE(x)$
                 \EndFor
                 \State \Return $state$
             \EndFunction
         \end{algorithm}
         
-        % \renewcommand{\algletter}{C}  
         \begin{algorithm}[H]
             \caption{\BFTREAD}
             \Function{$\BFTREAD$}{$\bot$}
                 \State $results \gets \emptyset$
-                \For{\textbf{each } $DL_U \in K$}
+                \For{\textbf{each } $U \in \mathcal{U}$}
                     \State $results \gets results \cup DL_U.\READ()$
                 \EndFor
                 \State \Return $results$
@@ -124,39 +103,39 @@ There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that :
         \end{algorithm}
     \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 $\BFTAPPEND(x)$ before $op$ in $\Seq$.
-
-    \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$.
 
     \begin{itemize}
-        % \item \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.
-        
         \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 \textbf{PROVE Validity} of $\DL$, the induced $DL_U.\PROVE(x)$ is invalid. As this holds for every $T\in\mathcal{T}$, there is \emph{no} component $DL_U$ where $\PROVE(x)$ is valid, so $op$ is invalid.
+        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$.}
-        Fix any $U\in\mathcal{U}$, 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 V=\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 by the lifting convention $op$ is valid.
+        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.
 
-    \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$.
+    \paragraph{BFT-PROVE Anti-Flickering.} Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$ that is \emph{invalid} in $\Seq$.
     By BFT-PROVE Validity, 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 $U\in\mathcal{U}$. We have $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND^{(j)}(x)$ triggers a call $DL_U.\APPEND(x)$. Moreover, because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, the induced $DL_U.\APPEND(x)$ appears before the induced $DL_U.\PROVE(x)$ of $op$ in the projection $\Seq_U$.
 
     Hence, in $\Seq_U$, there exists a \emph{valid} $DL_U.\APPEND(x)$ that appears before the $DL_U.\PROVE(x)$ induced by $op$. By \textbf{PROVE Validity} the base $\DL$ object, the induced $DL_U.\PROVE(x)$ is therefore \emph{invalid} in $\Seq_U$.
 
-    Now let $op'=\BFTPROVE(x)$ be any invocation such that $op\prec op'$ in $\Seq$. Fix again any $U\in\mathcal{U}$. Hence, the $DL_U.\PROVE(x)$ induced by $op'$ appears after the $DL_U.\PROVE(x)$ induced by $op$ in $\Seq_U$. Since the induced $DL_U.\PROVE(x)$ of $op$ is invalid, by \textbf{PROVE Anti-Flickering} of $\DL$, \emph{every} subsequent $DL_U.\PROVE(x)$ in $\Seq_U$ is invalid.
+    Let $op'=\BFTPROVE(x)$ be any invocation such that $op\prec op'$ in $\Seq$. Fix again any $U\in\mathcal{U}$. Hence, the $DL_U.\PROVE(x)$ induced by $op'$ appears after the $DL_U.\PROVE(x)$ induced by $op$ in $\Seq_U$. Since the induced $DL_U.\PROVE(x)$ of $op$ is invalid, by \textbf{PROVE Anti-Flickering} of $\DL$, \emph{every} subsequent $DL_U.\PROVE(x)$ in $\Seq_U$ is invalid.
 
     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.
     
-
+    \paragraph{READ Liveness.} 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}$.
-    \paragraph{Local consistency.}
     
-    \paragraph{Liveness.}
+    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)$
+
+    \paragraph{READ Anti-Flickering.}
+    
+    \paragraph{READ Safety.}
 
 \end{proof}
 
@@ -270,11 +249,3 @@ Each process $p_i$ maintains the following local variables:
         \EndFunction
     \end{algorithmic}
 \end{algorithm}
-
-% \subsection{Example execution}
-
-% \begin{figure}[H]
-%   \centering
-%   \input{diagrams/classic_seq.tex}
-%   \caption{Expected Executions of P1 willing to send a message at round r}
-% \end{figure}