From 23e4a7ff8d7172f48622f31a6c71bfc3699227da Mon Sep 17 00:00:00 2001 From: couchot Date: Mon, 13 Apr 2015 10:25:40 +0200 Subject: [PATCH] dfqsfsfese --- annexePreuveMixage.tex | 104 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 104 insertions(+) create mode 100644 annexePreuveMixage.tex diff --git a/annexePreuveMixage.tex b/annexePreuveMixage.tex new file mode 100644 index 0000000..4757b0b --- /dev/null +++ b/annexePreuveMixage.tex @@ -0,0 +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} + +\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 + \class{p} $\preceq$ \class{q}. + \begin{Proof} + % We first define a renaming process method and later show that it fulfills + % the requirements. + + 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. + + 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. + + 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} +\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} + +\begin{Proof}[of Theorem~\ref{th:cvg}] + + % 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]$. + + 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. + + 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$. + + 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} + + + -- 2.39.5