intro et algo propre. Proof en cours

recherches/ALDLoverAB/intro/index.tex

@@ -1,61 +1,77 @@
 
 \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.\\
+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{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}
-
+\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}
 
-\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}
+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{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{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{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{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{theorem}{READ Validity}
+\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{theorem}
+\end{property}