amaury_joly/bwconsistency
1
0
Fork 0
Code Issues 5 Pull Requests Packages Projects 3 Releases Wiki Activity

encore pas bon

Browse Source
This commit is contained in:
Amaury JOLY
2025-06-27 07:53:09 +00:00
parent b5719a7d6b
commit 35a9d91779
3 changed files with 110 additions and 90 deletions
Download Patch File Download Diff File Expand all files Collapse all files

141
Recherche/ALDLoverAB/proof/index.tex
View File

@ -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}