X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/e3c2188521eaa2c6e2c6eee2da43b0f42fc47a89..251b65007a909068d3344bd82b7c5ec0ffb0a21a:/annexePromelaProof.tex?ds=sidebyside diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex index 8c95761..dbc5774 100644 --- a/annexePromelaProof.tex +++ b/annexePromelaProof.tex @@ -1,2 +1,284 @@ \JFC{Voir section~\ref{sec:spin:proof}} +Cette section donne les preuves des deux théorèmes de correction et complétude +du chapitre~\ref{chap:promela}. + + +\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. + + +Secondly, let us focus on the formula~(\ref{eq:correct_retrieve}). At iteration +$l+1$, let $c'$ be defined as $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Two cases +have to be considered depending on whether $D_{ji}^{l}$ and $D_{ji}^{l-1}$ are +equal or not. +\begin{itemize} +\item If $D_{ji}^{l} = D_{ji}^{l-1}$, since $D_{ji}^{c'} > D_{ji}^{l-1}$, then + $D_{ji}^{c'} > D_{ji}^{l}$ and then $c'$ is distinct from $l$. Thus, the SPIN + execution detailed above does not modify $Xd_{ji}^{l+1}$. It is obvious to + establish that $Xd_{ji}^{l+1} = Xd_{ji}^{l} = X_i^{D_{ji}^{l-1}} = + X_i^{D_{ji}^{l}}$. +\item Otherwise $D_{ji}^{l}$ is greater than $D_{ji}^{l-1}$ and $c$ is thus $l$. + According to \Equ{eq:Mij0} we have proved, we have + $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$. Then the SPIN execution + detailed above assigns $X_i^{D_{ji}^{l}}$ to $Xd_{ji}^{l+1}$, which ends the + proof of (\ref{eq:correct_retrieve}). +\end{itemize} + +We are left to prove the induction of the third part of the lemma. Let $k$, $k +\in S^{l+1}$. % and $\verb+k'+ = k-1$. +At the end of the first execution of the \verb+update_elems+ process, we have +$\verb+Xp[+k\verb+]+= F(\verb+Xd[+k\verb+][0]+, +\ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$. By definition of $Xd$, it is equal +to $F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$. Thanks to +\Equ{eq:correct_retrieve} we have proved, we can conclude the proof. +\end{Proof} + + +\begin{lemma} + Bounding the size of channels to $\textit{max} = \delta_0$ is sufficient when + simulating a DDN where delays are bounded by $\delta_0$. +\end{lemma} + +\begin{Proof} + For any $i$, $j$, at each iteration $t+1$, thanks to bounded delays (by + $\delta_0$), element $i$ has to know at worst $\delta_0$ values that are + $X_j^{t}$, \ldots, $X_j^{t-\delta_0+1}$. They can be stored into any channel + of size $\delta_0$. +\end{Proof} + + +\begin{theorem}[Soundness wrt universal convergence property]\label{Theo:sound} + Let $\phi$ be a DDN model and $\psi$ be its translation. If $\psi$ verifies + the LTL property (\ref{eq:ltl:conv}) under weak fairness property, then + iterations of $\phi$ are universally convergent. +\end{theorem} +\begin{Proof} +% For the case where the strategy is finite, one notice that property +% verification is achieved under weak fairness property. Instructions that +% write or read into \verb+channels[j].sent[i]+ are continuously enabled leading +% to convenient available dates $D_{ji}$. It is then easy to construct +% corresponding iterations of the DDN that are convergent. +% \ANNOT{quel sens donnes-tu a \emph{convenient} ici ?} + + Let us show the contraposition of the theorem. The previous lemmas have shown + that for any sequence of iterations of the DDN, there exists an execution of + the PROMELA model that simulates them. If some iterations of the DDN are + divergent, then they prevent the PROMELA model from stabilizing, \textit{i.e.}, not + verifying the LTL property (\ref{eq:ltl:conv}). +\end{Proof} + + +% \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound} +% Let $\phi$ be a DDN model where strategy, $X^(0)$ +% are only constrained to be pseudo-periodic and +% in $E$ respectively. +% Let $\psi$ be its translation. +% If all the executions of $\psi$ converge, +% then iterations of $\phi$ are universally convergent. +% \end{Corol} + + + +\begin{theorem}[Completeness wrt universal convergence property]\label{Theo:completeness} + Let $\phi$ be a DDN model and $\psi$ be its translation. If $\psi$ does not + verify the LTL property (\ref{eq:ltl:conv}) under weak fairness property then + the iterations of $\phi$ are divergent. +\end{theorem} +\begin{Proof} + For models $\psi$ that do not verify the LTL property (\ref{eq:ltl:conv}) it + is easy to construct corresponding iterations of the DDN, whose strategy is + pseudo-periodic since weak fairness property is taken into account. + +% i.e. iterations that are divergent. Executions are +% performed under weak fairness property; we then detail what are continuously +% enabled: +% \begin{itemize} +% \item if the strategy is not defined as periodic, elements $0$, \ldots, $n$ are +% infinitely often updated leading to pseudo-periodic strategy; +% \item instructions that write or read into \verb+channels[j].sent[i]+ are +% continuously enabled leading to convenient available dates $D_{ji}$. +% \end{itemize} +% The simulated DDN does not stabilize and its iterations are divergent. + \end{Proof} +