preuve promela:debut de traduction

[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 le scheduler met à jour les  elements of $S^t$
  donnés par \verb+update_elems+ à l'iteration $t$.
\end{lemma}
\begin{Proof}
  La preuve est directe pour $t=0$.
  Supposons qu'elle est établie jusqu'en $t$ vallant 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'iteration $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 cannal \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 cannal
\verb+channels[i].sent[j]+ à l'iterations $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  function   $M_{ij}^{t+1}$  est  obtenue à l'aide de mises à jour successives
de  $M_{ij}^{t}$  au travers des deux   functions   \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écution l'instruction qui 
ajoute la valeur  \verb+Xp[i]+   dans la queue du cannal
\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  sequence $(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{th}}$ 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 definition 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'equation (\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écutions 
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})$.      
Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
\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}


\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 ?}

  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}


\promelacomplete*

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