-
+\JFC{donner dans les rappels les délais et les propriétés de convergence uniforme}
\section{Rappels sur le langage PROMELA}
chan sync_mutex=[1] of {bool};
\end{lstlisting}
\end{scriptsize}
-\caption{Type declaration of the DDNs translation.}
+\caption{Declaration des types de la traduction.}
\label{fig:arrayofchannels}
\end{figure}
}
\end{lstlisting}
\end{scriptsize}
-\caption{PROMELA init process.}\label{fig:spin:init}
+\caption{Process init.}\label{fig:spin:init}
\end{minipage}\hfill
\begin{minipage}[h]{.42\linewidth}
\begin{scriptsize}
}
\end{lstlisting}
\end{scriptsize}
-\caption{Scheduler process for common pseudo-periodic strategy.
+\caption{Process scheduler pour la stratégie pseudo-periodique.
\label{fig:scheduler}}
\end{minipage}
\end{figure}
suivi par des mis àjour: ceci est réalisé grace à 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:
+\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
+{\sc Figure}~\ref{fig:proc}.
+Ce process actif attend jusqu'à ce qu'il soit déblocqué par le process
+\verb+scheduler+ à l'aide du sémaphore \verb+unlock_elements_update+.
+L'implantation contient donc cinq étapes:
\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}).
+\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 function \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 itérativement la valeur de $j$ (grace à 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 symbolicallement envoyés aux
+ autres éléments qui en dépendent grâce à la fonction
+ \texttt{diffuse\_values(Xp)} (cf. \Sec{sub:spin:vt});
+\item finallement, le process informe le scheduler de la fin de la tâche
+ (au travers du semaphore \texttt{sync\_mutex}).
\end{enumerate}
}
\end{lstlisting}
\end{scriptsize}
-\caption{Updatings of the elements.}\label{fig:proc}
+\caption{Mise à jour des éléments.}\label{fig:proc}
\end{minipage}\hfill%
%\end{figure}
%\begin{figure}
}
\end{lstlisting}
\end{scriptsize}
-\caption{Application of function $F$.}\label{fig:p}
+\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{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 iné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}
}
\end{lstlisting}
\end{scriptsize}
-\caption{Fetching of the elements values\label{fig:val}}
+\caption{Récupérer les valeurs des elements\label{fig:val}}
\end{minipage}\hfill%
\begin{minipage}[h]{.475\linewidth}
\begin{scriptsize}
}
\end{lstlisting}
\end{scriptsize}
-\caption{Diffusion of the elements values}\label{fig:broadcast}
+\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 array \verb+Xd+ recquis 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 libélé est $i$)
+dont $j$ dépend. \JFC{vérifier si c'est ce sens ici}
+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 allé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'arce 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;
+ 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
+ dansle cannal \verb+channels[i].sent[j]+ (pour peu que celui-ci ne soit pas vide).
+ Les valeurs des éléments sont ajoutées dans ce cannal au travers de la fonction \verb+diffuse_values+
+ donnée juste après.
\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}$:
+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 cannal \verb+channels+.
+Il permet au modèle-checker SPIN d'exécuter
+le modèle PROMELA model 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 cannal \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
+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-determinism était uniquement
+utilisé dans la fonction \verb+diffuse_values+, alors chaque fois qu'une valeur serait
+mise dans le cannal, elle serait immédiatement consommé, 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éte de convergence universelle}
+Il reste à formaliser dans le model checker SPIN que les itérations d'un système
+dynamique à $n$ éléments est universellement 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
