expe ANN

[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}[Strategy Equivalence]\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{th}}$ 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 fonctions pendant l'itération
 $t$.

Dans ce qui suit, on  considère les éléments  $i$ et  $j$
dans  $\llbracket  n  \rrbracket$. 
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$ in  $\llbracket n \rrbracket$  
  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{sit $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 valeurde 
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_{n}^{D_{k\,{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, lepremier 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  n-1$. 
A la fin de la première exécution du processus \verb+update_elems+,
la valur   de
\verb+Xp[k]+       est       $F(\verb+Xd[+k\verb+].v[0]+,       \ldots,
\verb+Xd[+k\verb+].v[+n-1\verb+]+)$.  
Ainsi par définition de  $Xd$, ceci est égal à 
$F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,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  \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}


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