annexePreuveMixage.tex

   1
   2 Let  us introduce an  ordering $\preceq$  between classes.   Formally, \class{p}
   3 $\preceq$   \class{q}   if   there    exists   a   path   of   length   $\alpha$
   4 ($0<\alpha<|\mathcal{K}|$)  from  an  element  of  \class{p} to  an  element  of
   5 \class{q}.  One can  remark that if \class{p}$\preceq$\class{q}, then  it is not
   6 possible to also have \class{q}$\preceq$\class{p}.
   7
   8 % \begin{lemma}
   9 %   The relation $ \preceq$ is a partial order
  10 %   \begin{Proof}
  11 %     Reflexivity is established  since for any $p_0 \in [p]$  there exists a path
  12 %     of length  0 from  $p_0$ to $p_0$.
  13 %     For antisymmetry, suppose  there exists two classes $[p]$ and
  14 %     $[q]$ such that $[p] \preceq [q]$ and $[q] \preceq [p]$.
  15 %     There exists then $p_0,p'_0 \in [p]$, $q_0, q'_0 \in [q]$ with paths
  16 %     from $p_0$ to $q_0$ and from $q'_0$  to $p_0$.
  17 %     Thus, elements $p_0$, $p'_0$, $q_0$ and $q'_0$ belong to the same
  18 %     strongly connected component and then
  19 %     $[p]$ = $[q]$.  Transitivity is obviously established.
  20 %   \end{Proof}
  21 % \end{lemma}
  22
  23 \begin{lemma}
  24   There exists a renaming process  method that assigns new identifier numbers to
  25   processes  $i\in$ \class{p}  and $j  \in$ \class{q}  s.t. $i  \le  j$ provided
  26   \class{p} $\preceq$ \class{q}.
  27   \begin{Proof}
  28     % We first  define a renaming process  method and later show  that it fulfills
  29     % the requirements.
  30
  31     First  of   all,  let  \class{p_1},   \ldots,  \class{p_l}  be   classes  of
  32     $n_1$,\ldots,  $n_l$  elements respectively  that  do  not  depend on  other
  33     classes.   Elements of  \class{p_1} are  renamed by  $1$, \ldots,  $n_1$ and
  34     elements   of  \class{p_i},   $2  \le   i  \le   l$  are   renamed   by  $1+
  35     \Sigma_{k=1}^{i-1}  n_k$, \ldots, $\Sigma_{k=1}^{i}  n_k$.  We  now consider
  36     the  classes \class{p_1},  \ldots, \class{p_{l'}}  whose elements  have been
  37     renamed and let $m$ be the maximum index of elements of \class{p_1}, \ldots,
  38     \class{p_{l'}}.  Given  another class \class{p} that  exclusively depends on
  39     some \class{p_i}, $1 \le i \le l'$ and that contains $k$ elements.  Elements
  40     of \class{p} are then renamed by $m+1$, \ldots, $m+k$.
  41 % In the end for remaining classes, i.e. those which do not depend on anything,
  42 % elements are arbitrarily numbered.
  43     This renaming  process method has then  been applied on  $l'+1$ classes.  It
  44     ends since it  decreases the number of elements to  assign a number.  Notice
  45     that this process is not determinist.
  46
  47     We  are then  ready to  prove that  this renaming  method  verifies property
  48     expressed in the lemma.  The proof is done by induction on the length $l$ of
  49     the longest dependency path between classes.
  50
  51     First, if \class{p} $\preceq$ \class{q} and \class{q} immediately depends on
  52     \class{p},  \textit{i.e.} the  longest path  from elements  of  \class{p} to
  53     elements of \class{q} has length 1.  Due to the renaming method, all element
  54     numbers of \class{q}  are greater than the ones of  \class{p} and the result
  55     is established.   Let \class{p} and  \class{q} s.t.  the  longest dependency
  56     path from \class{p}  to \class{q} has length $l+1$.   Then there exists some
  57     \class{q'} s.t.  \class{q} immediately depends on \class{q'} and the longest
  58     dependency path from \class{p} and  \class{q'} has length $l$.  We have then
  59     \class{q'}  $\preceq$ \class{q}  and  then for  all  $k$, $j$  s.t. $k  \in$
  60     \class{q'}  and $j  \in$  \class{q},  $k \le  j$.   By induction  hypothesis
  61     \class{p}  $\preceq$ \class{q'}  and  then for  all  $i$, $k$  s.t. $i  \in$
  62     \class{p} and $k \in$ \class{q'}, $i \le k$ and the result is established.
  63   \end{Proof}
  64 \end{lemma}
  65
  66 It can  be noticed that  the renaming process  is inspired from  \emph{graphs by
  67   layer} of Golès and Salinas~\cite{GS08}. It ensures that identifier numbers of
  68 a layer are greater than all the identifier numbers of any lower layers.
  69
  70 \begin{xpl}
  71   We  have \class{1}  $=\{1,2\}$, \class{3}  $=\{3\}$ and  \class{4} $=\{4,5\}$.
  72   Processes numbers are already compliant with the order $\preceq$.
  73 \end{xpl}
  74
  75 \begin{Proof}[of Theorem~\ref{th:cvg}]
  76
  77   % Since $\preceq$ is a partial order,  [[JFC citer un theoreme qui dit cela ou
  78   % le prouver]]  there exists  a renaming process  that assigns  new identifier
  79   % number to processes $i\in [p]$ and $j  \in [q]$ s.t. $i \le j$ provided $[p]
  80   % \preceq [q]$.
  81   % % $i \in [p]$ and $j \in [q]$.
  82
  83   The  rest of  the proof  is done  by  induction on  the class  index.  Let  us
  84   consider  the first class  \class{b_1} with  $n_1$ elements  \textit{i.e.} the
  85   class with the smallest identifiers.
  86
  87   By theorem hypotheses, %following the strategy $(S^t)$,
  88   synchronous  iterations converge  to the  fixed point  in a  finite  number of
  89   iterations. %pseudo periods. % [[JFC : borner m1/n1]].
  90   So, all  \emph{source classes}  (independant from any  other class)  will also
  91   converge in mixed mode.  Let us suppose now that mixed iterations with uniform
  92   delays converge for classes \class{b_1},  \ldots, \class{b_k} in a time $t_k$.
  93   By  construction, \class{b_{k+1}}  only depends  on some  \class{b_1}, \ldots,
  94   \class{b_k} and \class{b_{k+1}}.  There  exists then a sufficiently large time
  95   $t_0$  s.t.  $D^{t_0}_{p_{k+1}p_j}$  is  greater  or equal  to  $t_k$ for  any
  96   $p_{k+1} \in$ \class{b_{k+1}} and $p_j \in$ \class{b_j}, $1 \le j \le k$.
  97
  98   We are  then left with  synchronous iterations of elements  of \class{b_{k+1}}
  99   starting with configurations  where all the elements of  \class{b_j}, $1 \le j
 100   \le k$, have constant values.  By theorem hypotheses, it converges.
 101 \end{Proof}
 102
 103
 104