annexePromelaProof.tex

   1 %\JFC{Voir section~\ref{sec:spin:proof}}
   2
   3 Cette section donne les preuves des deux théorèmes de correction et complétude
   4 du chapitre~\ref{chap:promela}.
   5
   6
   7 \begin{lemma}[Stratégie équivalente]\label{lemma:strategy}
   8   Soit $\phi$  un système dynamique discret de stratégie  $(S^t)^{t \in  \Nats}$
   9   et $\psi$  sa traduction en PROMELA.
  10   Il existe une exécution de $\psi$ sous hypothèse d'équité faible telle
  11   le scheduler met à jour les  éléments of $S^t$
  12   donnés par \verb+update_elems+ à l'itération $t$.
  13 \end{lemma}
  14 \begin{proof}
  15   La preuve est directe pour $t=0$.
  16   Supposons qu'elle est établie jusqu'en $t$ valant un certain $t_0$.
  17   On considère des stratégies pseudo-périodiques.
  18   Grâce à l'hypothèse d'équité faible, \verb+update_elems+ modifie
  19   les éléments de $S^t$ à l'itération $t$.
  20 \end{proof}
  21
  22 Dans ce qui suit, soit     $Xd^t_{ji}$     la valeur de
  23 \verb+Xd[+$j$\verb+].v[+$i$\verb+]+  après le   $t^{\text{ème}}$ appel
  24 à la fonction
  25 \verb+fetch_values+.
  26 De plus, soit $Y^k_{ij}$  l'élément à l'indice $k$
  27 dans le canal  \verb+channels[i].sent[j]+ de taille  $m$,  $m  \le
  28 \delta_0$; $Y^0_{ij}$ et $Y^{m-1}_{ij}$ sont  respectivement la tête et la queue
  29 du canal.
  30 De plus, soit $(M_{ij}^t)^{t \in  \{1, 1.5, 2, 2.5,\ldots\}}$ une séquence telle que
  31 $M_{ij}^t$ est une fonction partielle qui associe à chaque
  32 $k$, $0 \le k \le  m-1$, le tuple $(Y^k_{ij},a^k_{ij},c^k_{ij})$ en entrant
  33 dans la fonction \verb+update_elems+ à l'itération $t$ où
  34 % \begin{itemize}
  35 % \item
  36  $Y^k_{ij}$ est la valeur du canal \verb+channels[i].sent[j]+
  37   à l'indice $k$,
  38 %\item
  39 $a^k_{ij}$ est la  date (antérieure à $t$) mémorisant quand $Y^k_{ij}$ est ajouté et
  40 %\item
  41 $c^k_{ij}$ est le premier temps où cette valeur est accessible à $j$.
  42 La valeur est supprimée du canal $i\rightarrow j$ à la date $c^k_{ij}+1$.
  43 %\end{itemize}
  44 $M_{ij}^t$ a la signature suivante:
  45 \begin{equation*}
  46 \begin{array}{rrcl}
  47 M_{ij}^t: &
  48 \{0,\ldots, \textit{max}-1\} &\rightarrow & E_i\times \Nats \times \Nats \\
  49 & k  \in \{0,\ldots, m-1\} & \mapsto & M_{ij}(k)= (Y^k_{ij},a^k_{ij},c^k_{ij}).
  50 \end{array}
  51 \end{equation*}
  52
  53 Intuitivement,  $M_{ij}^t$  est la mémoire du canal
  54 \verb+channels[i].sent[j]+ à l'itération $t$.
  55 On note que le domaine de chaque $M_{ij}^1$ est $\{0\}$ et
  56 $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$:    en effet le processus
  57 \verb+init+  initialise \verb+channels[i].sent[j]+ avec \verb+Xp[i]+.
  58
  59 Montrons comment l'indéterminisme des deux fonctions
  60 \verb+fetch_values+ et  \verb+diffuse_values+
  61 permet de modéliser l'équation  \Equ{eq:async}.
  62 La  fonction   $M_{ij}^{t+1}$  est  obtenue à l'aide de mises à jour successives
  63 de  $M_{ij}^{t}$  au travers des deux   fonctions   \verb+fetch_values+  and
  64 \verb+diffuse_values+.   Par abus,   soit  $M_{ij}^{t+1/2}$
  65 la valeur de  $M_{ij}^{t}$ après la première fonction pendant l'itération
  66  $t$.
  67
  68 Dans ce qui suit, on  considère les éléments  $i$ et  $j$
  69 dans  $[  \mathsf{N}  ]$.
  70 A l'itération   $t$,  $t   \geq  1$,   soit
  71 $(Y^0_{ij},a^0_{ij},c^0_{ij})$ la valeur de  $M_{ij}^t(0)$ en entrant
  72 dans la fonction
  73 \verb+fetch_values+.
  74 Si  $t$  est égal à  $c^0_{ij}+1$ alors on exécute
  75 l'instruction qui affecte $Y^0_{ij}$   (\textit{i.e.}, la valeur de tête du
  76 \verb+channels[i].sent[j]+) à  $Xd_{ji}^t$.  Dans ce cas,  la  fonction
  77 $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}$.
  78 Sinon, (\textit{i.e.}, lorsque  $t < c^0_{ij}+1$ ou lorsque le domaine de $M_{ij}$
  79 est vide)  l'instruction  \verb+skip+  est exécutée et   $M_{ij}^{t+1/2}  =
  80 M_{ij}^{t}$.
  81
  82 Dans la fonction \verb+diffuse_values+,
  83 s'il existe un $\tau$, $\tau\ge t$
  84 tel que \mbox{$D^{\tau}_{ji} = t$}, soit alors   $c_{ij}$ défini par $ \min\{l \mid
  85 D^{l}_{ji} =  t \} $.  Dans ce cas, on exécute l'instruction qui
  86 ajoute la valeur  \verb+Xp[i]+   dans la queue du canal
  87 \verb+channels[i].sent[j]+.    Alors,
  88 $M_{ij}^{t+1}$ est défini en étendant $M_{ij}^{t+1/2}$  à $m$ de sorte que
  89 $M_{ij}^{t+1}(m)$ est $(\verb+Xp[i]+,t,c_{ij})$.
  90 Sinon, (\textit{i.e.}, lorsque $\forall l
  91 \, .  \, l \ge t  \Rightarrow D^{l}_{ji} \neq t$ est établie) l'instruction
  92 \verb+skip+
  93 est  exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.
  94
  95
  96 \begin{lemma}[Existence d'une exécution SPIN]\label{lemma:execution}
  97   Pour chaque  séquence $(S^t)^{t  \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$,
  98   pour chaque fonction $F$,
  99   il existe une exécution SPIN  telle que pour toute itération $t$, $t
 100   \ge  1$, et pour chaque  $i$ et $j$ dans  $[ \mathsf{N} ]$
 101   on a la propriété suivante:
 102
 103 \noindent Si le domaine de $M_{ij}^t$ n'est pas vide, alors
 104 \begin{equation}
 105   \left\{
 106     \begin{array}{rcl}
 107       M_{ij}^1(0) & = & \left(X_i^{D_{ji}^{0}}, 0,0 \right) \\
 108       \textrm{si $t \geq 2$ alors }M_{ij}^t(0) & = &
 109       \left(X_i^{D_{ji}^{c}},D_{ji}^{c},c \right) \textrm{, }
 110       c = \min\{l | D_{ji}^l > D_{ji}^{t-2} \}
 111     \end{array}
 112   \right.
 113   \label{eq:Mij0}
 114 \end{equation}
 115 \noindent De plus, on a :
 116 \begin{equation}
 117   \forall t'\, .\,   1 \le t' \le t  \Rightarrow   Xd^{t'}_{ji} = X^{D^{t'-1}_{ji}}_i
 118   \label{eq:correct_retrieve}
 119 \end{equation}
 120 \noindent Enfin, pour chaque $k\in S^t$, la valeur de
 121 la variable  \verb+Xp[k]+  en sortant du processus
 122 \verb+update_elems+  est  égale à
 123 $X_k^{t}$          \textit{i.e.},          $F_{k}\left(         X_1^{D_{k\,1}^{t-1}},\ldots,
 124   X_{\mathsf{N}}^{D_{k\,{\mathsf{N}}}^{t-1}}\right)$ à la fin de la  $t^{\text{ème}}$ itération.
 125 \end{lemma}
 126 \begin{proof}
 127 La preuve est faite par induction sur le nombre d'itérations.
 128
 129 \paragraph{Situation initiale:}
 130 Pour le premier item, par définition de $M_{ij}^t$, on a $M_{ij}^1(0) = \left(
 131   \verb+Xp[i]+, 0,0 \right)$ qui est égal à  $\left(X_i^{D_{ji}^{0}},
 132   0,0 \right)$.
 133 Ensuite, le premier appel à la  fonction \verb+fetch_value+
 134 soit affecte la tête de \verb+channels[i].sent[j]+
 135 à   \verb+Xd[j].v[i]+ soit ne modifie par
 136 \verb+Xd[j].v[i]+.
 137 Grâce au processus \verb+init+ process,
 138 les deux cas sont égaux à
 139 \verb+Xp[i]+,  \textit{i.e.}, $X_i^0$.  L'équation (\ref{eq:correct_retrieve})  est ainsi établie.
 140
 141 Pour le dernier item, soit $k$, $0  \le  k \le  \mathsf{N}-1$.
 142 A la fin de la première exécution du processus \verb+update_elems+,
 143 la valeur   de
 144 \verb+Xp[k]+       est       $F(\verb+Xd[+k\verb+].v[0]+,       \ldots,
 145 \verb+Xd[+k\verb+].v[+\mathsf{N}-1\verb+]+)$.
 146 Ainsi par définition de  $Xd$, ceci est égal à
 147 $F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,\mathsf{N}-1})$.  Grâce à l'équation \Equ{eq:correct_retrieve},
 148 on peut conclure la preuve.
 149
 150
 151
 152 \paragraph{Induction:}
 153 Supposons maintenant que le lemme~\ref{lemma:execution} est établi jusqu'à
 154 l'itération $l$.
 155
 156 Tout d'abord, si le domaine  de définition  de la   fonction $M_{ij}^l$
 157 n'est pas vide, par hypothèse d'induction $M_{ij}^{l}(0)$  est
 158 $\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
 159 \right)$ où $c$ est $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
 160
 161 A l'itération $l$, si  $l < c + 1$ alors l'instruction
 162  \verb+skip+ est exécutée dans la fonction \verb+fetch_values+.
 163  Ainsi,   $M_{ij}^{l+1}(0)$  est égal à
 164 $M_{ij}^{l}(0)$.  Puisque $c > l-1$, alors $D_{ji}^c > D_{ji}^{l-1}$ et donc, $c$
 165 est $\min\{k  | D_{ji}^k  > D_{ji}^{l-1} \}$.
 166 Cela implique que
 167 $D_{ji}^c > D_{ji}^{l-2}$ et $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
 168
 169 On considère maintenant qu'à l'itération $l$, celui-ci vaut $c + 1$.
 170 Dit autrement, $M_{ij}$ est modifié en fonction du domaine $\dom(M^l_{ij})$ de
 171  $M^l_{ij}$:
 172 \begin{itemize}
 173 \item  si $\dom(M_{ij}^{l})=\{0\}$  et $\forall  k\,  . \,  k\ge l  \Rightarrow
 174   D^{k}_{ji} \neq l$ sont vraies, alors  $\dom(M_{ij}^{l+1})$ est vide et le premier
 175   item du lemme est vérifié;
 176 \item si $\dom(M_{ij}^{l})=\{0\}$ et $\exists  k\, . \, k\ge l \land D^{k}_{ji}
 177   = l$  sont vraies, alors $M_{ij}^{l+1}(0)$  vaut  $(\verb+Xp[i]+,l,c_{ij})$ qui est ajouté
 178   dans  la fonction \verb+diffuse_values+ de sorte que   $c_{ij}  =
 179   \min\{k  \mid  D^{k}_{ji}  = l  \}  $.
 180   Prouvons qu'on peut exprimer
 181   $M_{ij}^{l+1}(0)$  comme  $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$  où
 182   $c'$ vaut  $\min\{k |  D_{ji}^k > D_{ji}^{l-1}  \}$.
 183   Tout d'abord, il n'est pas difficile de prouver que
 184   $D_{ji}^{c_{ij}}= l \geq  D_{ji}^{l} > D_{ji}^{l-1}$  et que
 185   $c_{ij}  \geq   c'$.
 186   Ensuite, comme   $\dom(M_{ij}^{l})=\{0\}$,  alors, entre les
 187   itérations $D_{ji}^{c}+1$ et $l-1$, la fonction  \texttt{diffuse\_values} n'a pas mis à jour
 188    $M_{ij}$. On a ainsi la propriété
 189 $$
 190 \forall t,k  \, .\, D_{ji}^c <  t < l \land  k \geq t  \Rightarrow D_{ji}^k \neq
 191 t.$$
 192
 193 En particulier, on a   $D_{ji}^{c'} \not  \in \{D_{ji}^{c}+1,\ldots,l-1\}$.
 194 On peut donc appliquer le troisième item de l'hypothèse d'induction pour déduire
 195 $\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ et on peut conclure.
 196
 197 \item  Si   $\{0,1\}  \subseteq  \dom(M_{ij}^{l})$, alors  $M_{ij}^{l+1}(0)$ vaut
 198   $M_{ij}^{l}(1)$.   Soit  $M_{ij}^{l}(1)=  \left(\verb+Xp[i]+, a_{ij}  ,  c_{ij}
 199   \right)$.   Par construction,  $a_{ij}$  vaut $\min\{t'  |  t' >  D_{ji}^c  \land
 200   (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$  et  $c_{ij}$ est $\min\{k |
 201   D_{ji}^k = a_{ij}\}$.  Montrons que   $c_{ij}$ est égal à  $\min\{k | D_{ji}^k >
 202   D_{ji}^{l-1} \}$, noté plus tard $c'$.  On a tout d'abord $D_{ji}^{c_{ij}} =
 203   a_{ij} >  D_{ji}^c$. Puisque $c$  par définition est supérieur ou égal à  $l-1$,
 204   alors $D_{ji}^{c_{ij}}>  D_{ji}^{l-1}$ et donc $c_{ij} \geq  c'$.  Ensuite, puisque
 205   $c=l-1$, $c'$ vaut  $\min\{k |  D_{ji}^k > D_{ji}^{c} \}$  et donc $a_{ij}
 206   \leq  D_{ji}^{c'}$. Ainsi,  $c_{ij} \leq  c'$  et on peut conclure comme dans la partie précédente.
 207 \end{itemize}
 208
 209
 210 Le cas où le domaine $\dom(M^l_{ij})$ est vide mais où la formule  $\exists k
 211 \, .\, k \geq  l \land D_{ji}^k = l$ est vraie est équivalent au second
 212 cas ci-dessus et n'est pas présenté.
 213
 214
 215 Concentrons nous sur la formule~(\ref{eq:correct_retrieve}).  A l'itération
 216 $l+1$, soit $c'$ défini par  $c'=\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$.  Deux cas peuvent
 217 apparaître selon que $D_{ji}^{l}$ et  $D_{ji}^{l-1}$ sont égaux ou non.
 218 \begin{itemize}
 219 \item Si  $D_{ji}^{l} = D_{ji}^{l-1}$, puisque $D_{ji}^{c'}  > D_{ji}^{l-1}$, alors
 220   $D_{ji}^{c'} > D_{ji}^{l}$ et donc $c'$  est différent de  $l$. L'exécution de SPIN
 221   ne modifie pas $Xd_{ji}^{l+1}$.  On a ainsi  $Xd_{ji}^{l+1}  =   Xd_{ji}^{l}   =  X_i^{D_{ji}^{l-1}}   =
 222   X_i^{D_{ji}^{l}}$.
 223 \item Sinon, $D_{ji}^{l}$ et plus grand que $D_{ji}^{l-1}$ et $c$ est donc égal à $l$.
 224   Selon l'équation \Equ{eq:Mij0},    on a
 225   $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$.  Ainsi l'exécution SPIN
 226   affecte  $X_i^{D_{ji}^{l}}$ à $Xd_{ji}^{l+1}$,  ce qui termine la preuve
 227 (\ref{eq:correct_retrieve}).
 228 \end{itemize}
 229
 230 Il reste à prouver la partie inductive de la troisième partie du lemme.
 231 Soit $k$, $k
 232 \in S^{l+1}$. % and $\verb+k'+ = k-1$.
 233 A l'issue de la première exécution
 234 du processus \verb+update_elems+, on a
 235 $\verb+Xp[+k\verb+]+=                                   F(\verb+Xd[+k\verb+][0]+,
 236 \ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$.
 237 Par définition $Xd=F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.
 238 Grâce à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
 239 \end{proof}
 240
 241
 242 \begin{lemma}
 243   Borner la taille du canal à $\textit{max} = \delta_0$ est suffisant
 244   lorsqu'on simule un système dynamique dont les délais sont bornés par
 245   $\delta_0$.
 246 \end{lemma}
 247
 248 \begin{proof}
 249   Pour chaque $i$ et $j$, à chaque itération $t+1$, comme les délais sont bornés par
 250   $\delta_0$,  l'élément $i$  doit connaître au plus $\delta_0$
 251   valeurs qui sont
 252   $X_j^{t}$, \ldots, $X_j^{t-\delta_0+1}$. Elles peuvent être mémorisées dans n'importe quel canal
 253   de taille $\delta_0$.
 254 \end{proof}
 255
 256
 257 \promelasound*
 258 \begin{proof}
 259 %   For  the  case  where  the  strategy  is  finite,  one  notice  that  property
 260 %   verification  is achieved  under  weak fairness  property.  Instructions  that
 261 %   write or read into \verb+channels[j].sent[i]+ are continuously enabled leading
 262 %   to  convenient  available  dates  $D_{ji}$.   It is  then  easy  to  construct
 263 %   corresponding iterations of the DDN that are convergent.
 264 % \ANNOT{quel sens donnes-tu a \emph{convenient} ici ?}
 265   Montrons la contraposée du théorème.
 266   Le lemme  précédent a montré que pour chaque séquence d'itérations du système dynamique discret,
 267   Il existe une exécution du modèle PROMELA qui la simule.
 268   Si des itérations du système dynamique discret sont divergentes, leur exécution vont empêcher
 269   le modèle PROMELA de se stabiliser,  \textit{i.e.}
 270   ce dernier ne vérifiera pas la propriété LTL (\ref{eq:ltl:conv}).
 271 \end{proof}
 272
 273
 274 % \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}
 275 % Let $\phi$ be a DDN model where strategy, $X^(0)$
 276 % are only constrained to be pseudo-periodic and
 277 % in $E$ respectively.
 278 % Let $\psi$ be its translation.
 279 % If all the executions of $\psi$ converge,
 280 % then  iterations of $\phi$ are universally convergent.
 281 % \end{Corol}
 282
 283
 284 \promelacomplete*
 285
 286 \begin{proof}
 287   Pour chaque  modèle  $\psi$
 288   qui ne vérifie pas la propriété  LTL  (\ref{eq:ltl:conv}),
 289   il est immédiat de construire les itérations correspondantes du
 290   système dynamique, dont la stratégie est pseudo-périodique en raison
 291   de la propriété d'équité faible..
 292
 293 %   i.e. iterations that  are divergent.   Executions are
 294 %   performed under weak  fairness property; we then detail  what are continuously
 295 %   enabled:
 296 % \begin{itemize}
 297 % \item if the strategy is not  defined as periodic, elements $0$, \ldots, $\mathsf{N}$ are
 298 %   infinitely often updated leading to pseudo-periodic strategy;
 299 % \item  instructions  that  write  or read  into  \verb+channels[j].sent[i]+  are
 300 %   continuously enabled leading to convenient available dates $D_{ji}$.
 301 % \end{itemize}
 302 % The simulated DDN does not stabilize and its iterations are divergent.
 303  \end{proof}
 304