X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/251b65007a909068d3344bd82b7c5ec0ffb0a21a..cb56b165bc864d9858b71195e2fb3ea9cb899683:/modelchecking.tex?ds=inline diff --git a/modelchecking.tex b/modelchecking.tex index f69df76..ca223fb 100644 --- a/modelchecking.tex +++ b/modelchecking.tex @@ -1,4 +1,64 @@ -\JFC{donner dans les rappels les délais et les propriétés de convergence uniforme} +\JFC{donner dans les rappels les délais et les propriétés de convergence universelle} + +\JFC{Statuer sur la taille des exemples traitables par la démarche, cf données pratiques} + +\section{Exemple jouet} + +\begin{xpl} + On considère dans ce chapitre l'exemple où trois éléments dans $\Bool$. + Chaque configuration est ainsi un élement de $\{0,1\}^3$, \textit{i.e.}, + un nombre entre 0 et 7. + La \Fig{fig:map} précise la fonction $f$ considérée et + la \Fig{fig:xplgraph} donne son graphe d'intéraction. + +\begin{figure}[ht] + \centering + \begin{minipage}%[h] + {.6\linewidth} + \begin{center} + $ F(x)= \left \{ + \begin{array}{rcl} + f_1(x_1,x_2,x_3) & = & x_1.\overline{x_2} + x_3 \\ + f_2(x_1,x_2,x_3) & = & x_1 + \overline{x_3} \\ + f_3(x_1,x_2,x_3) & = & x_2.x_3 + \end{array} + \right. + $ + \end{center} + \caption{Fonction à itérer} \label{fig:map} + \end{minipage} + \begin{minipage}%[h] + {.35\linewidth} + \begin{center} + \includegraphics[width=4cm]{images/xplCnxMc.eps} + \end{center} + \caption{Graphe d'intéraction} + \label{fig:xplgraph} + \end{minipage} + \caption{Exemple pour SDD $\approx$ SPIN.} +\end{figure} + + + + + + +On peut facilement vérifier que toutes les itérations parallèles initialisées +avec $x^0 \neq 7$ soit $(111)$ +convergent vers $2$ soit $(010)$; celles initialisées avec +$x^0=7$ restent en 7. +Pour les autres modes synchrones avec une +stratégie pseudo périodique, les comportements selon la configuration initiale: +\begin{itemize} +\item initialisée avec 7, les itérations restent en 7; +\item initialisée avec 0, 2, 4 ou 6 les itérations convergent vers 2; +\item initialisées avec 1, 3 ou 5, les itérations convergent vers un des +deux points fixes 2 ou 7. +\end{itemize} +\end{xpl} + + + \section{Rappels sur le langage PROMELA} @@ -37,7 +97,7 @@ Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte}, on peut déclarer des tableaux à une dimension de taille constante ou des nouveaux types de données (introduites par le mot clef \verb+typedef+). Ces derniers sont utilisés pour définir des tableaux à deux -dimension. +dimensions. \begin{xpl} Le programme donné à la {\sc Figure}~\ref{fig:arrayofchannels} correspond à des @@ -47,23 +107,23 @@ Il définit tout d'abord: \item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le nombre $n$ d'éléments et le délais maximum $\delta_0$; \item les deux tableaux (\verb+X+ et \verb+Xp+) de \verb+N+ variables booléennes; -les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associées à la variables $X_{i+1}$ +les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associées à la variables $x_{i+1}$ d'un système dynamique discret (le décalages d'un entier est dû à l'indexation à partir de zéro des cellules d'un tableau); Elles mémorisent les valeurs de $X_{i+1}$ respectivement avant et après sa mise à jour; -il suffit ainsi de comparer \verb+X+ et \verb+Xp+ pour constater si $X$ à changé ou pas; +il suffit ainsi de comparer \verb+X+ et \verb+Xp+ pour constater si $x$ à changé ou pas; \item le tableau \verb+mods+ contient les éléments qui doivent être modifiés lors de l'itération -en cours; cela correspond naturellement à l'ensemble des éléments $S^t$; +en cours; cela correspond naturellement à l'ensemble des éléments $s^t$; \item le type de données structurées \verb+vals+ et le tableau de tableaux - \verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise à mémoriser $X_{j+1}^{D^{t-1}_{i+1j+1}}$ - pour l'itération au temps $t$ (en d'autres termes, utile lors du calcul de $X^{t}$). + \verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise à mémoriser $x_{j+1}^{D^{t-1}_{i+1j+1}}$ + pour l'itération au temps $t$ (en d'autres termes, utile lors du calcul de $x^{t}$). \end{itemize} Puisque le décalage d'un indices ne change pas fondamentalement le comportement de la version PROMELA par rapport au modèle initial et pour des raisons de clarté, on utilisera par la suite la même -lettre d'indice entre les deux niveaux (pour le modèle: $X_i$ et pour PROMELA: +lettre d'indice entre les deux niveaux (pour le modèle: $x_i$ et pour PROMELA: \texttt{X[i]}). Cependant, ce décalage devra être conservé mémoire. Une donnée de type \texttt{channel} permet le @@ -74,7 +134,7 @@ Dans l'exemple précédent, on déclare successivement: \begin{itemize} \item un canal \verb+sent+ qui vise à mémoriser\verb+d_0+ messages de type \verb+bool+; le tableau nommé \verb+channels+ de \verb+N+*\verb+N+ - éléments de type \verb+a_send+ est utilisé pour mémoriser les valeurs intermédiaires $X_j$; + éléments de type \verb+a_send+ est utilisé pour mémoriser les valeurs intermédiaires $x_j$; Il permet donc de temporiser leur emploi par d'autres elements $i$. \item les deux canaux \verb+unlock_elements_update+ et \verb+sync_mutex+ contenant chacun un message booléen et utilisé ensuite comme des sémaphores. @@ -92,13 +152,13 @@ d'initialiser les variables, lancer d'autres process\ldots Les instructions d'affectation sont interprétées usuellement. -Les canaux sont cernés par des instructions particulières d'envoi et de +Les canaux sont concernés par des instructions particulières d'envoi et de réception de messages. Pour un canal -\verb+ch+, ces instruction sont respectivement notées -\verb+ch ! m+ et \verb+ch ? m+. +\verb+ch+, ces instructions sont respectivement notées +\verb+ch ! m+ et \verb+ch ? m+. L'instruction de réception consomme la valeur en tête du canal \verb+ch+ et l'affecte à la variable \verb+m+ (pour peu que \verb+ch+ soit initialisé et non vide). -De manière similaire,l'instruction d'envoi ajoute la valeur de \verb+m+ à la queue du canal +De manière similaire, l'instruction d'envoi ajoute la valeur de \verb+m+ à la queue du canal \verb+ch+ (pour peu que celui-ci soit initialisé et non rempli). Dans les cas problématiques, canal non initialisé et vide pour une réception ou bien rempli pour un envoi, le processus est bloqué jusqu'à ce que les conditions soient remplies. @@ -111,18 +171,17 @@ sera choisi aléatoirement puis exécuté. Dans le process \verb+init+ détaillé à la {\sc Figure}~\ref{fig:spin:init}, une boucle de taille $N$ initialise aléatoirement la variable globale de type tableau \verb+Xp+. Ceci permet par la suite de vérifier si les itérations sont convergentes pour n'importe -quelle configuration initiale $X^{(0)}$. +quelle configuration initiale $x^{(0)}$. Pour chaque élément $i$, si les itérations sont asynchrones \begin{itemize} \item on stocke d'abord la valeur de \verb+Xp[i]+ dans chaque \verb+Xd[j].v[i]+ -puisque la matrice $S^0$ est égale à $(0)$, +puisque la matrice $s^0$ est égale à $(0)$, \item puis, la valeur de $i$ (représentée par \verb+Xp[i]+) devrait être transmise à $j$ s'il y a un arc de $i$ à $j$ dans le graphe d'incidence. Dans ce cas, - c'est la fonction \verb+hasnext+ (non détaillée ici) - \JFC{la détailler} + c'est la fonction \verb+hasnext+ (détaillée à la~\Fig{fig:spin:hasnext}) qui mémorise ce graphe en fixant à \texttt{true} la variable \verb+is_succ+, naturellement et à \texttt{false} dans le cas contraire. @@ -130,7 +189,7 @@ puisque la matrice $S^0$ est égale à $(0)$, \end{itemize} \begin{figure}[t] - \begin{minipage}[h]{.52\linewidth} + \begin{minipage}[h]{.32\linewidth} \begin{tiny} \begin{lstlisting} init{ @@ -167,7 +226,7 @@ init{ \end{tiny} \caption{Process init.}\label{fig:spin:init} \end{minipage}\hfill - \begin{minipage}[h]{.42\linewidth} + \begin{minipage}[h]{.32\linewidth} \begin{tiny} \begin{lstlisting} active proctype scheduler(){ @@ -193,6 +252,28 @@ active proctype scheduler(){ \caption{Process scheduler pour la stratégie pseudo pérodique. \label{fig:scheduler}} \end{minipage} +\begin{minipage}[h]{.30\linewidth} +\begin{tiny} +\begin{lstlisting} +inline hasnext(i,j){ + if + :: i==0 && j ==0 -> is_succ = 1 + :: i==0 && j ==1 -> is_succ = 1 + :: i==0 && j ==2 -> is_succ = 0 + :: i==1 && j ==0 -> is_succ = 1 + :: i==1 && j ==1 -> is_succ = 0 + :: i==1 && j ==2 -> is_succ = 1 + :: i==2 && j ==0 -> is_succ = 1 + :: i==2 && j ==1 -> is_succ = 1 + :: i==2 && j ==2 -> is_succ = 1 + fi +} +\end{lstlisting} +\end{tiny} +\caption{Codage du graphe d'intéraction de $f$. + \label{fig:spin:hasnext}} +\end{minipage} + \end{figure} @@ -208,7 +289,7 @@ ces notions est traduite vers un modèle PROMELA. \subsection{La stratégie}\label{sub:spin:strat} Regardons comment une stratégie pseudo périodique peut être représentée en PROMELA. Intuitivement, un process \verb+scheduler+ (comme représenté à la {\sc Figure}~\ref{fig:scheduler}) -est iterrativement appelé pour construire chaque $S^t$ représentant +est iterrativement appelé pour construire chaque $s^t$ représentant les éléments possiblement mis à jour à l'itération $t$. Basiquement, le process est une boucle qui est débloquée lorsque la valeur du sémaphore @@ -216,37 +297,36 @@ Basiquement, le process est une boucle qui est débloquée lorsque la valeur du aléatoirement (grâce à $n$ choix successifs) et sont mémorisés dans le tableau \verb+mods+, dont la taille est \verb+ar_len+. Dans la séquence d'exécution, le choix d'un élément mis à jour est directement -suivi par des mis à jour: ceci est réalisé grâce à la modification de la valeur du sémaphore +suivi par des mises à jour: ceci est réalisé grâce à la modification de la valeur du sémaphore \verb+unlock_elements_updates+. -\subsection{Itérer la fonction $F$}\label{sub:spin:update} -La mise à jour de l'ensemble $S^t=\{s_1,\ldots, s_m\}$ des éléments qui constituent la stratégie -$(S^t)^{t \in \Nats}$ est implanté à l'aide du process \verb+update_elems+ fourni à la +\subsection{Itérer la fonction $f$}\label{sub:spin:update} +La mise à jour de l'ensemble $s^t=\{s_1,\ldots, s_m\}$ des éléments qui constituent la stratégie +$(s^t)^{t \in \Nats}$ est implantée à l'aide du process \verb+update_elems+ fourni à la {\sc Figure}~\ref{fig:proc}. Ce process actif attend jusqu'à ce qu'il soit débloqué par le process \verb+scheduler+ à l'aide du sémaphore \verb+unlock_elements_update+. -L'implantation contient donc cinq étapes: - -\begin{enumerate} -\item elle commence en mettant à jour la variable \texttt{X} avec les valeurs de \texttt{Xp} - dans la fonction \texttt{update\_X} (non détaillée ici); -\item elle mémorise dans \texttt{Xd} la valeurs disponibles des éléments grâce à - la fonction \texttt{fetch\_values} (cf. \Sec{sub:spin:vt}); -\item une boucle sur les \texttt{ar\_len} éléments qui peuvent être modifiés - met à jour iterrativement la valeur de $j$ (grâce à l'appel de fonction \texttt{F(j)}) - pour peu que celui-ci doive être modifié, \textit{i.e.}, pour peu qu'il soit renseigné dans - \texttt{mods[count]}; le code source de \texttt{F} est donné en {\sc Figure}~\ref{fig:p} et est une - traduction directe de l'application $F$; -\item les nouvelles valeurs des éléments \texttt{Xp} sont symboliquement envoyés aux - autres éléments qui en dépendent grâce à la fonction - \texttt{diffuse\_values(Xp)} (cf. \Sec{sub:spin:vt}); -\item finalement, le process informe le scheduler de la fin de la tâche - (au travers du sémaphore \texttt{sync\_mutex}). -\end{enumerate} - +L'implantation se déroule en cinq étapes: \begin{figure}[t] - \begin{minipage}[h]{.475\linewidth} +\begin{minipage}[b]{.32\linewidth} +\begin{tiny} +\begin{lstlisting} +inline update_X(){ + int countu; + countu = 0; + do + :: countu == N -> break ; + :: countu != N -> + X[countu] = Xp[countu]; + countu ++ ; + od +} +\end{lstlisting} +\end{tiny} +\caption{Sauvegarde de l'état courant}\label{fig:spin:sauve} +\end{minipage}\hfill% +\begin{minipage}[b]{.32\linewidth} \begin{tiny} \begin{lstlisting} active proctype update_elems(){ @@ -278,7 +358,7 @@ active proctype update_elems(){ \end{minipage}\hfill% %\end{figure} %\begin{figure} - \begin{minipage}[h]{.45\linewidth} + \begin{minipage}[b]{.33\linewidth} \begin{tiny} \begin{lstlisting} inline F(){ @@ -294,11 +374,35 @@ inline F(){ } \end{lstlisting} \end{tiny} -\caption{Application de la fonction $F$.}\label{fig:p} +\caption{Application de la fonction $f$.}\label{fig:p} \end{minipage} \end{figure} +\begin{enumerate} +\item elle commence en mettant à jour la variable \texttt{X} avec les valeurs de \texttt{Xp} dans la fonction \texttt{update\_X},~\Fig{fig:spin:sauve} +\item elle mémorise dans \texttt{Xd} la valeurs disponible pour chaque élément grâce à la fonction \texttt{fetch\_values}; cette fonction est détaillée +dans la section suivante; +\item une boucle %sur les \texttt{ar\_len} éléments qui peuvent être modifiés + met à jour iterrativement la valeur de $j$ (grâce à l'appel de fonction \texttt{f(j)}) + pour peu que celui-ci doive être modifié, \textit{i.e.}, pour peu qu'il soit renseigné dans + \texttt{mods[count]}; le code source de \texttt{F} est donné en {\sc Figure}~\ref{fig:p} et est une + traduction directe de l'application $f$; +\item les nouvelles valeurs des éléments \texttt{Xp} sont symboliquement + envoyés aux autres éléments qui en dépendent grâce à la fonction + \texttt{diffuse\_values(Xp)}; cette dernière fonction est aussi détaillée + dans la section suivante; +\item finalement, le process informe le scheduler de la fin de la tâche + (au travers du sémaphore \texttt{sync\_mutex}). +\end{enumerate} + + + + + + + + \subsection{Gestion des délais}\label{sub:spin:vt} Cette section montre comment les délais inhérents au mode asynchrone sont traduits dans le modèle PROMELA grâce à deux @@ -377,7 +481,7 @@ La première fonction met à jour le tableau \verb+Xd+ requis pour les éléme qui doivent être modifiés. Pour chaque élément dans \verb+mods+, identifié par la variable $j$, la fonction récupère les valeurs des autres éléments (dont le libellé est $i$) -dont $j$ dépend. \JFC{vérifier si c'est ce sens ici} +dont $j$ dépend. Il y a deux cas. \begin{itemize} \item puisque $i$ connaît sa dernière valeur (\textit{i.e.}, $D^t_{ii}$ est toujours $t$) @@ -388,17 +492,16 @@ Il y a deux cas. \item depuis la perspective de $j$ la valeur de $i$ peut ne pas avoir changé ( c'est l'instruction \verb+skip+) ou n'est pas utile; ce dernier cas apparaît lorsqu'il n'y a pas d'arc de $i$ à $j$ dans le graphe d'incidence, \textit{i.e.}, lorsque - la valeur de \verb+is_succ+ qui est calculée par \verb+hasnext(i,j)+ is 0; + la valeur de \verb+is_succ+ qui est calculée par \verb+hasnext(i,j)+ est 0; dans ce cas, la valeur de \verb+Xd[j].v[i]+ n'est pas modifiée; \item sinon, on affecte à \verb+Xd[j].v[i]+ la valeur mémorisée dans le canal \verb+channels[i].sent[j]+ (pour peu que celui-ci ne soit pas vide). - Les valeurs des éléments sont ajoutées dans ce canal au travers de la fonction \verb+diffuse_values+ - donnée juste après. \end{itemize} \end{itemize} -L'objectif de la fonction \verb+diffuse_values+ est de stocker les valeurs de $X$ représenté -dans le modèle par \verb+Xp+ dans le canal \verb+channels+. +Les valeurs des éléments sont ajoutées dans ce canal au travers de la fonction \verb+diffuse_values+. L'objectif de cette fonction +est de stocker les valeurs de $x$ (représenté +dans le modèle par \verb+Xp+) dans le canal \verb+channels+. Il permet au modèle-checker SPIN d'exécuter le modèle PROMELA comme s'il pouvait y avoir des délais entre processus Il y a deux cas différents pour la valeur de $X_{j}$: @@ -411,11 +514,11 @@ n'y a pas d'arc de $j$ à $i$ dans le graphe d'incidence; L'introduction de l'indéterminisme à la fois dans les fonctions \verb+fetch_values+ et \verb+diffuse_values+ est nécessaire dans notre contexte. Si celui-ci n'était -présent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple récupérer -la valeur $X_i^{(t)}$ sans considérer la valeur $X_i^{(t-1)}$. +présent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple récupérer * +la valeur $x_i^{(t)}$ sans considérer la valeur $x_i^{(t-1)}$. De manière duale, si le non déterminisme était uniquement utilisé dans la fonction \verb+diffuse_values+, alors chaque fois qu'une valeur serait -mise dans le canal, elle serait immédiatement consommé, ce qui est contradictoire avec la notion de +mise dans le canal, elle serait immédiatement consommée, ce qui est contradictoire avec la notion de délai. % \subsection{Discussion} @@ -434,11 +537,12 @@ délai. % instructions, making the PROMELA code and the DDN as closed as possible. \subsection{Propriété de convergence universelle} -Il reste à formaliser dans le model checker SPIN que les itérations d'un système +Il reste à formaliser dans le model checker SPIN le fait que les +itérations d'un système dynamique à $n$ éléments est universellement convergent. Rappelons tout d'abord que les variables \verb+X+ et \verb+Xp+ -contiennent respectivement la valeur de $X$ avant et après la mise à jour. +contiennent respectivement la valeur de $x$ avant et après la mise à jour. Ainsi, si l'on effectue une initialisation non déterministe de \verb+Xp+ et si l'on applique une stratégie pseudo périodique, il est nécessaire et suffisant @@ -447,18 +551,22 @@ de prouver la formule temporelle linéaire (LTL) suivante: \diamond (\Box \verb+Xp+ = \verb+X+) \label{eq:ltl:conv} \end{equation} -où les opérateur $\diamond$ et $\Box$ on la sémantique usuelle \textit{i.e.}, à savoir +où les opérateur $\diamond$ et $\Box$ ont +la sémantique usuelle, à savoir respectivement {\em éventuellement} et {\em toujours} dans les chemins suivants. -On note que cette propriété assure seulement la stabilisation du système, -mais ne donne aucune métrique quant à la manière dont celle-ci est obtenue. +On note que cette propriété, si elle est établie, garantit +la stabilisation du système. +Cependant elle ne donne aucune métrique quant à +la manière dont celle-ci est obtenue. En particulier, on peut converger très lentement ou le système peut même disposer de plusieurs points fixes. -vers plusieurs + \section{Correction et complétude de la démarche}\label{sec:spin:proof} -Cette section présente les théorème de correction et de complétude de l'approche. +Cette section présente les théorèmes +de correction et de complétude de l'approche. (Théorèmes~\ref{Theo:sound} et~\ref{Theo:completeness}). Toutes les preuves sont déplacées en annexes~\ref{anx:promela}. @@ -488,9 +596,10 @@ Cette section donne tout d'abord quelques mesures de complexité de l'approche puis présente ensuite les expérimentations issues de ce travail. \begin{theorem}[Nombre d'états ] - Soit $\phi$ un modèle de système dynamique discret à $n$ éléments, $m$ arc dans le graphe d'incidence + Soit $\phi$ un modèle de système dynamique discret à $n$ éléments, $m$ + arcs dans le graphe d'incidence et $\psi$ sa traduction en PROMELA. Le nombre de configurations - de l'exécution en SPIN de $\psi$ est bornée par $2^{m\times(\delta_0+1)+n(n+2)}$. + de l'exécution en SPIN de $\psi$ est bornée par $2^{m(\delta_0+1)+n(n+2)}$. \end{theorem} \begin{Proof} Une configuration est une valuation des variables globales. @@ -502,8 +611,8 @@ puis présente ensuite les expérimentations issues de ce travail. Chaque canal de \verb+array_of_channels+ peut engendrer $1+2^1+\ldots+2^{\delta_0}= 2^{\delta_0+1}-1$ états. Puisque le nombre d'arêtes du graphe d'incidence est $m$, - il y a $m$ canaux non constants, ce qui génère approximativement $2^{m\times(\delta_0+1)}$ états. - Le nombre de configurations est donc borné par $2^{m\times(\delta_0+1)+n(n+2)}$. + il y a $m$ canaux non constants, ce qui génère approximativement $2^{m(\delta_0+1)}$ états. + Le nombre de configurations est donc borné par $2^{m(\delta_0+1)+n(n+2)}$. On remarque que cette borne est traitable par SPIN pour des valeurs raisonnables de $n$, $m$ et $\delta_0$. \JFC{Donner un ordre de grandeur de cet ordre de grandeur} @@ -511,28 +620,32 @@ puis présente ensuite les expérimentations issues de ce travail. \end{Proof} La méthode détaillée ici a pu être appliquée sur l'exemple jouet -pour prouver formellement sa convergence uniforme. +pour prouver formellement sa convergence universelle. On peut remarquer que SPIN n'impose l'équité faible qu'entre les process alors que les preuves des deux théorèmes précédentes reposent sur le fait que celle-ci est établie dès qu'un choix indéterministe est effectué. Naïvement, on pourrait considérer comme hypothèse la formule suivante chaque fois qu'un choix indéterministe se produit entre $k$ événements -respectivement notés $l1$, \ldots $lk$: +respectivement notés $l_1$, \ldots $l_k$: $$ -[] <> (l == l0) \Rightarrow -(([] <> (l== l1)) \land \ldots \land ([] <> (l == lk))) +\Box \diamond (l == l_0) \Rightarrow +((\Box \diamond (l== l_1)) \land \ldots \land (\Box \diamond (l == l_k))) $$ -où le libellé $l0$ dénote le libellé de la ligne précédent le choix indéterministe. +où le libellé $l_0$ dénote le libellé de la ligne précédent +le choix indéterministe. Cette formule traduit exactement l'équité faible. Cependant en raison de l'explosion de la taille du produit entre l'automate de Büchi issu de cette formule et celui issu du programme PROMELA, -SPIN n'arrive pas à vérifier si la convergence uniforme est établie ou non sur des exemples +SPIN n'arrive pas à vérifier si la convergence universelle est établie +ou non sur des exemples simples\JFC{faire référence à un tel exemple}. -Ce problème a été pratiquement résolu en laissant SPIN générer toutes les traces d'exécution, -même les non équitables, puis en le laissant vérifier la propriété de convergence dessus. +Ce problème a été pratiquement résolu en laissant SPIN +générer toutes les traces d'exécution, +même celles qui ne sont pas équitables, +puis ensuite vérifier la propriété de convergence sur toutes celles-ci. Il reste alors à interpréter les résultats qui peuvent être de deux types. Si la convergence est établie pour toutes les traces, elle le reste en particulier pour les traces équitables. Dans le cas contraire on doit analyser le contre exemple produit par SPIN. @@ -551,17 +664,46 @@ Dans le cas contraire on doit analyser le contre exemple produit par SPIN. La méthode détaillée ici a été appliquée sur des exemples pour prouver formellement -leur convergence ou leur divergence (Fig.~\ref{fig:async:exp}). -Dans ces expériences, les délais on été bornés par $\delta_0=10$. -Dans ce tableau, $P$ est vrai ($\top$) si et seulement si la convergence uniforme -est établie et faux ($\bot$) sinon. Le nombre $M$ et la taille de la mémoire consommée (en MB) et +leur convergence ou leur divergence (\Fig{fig:async:exp}). +Dans ces expériences, les délais ont été bornés par $\delta_0=10$. +Dans ce tableau, $P$ est vrai ($\top$) si et seulement si la convergence +universelle +est établie et faux ($\bot$) sinon. Le nombre $M$ est +la taille de la mémoire consommée (en MB) et $T$ est le temps d'exécution sur un Intel Centrino Dual Core 2 Duo @1.8GHz avec 2GB de mémoire vive pour établir un verdict. -L'exemple RE est l'exemple jouet de ce chapitre, -AC2D est un automate cellulaire avec 9 elements prenant des valeurs booléennes en fonction de -de 4 voisins et BM99, issu de~\cite{BM99} consiste en 10 process -qui modifient leur valeur booléennes dans un graphe d'adjacence proche du graphe complet. + +\begin{figure} +\begin{center} +\begin{tiny} +\begin{tabular}{|*{7}{c|}} +\cline{2-7} +\multicolumn{1}{c|}{ } +&\multicolumn{3}{|c|}{Parallèles} & \multicolumn{3}{|c|}{Chaotiques} \\ +\cline{2-7} +\multicolumn{1}{c|}{ }& +P & M & T& +P & M & T \\ +\hline %\cline{2-7} +\textit{RE} & +$\top$ & 2.7 & 0.01s & +$\bot$ & 369.371 & 0.509s \\ +\hline %\cline{2-7} +\cite{RC07} & +$\bot$ & 2.5 & 0.001s & % RC07_sync.spin +$\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin +\hline +\cite{BM99} & +$\top$ & 36.7 & 12s & % BM99_sync_para.spin +$\top$ & & \\ % BM99_sync_chao.spin +\hline +\end{tabular} +\end{tiny} +\end{center} +\caption{Expérimentations avec des itérations synchrones}\label{fig:sync:exp} +\end{figure} + \begin{figure} @@ -582,7 +724,7 @@ P & M & T & P & M & T& P & M & T \\ \hline %cline{2-13} -Running Example & +\textit{RE} & $\top$ & 409 & 1m11s& $\bot$ & 370 & 0.54 & $\bot$ & 374 & 7.7s& @@ -594,7 +736,7 @@ AC2D &$\bot$ & 2.5 & 0.01s % RC07_async.spin &$\bot$ & 2.5 & 0.01s \\ % RC07_async_all.spin \hline %\cline{2-13} -BM99 +\cite{BM99} &$\top$ & & %BM99_mixed_para.spin &$\top$ & & % RC07_async_mixed_all.spin &$\bot$ & & % RC07_async.spin @@ -607,50 +749,40 @@ BM99 -L'exemple~\cite{RC07} concerne un réseau composé de deux gènes à valeur dans $\{0,1,2\}$. -Comme la convergence n'est déjà pas établie pour les itérations parallèles, il en est donc +L'exemple \textit{RE} est l'exemple jouet de ce chapitre, +\cite{RC07} concerne un réseau composé de deux gènes +à valeur dans $\{0,1,2\}$, +AC2D est un automate cellulaire avec 9 elements prenant des +valeurs booléennes en fonction de +de 4 voisins et +\cite{BM99} consiste en 10 process +qui modifient leur valeur booléennes dans un graphe d'adjacence proche +du graphe complet. + + +L'exemple jouet \textit{RE} a été prouvé comme universellement convergent. +\JFC{statuer sur AC2D} +Comme la convergence n'est déjà pas établie pour les itérations parallèles +de~\cite{RC07}, il en est donc de même pour les itérations asynchrones. -LA {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN de menant à la violation +La {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN de menant à la violation de la convergence. Celle-ci correspond à une stratégie périodique qui répète -$\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ et débute avec $X=(0,0)$. - - -Dans l'exemple issu de~\cite{BM99}, nous avons 10 process -à valeur booléennes. En raison de la dépendance forte entre les éléments, +$\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ et débute avec $x=(0,0)$. +En raison de la dépendance forte entre les éléments +de~\cite{BM99}, $\delta_0$ est réduit à 1. Cela aboutit cependant à $2^{100}$ configurations dans le mode des itérations asynchrones. + +\JFC{Quid de ceci?} La convergence des itérations asynchrones de l'exemple~\cite{BCVC10:ir} n'est pas établie -lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence uniforme. +lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle. \begin{figure} -\begin{center} -\begin{tiny} -\begin{tabular}{|*{7}{c|}} -\cline{2-7} -\multicolumn{1}{c|}{ } -&\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\ -\cline{2-7} -\multicolumn{1}{c|}{ }& -P & M & T& -P & M & T \\ -\hline %\cline{2-7} -Running & -$\top$ & 2.7 & 0.01s & -$\bot$ & 369.371 & 0.509s \\ -\hline %\cline{2-7} -\cite{RC07} exemples & -$\bot$ & 2.5 & 0.001s & % RC07_sync.spin -$\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin -\hline -\cite{BM99} exemple & -$\top$ & 36.7 & 12s & % BM99_sync_para.spin -$\top$ & & \\ % BM99_sync_chao.spin -\hline -\end{tabular} -\end{tiny} -\end{center} -\caption{Expérimentations avec des itérations synchrones}\label{fig:sync:exp} -\end{figure} +\centering +\includegraphics[scale=0.6]{images/RC07ce.eps} +\caption{Contre exemple de convergence pour~\ref{fig:RC07CE}} \label{fig:RC07CE} +\end{figure} + @@ -685,7 +817,8 @@ ont déjà été présentées~\cite{BM99,BCV02}. Cependant, comme ces implantations ne sont pas exhaustives, elles ne donnent un résultat formel que lorsqu'elles fournissent un contre-exemple. Lorsqu'elles exhibent une convergence, cela ne permet que donner une intuition de convergence, pas une preuve. -Autant que nous sachions, aucune démarche de preuve formelle de convergence n'a jamais été établie. +Autant que nous sachions, aucune démarche de preuve formelle automatique +de convergence n'a jamais été établie. Dans le travail théorique~\cite{Cha06}, Chandrasekaran a montré que les itérations asynchrones sont convergentes si et seulement si on peut construire une fonction de Lyaponov décroissante, mais il ne donne pas de méthode automatique pour construire cette fonction. @@ -695,9 +828,9 @@ Among drawbacks of the method, one can argue that bounded delays is only realistic in practice for close systems. However, in real large scale distributed systems where bandwidth is weak, this restriction is too strong. In that case, one should only consider that -matrix $S^{t}$ follows the iterations of the system, \textit{i.e.}, +matrix $s^{t}$ follows the iterations of the system, \textit{i.e.}, for all $i$, $j$, $1 \le i \le j \le n$, we have$ -\lim\limits_{t \to \infty} S_{ij}^t = + \infty$. +\lim\limits_{t \to \infty} s_{ij}^t = + \infty$. One challenge of this work should consist in weakening this constraint. We plan as future work to take into account other automatic approaches to discharge proofs notably by deductive analysis~\cite{CGK05}.