77 lines
3.1 KiB
TeX
77 lines
3.1 KiB
TeX
|
|
\subsubsection{Model Properties}
|
|
|
|
The system consists of \textit{n} asynchronous processes communicating via reliable point-to-point message passing. \\
|
|
Each process has a unique, unforgeable identifier and knows the identifiers of all other processes. \\
|
|
Up to $f<n$ processes may crash (fail-stop). \\
|
|
The network is reliable: if a correct process sends a message to another correct process, it is eventually delivered. \\
|
|
Messages are uniquely identifiable: two messages sent by distinct processes or at different rounds are distinguishable \\
|
|
2 messages sent by the same processus in two differents rounds are differents \\
|
|
|
|
\begin{property}[Message Uniqueness]
|
|
If two messages are sent by different processes, or by the same process in different rounds, then the messages are distinct. \\
|
|
Formally : \\
|
|
\[
|
|
\forall p_1, p_2,\ \forall r_1, r_2,\ \forall m_1, m_2,\
|
|
\left(
|
|
\begin{array}{l}
|
|
\text{send}(p_1, r_1, m_1) \land \text{send}(p_2, r_2, m_2) \\
|
|
\land\ (p_1 \ne p_2 \lor r_1 \ne r_2)
|
|
\end{array}
|
|
\right)
|
|
\Rightarrow m_1 \ne m_2
|
|
\]
|
|
\end{property}
|
|
|
|
|
|
\subsubsection{Reliable Broadcast Properties}
|
|
|
|
\begin{property}{Integrity}
|
|
Every message received was previously sent. \\
|
|
Formally : \\
|
|
$\forall p_i : \text{bc-recv}_i(m) \Rightarrow \exists p_j : \text{bc-send}_j(m)$
|
|
\end{property}
|
|
|
|
\begin{property}{No Duplicates}
|
|
No message is received more than once at any single processor. \\
|
|
Formally : \\
|
|
$\forall m, \forall p_i: \text{bc-recv}_i(m) \text{ occurs at most once}$ \\
|
|
\end{property}
|
|
|
|
\begin{property}{Validity}
|
|
All messages broadcast by a correct process are eventually received by all non faulty processors. \\
|
|
Formally : \\
|
|
$\forall m, \forall p_i: \text{correct}(p_i) \wedge \text{bc-send}_i(m) => \forall p_j : \text{correct}(p_j) \Rightarrow \text{bc-recv}_j(m)$
|
|
\end{property}
|
|
|
|
\subsubsection{AtomicBroadcast Properties}
|
|
|
|
\begin{property}{AB Totally ordered}
|
|
$\forall m_1, m_2, \forall p_i, p_j : \text{ab-recv}_{p_i}(m_1) < \text{ab-recv}_{p_i}(m_2) \Rightarrow \text{ab-recv}_{p_j}(m_1) < \text{ab-recv}_{p_j}(m_2)$
|
|
\end{property}
|
|
|
|
|
|
\subsubsection{DenyList Properties}
|
|
|
|
Let $\Pi_M$ be the set of processes authorized to issue \texttt{APPEND} operations,
|
|
and $\Pi_V$ the set of processes authorized to issue \texttt{PROVE} operations. \\
|
|
Let $S$ be the set of valid values that may be appended. Let $\texttt{Seq}$ be
|
|
the linearization of operations recorded in the DenyList.
|
|
|
|
\begin{property}{APPEND Validity}
|
|
An operation $\texttt{APPEND}(x)$ is valid iff :
|
|
the issuing process $p \in \Pi_M$, and the value $x \in S$
|
|
\end{property}
|
|
|
|
\begin{property}{PROVE Validity}
|
|
An operation $\texttt{PROVE}(x)$ is valid iff:
|
|
the issuing process $p \in \Pi_V$, and there exists no $\texttt{APPEND}(x)$ that appears earlier in $\texttt{Seq}$.
|
|
\end{property}
|
|
|
|
\begin{property}{PROGRESS}
|
|
If an APPEND(x) is invoked by a correct process, then all correct processes will eventually be unable to PROVE(x).
|
|
\end{property}
|
|
|
|
\begin{property}{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{property} |