nouvel algo + proofs
This commit is contained in:
Amaury JOLY
parent
d1caa2e54a
commit
b5719a7d6b
@ -1,60 +1,59 @@
|
||||
We consider a set of processes communicating asynchronously over reliable point-to-point channels. Each process maintains the following shared variables:
|
||||
We consider a set of processes communicating asynchronously over reliable point-to-point channels. Each process maintains the following local or shared variables:
|
||||
|
||||
\begin{itemize}
|
||||
\item \textbf{received}: the set of messages received (but not yet delivered).
|
||||
\item \textbf{delivered}: the set of messages that have been received, ordered, and delivered.
|
||||
\item \textbf{prop[$r$][$j$]}: the proposal set of process $j$ at round $r$. It contains the set of messages that process $j$ claims to have received but not yet delivered at round $r$, concatenated with its newly broadcast message.
|
||||
\item \textbf{proves}: the current content of the \texttt{DenyList} registry, accessible via the operation \texttt{READ()}. It returns a list of tuples $(j, \texttt{PROVE}(r))$, each indicating that process $j$ has issued a valid \texttt{PROVE} for round $r$.
|
||||
\item \textbf{winner$^r$}: the set of processes that have issued a valid \texttt{PROVE} operation for round $r$.
|
||||
\item \textbf{RB-cast}: a reliable broadcast primitive that satisfies the properties defined in Section~1.1.2.
|
||||
\item \textbf{APPEND$(r)$}, \textbf{PROVE$(r)$}: operations that respectively insert (APPEND) and attest (PROVE) the participation of a process in round $r$ in the DenyList registry.
|
||||
\item \textbf{READ()}: retrieves the current local view of valid operations (APPENDs and PROVEs) from the DenyList.
|
||||
\item \textbf{ordered$(S)$}: returns a deterministic total order over a set $S$ of messages (e.g., via hash or lexicographic order).
|
||||
\item \textbf{\textit{received}}: the set of messages that have been received via the reliable broadcast primitive but not yet ordered.
|
||||
\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{\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.
|
||||
\end{itemize}
|
||||
|
||||
\resetalgline
|
||||
\begin{algorithm}
|
||||
\caption{Atomic Broadcast with DenyList}
|
||||
\begin{algorithmic}[1]
|
||||
\State $\textit{proves} \gets \emptyset$
|
||||
\State $\textit{received} \gets \emptyset$
|
||||
\State $\textit{delivered} \gets \emptyset$
|
||||
\State $r_1 \gets 0$
|
||||
|
||||
\vspace{1em}
|
||||
\textbf{RB-received$(m, S, r_0, j_0)$}
|
||||
\begin{algorithmic}[1]
|
||||
\State \nextalgline $\textit{received} \gets \textit{received} \cup \{m\}$
|
||||
\State \nextalgline $\textit{prop}[r_0][j_0] \gets S$
|
||||
\end{algorithmic}
|
||||
% --- AB-Broadcast ---
|
||||
\State \nextalgline \textbf{AB-Broadcast}$_j(m)$
|
||||
\State \nextalgline \hspace{1em} $\texttt{RB-Broadcast}_j(m)$
|
||||
|
||||
\vspace{1em}
|
||||
\textbf{AB-broadcast$(m, j_0)$}
|
||||
\begin{algorithmic}[1]
|
||||
\State \nextalgline $\textit{proves} \gets \texttt{READ}()$
|
||||
\State \nextalgline $r_0 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} + 1$
|
||||
\State \nextalgline $\texttt{RB-cast}(m, (\textit{received} \setminus \textit{delivered}) \cup \{m\}, r_0, j_0)$
|
||||
\State \nextalgline \texttt{PROVE}$(r_0)$
|
||||
\State \nextalgline \texttt{APPEND}$(r_0)$
|
||||
\Repeat
|
||||
\State \nextalgline $\textit{proves} \gets \texttt{READ}()$
|
||||
\State \nextalgline $r_1 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} - 1$
|
||||
\State \nextalgline $\textit{winner}^{r_1} \gets \{j : (j, \texttt{PROVE}(r_1)) \in \textit{proves}\}$
|
||||
\State \nextalgline \textbf{wait} $\forall j \in \textit{winner}^{r_1},\ \textit{prop}[r_1][j] \neq \bot$
|
||||
\Until{\nextalgline $\forall r_2,\ \exists j_2 \in \textit{winner}^{r_2},\ m \in \textit{prop}[r_2][j_2]$} \nextalgline
|
||||
\end{algorithmic}
|
||||
% --- 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{2em} $S \gets \textit{received} \setminus \textit{delivered}$
|
||||
\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)$
|
||||
|
||||
\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}$
|
||||
|
||||
\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$
|
||||
|
||||
\vspace{1em}
|
||||
\textbf{AB-listen}
|
||||
\begin{algorithmic}[1]
|
||||
\While{true}
|
||||
\State \nextalgline $\textit{proves} \gets \texttt{READ}()$
|
||||
\State \nextalgline $r_1 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} - 1$
|
||||
\For{$r_2 \in [r_0, \dots, r_1]$} \nextalgline
|
||||
\State \nextalgline \texttt{APPEND}$(r_2)$
|
||||
\State \nextalgline $\textit{proves} \gets \texttt{READ}()$
|
||||
\State \nextalgline $\textit{winner}^{r_2} \gets \{j : (i, \texttt{PROVE}(r_2)) \in \textit{proves}\}$
|
||||
\State \nextalgline \textbf{wait} $\forall j \in \textit{winner}^{r_2},\ \textit{prop}[r_2][j] \neq \bot$
|
||||
\State \nextalgline $M^{r_2} \gets \bigcup_{j \in \textit{winner}^{r_2}} \textit{prop}[r_2][j]$
|
||||
\ForAll{$m \in \texttt{ordered}(M^{r_2})$} \nextalgline
|
||||
\State \nextalgline $\textit{delivered} \gets \textit{delivered} \cup \{m\}$
|
||||
\State \nextalgline \texttt{AB-deliver}$(m)$
|
||||
\EndFor
|
||||
\EndFor
|
||||
\EndWhile
|
||||
% --- 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$
|
||||
|
||||
\end{algorithmic}
|
||||
\end{algorithm}
|
||||
2416
Recherche/ALDLoverAB/main.bcf
Normal file
2416
Recherche/ALDLoverAB/main.bcf
Normal file
File diff suppressed because it is too large
Load Diff
Binary file not shown.
@ -41,9 +41,9 @@
|
||||
\affil{Aix-Marseille Université, Scille}
|
||||
\date{\today}
|
||||
|
||||
\begin{titlepage}
|
||||
\maketitle
|
||||
\end{titlepage}
|
||||
% \begin{titlepage}
|
||||
% \maketitle
|
||||
% \end{titlepage}
|
||||
|
||||
|
||||
\section{Introduction}
|
||||
|
||||
@ -2,120 +2,106 @@
|
||||
If a message $m$ is delivered by any process, then it was previously broadcast by some process via the \texttt{AB-broadcast} primitive.
|
||||
\end{theorem}
|
||||
|
||||
|
||||
\begin{proof}
|
||||
Let $j$ be a process such that $\text{AB-deliver}_j(m)$ occurs.
|
||||
Let $j$ be a process such that $\texttt{AB-deliver}_j(m)$ occurs.
|
||||
|
||||
\begin{align*}
|
||||
&\text{AB-deliver}_j(m) & \text{(line 24)} \\
|
||||
\Rightarrow\; &\exists r_0 : m \in \texttt{ordered}(M^{r_0}) & \text{(line 22)} \\
|
||||
\Rightarrow\; &\exists j_0 : j_0 \in \textit{winner}^{r_0} \land m \in \textit{prop}[r_0][j_0] & \text{(line 21)} \\
|
||||
\Rightarrow\; &\exists m_0, S_0 : \text{RB-received}_{j_0}(m_0, S_0, r_0, j_0) \land m \in S_0 & \text{(line 2)} \\
|
||||
\Rightarrow\; &S_0 = (\textit{received}_{j_0} \setminus \textit{delivered}_{j_0}) \cup \{m_1\} & \text{(line 5)} \\
|
||||
\Rightarrow\; &\textbf{if } m_1 = m: \exists\, \text{AB-broadcast}_{j_0}(m) \hspace{1em} \square \\
|
||||
&\textbf{else if } m_1 \neq m: \\
|
||||
&\quad m \in \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} \Rightarrow m \in \textit{received}_{j_0} \land m \notin \textit{delivered}_{j_0} \\
|
||||
&\quad \exists j_1, S_1, r_1 : \text{RB-received}_{j_1}(m, S_1, r_1, j_1) & \text{(line 1)} \\
|
||||
&\quad \Rightarrow \exists\, \text{AB-broadcast}_{j_1}(m) \hspace{1em} \square & \text{(line 5)}
|
||||
&\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}.
|
||||
\end{proof}
|
||||
|
||||
|
||||
|
||||
|
||||
\begin{theorem}[No Duplication]
|
||||
No message is delivered more than once by any process.
|
||||
\end{theorem}
|
||||
|
||||
\begin{proof}
|
||||
Let $j$ be a process such that both $\text{AB-deliver}_j(m_0)$ and $\text{AB-deliver}_j(m_1)$ occur, with $m_0 = m_1$.
|
||||
|
||||
\begin{align*}
|
||||
&\text{AB-deliver}_j(m_0) \wedge \text{AB-deliver}_j(m_1) & \text{(line 24)} \\
|
||||
\Rightarrow\; & m_0, m_1 \in \textit{delivered}_j & \text{(line 23)} \\
|
||||
\Rightarrow\; &\exists r_0, r_1 : m_0 \in M^{r_0} \wedge m_1 \in M^{r_1} & \text{(line 22)} \\
|
||||
\Rightarrow\; &\exists j_0, j_1 : m_0 \in \textit{prop}[r_0][j_0] \wedge m_1 \in \textit{prop}[r_1][j_1] \\
|
||||
&\hspace{2.5em} \wedge\ j_0 \in \textit{winner}^{r_0},\ j_1 \in \textit{winner}^{r_1} & \text{(line 21)}
|
||||
\end{align*}
|
||||
|
||||
We now distinguish two cases:
|
||||
|
||||
\vspace{0.5em}
|
||||
\noindent\textbf{Case 1:} $r_0 = r_1$:
|
||||
\begin{itemize}
|
||||
\item If $j_0 \neq j_1$: this contradicts message uniqueness, since two different processes would include the same message in round $r_0$.
|
||||
\item If $j_0 = j_1$:
|
||||
\begin{align*}
|
||||
\Rightarrow & |{(j_0, \texttt{PROVE}(r_0)) \in proves}| \geq 2 & \text{(line 19)}\\
|
||||
\Rightarrow &\texttt{PROVE}_{j_0}(r_0) \text{ occurs 2 times} & \text{(line 6)}\\
|
||||
\Rightarrow &\texttt{AB-Broadcast}_{j_0}(m_0) \text{ were invoked two times} \\
|
||||
\Rightarrow &(max\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1) & \text{(line 4)}\\
|
||||
&\text{ returned the same value in two differents invokations of \texttt{AB-Broadcast}} \\
|
||||
&\textbf{But } \texttt{PROVE}(r_0) \Rightarrow \texttt{max}\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1 > r_0 \\
|
||||
&\text{It's impossible for a single process to submit two messages in the same round} \hspace{1em} \\
|
||||
\end{align*}
|
||||
\end{itemize}
|
||||
|
||||
% \vspace{0.5em}
|
||||
\noindent\textbf{Case 2:} $r_0 \ne r_1$:
|
||||
\begin{itemize}
|
||||
\item If $j_0 \neq j_1$: again, message uniqueness prohibits two different processes from broadcasting the same message in different rounds.
|
||||
\item If $j_0 = j_1$: message uniqueness also prohibits the same process from broadcasting the same message in two different rounds.
|
||||
\end{itemize}
|
||||
|
||||
In all cases, we reach a contradiction. Therefore, it is impossible for a process to deliver the same message more than once. $\square$
|
||||
\end{proof}
|
||||
|
||||
% \subsubsection{No Duplication}
|
||||
|
||||
% $M = (\bigcup_{i \rightarrow |P|} AB\_receieved_{i}(m)), \not\exists m_0 m_1 \in M \text{s.t. } m_1 = m_2$
|
||||
% \\
|
||||
% Proof \\
|
||||
% \begin{align*}
|
||||
% &\text{Soit } i, m_0, m_1 \text{ tels que } m_0 = m_1 \\
|
||||
% &\exists r_0,\ m_0 \in M^{r_0} \\
|
||||
% &\exists r_1,\ m_1 \in M^{r_1} \\
|
||||
% &\text{if } r_0 = r_1 \\
|
||||
% &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\
|
||||
% &\quad \text{if} j_0 \neq j_1 \\
|
||||
% &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\
|
||||
% &\quad \text{if } j_0 = j_1 \\
|
||||
% &\quad\quad j_0 \text{ a émis son } \text{PROVE}(r_0) \text{ valide 2 fois}\\
|
||||
% &\quad\quad \text{Impossible si } j_0 \text{ correct} \\
|
||||
% &\text{else} \\
|
||||
% &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\
|
||||
% &\quad \text{if } j_0 \neq j_1 \\
|
||||
% &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\
|
||||
% &\quad \text{if } j_0 = j_1 \\
|
||||
% &j_0 \text{ à emis et validé 2 fois le même messages a des rounds différents.}\\
|
||||
% &\text{On admet que deux message identiques soumis a des rounds différents ne peuvent être identiques}
|
||||
% \end{align*}
|
||||
|
||||
\subsubsection{Broadcast Validity}
|
||||
$\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1 \quad AB\_received_{j_1}(m_0)$ \\
|
||||
|
||||
Proof:
|
||||
\begin{align*}
|
||||
&\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \\
|
||||
&\forall j_1, \exists r_1 \quad RB\_deliver_{j_1}^{r_1}(m_0) \\
|
||||
&\exists receieved : m_0 \in receieved_{j_1} \\
|
||||
&\exists r_0 : RB\_deliver(PROP, r_0, m_0) & LOOP\\
|
||||
&\exists prop: \text{prop}[r_0][j_0] = m_0 \\
|
||||
&\text{if } \not\exists (j_0, PROVE(r_0)) \in \text{proves} \\
|
||||
&\quad r_0 += 1 \\
|
||||
&\quad \text{jump to LOOP} \\
|
||||
&\text{else} \\
|
||||
&\quad \exists \text{winner}, \text{winner}^{r_0} \ni j_0 \\
|
||||
&\quad \exists M^{r_0} \ni (\text{prop}[r_0][j_0] = m_0) \\
|
||||
&\quad \forall j_1, \quad AB\_deliver_{j_1}(m_0)
|
||||
\end{align*}
|
||||
|
||||
\subsubsection*{AB receive width}
|
||||
Assume by contradiction that a process $j$ delivers the same message $m$ more than once, i.e.,
|
||||
\[
|
||||
\exists j_0, m_0 \quad AB\_deliver_{j_0}(m_0) \Rightarrow \forall j_1\ AB\_deliver_{j_1}
|
||||
\texttt{AB-deliver}_j(m) \text{ occurs at least twice.}
|
||||
\]
|
||||
|
||||
Proof:
|
||||
\begin{align*}
|
||||
&\forall j_0, m_0\ AB\_deliver_{j_0}(m_0) \Rightarrow \exists j_1 \text{ correct }, AB\_broadcast(m_0) \\
|
||||
&\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1,\ AB\_deliver_{j_1}(m_0)
|
||||
&\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$
|
||||
\end{proof}
|
||||
|
||||
\begin{theorem}[Validity]
|
||||
If a correct process invokes $\texttt{AB-Broadcast}_j(m)$, then all correct processes eventually deliver $m$.
|
||||
\end{theorem}
|
||||
|
||||
\begin{proof}
|
||||
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*}
|
||||
|
||||
\end{proof}
|
||||
|
||||
\begin{theorem}[Total Order]
|
||||
If two correct processes deliver two messages $m_1$ and $m_2$, then they deliver them in the same order.
|
||||
\end{theorem}
|
||||
|
||||
\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*}
|
||||
|
||||
Therefore, for all correct processes, messages are delivered in the same total order.
|
||||
\end{proof}
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user