X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/1b923f193392e3ce847882c24a128eff4bee9992..fd3c8d84472bbc887a48fc8e441bd3fafedf96a7:/modelchecking.tex?ds=inline diff --git a/modelchecking.tex b/modelchecking.tex index 936835b..1919416 100644 --- a/modelchecking.tex +++ b/modelchecking.tex @@ -1,6 +1,114 @@ +L'étude de convergence de systèmes dynamiques discrets est simple à vérifier +pratiquement pour le mode synchrone. Lorsqu'on introduit des stratégies +pseudo périodiques pour les modes unaires et généralisées, le problème +se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones +et mixes prenant de plus en compte les délais. + +Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement +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 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. + +Un outil qui construirait automatiquement toutes +les transitons serait le bienvenu. +Pour peu qu'on établisse la preuve de correction et de complétude de la +démarche, la convergence du réseau discret ne repose alors que sur le verdict +donné par l'outil. +Cependant, même pour des réseaux discrets à peu d'éléments, +le nombre de configurations induites explose rapidement. +Les \emph{Model-Checkers}~\cite{Hol03,nusmv02,Blast07,MCErlang07,Bogor03} +sont des classes d'outils qui adressent le problème de vérifier automatiquement +qu'un modèle vérifie une propriété donnée. Pour traiter le problème d'explosion +combinatoire, ces outils appliquent des méthodes d'ordre partiel, d'abstraction, +de quotientage selon une relation d'équivalence. + +Ce chapitre montre comment nous simulons +des réseaux discrets selon toutes les sortes d'itérations pour établir +formellement leur convergence (ou pas). +Nous débutons par un exemple et faisons quelques rappels sur +le langage PROMELA qui est le langage du model-checker +SPIN~\cite{Hol03} (\Sec{sec:spin:promela}). +Nous présentons ensuite la démarche de traduction +de réseaux discrets dans PROMELA (\Sec{sec:spin:translation}). +Les théorèmes de correction et de complétude de la démarche +sont ensuite donnés à la (\Sec{sec:spin:proof}). +Des données pratiques comme la complexité et des synthèses d'expérimentation +sont ensuite fournies (\Sec{sec:spin:practical}). + + + + + + + +%\section{Exemple jouet} + + +\begin{figure}[ht] + \begin{center} + \subfigure[Fonction à itérer]{ + $ 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. + $ + \label{fig:map} + } + \hfill + \subfigure[Graphe d'intéraction]{ + \includegraphics[width=4cm]{images/xplCnxMc.eps} + \label{fig:xplgraph:inter:mc} + } + \end{center} + \caption{Exemple pour SDD $\approx$ SPIN.} +\end{figure} + + + +\begin{xpl} + On considère un exemple à trois éléments dans $\Bool$. + Chaque configuration est ainsi un élément de $\Bool^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:inter:mc} donne son graphe d'intéraction. + + + + + + + +On peut facilement vérifier que toutes les itérations synchrones 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 mode unaires ou généralisés avec une +stratégie pseudo périodique, on a des comportements qui dépendent +de 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} \label{sec:spin:promela} @@ -11,7 +119,7 @@ On peut trouver davantage de détails dans~\cite{Hol03,Wei97}. \begin{figure}[ht] -\begin{scriptsize} +\begin{tiny} \begin{lstlisting} #define N 3 #define d_0 5 @@ -26,82 +134,85 @@ a_send channels [N]; chan unlock_elements_update=[1] of {bool}; chan sync_mutex=[1] of {bool}; \end{lstlisting} -\end{scriptsize} -\caption{Type declaration of the DDNs translation.} +\end{tiny} +\caption{Declaration des types de la traduction.} \label{fig:arrayofchannels} \end{figure} -Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte}, -\texttt{short} et \texttt{int}. Comme dans le langage C par exemple, -on peut declarer des tableaux à une dimension de taille constante +% Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte}, +% \texttt{short} et \texttt{int}. +Comme en C, +on peut déclarer des tableaux à une dimension 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. +\verb+typedef+). % Ces derniers sont utilisés +% pour définir des tableaux à deux +% dimensions. \begin{xpl} Le programme donné à la {\sc Figure}~\ref{fig:arrayofchannels} correspond à des -déclarations de variables qui serviront dans l'exemple jouet de ce chapitre. -Il définit tout d'abord: +déclarations de variables qui servent dans l'exemple de ce chapitre. +Il définit: \begin{itemize} -\item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le numbre +\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}$ -d'un systène dynamique discret -(le décallage d'un entier est dû à l'indexation à partir de zéro des cellules d'un tableau); -Elles memorisent 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; -\item le tableau \verb+mods+ contient les éléments qui doivent être modifiés lors de l'iteration -en cours; cela correspond naturellement à l'ensemble des éléments $S^t$; +les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associées à la variables $x_{i+1}$ +d'un système dynamique discret; +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; +\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$; \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écallage d'un indices ne change pas fondamentalement -le comportement de la version PROMELA par rapport au modèle initial -et pour des raisons de clareté, on utilisera par la suite la même -lettre d'indice entre les deux niveaux (pour le modèle: $X_i$ et pour PROMELA: -\texttt{X[i]}). Cependant, ce décallage devra être conservé mémoire. +% 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: +% \texttt{X[i]}). Cependant, ce décalage devra être conservé mémoire. -Une donnée de type \texttt{channel} permet le +Déclarée avec le mot clef \verb+chan+, +une donnée de type \texttt{channel} permet le transfert de messages entre processus dans un ordre FIFO. -Elles serait déclarée avec le mot clef \verb+chan+ suivi par sa capacité -(qui est constante), son nom et le type des messages qui sont stockés dans ce cannal. +% Elles serait suivi par sa capacité +% (qui est constante), son nom et le type des messages qui sont stockés dans ce canal. Dans l'exemple précédent, on déclare successivement: \begin{itemize} -\item un cannal \verb+sent+ qui vise à mémoriser\verb+d_0+ messages de type +\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 cannaux \verb+unlock_elements_update+ et \verb+sync_mutex+ contenant +\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. \end{itemize} \end{xpl} %\subsection{PROMELA Processes} -Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurence -au sein de systèmes. Un process est déclaréavec le mot-clef -\verb+proctype+ et est instancié soit imédiatement (lorsque sa déclaration est préfixée +Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurrence +au sein de systèmes. Un process est instancié soit immédiatement +(lorsque sa déclaration est préfixée par le mot-clef \verb+active+) ou bien au moment de l'exécution de l'instruction \texttt{run}. Parmi tous les process, \verb+init+ est le process initial qui permet -d'initialiser les variables, lancer d'autres processes\ldots +d'initialiser les variables, lancer d'autres process\ldots -Les instructions d'affecatation sont interprétées usuellement. -Les cannaux sont cernés par des instructions particulières d'envoi et de -réception de messages. Pour un cannal -\verb+ch+, ces instruction sont respectivement notées -\verb+ch ! m+ et \verb+ch ? m+. -L'instruction de réception consomme la valeur en tête du cannal \verb+ch+ +Les instructions d'affectation sont interprétées usuellement. +Les canaux sont concernés par des instructions particulières d'envoi et de +réception de messages. Pour un canal +\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 reception ou bien rempli pour un envoi, -le processus est blocké jusqu'à ce que les conditions soient remplies. +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. La structures de contrôle \verb+if+ (resp. \verb+do+) définit un choix non déterministe (resp. une boucle non déterministe). Que ce soit pour la conditionnelle ou la boucle, @@ -110,28 +221,27 @@ 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 verifier si les itérations sont convergentes pour n'importe -quelle configuration initiale $X^{(0)}$. +Ceci permet par la suite de vérifier si les itérations sont convergentes pour n'importe +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} - qui memorise ce graphe + 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. Cela permet d'envoyer la valeur de $i$ dans le canal au travers de \verb+channels[i].sent[j]+. \end{itemize} \begin{figure}[t] - \begin{minipage}[h]{.52\linewidth} -\begin{scriptsize} + \begin{minipage}[h]{.32\linewidth} +\begin{tiny} \begin{lstlisting} init{ int i=0; int j=0; bool is_succ=0; @@ -164,11 +274,11 @@ init{ sync_mutex ! 1; } \end{lstlisting} -\end{scriptsize} -\caption{PROMELA init process.}\label{fig:spin:init} +\end{tiny} +\caption{Process init.}\label{fig:spin:init} \end{minipage}\hfill - \begin{minipage}[h]{.42\linewidth} -\begin{scriptsize} + \begin{minipage}[h]{.32\linewidth} +\begin{tiny} \begin{lstlisting} active proctype scheduler(){ do @@ -189,10 +299,32 @@ active proctype scheduler(){ od } \end{lstlisting} -\end{scriptsize} -\caption{Scheduler process for common pseudo-periodic strategy. +\end{tiny} +\caption{Process scheduler pour la stratégie pseudo périodique. \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} @@ -206,48 +338,47 @@ 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. +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 itérativement appelé pour construire chaque $S^t$ représentant +est itérativement 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 \verb+sync_mutex+ est 1. Dans ce cas, les éléments à modifier sont choisis 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'éxécution, le choix d'un élément mis à jour est directement -suivi par des mis à jour: ceci est réalisé grace à la modification de la valeur du sémaphore +Dans la séquence d'exécution, le choix d'un élément mis à jour est directement +suivi par des mises à jour: ceci est réalisé grâce à la modification de la valeur du sémaphore \verb+unlock_elements_updates+. -\subsection{Applying the function $F$}\label{sub:spin:update} -Updating a set $S^t=\{s_1,\ldots, s_m\}$ of elements that occur in the strategy -$(S^t)^{t \in \Nats}$ is implemented by the \verb+update_elems+ process given -in~\ref{fig:proc}. This active process waits until it is unlocked by the -\verb+scheduler+ process through the semaphore \verb+unlock_elements_update+. -The implementation is then fivefold: - -\begin{enumerate} -\item it starts with updating the variable \texttt{X} with the values of \texttt{Xp} - thanks to the \texttt{update\_X} function (not detailed here); - %%we recall that the variable \texttt{X} is only defined as -\item it stores in \texttt{Xd} the current available values of the elements thanks - to the function \texttt{fetch\_values} (see \Sec{sub:spin:vt}); -\item a loop over the number \texttt{ar\_len} of elements that have to evolve - iteratively updates the value of $j$ (through the function call \texttt{F(j)}) - provided this has to evolve, \textit{i.e.}, it is referenced by - \texttt{mods[count]}; source code of \texttt{F} is given in~\ref{fig:p} and is a - direct translation of the map $F$; -\item the new components values in \texttt{Xp} are symbolically sent to the other - components requiring them % for future access - thanks to the \texttt{diffuse\_values(Xp)} function (see \Sec{sub:spin:vt}); -\item finally, this process informs the scheduler about the end of the task - (through the semaphore \texttt{sync\_mutex}). -\end{enumerate} - +\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 processus 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 se déroule en cinq étapes: \begin{figure}[t] - \begin{minipage}[h]{.475\linewidth} -\begin{scriptsize} +\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(){ do @@ -273,13 +404,13 @@ active proctype update_elems(){ od } \end{lstlisting} -\end{scriptsize} -\caption{Updatings of the elements.}\label{fig:proc} +\end{tiny} +\caption{Mise à jour des éléments.}\label{fig:proc} \end{minipage}\hfill% %\end{figure} %\begin{figure} - \begin{minipage}[h]{.45\linewidth} -\begin{scriptsize} + \begin{minipage}[b]{.33\linewidth} +\begin{tiny} \begin{lstlisting} inline F(){ if @@ -293,45 +424,46 @@ inline F(){ fi } \end{lstlisting} -\end{scriptsize} -\caption{Application of function $F$.}\label{fig:p} +\end{tiny} +\caption{Application de la fonction $f$.}\label{fig:p} \end{minipage} \end{figure} -% \subsection{Modifying Values of one Element} -% Each element $i$ may modify its value through the coresponding -% active process \verb+pi+. -% In Fig.~\ref{fig:p4} that gives the translation of -% modifying the element $4$, the process is waiting until it is unlocked -% and then it computes the new value of $X_4$, represented by $X'_4$ -% and memorized as \verb+Xp[4]+. +\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 itérativement 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} + -% \begin{ProofCr} -% First of all, the second hypothesis of the previous proof is established. -% In this part, we prove that for any time $t$, - -% The proof is achieved under the hypothesis that at current time $t$, -% For $j$ in $J^t$, variables -% \verb+v0+, \ldots \verb+vn-1+ are respectively -% $X_0^{S_{j0}^t},\ldots, X_{n-1}^{S_{jn-1}^t}$. -% Since \verb+F+ is the direct translation of $F$, rest of the proof is obvious. - - -% \end{ProofCr} -\subsection{Delays Handling}\label{sub:spin:vt} -This section shows how delays are translated into PROMELA through the two -functions \verb+fetch_values+ and \verb+diffuse_values+, given in~\ref{fig:val} and~\ref{fig:broadcast}, that respectively store and transmit the -element values. + +\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 +fonctions \verb+fetch_values+ et \verb+diffuse_values+. +Celles-ci sont données en {\sc Figure}~\ref{fig:val} et~\ref{fig:broadcast}, +qui récupèrent et diffusent respectivement les valeurs des elements. \begin{figure}[t] \begin{minipage}[h]{.475\linewidth} -\begin{scriptsize} +\begin{tiny} \begin{lstlisting} inline fetch_values(){ int countv = 0; @@ -360,11 +492,11 @@ inline fetch_values(){ od } \end{lstlisting} -\end{scriptsize} -\caption{Fetching of the elements values\label{fig:val}} +\end{tiny} +\caption{Récupérer les valeurs des elements\label{fig:val}} \end{minipage}\hfill% \begin{minipage}[h]{.475\linewidth} -\begin{scriptsize} +\begin{tiny} \begin{lstlisting} inline diffuse_values(values){ int countb=0; @@ -391,593 +523,328 @@ inline diffuse_values(values){ od } \end{lstlisting} -\end{scriptsize} -\caption{Diffusion of the elements values}\label{fig:broadcast} +\end{tiny} +\caption{Diffuser les valeurs des elements}\label{fig:broadcast} \end{minipage} \end{figure} -The former potentially updates the array \verb+Xd+ needed by elements that have -to be modified. For each element in \verb+mods+, identified by the variable -$j$, the function retrieves the values of the other elements (labeled by $i$) -whose $j$ depends on. There are two cases: +La première fonction met à jour le tableau \verb+Xd+ requis pour les éléments +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. +Il y a deux cas. \begin{itemize} -\item since $i$ knows its last value (\textit{i.e.}, $D^t_{ii}$ is always $t$) - \verb+Xd[i].v[i]+ is then \verb+Xp[i]+. -\item otherwise, there are two sub-cases which potentially update the value that - $j$ knows about $i$ (that may be chosen in a random way): +\item puisque $i$ connaît sa dernière valeur (\textit{i.e.}, $D^t_{ii}$ est toujours $t$) + \verb+Xd[i].v[i]+ est donc \verb+Xp[i]+; +\item sinon, il y a deux sous cas qui peuvent peuvent potentiellement modifier la valeur + que $j$ a de $i$ (et qui peuvent être choisies de manière aléatoire): \begin{itemize} - \item from the viewpoint of $j$ the value of $i$ may not change (the - \verb+skip+ statement) or is not relevant; this latter case arises when - there is no edge from $i$ to $j$ in the incidence graph, \textit{i.e.}, when - the value of \verb+is_succ+ that is computed by \verb+hasnext(i,j)+ is 0; - then the value of \verb+Xd[j].v[i]+ is not modified; - \item otherwise, \verb+Xd[j].v[i]+ is assigned with the value stored in the - channel \verb+channels[i].sent[j]+ (provided this one is not empty). - Element values are added into this channel during the \verb+diffuse_values+ - function as follows. + \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)+ 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). \end{itemize} \end{itemize} -The \verb+diffuse_values+ function aims at storing the values of $X$ represented by -\verb+Xp+ in the \verb+channels+. It allows the SPIN model-checker to execute -the PROMELA model as if it allowed delays between processes. -% as if computation mode were asynchronous. -%For that reason, when an iteration has to synchronize the elements $i$ and -%$j$ (\textit{i.e.} when \verb+sync[j] == sync[i]+ is true), -% no delay emulation is performed. -%In the asynchronous mode, -There are two cases concerning the value of $X_{j}$: +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 model-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}$: \begin{itemize} -\item either it is left out to allow $i$ not to take into account all the values - of $j$; this case occurs either through the \verb+skip+ statement or when - there is no edge from $j$ to $i$ in the incidence graph; -\item or it is stored in the channel \verb+channels[j].sent[i]+ (provided it is - not full). +\item soit elle est \og perdue\fg{}, \og oubliée\fg{} pour permettre à $i$ de ne pas tenir compte d'une +des valeurs de $j$; ce cas a lieu soit lors de l'instruction \verb+skip+ ou lorsqu'il +n'y a pas d'arc de $j$ à $i$ dans le graphe d'incidence; +\item soit elle est mémorisée dans le canal \verb+channels[j].sent[i]+ (pour peu que celui-ci ne soit pas plein). \end{itemize} -Introducing non-determinism both in \verb+fetch_values+ and -\verb+diffuse_values+ functions is necessary in our context. If the -non-determinism would be used only in \verb+fetch_values+, then it would not be -possible for instance to retrieve the value $X_i^{(t)}$ without taking into -account the value $X_i^{(t-1)}$. On the other hand, if the non-determinism is -only used in \verb+diffuse_values+, then each time a value is pushed into the -channel, this value is immediately consumed, which contradicts the notion of -delays. - -\subsection{Discussion} -A coarse approach could consist in providing one process for each element. -However, the distance with the mathematical model given in \Equ{eq:async} of -such a translation would be larger than the method presented along these lines. -It induces that it would be harder to prove the soundness and completeness of -such a translation. For that reason we have developed a PROMELA model that is -as close as possible to the mathematical one. - -Notice furthermore that PROMELA is an imperative language which -often results in generating intermediate states -(to execute a matrix assignment for -instance). -The use of the \verb+atomic+ keyword allows the grouping of -instructions, making the PROMELA code and the DDN as closed as possible. - -\subsection{Universal Convergence Property} -We are left to show how to formalize into the SPIN model-checker that iterations -of a DDN with $n$ elements are universally convergent. We first recall that the -variables \verb+X+ and \verb+Xp+ respectively contain the value of $X$ before -and after an update. Then, by applying a non-deterministic initialization of -\verb+Xp+ and applying a pseudo-periodic strategy, it is necessary and -sufficient to establish the following Linear Temporal Logic (LTL) formula: +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)}$. +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ée, ce qui est contradictoire avec la notion de +délai. + +% \subsection{Discussion} +% A coarse approach could consist in providing one process for each element. +% However, the distance with the mathematical model given in \Equ{eq:async} of +% such a translation would be larger than the method presented along these lines. +% It induces that it would be harder to prove the soundness and completeness of +% such a translation. For that reason we have developed a PROMELA model that is +% as close as possible to the mathematical one. + +% Notice furthermore that PROMELA is an imperative language which +% often results in generating intermediate states +% (to execute a matrix assignment for +% instance). +% The use of the \verb+atomic+ keyword allows the grouping of +% 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 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. +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 +de prouver la formule temporelle linéaire (LTL) suivante: \begin{equation} \diamond (\Box \verb+Xp+ = \verb+X+) \label{eq:ltl:conv} \end{equation} -where $\diamond$ and $\Box$ have the usual meaning \textit{i.e.}, respectively -{\em eventually} and {\em always} in the subsequent path. It is worth noticing -that this property only ensures the stabilization of the system, but it does not -provide any information over the way the system converges. In particular, some -indeterminism may still be present under the form of multiple fixed points -accessible from some initial states. - - - -\section{Proof of Translation Correctness}\label{sec:spin:proof} -\JFC{Déplacer les preuves en annexes} - -This section establishes the soundness and completeness of the approach -(Theorems~\ref{Theo:sound} and ~\ref{Theo:completeness}). Technical lemmas are -first shown to ease the proof of the two theorems. - - -% \begin{Lemma}[Absence of deadlock]\label{lemma:deadlock} -% Let $\phi$ be a DDN model and $\psi$ be its translation. There is no deadlock -% in any execution of $\psi$. -% \end{Lemma} -% \begin{Proof} -% In current translation, deadlocks of PROMELA may only be introduced through -% sending or receiving messages in channels. Sending (resp. receiving) a -% message in the \verb+diffuse_values+ (resp. \verb+fetch_values+) function is -% executed only if the channel is not full (resp. is not empty). In the -% \verb+update_elems+ and \verb+scheduler+ processes, each time one adds a value -% in any semaphore channel (\verb+unlock_elements_update+ and -% \verb+sync_mutex+), the corresponding value is read; avoiding deadlocks by the -% way. -% \end{Proof} - - -\begin{lemma}[Strategy Equivalence]\label{lemma:strategy} - Let $\phi$ be a DDN with strategy $(S^t)^{t \in \Nats}$ and $\psi$ be its - translation. There exists an execution of $\psi$ with weak fairness s.t. the - scheduler makes \verb+update_elems+ update elements of $S^t$ at iteration $t$. -\end{lemma} -\begin{Proof} - The proof is direct for $t=0$. Let us suppose it is established until $t$ is - some $t_0$. Let us consider pseudo-periodic strategies. Thanks to the weak - fairness equity property, \verb+update_elems+ will modify elements of $S^t$ at - iteration $t$. -\end{Proof} - -In what follows, let $Xd^t_{ji}$ be the value of -\verb+Xd[+$j$\verb+].v[+$i$\verb+]+ after the $t^{\text{th}}$ call to the -function \verb+fetch_values+. Furthermore, let $Y^k_{ij}$ be the element at -index $k$ in the channel \verb+channels[i].sent[j]+ of size $m$, $m \le -\delta_0$; $Y^0_{ij}$ and $Y^{m-1}_{ij}$ are respectively the head and the tail -of the channel. Secondly, let $(M_{ij}^t)^{t \in \{1, 1.5, 2, 2.5,\ldots\}}$ be a -sequence such that $M_{ij}^t$ is the partial function that associates to each -$k$, $0 \le k \le m-1$, the tuple $(Y^k_{ij},a^k_{ij},c^k_{ij})$ while entering -into the \verb+update_elems+ at iteration $t$ where -% \begin{itemize} -% \item - $Y^k_{ij}$ is the value of the channel \verb+channels[i].sent[j]+ - at index $k$, -%\item -$a^k_{ij}$ is the date (previous to $t$) when $Y^k_{ij}$ has been added and -%\item -$c^k_{ij}$ is the first date at which the value is available on $j$. So, - the value is removed from the channel $i\rightarrow j$ at date $c^k_{ij}+1$. -%\end{itemize} -$M_{ij}^t$ has the following signature: -\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*} - -Intuitively, $M_{ij}^t$ is the memory of \verb+channels[i].sent[j]+ while -starting the iteration $t$. Notice that the domain of any $M_{ij}^1$ is $\{0\}$ -and $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$: indeed, the \verb+init+ process -initializes \verb+channels[i].sent[j]+ with \verb+Xp[i]+. - -Let us show how to make the indeterminism inside the two functions\linebreak -\verb+fetch_values+ and \verb+diffuse_values+ compliant with \Equ{eq:async}. -The function $M_{ij}^{t+1}$ is obtained by the successive updates of -$M_{ij}^{t}$ through the two functions\linebreak \verb+fetch_values+ and -\verb+diffuse_values+. Abusively, let $M_{ij}^{t+1/2}$ be the value of -$M_{ij}^{t}$ after the former function during iteration $t$. - -In what follows, we consider elements $i$ and $j$ both in $\llbracket 1, n -\rrbracket$ that are updated. At iteration $t$, $t \geq 1$, let -$(Y^0_{ij},a^0_{ij},c^0_{ij})$ be the value of $M_{ij}^t(0)$ at the beginning of -\verb+fetch_values+. If $t$ is equal to $c^0_{ij}+1$ then we execute the -instruction that assigns $Y^0_{ij}$ (\textit{i.e.}, the head value of -\verb+channels[i].sent[j]+) to $Xd_{ji}^t$. In that case, the function -$M_{ij}^t$ is updated as follows: $M_{ij}^{t+1/2}(k) = M_{ij}^{t}(k+1)$ for each -$k$, $0 \le k \le m-2$ and $m-1$ is removed from the domain of $M_{ij}^{t+1/2}$. -Otherwise (\textit{i.e.}, when $t < c^0_{ij}+1$ or when the domain of $M_{ij}$ -is empty) the \verb+skip+ statement is executed and $M_{ij}^{t+1/2} = -M_{ij}^{t}$. - -In the function \verb+diffuse_values+, if there exists some $\tau$, $\tau\ge t$ -such that \mbox{$D^{\tau}_{ji} = t$}, let $c_{ij}$ be defined by $ \min\{l \mid -D^{l}_{ji} = t \} $. In that case, we execute the instruction that adds the -value \verb+Xp[i]+ to the tail of \verb+channels[i].sent[j]+. Then, -$M_{ij}^{t+1}$ is defined as an extension of $M_{ij}^{t+1/2}$ in $m$ such that -$M_{ij}^{t+1}(m)$ is $(\verb+Xp[i]+,t,c_{ij})$. Otherwise (\textit{i.e.}, when $\forall l -\, . \, l \ge t \Rightarrow D^{l}_{ji} \neq t$ is established) the \verb+skip+ -statement is executed and $M_{ij}^{t+1} = M_{ij}^{t+1/2}$. - - -\begin{lemma}[Existence of SPIN Execution]\label{lemma:execution} - For any sequences $(S^t)^{t \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$, for - any map $F$ there exists a SPIN execution such that for any iteration $t$, $t - \ge 1$, for any $i$ and $j$ in $\llbracket 1, n \rrbracket$ we have the - following properties: - -\noindent If the domain of $M_{ij}^t$ is not empty, then -\begin{equation} - \left\{ - \begin{array}{rcl} - M_{ij}^1(0) & = & \left(X_i^{D_{ji}^{0}}, 0,0 \right) \\ - \textrm{if $t \geq 2$ then }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 Secondly we have: -\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 Thirdly, for any $k\in S^t$. Then, the value of the computed variable -\verb+Xp[k]+ at the end of the \verb+update_elems+ process is equal to -$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)$ at the end of the $t^{\text{th}}$ iteration. -\end{lemma} -\begin{Proof} -The proof is done by induction on the number of iterations. - -\paragraph{Initial case:} - -For the first item, by definition of $M_{ij}^t$, we have $M_{ij}^1(0) = \left( - \verb+Xp[i]+, 0,0 \right)$ that is obviously equal to $\left(X_i^{D_{ji}^{0}}, - 0,0 \right)$. - -Next, the first call to the function \verb+fetch_value+ either assigns the head -of \verb+channels[i].sent[j]+ to \verb+Xd[j].v[i]+ or does not modify -\verb+Xd[j].v[i]+. Thanks to the \verb+init+ process, both cases are equal to -\verb+Xp[i]+, \textit{i.e.}, $X_i^0$. The equation (\ref{eq:correct_retrieve}) is then -established. - - -For the last item, let $k$, $0 \le k \le n-1$. At the end of the first -execution\linebreak of the \verb+update_elems+ process, the value of -\verb+Xp[k]+ is\linebreak $F(\verb+Xd[+k\verb+].v[0]+, \ldots, -\verb+Xd[+k\verb+].v[+n-1\verb+]+)$. Thus, by definition of $Xd$, it is equal -to $F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$. Thanks to \Equ{eq:correct_retrieve}, -we can conclude the proof. - - - -\paragraph{Inductive case:} - -Suppose now that lemma~\ref{lemma:execution} is established until iteration $l$. - -First, if domain of definition of the function $M_{ij}^l$ is not empty, by -induction hypothesis $M_{ij}^{l}(0)$ is $\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c -\right)$ where $c$ is $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$. - -At iteration $l$, if $l < c + 1$ then the \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} +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é, 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. -\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} +\section{Correction et complétude de la démarche}\label{sec:spin:proof} +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}. -\begin{theorem}[Soundness wrt universal convergence property]\label{Theo:sound} - Let $\phi$ be a DDN model and $\psi$ be its translation. If $\psi$ verifies - the LTL property (\ref{eq:ltl:conv}) under weak fairness property, then - iterations of $\phi$ are universally convergent. -\end{theorem} -\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{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound} +\label{Theo:sound} +% + Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA. + Si $\psi$ vérifie + la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible, alors + les itérations de $\phi$ sont universellement convergentes. +\end{restatable} -% \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} +\begin{restatable}[Complétude de la traduction vers Promela]{theorem}{promelacomplete} +\label{Theo:completeness} +% + Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction. Si $\psi$ ne vérifie pas + la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible, + alors les itérations de $\phi$ ne sont pas universellement convergentes. +\end{restatable} -\begin{theorem}[Completeness wrt universal convergence property]\label{Theo:completeness} - Let $\phi$ be a DDN model and $\psi$ be its translation. If $\psi$ does not - verify the LTL property (\ref{eq:ltl:conv}) under weak fairness property then - the iterations of $\phi$ are divergent. -\end{theorem} -\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} -\section{Practical Issues} +\section{Données pratiques} \label{sec:spin:practical} -This section first gives some notes about complexity and later presents -experiments. -%\subsection{Complexity Analysis} -%\label{sub:spin:complexity} -\begin{theorem}[Number of states] - Let $\phi$ be a DDN model with $n$ elements, $m$ edges in the incidence graph - and $\psi$ be its translation into PROMELA. The number of configurations of - the $\psi$ SPIN execution is bounded by $2^{m\times(\delta_0+1)+n(n+2)}$. +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$ + 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(\delta_0+1)+n(n+2)}$. \end{theorem} \begin{Proof} - A configuration is a valuation of global variables. Their number only depends - on those that are not constant. - - The variables \verb+Xp+ \verb+X+ lead to $2^{2n}$ states. The variable - \verb+Xs+ leads to $2^{n^2}$ states. Each channel of \verb+array_of_channels+ - may yield $1+2^1+\ldots+2^{\delta_0}= 2^{\delta_0+1}-1$ states. Since the - number of edges in the incidence graph is $m$, there are $m$ non-constant - channels, leading to approximately $2^{m\times(\delta_0+1)}$ states. The - number of configurations is then bounded by $2^{m\times(\delta_0+1)+n(n+2)}$. - Notice that this bound is tractable by SPIN for small values of $n$, - $m$ and $\delta_0$. + Une configuration est une évaluation des variables globales. + Leur nombre ne dépend que de celles qui ne sont pas constantes. + + Les variables \verb+Xp+ et \verb+X+ engendrent $2^{2n}$ états. + La variable + \verb+Xs+ génère $2^{n^2}$ états. + 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(\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} + \end{Proof} +La méthode détaillée ici a pu être appliquée sur l'exemple +pour prouver formellement sa convergence universelle. - -The method detailed along the line of this article has been applied on the -running example to formally prove its universally convergence. - -First of all, SPIN only considers weak fairness property between processes -whereas above proofs need such a behavior to be established each time a -non-deterministic choice is done. - - -A first attempt has consisted in building the following formula -each time an undeterministic choice between $k$ elements -respectively labeled $l1$, \ldots $lk$ occurs: +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 $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))) $$ -where label $l0$ denotes the line before the choice. -This formula exactly translates the fairness property. -The negation of such a LTL formula may then be efficiently translated -into a Büchi automata with the tool ltl2ba~\cite{GO01}. -However due to an explosion of the size of the product -between this automata and the automata issued from the PROMELA program -SPIN did not success to verify whether the property is established or not. - -This problem has been practically tackled by leaving spin generating all the (not necessarily fair) computations and verifying convergence property on them. -We are then left to interpret its output with two issues. -If property is established for all the computations, -it is particularly established for fair ones and iterations are convergent. -In the opposite case, when facing to a counter example, an analysis of the SPIN -output is achieved. -\begin{xpl} -Experiments have shown that all the iterations of the running example are -convergent for a delay equal to 1 in less than 10 min. -The example presented in~\cite{abcvs05} with five elements taking boolean -values has been verified with method presented in this article. -Immediately, SPIN computes a counter example, that unfortunately does not -fulfill fairness properties. Fair counter example is obtained -after few minutes. -All the experimentation have been realized in a classic desktop computer. -\end{xpl} - +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 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 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. + +% \begin{xpl} +% \JFC{Reprendre ce qui suit} +% Experiments have shown that all the iterations of the running example are +% convergent for a delay equal to 1 in less than 10 min. +% The example presented in~\cite{abcvs05} with five elements taking boolean +% values has been verified with method presented in this article. +% Immediately, SPIN computes a counter example, that unfortunately does not +% fulfill fairness properties. Fair counter example is obtained +% after few minutes. +% All the experimentation have been realized in a classic desktop computer. +% \end{xpl} + + +La méthode détaillée ici a été appliquée sur des exemples pour prouver formellement +leur convergence ou leur divergence (\Fig{fig:exp:promela}) +avec ou sans délais. +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. +\begin{figure}[ht] + \begin{center} + \begin{tiny} + \subfigure[Sans délais]{ + \begin{tabular}{|*{7}{c|}} + \cline{2-7} + \multicolumn{1}{c|}{ } + &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Généralisées} \\ + \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} + \label{fig:sync:exp} + } + + \subfigure[Avec délais]{ + \begin{tabular}{|*{13}{c|}} + \cline{2-13} + \multicolumn{1}{c|}{ } + &\multicolumn{6}{|c|}{Mode Mixe} & \multicolumn{6}{|c|}{Seulement borné} \\ + \cline{2-13} + \multicolumn{1}{c|}{ } + &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Pseudo-Périodique} & + \multicolumn{3}{|c|} {Synchrones} & \multicolumn{3}{|c|}{Pseudo-Périodique} \\ + \cline{2-13} + \multicolumn{1}{c|}{ } + &P & M & T & + P & M & T & + P & M & T& + P & M & T \\ + \hline %cline{2-13} + \textit{RE} & + $\top$ & 409 & 1m11s& + $\bot$ & 370 & 0.54 & + $\bot$ & 374 & 7.7s& + $\bot$ & 370 & 0.51s \\ + \hline %\cline{2-13} + AC2D + &$\bot$ & 2.5 & 0.001s % RC07_async_mixed.spin + &$\bot$ & 2.5 & 0.01s % RC07_async_mixed_all.spin + &$\bot$ & 2.5 & 0.01s % RC07_async.spin + &$\bot$ & 2.5 & 0.01s \\ % RC07_async_all.spin + \hline %\cline{2-13} + \cite{BM99} + &$\top$ & & %BM99_mixed_para.spin + &$\top$ & & % RC07_async_mixed_all.spin + &$\bot$ & & % RC07_async.spin + &$\bot$ & & \\ % RC07_async_all.spin + \hline %\cline{2-13} + \end{tabular} + \label{fig:async:exp} + } + \end{tiny} + \end{center} + \caption{Résultats des simulations Promela des SDDs}\label{fig:exp:promela} +\end{figure} + + + +L'exemple \textit{RE} est l'exemple 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 leurs valeurs booléennes dans un graphe d'adjacence proche +du graphe complet. + + +L'exemple \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 synchrones +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 +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)$. +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 universelle. + +\begin{figure} +\centering +\includegraphics[scale=0.6]{images/RC07ce.eps} +\caption{Contre exemple de convergence pour~\ref{fig:RC07CE}} \label{fig:RC07CE} +\end{figure} -%However preliminary experiments have shown the interest of the approach. - - - -% The method detailed along the line of this article has been -% applied on some examples to formally prove their convergence -% (Fig.~\ref{fig:async:exp}). -% In these experiments, Delays are supposed to be bounded by $\delta_0$ set to 10. -% In these arrays, -% $P$ is true ($\top$) provided the uniform convergence property is established, false ($\bot$) otherwise, -% $M$ is the amount of memory usage (in MB) and -% $T$ is the time needed on a Intel Centrino Dual Core 2 Duo @1.8GHz with 2GB of memory, both -% to establish or refute the property. - -% RE is the running example of this article, -% AC2D is a cellular automata with 9 elements taking boolean values -% according their four neighbors -% and BM99 is has been proposed in~\cite{BM99} and consists of 10 process -% modifying their boolean values, but with many connected connection graph. - - - - - -% \begin{figure} -% \begin{center} -% \scriptsize -% \begin{tabular}{|*{13}{c|}} -% \cline{2-13} -% \multicolumn{1}{c|}{ } -% &\multicolumn{6}{|c|}{Mixed Mode} & \multicolumn{6}{|c|}{Only Bounded} \\ -% \cline{2-13} -% \multicolumn{1}{c|}{ } -% &\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} & -% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\ -% \cline{2-13} -% \multicolumn{1}{c|}{ } -% &P & M & T & -% P & M & T & -% P & M & T& -% P & M & T \\ -% \hline %cline{2-13} -% Running Example & -% $\top$ & 409 & 1m11s& -% $\bot$ & 370 & 0.54 & -% $\bot$ & 374 & 7.7s& -% $\bot$ & 370 & 0.51s \\ -% \hline %\cline{2-13} -% AC2D -% &$\bot$ & 2.5 & 0.001s % RC07_async_mixed.spin -% &$\bot$ & 2.5 & 0.01s % RC07_async_mixed_all.spin -% &$\bot$ & 2.5 & 0.01s % RC07_async.spin -% &$\bot$ & 2.5 & 0.01s \\ % RC07_async_all.spin -% \hline %\cline{2-13} -% BM99 -% &$\top$ & & %BM99_mixed_para.spin -% &$\top$ & & % RC07_async_mixed_all.spin -% &$\bot$ & & % RC07_async.spin -% &$\bot$ & & \\ % RC07_async_all.spin -% \hline %\cline{2-13} -% \end{tabular} -% \end{center} -% \caption{Experimentations with Asynchronous Iterations}\label{fig:async:exp} -% \end{figure} - - - -% The example~\cite{RC07} deals with a network composed of two genes taking their -% values into $\{0,1,2\}$. Since parallel iterations is already diverging, -% the same behavior is observed for all other modes. -% The Figure~\ref{fig:RC07CE} gives the trace leading to convergence property -% violation output by SPIN. -% It corresponds to peridic strategy that repeats $\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ and starts with $X=(0,0)$. - - -% In the example extracted from~\cite{BM99}, -% we have 10 processors computing a binary value. -% Due to the huge number of dependencies between these calculus, -% $\delta_0$ is reduced to 1. It nevertheless leads to about $2^{100}$ -% configurations in asynchronous iterations. - -% Let us focus on checking universal convergence of asynchronous iterations -% of example~\cite{BCVC10:ir}. -% With a $\delta_0$ set to 5, SPIN generates an out of memory error. -% However, it succeed to prove that the property is not established even -% with $\delta_0$ set to 1 which is then sufficient. - - -% \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} example & -% $\bot$ & 2.5 & 0.001s & % RC07_sync.spin -% $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin -% \hline -% \cite{BM99} example & -% $\top$ & 36.7 & 12s & % BM99_sync_para.spin -% $\top$ & & \\ % BM99_sync_chao.spin -% \hline -% \end{tabular} -% \end{tiny} -% \end{center} -% \caption{Experimentations with Synchronous Iterations}\label{fig:sync:exp} -% \end{figure} -% \begin{tabular}{|*{}{c|}} +% \begin{tabular}{|*{19}{c|}} % % \hline % % e \\ % % @@ -995,45 +862,12 @@ All the experimentation have been realized in a classic desktop computer. % \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} \\ -% \end{tabular} +% \end{tabular} -\section{Conclusion and Future Work} +\section{Conclusion} \label{sec:spin:concl} -Stochastic based prototypes have been implemented to generate both -strategies and delays for asynchronous iterations in first in~\cite{BM99,BCV02}. -However, since these research softwares are not exhaustive, they really give an -formal answer when they found a counterexample. When facing convergence, they only convince -the user about this behavior without exhibiting a proof. - -As far as we know, no implemented formal method tackles the problem of -proving asynchronous iterations convergence. -In the theoretical work~\cite{Cha06} Chandrasekaran shows that asynchronous iterations -are convergent iff we can build a decreasing Lyaponov function, -but does not gives any automated method to compute it. - -In this work, we have shown how convergence proof for any asynchronous -iterations of discrete dynamical networks with bounded delays -can be automatically achieved. -The key idea is to translate the network (map, strategy) into PROMELA and -to leave the SPIN model checker establishing the validity -of the temporal property corresponding to the convergence. -The correctness and completeness of the approach have been proved, notably -by computing a SPIN execution of the PROMELA model that have the same -behaviors than initial network. -The complexity of the problem is addressed. It shows that non trivial example -may be addressed by this technique. - -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.}, -for all $i$, $j$, $1 \le i \le j \le n$, we have$ -\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}. +