[hdrcouchot.git] / annexePromelaProof.tex

\JFC{Voir section~\ref{sec:spin:proof}}

Cette section donne les preuves des deux théorèmes de correction et complétude 
du chapitre~\ref{chap:promela}.


\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}


\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}


\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{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{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}