diff --git a/Recherche/BFT-ARBover/6_BFT_ARB/index.tex b/Recherche/BFT-ARBover/6_BFT_ARB/index.tex index 17f7d60..f517efa 100644 --- a/Recherche/BFT-ARBover/6_BFT_ARB/index.tex +++ b/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} -% 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} +\subsubsection{t-BFT-GE} -% \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} -% \item \textbf{Termination} -% \end{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$. -\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 : - -\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} +\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{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} - \begin{algorithmic}[1] - \Function{ABcast}{$m$} - \State $S \gets (\received \setminus \delivered) \cup \{m\}$ - \State $\RBcast(prop, S, r, i)$ - \State \textbf{wait until} $|X_r| \geq f+1$ - \State $\sigma_r \gets \COMBINE(X_r)$ - \State $\PROVE(\sigma_r); \APPEND(\sigma_r);$ - \State $\RBcast(submit, S, \sigma_r, r, i)$ - \EndFunction - \end{algorithmic} -\end{algorithm} - -\renewcommand{\algletter}{E} -\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} + \caption{ABbroadcast$(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 + \end{algorithmic} \end{algorithm} -\renewcommand{\algletter}{G} -\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} +% \subsection{Example execution} - -\renewcommand{\algletter}{H} -\begin{algorithm}[H] - \caption{Share received handler}\label{alg:share-handler} - \begin{algorithmic}[1] - \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} +% \begin{figure}[H] +% \centering +% \input{diagrams/classic_seq.tex} +% \caption{Expected Executions of P1 willing to send a message at round r} +% \end{figure} diff --git a/Recherche/BFT-ARBover/main.pdf b/Recherche/BFT-ARBover/main.pdf index 87cfe12..9e4758a 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 e2a82b5..1e868c9 100644 --- a/Recherche/BFT-ARBover/main.tex +++ b/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}