la veille

[hdrcouchot.git] / annexePromelaProof.tex

%\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}[Stratégie équivalente]\label{lemma:strategy}
  Soit $\phi$  un système dynamique discret de stratégie  $(S^t)^{t \in  \Nats}$ 
  et $\psi$  sa traduction en PROMELA. 
  Il existe une exécution de $\psi$ sous hypothèse d'équité faible telle 
  le scheduler met à jour les  éléments of $S^t$
  donnés par \verb+update_elems+ à l'itération $t$.
\end{lemma}
\begin{proof}
  La preuve est directe pour $t=0$.
  Supposons qu'elle est établie jusqu'en $t$ valant un certain $t_0$. 
  On considère des stratégies pseudo-périodiques.
  Grâce à l'hypothèse d'équité faible, \verb+update_elems+ modifie 
  les éléments de $S^t$ à l'itération $t$.
\end{proof}

Dans ce qui suit, soit     $Xd^t_{ji}$     la valeur de 
\verb+Xd[+$j$\verb+].v[+$i$\verb+]+  après le   $t^{\text{ème}}$ appel 
à la fonction 
\verb+fetch_values+. 
De plus, soit $Y^k_{ij}$  l'élément à l'indice $k$ 
dans le canal  \verb+channels[i].sent[j]+ de taille  $m$,  $m  \le
\delta_0$; $Y^0_{ij}$ et $Y^{m-1}_{ij}$ sont  respectivement la tête et la queue
du canal.  
De plus, soit $(M_{ij}^t)^{t \in  \{1, 1.5, 2, 2.5,\ldots\}}$ une séquence telle que 
$M_{ij}^t$ est une fonction partielle qui associe à chaque
$k$, $0 \le k \le  m-1$, le tuple $(Y^k_{ij},a^k_{ij},c^k_{ij})$ en entrant
dans la fonction \verb+update_elems+ à l'itération $t$ où
% \begin{itemize}
% \item
 $Y^k_{ij}$ est la valeur du canal \verb+channels[i].sent[j]+
  à l'indice $k$,
%\item 
$a^k_{ij}$ est la  date (antérieure à $t$) mémorisant quand $Y^k_{ij}$ est ajouté et 
%\item 
$c^k_{ij}$ est le premier temps où cette valeur est accessible à $j$. 
La valeur est supprimée du canal $i\rightarrow j$ à la date $c^k_{ij}+1$.
%\end{itemize}
$M_{ij}^t$ a la signature suivante:
\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*}

Intuitivement,  $M_{ij}^t$  est la mémoire du canal
\verb+channels[i].sent[j]+ à l'itération $t$. 
On note que le domaine de chaque $M_{ij}^1$ est $\{0\}$ et
$M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$:    en effet le processus 
\verb+init+  initialise \verb+channels[i].sent[j]+ avec \verb+Xp[i]+.

Montrons comment l'indéterminisme des deux fonctions 
\verb+fetch_values+ et  \verb+diffuse_values+  
permet de modéliser l'équation  \Equ{eq:async}.
La  fonction   $M_{ij}^{t+1}$  est  obtenue à l'aide de mises à jour successives
de  $M_{ij}^{t}$  au travers des deux   fonctions   \verb+fetch_values+  and
\verb+diffuse_values+.   Par abus,   soit  $M_{ij}^{t+1/2}$  
la valeur de  $M_{ij}^{t}$ après la première fonction pendant l'itération
 $t$.

Dans ce qui suit, on  considère les éléments  $i$ et  $j$
dans  $[  \mathsf{N}  ]$. 
A l'itération   $t$,  $t   \geq  1$,   soit
$(Y^0_{ij},a^0_{ij},c^0_{ij})$ la valeur de  $M_{ij}^t(0)$ en entrant 
dans la fonction 
\verb+fetch_values+.   
Si  $t$  est égal à  $c^0_{ij}+1$ alors on exécute 
l'instruction qui affecte $Y^0_{ij}$   (\textit{i.e.}, la valeur de tête du 
\verb+channels[i].sent[j]+) à  $Xd_{ji}^t$.  Dans ce cas,  la  fonction
$M_{ij}^t$ est mise à jour comme suit: $M_{ij}^{t+1/2}(k) = M_{ij}^{t}(k+1)$ pour chaque  $k$, $0 \le k \le m-2$ et $m-1$ est supprimée du domaine de $M_{ij}^{t+1/2}$.
Sinon, (\textit{i.e.}, lorsque  $t < c^0_{ij}+1$ ou lorsque le domaine de $M_{ij}$
est vide)  l'instruction  \verb+skip+  est exécutée et   $M_{ij}^{t+1/2}  =
M_{ij}^{t}$.

Dans la fonction \verb+diffuse_values+, 
s'il existe un $\tau$, $\tau\ge t$
tel que \mbox{$D^{\tau}_{ji} = t$}, soit alors   $c_{ij}$ défini par $ \min\{l \mid
D^{l}_{ji} =  t \} $.  Dans ce cas, on exécute l'instruction qui 
ajoute la valeur  \verb+Xp[i]+   dans la queue du canal
\verb+channels[i].sent[j]+.    Alors,
$M_{ij}^{t+1}$ est défini en étendant $M_{ij}^{t+1/2}$  à $m$ de sorte que 
$M_{ij}^{t+1}(m)$ est $(\verb+Xp[i]+,t,c_{ij})$.  
Sinon, (\textit{i.e.}, lorsque $\forall l
\, .  \, l \ge t  \Rightarrow D^{l}_{ji} \neq t$ est établie) l'instruction
\verb+skip+
est  exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.


\begin{lemma}[Existence d'une exécution SPIN]\label{lemma:execution}
  Pour chaque  séquence $(S^t)^{t  \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$, 
  pour chaque fonction $F$,
  il existe une exécution SPIN  telle que pour toute itération $t$, $t
  \ge  1$, et pour chaque  $i$ et $j$ dans  $[ \mathsf{N} ]$  
  on a la propriété suivante:
   
\noindent Si le domaine de $M_{ij}^t$ n'est pas vide, alors
\begin{equation}
  \left\{
    \begin{array}{rcl}
      M_{ij}^1(0) & = & \left(X_i^{D_{ji}^{0}}, 0,0 \right) \\
      \textrm{si $t \geq 2$ alors }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 De plus, on a :
\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 Enfin, pour chaque $k\in S^t$, la valeur de 
la variable  \verb+Xp[k]+  en sortant du processus 
\verb+update_elems+  est  égale à
$X_k^{t}$          \textit{i.e.},          $F_{k}\left(         X_1^{D_{k\,1}^{t-1}},\ldots,
  X_{\mathsf{N}}^{D_{k\,{\mathsf{N}}}^{t-1}}\right)$ à la fin de la  $t^{\text{ème}}$ itération.
\end{lemma}
\begin{proof}
La preuve est faite par induction sur le nombre d'itérations.

\paragraph{Situation initiale:}
Pour le premier item, par définition de $M_{ij}^t$, on a $M_{ij}^1(0) = \left(
  \verb+Xp[i]+, 0,0 \right)$ qui est égal à  $\left(X_i^{D_{ji}^{0}},
  0,0 \right)$.
Ensuite, le premier appel à la  fonction \verb+fetch_value+ 
soit affecte la tête de \verb+channels[i].sent[j]+
à   \verb+Xd[j].v[i]+ soit ne modifie par 
\verb+Xd[j].v[i]+. 
Grâce au processus \verb+init+ process, 
les deux cas sont égaux à 
\verb+Xp[i]+,  \textit{i.e.}, $X_i^0$.  L'équation (\ref{eq:correct_retrieve})  est ainsi établie.

Pour le dernier item, soit $k$, $0  \le  k \le  \mathsf{N}-1$. 
A la fin de la première exécution du processus \verb+update_elems+,
la valeur   de
\verb+Xp[k]+       est       $F(\verb+Xd[+k\verb+].v[0]+,       \ldots,
\verb+Xd[+k\verb+].v[+\mathsf{N}-1\verb+]+)$.  
Ainsi par définition de  $Xd$, ceci est égal à 
$F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,\mathsf{N}-1})$.  Grâce à l'équation \Equ{eq:correct_retrieve},
on peut conclure la preuve.



\paragraph{Induction:}
Supposons maintenant que le lemme~\ref{lemma:execution} est établi jusqu'à 
l'itération $l$.

Tout d'abord, si le domaine  de définition  de la   fonction $M_{ij}^l$  
n'est pas vide, par hypothèse d'induction $M_{ij}^{l}(0)$  est
$\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
\right)$ où $c$ est $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.

A l'itération $l$, si  $l < c + 1$ alors l'instruction 
 \verb+skip+ est exécutée dans la fonction \verb+fetch_values+. 
 Ainsi,   $M_{ij}^{l+1}(0)$  est égal à
$M_{ij}^{l}(0)$.  Puisque $c > l-1$, alors $D_{ji}^c > D_{ji}^{l-1}$ et donc, $c$
est $\min\{k  | D_{ji}^k  > D_{ji}^{l-1} \}$.
Cela implique que 
$D_{ji}^c > D_{ji}^{l-2}$ et $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.

On considère maintenant qu'à l'itération $l$, celui-ci vaut $c + 1$. 
Dit autrement, $M_{ij}$ est modifié en fonction du domaine $\dom(M^l_{ij})$ de
 $M^l_{ij}$:
\begin{itemize}
\item  si $\dom(M_{ij}^{l})=\{0\}$  et $\forall  k\,  . \,  k\ge l  \Rightarrow
  D^{k}_{ji} \neq l$ sont vraies, alors  $\dom(M_{ij}^{l+1})$ est vide et le premier
  item du lemme est vérifié;
\item si $\dom(M_{ij}^{l})=\{0\}$ et $\exists  k\, . \, k\ge l \land D^{k}_{ji}
  = l$  sont vraies, alors $M_{ij}^{l+1}(0)$  vaut  $(\verb+Xp[i]+,l,c_{ij})$ qui est ajouté 
  dans  la fonction \verb+diffuse_values+ de sorte que   $c_{ij}  =
  \min\{k  \mid  D^{k}_{ji}  = l  \}  $.   
  Prouvons qu'on peut exprimer 
  $M_{ij}^{l+1}(0)$  comme  $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$  où
  $c'$ vaut  $\min\{k |  D_{ji}^k > D_{ji}^{l-1}  \}$.  
  Tout d'abord, il n'est pas difficile de prouver que 
  $D_{ji}^{c_{ij}}= l \geq  D_{ji}^{l} > D_{ji}^{l-1}$  et que 
  $c_{ij}  \geq   c'$.   
  Ensuite, comme   $\dom(M_{ij}^{l})=\{0\}$,  alors, entre les 
  itérations $D_{ji}^{c}+1$ et $l-1$, la fonction  \texttt{diffuse\_values} n'a pas mis à jour
   $M_{ij}$. On a ainsi la propriété
$$
\forall t,k  \, .\, D_{ji}^c <  t < l \land  k \geq t  \Rightarrow D_{ji}^k \neq
t.$$

En particulier, on a   $D_{ji}^{c'} \not  \in \{D_{ji}^{c}+1,\ldots,l-1\}$.  
On peut donc appliquer le troisième item de l'hypothèse d'induction pour déduire
$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ et on peut conclure.

\item  Si   $\{0,1\}  \subseteq  \dom(M_{ij}^{l})$, alors  $M_{ij}^{l+1}(0)$ vaut
  $M_{ij}^{l}(1)$.   Soit  $M_{ij}^{l}(1)=  \left(\verb+Xp[i]+, a_{ij}  ,  c_{ij}
  \right)$.   Par construction,  $a_{ij}$  vaut $\min\{t'  |  t' >  D_{ji}^c  \land
  (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$  et  $c_{ij}$ est $\min\{k |
  D_{ji}^k = a_{ij}\}$.  Montrons que   $c_{ij}$ est égal à  $\min\{k | D_{ji}^k >
  D_{ji}^{l-1} \}$, noté plus tard $c'$.  On a tout d'abord $D_{ji}^{c_{ij}} =
  a_{ij} >  D_{ji}^c$. Puisque $c$  par définition est supérieur ou égal à  $l-1$,
  alors $D_{ji}^{c_{ij}}>  D_{ji}^{l-1}$ et donc $c_{ij} \geq  c'$.  Ensuite, puisque
  $c=l-1$, $c'$ vaut  $\min\{k |  D_{ji}^k > D_{ji}^{c} \}$  et donc $a_{ij}
  \leq  D_{ji}^{c'}$. Ainsi,  $c_{ij} \leq  c'$  et on peut conclure comme dans la partie précédente.
\end{itemize}


Le cas où le domaine $\dom(M^l_{ij})$ est vide mais où la formule  $\exists k
\, .\, k \geq  l \land D_{ji}^k = l$ est vraie est équivalent au second
cas ci-dessus et n'est pas présenté.


Concentrons nous sur la formule~(\ref{eq:correct_retrieve}).  A l'itération 
$l+1$, soit $c'$ défini par  $c'=\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$.  Deux cas peuvent 
apparaître selon que $D_{ji}^{l}$ et  $D_{ji}^{l-1}$ sont égaux ou non.
\begin{itemize}
\item Si  $D_{ji}^{l} = D_{ji}^{l-1}$, puisque $D_{ji}^{c'}  > D_{ji}^{l-1}$, alors
  $D_{ji}^{c'} > D_{ji}^{l}$ et donc $c'$  est différent de  $l$. L'exécution de SPIN
  ne modifie pas $Xd_{ji}^{l+1}$.  On a ainsi  $Xd_{ji}^{l+1}  =   Xd_{ji}^{l}   =  X_i^{D_{ji}^{l-1}}   =
  X_i^{D_{ji}^{l}}$.
\item Sinon, $D_{ji}^{l}$ et plus grand que $D_{ji}^{l-1}$ et $c$ est donc égal à $l$.
  Selon l'équation \Equ{eq:Mij0},    on a 
  $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$.  Ainsi l'exécution SPIN 
  affecte  $X_i^{D_{ji}^{l}}$ à $Xd_{ji}^{l+1}$,  ce qui termine la preuve 
(\ref{eq:correct_retrieve}).
\end{itemize}

Il reste à prouver la partie inductive de la troisième partie du lemme.
Soit $k$, $k
\in S^{l+1}$. % and $\verb+k'+ = k-1$.
A l'issue de la première exécution 
du processus \verb+update_elems+, on a 
$\verb+Xp[+k\verb+]+=                                   F(\verb+Xd[+k\verb+][0]+,
\ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$.  
Par définition $Xd=F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      
Grâce à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
\end{proof}


\begin{lemma}
  Borner la taille du canal à $\textit{max} = \delta_0$ est suffisant 
  lorsqu'on simule un système dynamique dont les délais sont bornés par  
  $\delta_0$.
\end{lemma}

\begin{proof}
  Pour chaque $i$ et $j$, à chaque itération $t+1$, comme les délais sont bornés par 
  $\delta_0$,  l'élément $i$  doit connaître au plus $\delta_0$ 
  valeurs qui sont
  $X_j^{t}$, \ldots, $X_j^{t-\delta_0+1}$. Elles peuvent être mémorisées dans n'importe quel canal
  de taille $\delta_0$.
\end{proof}


\promelasound*
\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 ?}
  Montrons la contraposée du théorème.
  Le lemme  précédent a montré que pour chaque séquence d'itérations du système dynamique discret,
  Il existe une exécution du modèle PROMELA qui la simule.
  Si des itérations du système dynamique discret sont divergentes, leur exécution vont empêcher 
  le modèle PROMELA de se stabiliser,  \textit{i.e.} 
  ce dernier ne vérifiera pas la propriété LTL (\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}


\promelacomplete*

\begin{proof}
  Pour chaque  modèle  $\psi$ 
  qui ne vérifie pas la propriété  LTL  (\ref{eq:ltl:conv}), 
  il est immédiat de construire les itérations correspondantes du
  système dynamique, dont la stratégie est pseudo-périodique en raison 
  de la propriété d'équité faible..

%   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, $\mathsf{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}