X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/23e4a7ff8d7172f48622f31a6c71bfc3699227da..44a56c5eb4a1dfdf7dc67735c5c00f478cef2ede:/annexePreuveMixage.tex diff --git a/annexePreuveMixage.tex b/annexePreuveMixage.tex index 4757b0b..71c1c8e 100644 --- a/annexePreuveMixage.tex +++ b/annexePreuveMixage.tex @@ -1,104 +1,104 @@ - -Let us introduce an ordering $\preceq$ between classes. Formally, \class{p} -$\preceq$ \class{q} if there exists a path of length $\alpha$ -($0<\alpha<|\mathcal{K}|$) from an element of \class{p} to an element of -\class{q}. One can remark that if \class{p}$\preceq$\class{q}, then it is not -possible to also have \class{q}$\preceq$\class{p}. - -% \begin{lemma} -% The relation $ \preceq$ is a partial order -% \begin{Proof} -% Reflexivity is established since for any $p_0 \in [p]$ there exists a path -% of length 0 from $p_0$ to $p_0$. -% For antisymmetry, suppose there exists two classes $[p]$ and -% $[q]$ such that $[p] \preceq [q]$ and $[q] \preceq [p]$. -% There exists then $p_0,p'_0 \in [p]$, $q_0, q'_0 \in [q]$ with paths -% from $p_0$ to $q_0$ and from $q'_0$ to $p_0$. -% Thus, elements $p_0$, $p'_0$, $q_0$ and $q'_0$ belong to the same -% strongly connected component and then -% $[p]$ = $[q]$. Transitivity is obviously established. -% \end{Proof} -% \end{lemma} +Introduisons tout d'abord une relation d'ordre +$\preceq$ entre les classes d'équivalences. +Formellement, \class{p} +$\preceq$ \class{q} +s'il existe un chemin de longueur $\alpha$ +($0\le\alpha<|\mathcal{K}|$) entre un élément le la classe +\class{p} vers un élément de +\class{q}. \begin{lemma} - There exists a renaming process method that assigns new identifier numbers to - processes $i\in$ \class{p} and $j \in$ \class{q} s.t. $i \le j$ provided + Il existe un processus de renommage qui affecte un nouvel identifiant aux + éléments $i\in$ \class{p} et $j \in$ \class{q} tel que + $i \le j$ si et seulement si \class{p} $\preceq$ \class{q}. - \begin{Proof} - % We first define a renaming process method and later show that it fulfills - % the requirements. + \begin{proof} - First of all, let \class{p_1}, \ldots, \class{p_l} be classes of - $n_1$,\ldots, $n_l$ elements respectively that do not depend on other - classes. Elements of \class{p_1} are renamed by $1$, \ldots, $n_1$ and - elements of \class{p_i}, $2 \le i \le l$ are renamed by $1+ - \Sigma_{k=1}^{i-1} n_k$, \ldots, $\Sigma_{k=1}^{i} n_k$. We now consider - the classes \class{p_1}, \ldots, \class{p_{l'}} whose elements have been - renamed and let $m$ be the maximum index of elements of \class{p_1}, \ldots, - \class{p_{l'}}. Given another class \class{p} that exclusively depends on - some \class{p_i}, $1 \le i \le l'$ and that contains $k$ elements. Elements - of \class{p} are then renamed by $m+1$, \ldots, $m+k$. -% In the end for remaining classes, i.e. those which do not depend on anything, -% elements are arbitrarily numbered. - This renaming process method has then been applied on $l'+1$ classes. It - ends since it decreases the number of elements to assign a number. Notice - that this process is not determinist. + Tout d'abord, soient \class{p_1}, \ldots, \class{p_l} des classes + contenant respectivement les éléments $n_1$,\ldots, $n_l$ + qui ne dépendent d'aucune autre classe. + Les éléments de \class{p_1} sont renommés par $1$, \ldots, $n_1$, + les éléments de \class{p_i}, $2 \le i \le l$ sont renommés par + $1+ + \Sigma_{k=1}^{i-1} n_k$, \ldots, $\Sigma_{k=1}^{i} n_k$. + On considère maintenant les classes \class{p_1}, \ldots, \class{p_{l'}} + dont les éléments ont été renommés et soit + $m$ le plus grand indice des éléments de \class{p_1}, \ldots, + \class{p_{l'}}. + Soit une autre classe \class{p} qui dépend exclusivement d'une classe + \class{p_i}, $1 \le i \le l'$ et qui contient $k$ éléments. + Les éléments de \class{p} sont renommés par $m+1$, \ldots, $m+k$. + Ce processus a été appliqué sur $l'+1$ classes. Il se termine + puisqu'il diminue le nombre d'éléments auquel il reste + à affecter un numéro. - We are then ready to prove that this renaming method verifies property - expressed in the lemma. The proof is done by induction on the length $l$ of - the longest dependency path between classes. + Il reste à montrer que cette méthode de renommage vérifie la propriété + énoncée dans le lemme. + Cette preuve se fait par induction sur la taille $l$ + du plus grand chemin de dépendance entre les classes. - First, if \class{p} $\preceq$ \class{q} and \class{q} immediately depends on - \class{p}, \textit{i.e.} the longest path from elements of \class{p} to - elements of \class{q} has length 1. Due to the renaming method, all element - numbers of \class{q} are greater than the ones of \class{p} and the result - is established. Let \class{p} and \class{q} s.t. the longest dependency - path from \class{p} to \class{q} has length $l+1$. Then there exists some - \class{q'} s.t. \class{q} immediately depends on \class{q'} and the longest - dependency path from \class{p} and \class{q'} has length $l$. We have then - \class{q'} $\preceq$ \class{q} and then for all $k$, $j$ s.t. $k \in$ - \class{q'} and $j \in$ \class{q}, $k \le j$. By induction hypothesis - \class{p} $\preceq$ \class{q'} and then for all $i$, $k$ s.t. $i \in$ - \class{p} and $k \in$ \class{q'}, $i \le k$ and the result is established. - \end{Proof} + Tout d'abord, si \class{p} $\preceq$ \class{q} et \class{q} + dépend immédiatement de + \class{p}, \textit{i.e.} + le chemin le plus long entre les éléments de \class{p} et les + éléments de \class{q} est de longueur 1. + En raison de la méthode renommage, chaque numéro d'élément + \class{q} est plus grand que tous ceux de \class{p} et la preuve est + établie. + Soit \class{p} et \class{q} tels que le plus long chemin de dépendance + entre \class{p} et \class{q} a une longueur de $l+1$. + Il existe alors une classe + \class{q'} telle que \class{q} + dépend immédiatement de \class{q'} et le chemin de dépendance le + plus long entre \class{p} et \class{q'} a pour longueur $l$. + On a ainsi + \class{q'} $\preceq$ \class{q} + et pour tout $k$, $j$ tels que $k \in$ + \class{q'} et $j \in$ \class{q}, $k \le j$. + Par hypothèse d'induction, + \class{p} $\preceq$ \class{q'} et pour chaque $i$, $k$ tels que $i \in$ + \class{p} et $k \in$ \class{q'}, $i \le k$ + et le résultat est établi. + \end{proof} \end{lemma} -It can be noticed that the renaming process is inspired from \emph{graphs by - layer} of Golès and Salinas~\cite{GS08}. It ensures that identifier numbers of -a layer are greater than all the identifier numbers of any lower layers. - -\begin{xpl} - We have \class{1} $=\{1,2\}$, \class{3} $=\{3\}$ and \class{4} $=\{4,5\}$. - Processes numbers are already compliant with the order $\preceq$. -\end{xpl} +On peut remarquer que ce processus de renommage est inspiré des \emph{graphes + par couches } de Golès et Salinas~\cite{GS08}. -\begin{Proof}[of Theorem~\ref{th:cvg}] +% \begin{xpl} +% We have \class{1} $=\{1,2\}$, \class{3} $=\{3\}$ and \class{4} $=\{4,5\}$. +% Processes numbers are already compliant with the order $\preceq$. +% \end{xpl} - % Since $\preceq$ is a partial order, [[JFC citer un theoreme qui dit cela ou - % le prouver]] there exists a renaming process that assigns new identifier - % number to processes $i\in [p]$ and $j \in [q]$ s.t. $i \le j$ provided $[p] - % \preceq [q]$. - % % $i \in [p]$ and $j \in [q]$. +\begin{proof}[du théorème~\ref{th:cvg}] - The rest of the proof is done by induction on the class index. Let us - consider the first class \class{b_1} with $n_1$ elements \textit{i.e.} the - class with the smallest identifiers. + Le reste de la preuve est fait par induction sur le numéro de classe. + Considérons la première classe \class{b_1} de $n_1$ éléments + \textit{i.e.} la classe avec le plus petit identifiant. - By theorem hypotheses, %following the strategy $(S^t)$, - synchronous iterations converge to the fixed point in a finite number of - iterations. %pseudo periods. % [[JFC : borner m1/n1]]. - So, all \emph{source classes} (independant from any other class) will also - converge in mixed mode. Let us suppose now that mixed iterations with uniform - delays converge for classes \class{b_1}, \ldots, \class{b_k} in a time $t_k$. - By construction, \class{b_{k+1}} only depends on some \class{b_1}, \ldots, - \class{b_k} and \class{b_{k+1}}. There exists then a sufficiently large time - $t_0$ s.t. $D^{t_0}_{p_{k+1}p_j}$ is greater or equal to $t_k$ for any - $p_{k+1} \in$ \class{b_{k+1}} and $p_j \in$ \class{b_j}, $1 \le j \le k$. + D'après les hypothèses du théorème, %following the strategy $(S^t)$, + les itérations synchrones convergent vers un point fixe en un nombre + fini d'itérations. %pseudo periods. % [[JFC : borner m1/n1]]. + Ainsi toutes les \emph{classes sources} + (indépendantes de toutes les autres classes) vont aussi converger + dans le mode mixte. + On peut ainsi supposer que le mode d'itération mixte avec délais + uniformes fait converger les classes \class{b_1}, \ldots, \class{b_k} + en un temps $t_k$. + Par construction, la classe \class{b_{k+1}} dépend uniquement + de certaines classes de \class{b_1}, \ldots, + \class{b_k} et éventuellement d'elle-même. + Il existe un nombre d'itérations suffisamment grand + $t_0$ tel que $D^{t_0}_{p_{k+1}p_j}$ est supérieur ou égal à $t_k$ + pour chaque + $p_{k+1} \in$ \class{b_{k+1}} et $p_j \in$ \class{b_j}, $1 \le j \le k$. - We are then left with synchronous iterations of elements of \class{b_{k+1}} - starting with configurations where all the elements of \class{b_j}, $1 \le j - \le k$, have constant values. By theorem hypotheses, it converges. -\end{Proof} + Il ne reste donc que des itérations synchrones entre les + éléments de \class{b_{k+1}} en démarrant dans des configurations + où tous les éléments de \class{b_j}, $1 \le j + \le k$, ont des valeurs constantes. + D'après les hypothèses du théorème, cela converge. +\end{proof}