-\section{Proof of Translation Correctness}\label{sec:spin:proof}
-\JFC{Déplacer les preuves en annexes}
-
-This section establishes the soundness and completeness of the approach
-(Theorems~\ref{Theo:sound} and ~\ref{Theo:completeness}). Technical lemmas are
-first shown to ease the proof of the two theorems.
-
-
-% \begin{Lemma}[Absence of deadlock]\label{lemma:deadlock}
-% Let $\phi$ be a DDN model and $\psi$ be its translation. There is no deadlock
-% in any execution of $\psi$.
-% \end{Lemma}
-% \begin{Proof}
-% In current translation, deadlocks of PROMELA may only be introduced through
-% sending or receiving messages in channels. Sending (resp. receiving) a
-% message in the \verb+diffuse_values+ (resp. \verb+fetch_values+) function is
-% executed only if the channel is not full (resp. is not empty). In the
-% \verb+update_elems+ and \verb+scheduler+ processes, each time one adds a value
-% in any semaphore channel (\verb+unlock_elements_update+ and
-% \verb+sync_mutex+), the corresponding value is read; avoiding deadlocks by the
-% way.
-% \end{Proof}
-
-
-\begin{lemma}[Strategy Equivalence]\label{lemma:strategy}
- Let $\phi$ be a DDN with strategy $(S^t)^{t \in \Nats}$ and $\psi$ be its
- translation. There exists an execution of $\psi$ with weak fairness s.t. the
- scheduler makes \verb+update_elems+ update elements of $S^t$ at iteration $t$.
-\end{lemma}
-\begin{Proof}
- The proof is direct for $t=0$. Let us suppose it is established until $t$ is
- some $t_0$. Let us consider pseudo-periodic strategies. Thanks to the weak
- fairness equity property, \verb+update_elems+ will modify elements of $S^t$ at
- iteration $t$.
-\end{Proof}
-
-In what follows, let $Xd^t_{ji}$ be the value of
-\verb+Xd[+$j$\verb+].v[+$i$\verb+]+ after the $t^{\text{th}}$ call to the
-function \verb+fetch_values+. Furthermore, let $Y^k_{ij}$ be the element at
-index $k$ in the channel \verb+channels[i].sent[j]+ of size $m$, $m \le
-\delta_0$; $Y^0_{ij}$ and $Y^{m-1}_{ij}$ are respectively the head and the tail
-of the channel. Secondly, let $(M_{ij}^t)^{t \in \{1, 1.5, 2, 2.5,\ldots\}}$ be a
-sequence such that $M_{ij}^t$ is the partial function that associates to each
-$k$, $0 \le k \le m-1$, the tuple $(Y^k_{ij},a^k_{ij},c^k_{ij})$ while entering
-into the \verb+update_elems+ at iteration $t$ where
-% \begin{itemize}
-% \item
- $Y^k_{ij}$ is the value of the channel \verb+channels[i].sent[j]+
- at index $k$,
-%\item
-$a^k_{ij}$ is the date (previous to $t$) when $Y^k_{ij}$ has been added and
-%\item
-$c^k_{ij}$ is the first date at which the value is available on $j$. So,
- the value is removed from the channel $i\rightarrow j$ at date $c^k_{ij}+1$.
-%\end{itemize}
-$M_{ij}^t$ has the following signature:
-\begin{equation*}
-\begin{array}{rrcl}
-M_{ij}^t: &
-\{0,\ldots, \textit{max}-1\} &\rightarrow & E_i\times \Nats \times \Nats \\
-& k \in \{0,\ldots, m-1\} & \mapsto & M_{ij}(k)= (Y^k_{ij},a^k_{ij},c^k_{ij}).
-\end{array}
-\end{equation*}
-
-Intuitively, $M_{ij}^t$ is the memory of \verb+channels[i].sent[j]+ while
-starting the iteration $t$. Notice that the domain of any $M_{ij}^1$ is $\{0\}$
-and $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$: indeed, the \verb+init+ process
-initializes \verb+channels[i].sent[j]+ with \verb+Xp[i]+.
-
-Let us show how to make the indeterminism inside the two functions\linebreak
-\verb+fetch_values+ and \verb+diffuse_values+ compliant with \Equ{eq:async}.
-The function $M_{ij}^{t+1}$ is obtained by the successive updates of
-$M_{ij}^{t}$ through the two functions\linebreak \verb+fetch_values+ and
-\verb+diffuse_values+. Abusively, let $M_{ij}^{t+1/2}$ be the value of
-$M_{ij}^{t}$ after the former function during iteration $t$.
-
-In what follows, we consider elements $i$ and $j$ both in $\llbracket 1, n
-\rrbracket$ that are updated. At iteration $t$, $t \geq 1$, let
-$(Y^0_{ij},a^0_{ij},c^0_{ij})$ be the value of $M_{ij}^t(0)$ at the beginning of
-\verb+fetch_values+. If $t$ is equal to $c^0_{ij}+1$ then we execute the
-instruction that assigns $Y^0_{ij}$ (\textit{i.e.}, the head value of
-\verb+channels[i].sent[j]+) to $Xd_{ji}^t$. In that case, the function
-$M_{ij}^t$ is updated as follows: $M_{ij}^{t+1/2}(k) = M_{ij}^{t}(k+1)$ for each
-$k$, $0 \le k \le m-2$ and $m-1$ is removed from the domain of $M_{ij}^{t+1/2}$.
-Otherwise (\textit{i.e.}, when $t < c^0_{ij}+1$ or when the domain of $M_{ij}$
-is empty) the \verb+skip+ statement is executed and $M_{ij}^{t+1/2} =
-M_{ij}^{t}$.
-
-In the function \verb+diffuse_values+, if there exists some $\tau$, $\tau\ge t$
-such that \mbox{$D^{\tau}_{ji} = t$}, let $c_{ij}$ be defined by $ \min\{l \mid
-D^{l}_{ji} = t \} $. In that case, we execute the instruction that adds the
-value \verb+Xp[i]+ to the tail of \verb+channels[i].sent[j]+. Then,
-$M_{ij}^{t+1}$ is defined as an extension of $M_{ij}^{t+1/2}$ in $m$ such that
-$M_{ij}^{t+1}(m)$ is $(\verb+Xp[i]+,t,c_{ij})$. Otherwise (\textit{i.e.}, when $\forall l
-\, . \, l \ge t \Rightarrow D^{l}_{ji} \neq t$ is established) the \verb+skip+
-statement is executed and $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.
-
-
-\begin{lemma}[Existence of SPIN Execution]\label{lemma:execution}
- For any sequences $(S^t)^{t \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$, for
- any map $F$ there exists a SPIN execution such that for any iteration $t$, $t
- \ge 1$, for any $i$ and $j$ in $\llbracket 1, n \rrbracket$ we have the
- following properties:
-
-\noindent If the domain of $M_{ij}^t$ is not empty, then
-\begin{equation}
- \left\{
- \begin{array}{rcl}
- M_{ij}^1(0) & = & \left(X_i^{D_{ji}^{0}}, 0,0 \right) \\
- \textrm{if $t \geq 2$ then }M_{ij}^t(0) & = &
- \left(X_i^{D_{ji}^{c}},D_{ji}^{c},c \right) \textrm{, }
- c = \min\{l | D_{ji}^l > D_{ji}^{t-2} \}
- \end{array}
- \right.
- \label{eq:Mij0}
-\end{equation}
-\noindent Secondly we have:
-\begin{equation}
- \forall t'\, .\, 1 \le t' \le t \Rightarrow Xd^{t'}_{ji} = X^{D^{t'-1}_{ji}}_i
- \label{eq:correct_retrieve}
-\end{equation}
-\noindent Thirdly, for any $k\in S^t$. Then, the value of the computed variable
-\verb+Xp[k]+ at the end of the \verb+update_elems+ process is equal to
-$X_k^{t}$ \textit{i.e.}, $F_{k}\left( X_1^{D_{k\,1}^{t-1}},\ldots,
- X_{n}^{D_{k\,{n}}^{t-1}}\right)$ at the end of the $t^{\text{th}}$ iteration.
-\end{lemma}
-\begin{Proof}
-The proof is done by induction on the number of iterations.
-
-\paragraph{Initial case:}
-
-For the first item, by definition of $M_{ij}^t$, we have $M_{ij}^1(0) = \left(
- \verb+Xp[i]+, 0,0 \right)$ that is obviously equal to $\left(X_i^{D_{ji}^{0}},
- 0,0 \right)$.
-
-Next, the first call to the function \verb+fetch_value+ either assigns the head
-of \verb+channels[i].sent[j]+ to \verb+Xd[j].v[i]+ or does not modify
-\verb+Xd[j].v[i]+. Thanks to the \verb+init+ process, both cases are equal to
-\verb+Xp[i]+, \textit{i.e.}, $X_i^0$. The equation (\ref{eq:correct_retrieve}) is then
-established.
-
-
-For the last item, let $k$, $0 \le k \le n-1$. At the end of the first
-execution\linebreak of the \verb+update_elems+ process, the value of
-\verb+Xp[k]+ is\linebreak $F(\verb+Xd[+k\verb+].v[0]+, \ldots,
-\verb+Xd[+k\verb+].v[+n-1\verb+]+)$. Thus, by definition of $Xd$, it is equal
-to $F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$. Thanks to \Equ{eq:correct_retrieve},
-we can conclude the proof.
-
-
-
-\paragraph{Inductive case:}
-
-Suppose now that lemma~\ref{lemma:execution} is established until iteration $l$.
-
-First, if domain of definition of the function $M_{ij}^l$ is not empty, by
-induction hypothesis $M_{ij}^{l}(0)$ is $\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
-\right)$ where $c$ is $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
-
-At iteration $l$, if $l < c + 1$ then the \verb+skip+ statement is executed in
-the \verb+fetch_values+ function. Thus, $M_{ij}^{l+1}(0)$ is equal to
-$M_{ij}^{l}(0)$. Since $c > l-1$ then $D_{ji}^c > D_{ji}^{l-1}$ and hence, $c$
-is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Obviously, this implies also that
-$D_{ji}^c > D_{ji}^{l-2}$ and $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
-
-We now consider that at iteration $l$, $l$ is $c + 1$. In other words, $M_{ij}$
-is modified depending on the domain $\dom(M^l_{ij})$ of $M^l_{ij}$:
-\begin{itemize}
-\item if $\dom(M_{ij}^{l})=\{0\}$ and $\forall k\, . \, k\ge l \Rightarrow
- D^{k}_{ji} \neq l$ is established then $\dom(M_{ij}^{l+1})$ is empty and the
- first item of the lemma is established;
-\item if $\dom(M_{ij}^{l})=\{0\}$ and $\exists k\, . \, k\ge l \land D^{k}_{ji}
- = l$ is established then $M_{ij}^{l+1}(0)$ is $(\verb+Xp[i]+,l,c_{ij})$ that
- is added in the \verb+diffuse_values+ function s.t.\linebreak $c_{ij} =
- \min\{k \mid D^{k}_{ji} = l \} $. Let us prove that we can express
- $M_{ij}^{l+1}(0)$ as $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$ where
- $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. First, it is not hard to
- establish that $D_{ji}^{c_{ij}}= l \geq D_{ji}^{l} > D_{ji}^{l-1}$ and thus
- $c_{ij} \geq c'$. Next, since $\dom(M_{ij}^{l})=\{0\}$, then between
- iterations $D_{ji}^{c}+1$ and $l-1$, the \texttt{diffuse\_values} function has
- not updated $M_{ij}$. Formally we have
-$$
-\forall t,k \, .\, D_{ji}^c < t < l \land k \geq t \Rightarrow D_{ji}^k \neq
-t.$$
-
-Particularly, $D_{ji}^{c'} \not \in \{D_{ji}^{c}+1,\ldots,l-1\}$. We can apply
-the third item of the induction hypothesis to deduce
-$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ and we can conclude.
-
-\item if $\{0,1\} \subseteq \dom(M_{ij}^{l})$ then $M_{ij}^{l+1}(0)$ is
- $M_{ij}^{l}(1)$. Let $M_{ij}^{l}(1)= \left(\verb+Xp[i]+, a_{ij} , c_{ij}
- \right)$. By construction $a_{ij}$ is $\min\{t' | t' > D_{ji}^c \land
- (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$ and $c_{ij}$ is $\min\{k |
- D_{ji}^k = a_{ij}\}$. Let us show $c_{ij}$ is equal to $\min\{k | D_{ji}^k >
- D_{ji}^{l-1} \}$ further referred as $c'$. First we have $D_{ji}^{c_{ij}} =
- a_{ij} > D_{ji}^c$. Since $c$ by definition is greater or equal to $l-1$ ,
- then $D_{ji}^{c_{ij}}> D_{ji}^{l-1}$ and then $c_{ij} \geq c'$. Next, since
- $c$ is $l-1$, $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{c} \}$ and then $a_{ij}
- \leq D_{ji}^{c'}$. Thus, $c_{ij} \leq c'$ and we can conclude as in the
- previous part.
-\end{itemize}
-
-
-The case where the domain $\dom(M^l_{ij})$ is empty but the formula $\exists k
-\, .\, k \geq l \land D_{ji}^k = l$ is established is equivalent to the second
-case given above and then is omitted.
