61 lines
2.2 KiB
TeX
61 lines
2.2 KiB
TeX
|
|
\subsubsection{Model Properties}
|
|
|
|
The model is defined as Message-passing Aysnchronous. \\
|
|
There is n process. Each process is associated to a unique unforgeable id $i$.\\
|
|
Each process know the identity of all the process in the system\\
|
|
Each process have a reliable communication channel with all the others process such as:
|
|
\begin{itemize}
|
|
\item send(m) is the send primitive
|
|
\item recv(m) is the reception primitive
|
|
\end{itemize}
|
|
A message send is eventualy received\\
|
|
The system is Crash-Prone. There is at most f process who can crash such as f < n.\\
|
|
|
|
|
|
\subsubsection{AtomicBroadcast Properties}
|
|
|
|
\begin{theorem}{AB\_broadcast Validity}
|
|
if a message is sent by a correct process, the message is eventually received by all the correct process.
|
|
\end{theorem}
|
|
|
|
\begin{theorem}{AB\_receive Validity}
|
|
if a message is received by a correct process, the message is eventually received by all the correct process.
|
|
\end{theorem}
|
|
|
|
\begin{theorem}{AB\_receive safety No creation}
|
|
if a message is received by a correct process, the message was emitted by a correct porcess.
|
|
\end{theorem}
|
|
|
|
\begin{theorem}{AB\_receive safety No duplication}
|
|
each message is received at most 1 time by each process.
|
|
\end{theorem}
|
|
|
|
\begin{theorem}{AB\_receive safety Ordering}
|
|
$\forall m_1, m_2$ two messages, $\forall p_i, p_j$ two process. \\
|
|
if AB\_recv(m1) and AB\_recv(m2) for $p_i, p_j$ \\
|
|
and AB\_recv(m1) is before AB\_recv(m2) for $p_i$ \\
|
|
so AB\_recv(m1) is before AB\_recv(m2) for $p_j$ \\
|
|
\end{theorem}
|
|
|
|
|
|
|
|
\subsubsection{DenyList Properties}
|
|
|
|
\begin{theorem}{APPEND Validity}
|
|
a APPEND(x) is valid iff the process p who sent the operation is such as $p \in \Pi_M$.
|
|
And iff $x \in S$ where S is a set of valid values.
|
|
\end{theorem}
|
|
|
|
\begin{theorem}{PROVE Validity}
|
|
a PROVE(x) is valid iff the process $p$ who sent the operation is such as $p \in \Pi_V$.
|
|
And iff $\exists$ APPEND(x) who appears before PROVE(x) in Seq.
|
|
\end{theorem}
|
|
|
|
\begin{theorem}{PROGRESS}
|
|
if an APPEND(x) is invoked, so there is a point in the linearization of the operations such as all PROVE(x) are valids.
|
|
\end{theorem}
|
|
|
|
\begin{theorem}{READ Validity}
|
|
READ() return a list of tuples who is a random permutation of all valids PROVE() associated to the identity of the emiter process.
|
|
\end{theorem} |