diff --git a/Recherche/ALDLoverAB/algo/index.tex b/Recherche/ALDLoverAB/algo/index.tex index b7e5fc2..a17bc48 100644 --- a/Recherche/ALDLoverAB/algo/index.tex +++ b/Recherche/ALDLoverAB/algo/index.tex @@ -5,19 +5,22 @@ We consider a set of processes communicating asynchronously over reliable point- \item \textbf{\textit{delivered}}: the set of messages that have been ordered. \item \textbf{\textit{prop}[$r$][$j$]}: the proposal set announced by process $j$ at round $r$. It contains a set of messages that process $j$ claims to have received but not yet delivered. \item \textbf{\textit{winner}$^r$}: the set of processes that have issued a valid \texttt{PROVE} for round $r$, as observed through the registry. + \item \textbf{\textit{window}}: the list of the ids from the $f+1$ last rounds. \textit{window.pop()} remove the first value of the array. \textit{window.push(x)} append x as the last value of the array. \item \textbf{\texttt{RB-cast}$(\texttt{PROP}, S, r, j)$}: a reliable broadcast invocation that disseminates the proposal $S$ from process $j$ for round $r$. \item \textbf{\texttt{RB-delivered}$(\texttt{PROP}, S, r, j)$}: the handler invoked upon reception of a \texttt{RB-cast}, which stores the received proposal $S$ into $\textit{prop}[r][j]$. \item \textbf{\texttt{READ}()} : returns the current view of all valid operations stored in the DenyList registry. \item \textbf{\texttt{ordered}$(S)$}: returns a deterministic total order over a set $S$ of messages. + \item \textbf{\texttt{hash}$(T, r)$}: returns the identifier of the next round as a deterministic function of the delivered set $T$ and current round $r$. \end{itemize} \resetalgline \begin{algorithm} \caption{Atomic Broadcast with DenyList} - \begin{algorithmic}[1] + \begin{algorithmic}[1] \State $\textit{proves} \gets \emptyset$ \State $\textit{received} \gets \emptyset$ \State $\textit{delivered} \gets \emptyset$ + \State $\textit{window} \gets [\bot]^{f+1}$ \State $r_1 \gets 0$ \vspace{1em} @@ -29,31 +32,47 @@ We consider a set of processes communicating asynchronously over reliable point- % --- RB-delivered --- \State \nextalgline \textbf{RB-delivered}$_j(m)$ \State \nextalgline \hspace{1em} $\textit{received} \gets \textit{received} \cup \{m\}$ - \State \nextalgline \hspace{1em} \textbf{repeat until} $\textit{received} \setminus \textit{delivered} \neq \emptyset$ + \State \nextalgline \hspace{1em} \textbf{repeat while} $\textit{received} \setminus \textit{delivered} \neq \emptyset$ \State \nextalgline \hspace{2em} $S \gets \textit{received} \setminus \textit{delivered}$ + \State \nextalgline \hspace{2em} $\texttt{RB-broadcast}(\texttt{PROP}, S, r_1, j)$ \State \nextalgline \hspace{2em} $\textit{proves} \gets \texttt{READ}()$ - \State \nextalgline \hspace{2em} $r_2 \gets \max\{r : j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} + 1$ - \State \nextalgline \hspace{2em} $\texttt{RB-cast}(\texttt{PROP}, S, r_2, j)$ - \State \nextalgline \hspace{2em} $\texttt{PROVE}(r_2)$ + \State \nextalgline \hspace{2em} $\texttt{PROVE}[j](r_1)$ + % \State \nextalgline \hspace{2em} $r_1 \gets \max\{r : j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} + 1$ + + \vspace{0.5em} + \State \nextalgline \hspace{2em} $\texttt{APPEND}[j](r_1)$ + \State \nextalgline \hspace{2em} $S \gets \{1, ..., n\}$ + \State \nextalgline \hspace{2em} \textbf{repeat while} $|S| \leq n - f$ + \State \nextalgline \hspace{3em} \textbf{forall} $i \in S$ + \State \nextalgline \hspace{4em} \textbf{if} $\neg \texttt{PROVE}[i](r_1)$ + \State \nextalgline \hspace{5em} $S \gets S \setminus i$ \vspace{0.5em} - \State \nextalgline \hspace{2em} \textbf{for } $r \in [r_1 + 1, \dots, r_2]$ \textbf{do} - \State \nextalgline \hspace{3em} $\texttt{APPEND}(r)$ - \State \nextalgline \hspace{3em} $\textit{proves} \gets \texttt{READ}()$ - \State \nextalgline \hspace{3em} $\textit{winner}^r \gets \{j : (j, \texttt{PROVE}(r)) \in \textit{proves}\}$ - \State \nextalgline \hspace{3em} \textbf{wait } $\forall j \in \textit{winner}^r,\ \textit{prop}[r][j] \neq \bot$ - \State \nextalgline \hspace{3em} $T \gets \bigcup_{j \in \textit{winner}^r} \textit{prop}[r][j] \setminus \textit{delivered}$ + \State \nextalgline \hspace{2em} $\textit{winner}[r_1] \gets \texttt{READ\_ALL}()$ + \State \nextalgline \hspace{2em} \textbf{wait } $\forall j \in \textit{winner}[r_1],\ |\textit{prop}[r_1][j] \neq \bot| \geq f+1$ + \State \nextalgline \hspace{2em} $T \gets \bigcup_{j \in \textit{winner}[r_1]} \textit{prop}[r_1][j] \setminus \textit{delivered}$ \vspace{0.5em} - \State \nextalgline \hspace{3em} \textbf{for each } $m \in \texttt{ordered}(T)$ - \State \nextalgline \hspace{4em} $\textit{delivered} \gets \textit{delivered} \cup \{m\}$ - \State \nextalgline \hspace{4em} $\texttt{AB-deliver}_j(m)$ - \State \nextalgline \hspace{2em} $r_1 \gets r_2$ + \State \nextalgline \hspace{2em} \textbf{for each } $m \in \texttt{ordered}(T)$ + \State \nextalgline \hspace{3em} $\textit{delivered} \gets \textit{delivered} \cup \{m\}$ + \State \nextalgline \hspace{3em} $\texttt{AB-deliver}_j(m)$ + \State \nextalgline \hspace{2em} $r_1 \gets \textit{hash}(T, r_1)$ \vspace{1em} - % --- RB-deliver(Prop) handler --- - \State \nextalgline \textbf{RB-delivered}$_j(\texttt{PROP}, S, r_1, j_1)$ - \State \nextalgline \hspace{1em} $\textit{prop}[r_1][j_1] \gets S$ + % --- READ_ALL() --- + \State \nextalgline \textbf{READ\_ALL}$(r)$ + \State \nextalgline \hspace{1em} \textbf{for each } $j \in (1, ... , n)$ + \State \nextalgline \hspace{2em} $win[j] \gets \{j_1: \texttt{READ}_{j_1}() \ni (j, \texttt{PROVE}(r))\}$ + \State \nextalgline \hspace{1em} \textbf{for} $i \in (1, ... , n)$ + \State \nextalgline \hspace{2em} \textbf{for} $j \in (1, ... , n)$ + \State \nextalgline \hspace{3em} \textbf{if} $i \in win[j]$ + \State \nextalgline \hspace{4em} $count[i] ++$ + \State \nextalgline \hspace{1em} \textbf{return} $\{i: count[i] \geq n-f\}$ - \end{algorithmic} -\end{algorithm} \ No newline at end of file + \end{algorithmic} +\end{algorithm} + +\subsection{Round mecansism} + +We assume that the hash function is deterministic and without collisions. Because we're sure that the round contains at least f + 1 processes as winners, the next round ID is unpredictable by a process who would not follow the protocol and would drop messages legally sent by non-byzantine process. +Also, it ensures that if a byzantine process try to go faster than the others, he will at least wait the faster non-byzantine process to progress. \ No newline at end of file diff --git a/Recherche/ALDLoverAB/main.pdf b/Recherche/ALDLoverAB/main.pdf index 75a217e..40cc6ba 100644 Binary files a/Recherche/ALDLoverAB/main.pdf and b/Recherche/ALDLoverAB/main.pdf differ diff --git a/Recherche/ALDLoverAB/proof/index.tex b/Recherche/ALDLoverAB/proof/index.tex index e4bba0e..a1172dd 100644 --- a/Recherche/ALDLoverAB/proof/index.tex +++ b/Recherche/ALDLoverAB/proof/index.tex @@ -4,53 +4,54 @@ \begin{proof} - Let $j$ be a process such that $\texttt{AB-deliver}_j(m)$ occurs. + % Let $j$ be a process such that $\texttt{AB-deliver}_j(m)$ occurs. - \begin{align*} - &\texttt{AB-deliver}_j(m) & \text{(line 18)} \\ - \Rightarrow\; & m \in \texttt{ordered}(T),\ \text{with } T = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r][j'] \setminus \textit{delivered} & \text{(lines 16-17)} \\ - \Rightarrow\; & \exists j_0,\ r_0 : m \in \textit{prop}[r_0][j_0] & \text{(line 16)} \\ - \Rightarrow\; & \textit{prop}[r_0][j_0] = S,\ \text{with } \texttt{RB-delivered}_{j}(PROP, S, r_0, j_0) & \text{(line 22)} \\ - \Rightarrow\; & S \text{ was sent in } \texttt{RB-cast}(PROP, S, r_0, j_0) & \text{(line 9)} \\ - \Rightarrow\; & S = \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} & \text{(line 6)} \\ - \Rightarrow\; & m' \in \textit{received}_{j_0}\ \text{where } m' \text{ broadcast by } j_0 & \text{(line 4)} \\ - \Rightarrow\; & \textbf{if } m = m' \\ - & \quad \Rightarrow \texttt{RB-Broadcast}_{j_0}(m) \text{ occurred} & \text{(line 3)} \\ - & \quad \Rightarrow \texttt{AB-Broadcast}_{j_0}(m) \text{ occurred} & \text{(line 1)} & \hspace{1em} \square \\ - & \textbf{else: } m \in \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} \\ - & \quad \Rightarrow m \in \textit{received}_{j_0} & \text{(line 4)} \\ - & \quad \Rightarrow \texttt{RB-delivered}_{j_0}(m) \text{ occurred} & \text{(line 3)} \\ - & \quad \Rightarrow \exists j_1 : \texttt{RB-Broadcast}_{j_1}(m) \text{ occurred} & \text{(line 2)} \\ - & \quad \Rightarrow \texttt{AB-Broadcast}_{j_1}(m) \text{ occurred} & \text{(line 1)} & \hspace{1em} \square - \end{align*} + % \begin{align*} + % &\texttt{AB-deliver}_j(m) & \text{(line 18)} \\ + % \Rightarrow\; & m \in \texttt{ordered}(T),\ \text{with } T = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r][j'] \setminus \textit{delivered} & \text{(lines 16-17)} \\ + % \Rightarrow\; & \exists j_0,\ r_0 : m \in \textit{prop}[r_0][j_0] & \text{(line 16)} \\ + % \Rightarrow\; & \textit{prop}[r_0][j_0] = S,\ \text{with } \texttt{RB-delivered}_{j}(PROP, S, r_0, j_0) & \text{(line 22)} \\ + % \Rightarrow\; & S \text{ was sent in } \texttt{RB-cast}(PROP, S, r_0, j_0) & \text{(line 9)} \\ + % \Rightarrow\; & S = \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} & \text{(line 6)} \\ + % \Rightarrow\; & m' \in \textit{received}_{j_0}\ \text{where } m' \text{ broadcast by } j_0 & \text{(line 4)} \\ + % \Rightarrow\; & \textbf{if } m = m' \\ + % & \quad \Rightarrow \texttt{RB-Broadcast}_{j_0}(m) \text{ occurred} & \text{(line 3)} \\ + % & \quad \Rightarrow \texttt{AB-Broadcast}_{j_0}(m) \text{ occurred} & \text{(line 1)} & \hspace{1em} \square \\ + % & \textbf{else: } m \in \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} \\ + % & \quad \Rightarrow m \in \textit{received}_{j_0} & \text{(line 4)} \\ + % & \quad \Rightarrow \texttt{RB-delivered}_{j_0}(m) \text{ occurred} & \text{(line 3)} \\ + % & \quad \Rightarrow \exists j_1 : \texttt{RB-Broadcast}_{j_1}(m) \text{ occurred} & \text{(line 2)} \\ + % & \quad \Rightarrow \texttt{AB-Broadcast}_{j_1}(m) \text{ occurred} & \text{(line 1)} & \hspace{1em} \square + % \end{align*} - Therefore, every delivered message $m$ must originate from some call to \texttt{AB-Broadcast}. + % Therefore, every delivered message $m$ must originate from some call to \texttt{AB-Broadcast}. \end{proof} + \begin{theorem}[No Duplication] No message is delivered more than once by any process. \end{theorem} \begin{proof} - Assume by contradiction that a process $j$ delivers the same message $m$ more than once, i.e., - \[ - \texttt{AB-deliver}_j(m) \text{ occurs at least twice.} - \] + % Assume by contradiction that a process $j$ delivers the same message $m$ more than once, i.e., + % \[ + % \texttt{AB-deliver}_j(m) \text{ occurs at least twice.} + % \] - \begin{align*} - &\texttt{AB-deliver}_j(m) \text{ occurs} & \text{(line 19)} \\ - \Rightarrow\; & m \in \texttt{ordered}(T),\ \text{where } T = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r][j'] \setminus \textit{delivered} & \text{(lines 16-17)} \\ - \Rightarrow\; & m \notin \textit{delivered} \text{ at that time} \\ - \\ - \text{However:} \\ - & \texttt{delivered} \gets \texttt{delivered} \cup \{m\} & \text{(line 18)} \\ - \Rightarrow\; & m \in \textit{delivered} \text{ permanently} \\ - \Rightarrow\; & \text{In any future round, } m \notin T' \text{ since } T' = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r'][j'] \setminus \textit{delivered} \\ - \Rightarrow\; & m \text{ will not be delivered again} \\ - \Rightarrow\; & \text{Contradiction.} - \end{align*} + % \begin{align*} + % &\texttt{AB-deliver}_j(m) \text{ occurs} & \text{(line 19)} \\ + % \Rightarrow\; & m \in \texttt{ordered}(T),\ \text{where } T = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r][j'] \setminus \textit{delivered} & \text{(lines 16-17)} \\ + % \Rightarrow\; & m \notin \textit{delivered} \text{ at that time} \\ + % \\ + % \text{However:} \\ + % & \texttt{delivered} \gets \texttt{delivered} \cup \{m\} & \text{(line 18)} \\ + % \Rightarrow\; & m \in \textit{delivered} \text{ permanently} \\ + % \Rightarrow\; & \text{In any future round, } m \notin T' \text{ since } T' = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r'][j'] \setminus \textit{delivered} \\ + % \Rightarrow\; & m \text{ will not be delivered again} \\ + % \Rightarrow\; & \text{Contradiction.} + % \end{align*} - Therefore, no message can be delivered more than once by the same process. $\square$ + % Therefore, no message can be delivered more than once by the same process. $\square$ \end{proof} \begin{theorem}[Validity] @@ -58,27 +59,27 @@ \end{theorem} \begin{proof} - Let $j$ be a correct process such that $\texttt{AB-Broadcast}_j(m)$ occurs (line 5). + % Let $j$ be a correct process such that $\texttt{AB-Broadcast}_j(m)$ occurs (line 5). - \begin{align*} - &\texttt{AB-Broadcast}_j(m) & \text{(line 1)}\\ - \Rightarrow\; & \texttt{RB-Broadcast}_j(m) \text{ occurs} & \text{(line 2)} \\ - \Rightarrow\; & \forall j_0 : \texttt{RB-delivered}_{j_0}(m) & \text{(line 3)} \\ - \Rightarrow\; & m \in \textit{received}_{j_0} & \text{(line 4)} \\ - \Rightarrow\; & \textbf{if } m \in \texttt{delivered}_{j_0} \\ - & \quad \Rightarrow \textit{delivered}_{j_0} \gets textit{delivered}_{j_0} \cup \{m\} & \text{(line 18)} \\ - & \quad \Rightarrow \texttt{AB-delivered}_{j_0}(m) & \text{(line 19)} & \hspace{1em} \square \\ - & \textbf{else } m \notin \textit{delivered}_{j_0} : \\ - & \quad \Rightarrow m \in S_{j_0}\ \text{since } S_{j_0} = \textit{receieved}_{j_0} \setminus \textit{delivered}_{j_0} & \text{(line 6)} \\ - & \quad \Rightarrow \exists r : \texttt{RB-cast}_{j_0}(texttt{PROP}, S_{j_0}, r, j_0) & \text{(line 9)} \\ - & \quad \quad \Rightarrow \forall j_1 : \texttt{RB-Deliver}_{j_1}(\texttt{PROP}, S_{j_0}, r, j_0)\ \text{occurs} & \text{(line 21)} \\ - & \quad \quad \Rightarrow \textit{prop}[r][j_0] = S_{j_0} & \text{(line 22)} \\ - & \quad \Rightarrow \exists j_2 \in j_0 : \texttt{PROVE}_{j_2}(r)\ \text{is valid} & \text{(line 10)} \\ - & \quad \Rightarrow j_2 \in textit{winner}^r & \text{(line 14)} \\ - & \quad \Rightarrow T_{j_0} \ni \textit{prop}[r][j_2] \setminus \textit{delivered}_{j_0} & \text{(line 16)} \\ - & \quad \Rightarrow T_{j_0} \ni S_{j_2} \setminus \textit{delivered}_{j_0} \ni m & \text{(line 16)} \\ - & \quad \Rightarrow \texttt{AB-deliver}_{j_0}(m) & \text{(line 19)} & \hspace{1em} \square \\ - \end{align*} + % \begin{align*} + % &\texttt{AB-Broadcast}_j(m) & \text{(line 1)}\\ + % \Rightarrow\; & \texttt{RB-Broadcast}_j(m) \text{ occurs} & \text{(line 2)} \\ + % \Rightarrow\; & \forall j_0 : \texttt{RB-delivered}_{j_0}(m) & \text{(line 3)} \\ + % \Rightarrow\; & m \in \textit{received}_{j_0} & \text{(line 4)} \\ + % \Rightarrow\; & \textbf{if } m \in \texttt{delivered}_{j_0} \\ + % & \quad \Rightarrow \textit{delivered}_{j_0} \gets textit{delivered}_{j_0} \cup \{m\} & \text{(line 18)} \\ + % & \quad \Rightarrow \texttt{AB-delivered}_{j_0}(m) & \text{(line 19)} & \hspace{1em} \square \\ + % & \textbf{else } m \notin \textit{delivered}_{j_0} : \\ + % & \quad \Rightarrow m \in S_{j_0}\ \text{since } S_{j_0} = \textit{receieved}_{j_0} \setminus \textit{delivered}_{j_0} & \text{(line 6)} \\ + % & \quad \Rightarrow \exists r : \texttt{RB-cast}_{j_0}(texttt{PROP}, S_{j_0}, r, j_0) & \text{(line 9)} \\ + % & \quad \quad \Rightarrow \forall j_1 : \texttt{RB-Deliver}_{j_1}(\texttt{PROP}, S_{j_0}, r, j_0)\ \text{occurs} & \text{(line 21)} \\ + % & \quad \quad \Rightarrow \textit{prop}[r][j_0] = S_{j_0} & \text{(line 22)} \\ + % & \quad \Rightarrow \exists j_2 \in j_0 : \texttt{PROVE}_{j_2}(r)\ \text{is valid} & \text{(line 10)} \\ + % & \quad \Rightarrow j_2 \in textit{winner}^r & \text{(line 14)} \\ + % & \quad \Rightarrow T_{j_0} \ni \textit{prop}[r][j_2] \setminus \textit{delivered}_{j_0} & \text{(line 16)} \\ + % & \quad \Rightarrow T_{j_0} \ni S_{j_2} \setminus \textit{delivered}_{j_0} \ni m & \text{(line 16)} \\ + % & \quad \Rightarrow \texttt{AB-deliver}_{j_0}(m) & \text{(line 19)} & \hspace{1em} \square \\ + % \end{align*} \end{proof} @@ -88,20 +89,20 @@ \begin{proof} - \begin{align*} - & \forall j_0 : \texttt{AB-Deliver}_{j_0}(m_0) \wedge \texttt{AB-Deliver}_{j_0}(m_1) & \text{(line 19)} \\ - \Rightarrow\; & \exists r_0, r_1 : m_0 \in \texttt{ordered}(T^{r_0}) \wedge m_1 \in \texttt{ordered}(T^{r_1}) & \text{(line 17)} \\ - \Rightarrow\; & T^{r_0} = \bigcup_{j' \in \textit{winner}^{r_0}} \textit{prop}[r_0][j'] \setminus \textit{delivered}\ \wedge \\ - & T^{r_1} = \bigcup_{j' \in \textit{winner}^{r_1}} \textit{prop}[r_1][j'] \setminus \textit{delivered} & \text{(line 16)} \\ - \Rightarrow\; & \textbf{if } r_0 = r_1 \\ - & \quad \Rightarrow T^{r_0} = T^{r_1} \\ - & \quad \Rightarrow m_0, m_1 \in \texttt{ordered}(T^{r_0})\ \text{since \texttt{ordered} is deterministic} \\ - & \quad \Rightarrow \textbf{if } m_0 < m_1 : \\ - & \quad \quad \Rightarrow \texttt{AB-Deliver}_{j_0}(m_0) < \texttt{AB-Deliver}_{j_0}(m_1) & & \hspace{1em} \square\\ - & \textbf{else if } r_0 < r_1 \\ - & \quad \Rightarrow \forall m \in T^{r_0}, \forall m' \in T^{r_1} : \texttt{AB-Deliver}(m) < \texttt{AB-Deliver}(m') & & \hspace{1em} \square\\ - \end{align*} + % \begin{align*} + % & \forall j_0 : \texttt{AB-Deliver}_{j_0}(m_0) \wedge \texttt{AB-Deliver}_{j_0}(m_1) & \text{(line 19)} \\ + % \Rightarrow\; & \exists r_0, r_1 : m_0 \in \texttt{ordered}(T^{r_0}) \wedge m_1 \in \texttt{ordered}(T^{r_1}) & \text{(line 17)} \\ + % \Rightarrow\; & T^{r_0} = \bigcup_{j' \in \textit{winner}^{r_0}} \textit{prop}[r_0][j'] \setminus \textit{delivered}\ \wedge \\ + % & T^{r_1} = \bigcup_{j' \in \textit{winner}^{r_1}} \textit{prop}[r_1][j'] \setminus \textit{delivered} & \text{(line 16)} \\ + % \Rightarrow\; & \textbf{if } r_0 = r_1 \\ + % & \quad \Rightarrow T^{r_0} = T^{r_1} \\ + % & \quad \Rightarrow m_0, m_1 \in \texttt{ordered}(T^{r_0})\ \text{since \texttt{ordered} is deterministic} \\ + % & \quad \Rightarrow \textbf{if } m_0 < m_1 : \\ + % & \quad \quad \Rightarrow \texttt{AB-Deliver}_{j_0}(m_0) < \texttt{AB-Deliver}_{j_0}(m_1) & & \hspace{1em} \square\\ + % & \textbf{else if } r_0 < r_1 \\ + % & \quad \Rightarrow \forall m \in T^{r_0}, \forall m' \in T^{r_1} : \texttt{AB-Deliver}(m) < \texttt{AB-Deliver}(m') & & \hspace{1em} \square\\ + % \end{align*} - Therefore, for all correct processes, messages are delivered in the same total order. + % Therefore, for all correct processes, messages are delivered in the same total order. \end{proof}