In this chapter, we describe a contract based \minimp{} verification
system.  It verifies an \minimp{} program against a specification in a
composite and modular way.

We first introduce the basic model checking and symbolic execution
algorithm for monolithic verification in
\S\ref{sec:minimp:system:symExe}.  In
\S\ref{sec:minimp:system:symExeModular}, we improve the basic
algorithm with respect to $\corule$ for composite and modular
verification.  Around the improved the algorithm, we discuss about a
procedure contract based verification system in
\S\ref{sec:minimp:modular:system}.  Finally, we give proofs for the
soundness of the algorithms in \S\ref{sec:minimp:system:proof}.

We fix the context of our discussion in this chapter with a vocabulary
$\vocab{} = (\myprocedure, \var, \globvar, \locvar)$, a domain $\dom$
and a \minimp{} model $\model$.


\section{Symbolic Execution and Model Checking for
  \minimp{}} \label{sec:minimp:system:symExe}

In this section, we introduce a basic algorithm for monolithic
verification of functional correctness of a \minimp{} program segment
against its contract.  This algorithm uses model checking and symbolic
execution techniques.

In order to do symbolic execution, we must allow variables in
\minimp{} to hold \emph{symbolic expressions}.  In addition, states of
\minimp{} programs must be associated with \emph{path conditions}
(PCs).

\begin{defn}
  Let $\sym$ be a set of symbols.  Let $\symexpr$ be the set of
  expressions over $\dom$ and $\sym$.  An expression in $\symexpr$ is
  said a \emph{symbolic expression}.  An element in $\sym$ is also
  said a \emph{symbolic constant}.  An element in $\dom$ is also said
  a \emph{concrete value}.  $\qed$
\end{defn}


\begin{defn}
  Let $\symexpr$ be the set of symbolic expressions.  A \emph{state
    for symbolic execution} is a pair: \[ (s, \pathcond), \] where
    $s\colon{}\mystates$ is a state and $\pathcond{}\colon{}\symexpr$
    is the boolean path condition.  Let $\mystates^{\sym}$ be the set
    of states for symbolic execution.  $\qed$
\end{defn}
Given a state $\omega \in \mystates^{\sym}$, by
$\mypathcond{}(\omega)$, we denote the path condition of $\omega$.

From now on, for the rest of this chapter, we call elements in
$\mystates^{\sym}$ \emph{states}.  Given a state
$\omega = (s, \pathcond{})$, we refer any component $c$ of $s$ as
``$c$ of $\omega$'', and we refer $\pathcond{}$ as ``the PC of
$\omega$'', which may also be said ``the path condition of $\omega$''.

The shortcut notations introduced in \S\ref{sec:minimp:semantics}
involving elements in $\mystates$ will be naturally extended with
respect to elements in $\mystates^{\sym}$.  For example, the call
stack of a process $p$ in a state $\omega \in \mystates^{\sym}$ can be
denoted $\mystack(\omega, p)$.  Correspondingly, the evaluation
functions with $n$ processes: $\myeval{~}_n$, $\myseval{~}_n$, and
$\myaeval{~}_n$, are also extended in a natural way for symbolic
expressions and $\mystates^{\sym}$.

\begin{defn}
Let $\symexpr$ be the symbolic expression set, $n$ be a positive
integer, and $\myeval{~}_n$ be an evaluation function.  Let $T$ be the
set of local transitions.  A $n$-processes \emph{interpretation for
symbolic execution}
$I_n^{\sym}\colon{} \mystates^{\sym} \times \nprocs{n} \times
T \rightarrow{} \powerset(\mystates^{\sym})$ is a function describes
the states, each of which is a possible result of executing a local
transition $(l, g, a, l') \in T$ from a state
$\omega \in \mystates^{\sym}$ by a process $p \in \nprocs{n}$.  We
define $I^{\sym}$ in
Fig.\ \ref{fig:minimp:system:interpretation}. $\qed$
\end{defn}

\begin{figure}
  \begin{center}
  \fbox{
  \parbox{.9\textwidth}{
    \begin{align}
      & I_n^{\sym}((s, \pathcond), p, (l, g, a, l')) =  \nonumber \\
      & \text{let } \pathcond{'} = \pathcond{} \wedge{}
        \myeval{g}_n(s, p)\text{ in} \nonumber \\
      & \{\omega'[\pathcond' / \pathcond] \in
        \mystates^{\sym} \mid{} \omega' \in I(s, p, (l, \texttt{true}, a, l'))\} \nonumber
  \end{align}
}}
\end{center}
%\textcolor{red}{Note to myself: for a wildcard receive, transitions
%  with recv actions over all channels will be enabled.  Pruning
% happens at the destination state of the enabled transitions}
\caption{The definition of the interpretation for symbolic execution
  with $n$ processes.}
\label{fig:minimp:system:interpretation}
\end{figure}
When the number of processes $n$ is clear in the context, we may
simplify $I^{\sym}_n$ to $I^{\sym}$.

Given a boolean symbolic expression $e$, $e$ is said
\emph{satisfiable} iff there is at least an assignment from symbols in
$e$ to concrete values that makes $e$ true.  If $e$ is true for any
assignment, $e$ is said valid.  If $e$ is false for any assignment,
$e$ is said invalid, or \emph{unsatisfiable}.  The intuition in
$I^{\sym}$ is that, given a source state, a process and a local
transition, $I^{\sym}$ always compute the target states regardless of
whether the guard is valid or not.  Besides, it adds the guard to the
path conditions of the target states.  If the path condition of a
state is unsatisfiable, paths containing the state are
\emph{infeasible}.

\begin{defn}
Let $\mcalgo$ be the monolithic algorithm that verifies the validity
of a collective triple for a fixed number processes.  $\mcalgo$ is a
function that consumes a model, a collective triple $\cotriplenoloc$, and a
positive integer $n$, and returns \textbf{T} iff
$\model \vdash \cotriplenoloc{}$ for $n$ processes. Formally,
\[
  \mcalgo(\model, \cotriplenoloc, n) = \textbf{T} \text{ iff
  } \model \vdash \cotriplenoloc{} \qed
\]      
\end{defn}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
$\mcalgo(\model, \cotriplenoloc{}, n)$ verifies the validity of the
triple through searching states and paths that violate the
specification in a \emph{state space graph for symbolic execution} of
$C$.

\begin{defn}
  Let $\cotriple{}$ be a collective triple and $T$ be the set of local
  transitions translated from $\progseg{l}{C}{l'}$.  The \emph{state
  space graph for symbolic execution} $G$ of $C$ with $n$ processes is
  a tuple: \[ G = (\omega_0, \Omega, \leadsto^{\sym}_{C}), \]
  where 

  \begin{itemize}       
        
 \item $\omega_0$ is an initial state that satisfies the following
   conditions
   
   \begin{enumerate}
   \item $\omega_0$ is a pre-state of $C$,

   \item for every $p\in\nprocs{n}$ and every $v \in \var$,
     $\mymem(\omega_0, p)(v)$ is a unique symbolic constant, and

   \item $\mypathcond(\omega_0)
     = \bigwedge\limits_{p\in\nprocs{n}}\myeval{\psi}(\omega_0, p)$,
     and $\myallemptyguard$ holds for all processes on
     $\omega_0$.  \end{enumerate}
    
  \item $\Omega$ is the set of states that are reachable from
    $\omega_0$ over $T$ with the interpretation $I^{\sym}$.
       
  \item
    $\leadsto^{\sym}_{C}\colon{} \mystates^{\sym} \times \nprocs{n}
    \times T \times \mystates^{\sym}$ is a set of global transitions
    defined as
    \[
      \{(\omega, p, \alpha, \omega') \mid \omega' \in I^{\sym}(\omega,
      p, \alpha), p \in \nprocs{n}, \omega \in \Omega, \alpha{} \in
      T\}
    \]
  \end{itemize}
  We also call $G$ the state space graph searched by
  $\mcalgo(\model, \cotriplenoloc{}, n)$.  $\qed$
\end{defn}
The definition of $\myact{}(t)$ is also extended for the global
transition
$t \in \mystates^{\sym} \times \nprocs{n} \times T \times
\mystates^{\sym}$ in a natural way.


Given a state space graph $G$ searched by
$\mcalgo(\model, \cotriplenoloc{}, n)$, processes are ``blocked'' once
they complete $C$ in any execution in $G$.  So it is not possible for
a process to send messages after it exits $C$.  In other words, $G$
excludes the extended executions of $C$ that may cause interference.
Then does it mean that it is not sufficient to prove the validity of
the triple by exhaustively exploring $G$?  In fact, it is sufficient
to verify the triple only within $G$, if one always make the worst
case assumption for interference, i.e., for any process $p$ that has
completed $C$, $p$ may send a message to any other process at any
time.  We now define a predicate $\mayInterfere$ for this worst case
assumption.

%%%%%%%%%%%%%%% Emanate DEFINITION %%%%%%%%%%%%%%%%%%
\begin{defn}
  Let $G = (n, \omega_0, \Omega, \leadsto^{\sym}_C)$ be a state space
  graph searched by the algorithm $\mcalgo(\model, \cotriplenoloc,
  n)$.  Let $\omega \in \Omega$ be a state.  By $\emana_G(\omega)$, we
  denote the set of global transitions that \emph{emanate from} $\omega$ in
  $G$, i.e., \[ t \in \emana_G(\omega) \text{ iff }
  t \in \leadsto^{\sym}_C~\wedge{}~\mysrc(t) = \omega.  \] Note for
  any $t \in \emana_G(\omega)$, $\mypathcond(\mydest(t))$ may be
  unsatisfiable. $\qed$
\end{defn}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%% MAY-INTERFERE DEFINITION %%%%%%%%%%%%%%%
\begin{defn}
  Let $G$ be a state space graph searched by
  $\mcalgo(\model, \cotriplenoloc, n)$.  Let $\omega$ be a state in a
  feasible path in $G$.  Let $p, q \in \nprocs{n}$ be some processes.
  By $\mayInterfere_G(\omega, p, q)$, we denote that the state
  $\omega$ can lead to an interference if process $p$ sends a message
  to $q$ in the next step.  Let $v \in \symexpr$ be some symbolic
  expression.  Formally, we have 
  \begin{align}
  & \mayInterfere(G, \omega, p, q, r) \text{ iff } \nonumber \\
  &\exists{t_q \in \emana_G(\omega)}.\, \neg{}\exists{t_p \in \emana_G(\omega)}.\, \nonumber \\
  &\myproc(t_q) = q \wedge{} \myproc(t_p) = p \wedge{} \myact(t_q)
  = \myactrecv{$v$}{$p$} \wedge{} \mychan(\omega)(p, q)
  = \epsilon. \qed \nonumber 
  \end{align} \label{defn:mayinterfere}
\end{defn}

The intuition in Def.\ \ref{defn:mayinterfere} is that if we assume
the worst case, for any state $\omega$ in a feasible path in $G$, no
transition $t \in \emana_G(\omega)$ shall be labeled by a receive
action over an empty channel from a ``completed'' process $p$ to
$\myproc(t)$.  Otherwise, by the worst case assumption, $p$ will send
a message to $\myproc(t)$ in the next step.  Then executing $t$
becomes feasible and can lead to an interference.  Now considering the
collective triple $\cotriplenoloc{}$ associated with $G$.  For an
execution $\pi$ in $G$ such that $\omega \in \mypathstates(\pi)$, if
\[
  \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\pi \Gamma,
\]
we know that $p$ will not send a message to $q$ until a process $r$
exits $C$.  Then the worst case assumption can be constrained to that
process $p$ will send a message to $q$ after exiting $C$ at any time
once $r$ exits $C$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%% ERROR DEFINITION %%%%%%%%%%%%%%%%%%%%
\begin{defn}
  A prefix $\rho$ of a feasible execution in the state space graph $G$
  searched by the algorithm $\mcalgo(\model, \cotriplenoloc{}, n)$
  violates the contract or contains a deadlock, denoted
  $\rho \not\models \cotriplenoloc$, if it belongs to one of the cases
  defined in Fig.\ \ref{fig:minimp:mono:error}.  We have
  $\mcalgo(\model, \cotriplenoloc{}, n) = \textbf{T}$, if for every
  prefix $\rho$ in $G$, $\rho$ contains no deadlock and does not
  violate the contract.  $\qed$
  \label{defn:minimp:mono:error}
\end{defn}

If $\mcalgo(\model, \cotriplenoloc{}, n) = \textbf{T}$, we also
informally say that the state space graph searched by
$\mcalgo(\model, \cotriplenoloc{}, n)$ is \emph{error free}.

\begin{figure}[h]
  \begin{center}
\fbox{
  \parbox{.8\textwidth}{
    \begin{align}
      &\textbf{DL, } \text{\textbf{d}ead\textbf{l}ock:}\nonumber\\
       &\text{~~let } \omega = \mydest(\mytail(\rho)) \text{ in }      \nonumber \\            
                &\text{~~$\omega$ is not a post-state of $C$, and} \nonumber \\
                &~~\forall{t} \in \emana_G(\omega).\, \mypathcond(\mydest(t)) = \textbf{F}
  \nonumber \\[\myskip]
%%%%%%%%%%%%%%%%%%%%%%  
%%%%%%%%%%% post-state fail:
  &\textbf{SGV, } \text{\textbf{s}tate
    \textbf{g}uarantee \textbf{v}iolation} \nonumber \\
      &\text{~~let } \omega = \mydest(\mytail(\rho)) \text{ in }
        \nonumber \\
      &~~\text{if }\omega\text{ is a post-state of }C, \text{ then} \bigwedge\limits_{p \in
        \nprocs{n}}\myseval{\myallemptyguard{} \texttt{ \&\& } \phi}(\omega, p) = \textbf{F}  \nonumber      \\[\myskip]
%%%%%%%%%%%%%%%%%%%%%%  
                                  %%%%%%%%%%% interfere:
  &\textbf{ITF, } \text{\textbf{i}n\textbf{t}er\textbf{f}erence}
    \nonumber \\
      &\text{~~let } \omega \in \mypathstates(\rho) \text{ in} \nonumber \\
       &~~\exists{p, q, r \in
                    \nprocs{n}}.\,
                    \mayInterfere_G(\omega, p,
                    q)  \wedge{} \nonumber \\
                &\neg\exists                 
                  \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_{\rho} \Gamma.\,
                  \nonumber \\
      &~~\omega \text{ appears before } \myexit^{C}_{r, \rho} \text{ on
        } \rho \nonumber \\[\myskip]
                      %%%%%%%%%%%%%%%%%%%%%
                      %%%%%%%%%%%%%%%%%%%%%%%% guaranty
  &\textbf{PGV, } \text{\textbf{p}ath \textbf{g}uarantee
    \textbf{v}iolation} \nonumber \\
       &\text{~~let } \omega = \mysrc(\myhead(\rho)) \text{ in }
   \nonumber \\            
                &~~\forall{p \in \nprocs{n}}. \rho \vdash{} \neg{}\myaeval{\textup{$\Upsilon$}}(\omega, p) \nonumber  
\end{align}
}}
\end{center}
\caption{The definition of contract violation and deadlock for a
  prefix $\rho$ of an execution in the state space graph $G$ searched
  by $\mcalgo(\model, \cotriplenoloc{}, n)$.}
\label{fig:minimp:mono:error}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We explain Fig.\ \ref{fig:minimp:mono:error} briefly.  Given a state
space graph $G$ searched by the algorithm
$\mcalgo(\model, \cotriplenoloc, n)$.  \textbf{DL} defines the
condition of deadlock, i.e., the final state of a feasible execution
is not a post-state of $C$; \textbf{SGV} defines the case where the
state-guarantee $\phi$ fails to hold on a post-state of $C$;
\textbf{ITF} defines the case where the path-requirement $\Gamma$
fails to prevent possible interferences; finally, \textbf{PGV} defines
the case where a feasible execution of $C$ fails to satisfy the
path-guarantee $\Upsilon$.

The soundness of $\mcalgo$ is proved in \S\ref{sec:minimp:mono:proof}