update

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

@@ -54,36 +54,19 @@ Otherwise, the operation is valid.
 
 \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.
 
-% \subsubsection{BFT DenyList}
+\subsubsection{t-BFT-GE}
-% We consider a \DL object that satisfies the following properties despite the presence of up to $f$ byzantine processes:
-% \begin{itemize}
-%   \item \textbf{Termination.} Every operation $\APPEND(x)$, $\PROVE(x)$, and $\READ()$ invoked by a correct process eventually returns.
-%   \item \textbf{APPEND/PROVE/READ Validity.} The preconditions for invoking $\APPEND(x)$, $\PROVE(x)$, and $\READ()$ are respected (cf. \#2.2). The return values of these operations conform to the sequential specification of the \DL object.
-%   \item \textbf{APPEND Justification.} For any element $x$, if an operation $\APPEND(x)$ invoked by a correct process completes successfully, then there exists at least one valid $\PROVE(x)$ operation that that precedes this $\APPEND(x)$ in the \DL linearization.
-%   \item \textbf{PROVE Anti-Flickering.} Once an element $x$ has been appended to the \DL by any process, all subsequent invocations of $\PROVE(x)$ by any process return ``invalid''.
-% \end{itemize}
 
-% \subsection{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.
 
-% We consider a Group Election object ($\GE[r]$) per round $r \in \mathcal{R}$ with the following properties.
+There are three operations: $\BFTVOTE(j, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$.
 
-% There are three operations: $\CANDIDATE(r), \CLOSE(r), \READGE()$ such that :
+\paragraph{Termination.} Every operation $\BFTVOTE(i, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$ invoked by a correct process always returns.
 
-% \begin{itemize}
+\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$.
-%   \item \textbf{Termination} 
-% \end{itemize}
 
-\subsubsection{t-out-of-n Threshold Random Number Generator}
+\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.
 
-We consider a function that with t out of n shares any process can reconstruct a deterministic random number $s$ from a given $t$. There are two operations $\SUBMIT(r), \RETRIEVE(r)$ such that :
+\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)$. 
-
-\begin{itemize}
-  \item \textbf{Agreement.} For all $s_1, s_2$ returned by two distinct invokations $\RETRIEVE(r)$, if $s_1, s_2 \neq \bot$ then $s_1 = s_2$.
-  \item \textbf{t-threshold.} If there exist a $s$ returned from an invokation of $\RETRIEVE(r)$. $s \neq \bot$ iff a set of process $X \subseteq \Pi$ such that $|X| \geq t$ invoke $\SUBMIT(r)$.
-  \item \textbf{non-forgability.} It's computationally infeasibile for the adversary to compute a valid value $s$ frome a given $r$ if he corrupt $f < t$ process.
-  \item \textbf{liveness.} If all correct processes invoke $\SUBMIT(r)$, then any correct process invoking $\RETRIEVE(r)$ eventually returns a value $s \neq \bot$.
-  \item \textbf{injectivity.} For any two distinct rounds $r_1 \neq r_2$, the values $s_1, s_2$ returned by $\RETRIEVE(r_1)$ and $\RETRIEVE(r_2)$ respectively are distinct.
-\end{itemize}
 
 
 \subsection{Algorithm}
@@ -96,98 +79,33 @@ Each process $p_i$ maintains the following local variables:
   \State $\delivered \gets \emptyset$
   \State $\prop[r][j] \gets \bot, \forall r, j$
   \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}{D}
+\renewcommand{\algletter}{A}
 \begin{algorithm}[H]
-  \caption{\ABbroadcast}\label{alg:ab-cast}
+  \caption{ABbroadcast$(m)$}
-  \begin{algorithmic}[1]
+    \begin{algorithmic}[1]
-    \Function{ABcast}{$m$}
+        \State $r \gets \current$
-    \State $S \gets (\received \setminus \delivered) \cup \{m\}$
+        \For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$}
-    \State $\RBcast(prop, S, r, i)$
+            \State $\RBcast(i, PROP, m, r)$
-    \State \textbf{wait until} $|X_r| \geq f+1$
+            \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r = \BFTRESULT[r]$
-    \State $\sigma_r \gets \COMBINE(X_r)$
+            \State $\BFTCOMMIT(r)$
-    \State $\PROVE(\sigma_r); \APPEND(\sigma_r);$
+            \State \textbf{wait} until $|\resolved[r]| \geq n - f$
-    \State $\RBcast(submit, S, \sigma_r, r, i)$
+            \State $W \gets \BFTRESULT[r]$
-    \EndFunction
+            \If{$i \in W_r \vee (\exists j, r': j \in W_r \wedge \prop[r'][j] \ni m)$}
-  \end{algorithmic}
+                \State \textbf{break}
-\end{algorithm}
+            \EndIf
-
+        \EndFor
-\renewcommand{\algletter}{E}
+    \end{algorithmic}
-\begin{algorithm}[H]
-  \caption{\ABdeliver}\label{alg:ab-deliver}
-  \begin{algorithmic}[1]
-    \Function{$\ABdeliver$}{}
-      \State $r \gets \current; \sigma_r \gets \resolved[r];$
-      \If{$\sigma_r == \bot$}
-        \State \Return $\bot$
-      \EndIf
-      \State $P \gets \READ()$
-      \If{$\forall j : (j,prove(\sigma_r)) \not\in P$}
-        \State \Return $\bot$
-      \EndIf
-      \State $\APPEND(\sigma_r); P \gets \READ();$
-      \State $W_r \gets \{j : (j, \PROVEtrace(\sigma_r)) \in P\}$
-      \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)[0]$
-      \State $\delivered \gets \delivered \cup \{m\};$
-      \If{$M_r \setminus \delivered = \emptyset$}
-        \State $\current \gets \current + 1;$
-      \EndIf
-      \State \Return $m$
-    \EndFunction
-  \end{algorithmic}
-
-\end{algorithm}
-
-\renewcommand{\algletter}{F}
-\begin{algorithm}[H]
-  \caption{RBreceived handler}\label{alg:rb-handler}
-  \begin{algorithmic}[1]
-    \Function{RBrcvd}{$prop, S_j, r_j, j$}
-    \If{$r_j \geq r$}
-    \State $\prop[r_j][j] = S_j$
-    \State $\sigma^i_{r_j} \gets \SHARE(r_j)$
-    \State $send_j(r, \sigma^i_{r_j})$
-    \EndIf
-    \EndFunction
-  \end{algorithmic}
 \end{algorithm}
 
 
-\renewcommand{\algletter}{G}
+% \subsection{Example execution}
-\begin{algorithm}[H]
-  \caption{RBreceived handler}\label{alg:rb-handler-2}
-  \begin{algorithmic}[1]
-    \Function{RBrcvd}{$submit, S_j, \sigma_{r_j}, r_j, j$}
-      \If{$\VERIFY(r_j, \sigma_{r_j})$}
-        \State $\resolved[r_j] \gets \sigma_{r_j}$
-      \EndIf
-    \EndFunction
-  \end{algorithmic}
-\end{algorithm}
 
-
+% \begin{figure}[H]
-\renewcommand{\algletter}{H}
+%   \centering
-\begin{algorithm}[H]
+%   \input{diagrams/classic_seq.tex}
-  \caption{Share received handler}\label{alg:share-handler}
+%   \caption{Expected Executions of P1 willing to send a message at round r}
-  \begin{algorithmic}[1]
+% \end{figure}
-    \Function{received}{$r_j, \sigma^j_{r_j}, j$}
-      \If{$r_j == r$}
-        \State $X_r \gets X_r \cup \sigma^j_{r}$
-      \EndIf
-    \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}

Recherche/BFT-ARBover/main.tex

@@ -80,6 +80,12 @@
 \newcommand{\GE}{\mathsf{GE}}
 \newcommand{\BFTDL}{\mathsf{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}}
+
+
 \crefname{theorem}{Theorem}{Theorems}
 \crefname{lemma}{Lemma}{Lemmas}
 \crefname{definition}{Definition}{Definitions}