In this chapter, we will describe the verification approaches for
MiniMP programs.  A verification approach is a procedure that takes a
MiniMP program and some inputs of the program and determines if the
program contains a set of properties.  This paper is only insterested
in verifying properties related to program correctness, which as we
have discussed in \S\ref{sec:correct-minimp} include the safety
property, deadlock freedom and functional correctness.

In order to illustrate approaches for verifying program correctness,
\S\ref{sec:verify:safe} extends the definition of the state space graph
$\mymath{G_{\model}}$ of a model $\model$ of a MiniMP program to a
\emph{safe state space graph} $\mymath{G_{safe_\model}}$, for which
the properties that we care about can all be interpreted as predicates
on states.  

One of the traditional approaches for verifying concurrent programs is
using the monolithic model checking technique.  We will briefly talk
about model checking for MiniMP in \S\ref{sec:verify:monolithic} as a
background.  In \S\ref{sec:verify:contract}, we introduce a new approach that uses
modular model checking and symbolic execution techniques to check
MiniMP programs against function contracts.

\section{The Safe State Space Graph and Error States} \label{sec:verify:safe}
Recall the informal description of the properties related to
correctness of MiniMP programs in \S\ref{sec:correct-minimp}, the
deadlock freedom and functional correctness properties are both about
whether some conditions hold at some states.  Hence it would be
straightforward to formally describe these properties in terms of
predicates on states.  The safety property, which states that no
evaluation results in \textbf{UNDEF} cannot be directly expressed as a
predicate on states since evaluation only happens when interpreting
transitions.  It will be easier for the discussion in the rest of this
chapter if we could also formally describe the safety property as a
predicate on states.  In order to do so, we will extend the definition
of the MiniMP model and semantics.

Let \textit{error} be an auxillary global variable that will always be
added into a MiniMP model $\model$.  We call the model with the
auxillary variable a \emph{safe model} $\mymath{\model_{safe}}$.  We also
extend the transition interpretation procedure $\mymath{next}$ to
$\mymath{next_{safe}}$:
\begin{itemize}
\item[] $\mymath{next_{safe}(s, p, (l, g, a, l'))} = $
\item $\mymath{
  \{\frac{\uparrow,\, \downarrow{}top(s, p)[l' / l],\, \textit{error} \rightarrow 1}{s, p}\}
}$, if one of the following holds
\begin{enumerate}
\item $\mymath{a = var} \texttt{=}
  \mymath{e} \text{, and } \myeval{e}(s, p) = \textbf{UNDEF}$
  
\item $\mymath{a = var\texttt{[}e_0\texttt{]}} \texttt{=}
  \mymath{e_1} \text{, and } \myeval{e_0}(s, p) = \textbf{UNDEF} \text{ or } \myeval{e_1}(s, p) = \textbf{UNDEF}$
  
\item $\mymath{a = \texttt{send } e_0 \texttt{ to } e_1}$, and
 $ \myeval{e_0}(s, p) = \textbf{UNDEF} \text{ or } \myeval{e_1}(s, p) =
  \textbf{UNDEF}$

\item $\mymath{a = \texttt{recv } var \texttt{ from } e}$, and $\myeval{e}(s, p) = \textbf{UNDEF}$
\end{enumerate}

\item $\mymath{next(s, p, (l, g, a, l'))}$, otherwise
\end{itemize}
Correspondingly, we have 
\begin{itemize}
\item[] $\mymath{nextAll_{safe}(S', Edge) = \bigcup\limits_{s \in S', p \in np(s), \\edge \in Edge} next_{safe}(s, p, edge)}$
\end{itemize}
The state space graph interpreted by $\mymath{next_{safe}}$ and
$\mymath{nextAll_{safe}}$ of a safe model $\mymath{\model_{safe}}$ is
\begin{itemize}
\item[] $\mymath{G_{\model_{safe}} = (S_{safe}, S_0, Edge_{\model_{safe}}, \leadsto_{\model_{safe}})}$ where,
\item $S_0$ is a set of initial states

\item $\mymath{Edge_{\model_{safe}}}$ is the set of edges of the safe
  model $\mymath{\model_{safe}}$

\item $\mymath{S_{safe} = nextAll^i_{safe}(S_0, Edge_{\model_{safe}}) \cup
  S_0}$, for some $i$ such that for every $j, i \leq j$, we have
  $\mymath{nextAll^i(S_0, Edge_{\model_{safe}}) = nextAll^j(S_0,
  Edge_{\model_{safe}})}$

\item $\mymath{\leadsto_{\model_{safe}} = \{(s, p, edge, s') \mid next_{safe}(s, p, edge) = s', p \in np(s), s, s' \in S_{safe}, edge \in Edge_{\model_{safe}}\}}$
\end{itemize}

Now we can define whether a state violates the safety or the deadlock
freedom properties for a state space $\mymath{G_{\model_{safe}} =
  (S_{safe}, S_0, Edge_{\model_{safe}}, \leadsto_{\model_{safe}})}$
with the following two predicates:
\begin{itemize}
\item a state $s$ violates the safety property if and only if
  $\mymath{\exists{p}. \myeval{\textit{error}}(s,
  p) = 1}$, for $p \in [n]$
\item a state $s$ violates the deadlock freedom property if and only
  if \\$\mymath{(\forall{p}.\, |stack(s, p)| > 0, \text{ for } p \in
    [n]) \wedge (\forall{t}.\, src(t) \not= s, \text{ for } t \in
    \leadsto_{\model_{safe}})}$
\end{itemize}
We call a state $s$ that violates the safety or deadlock freedom
property an \emph{error state}.  

The functional correctness property of MiniMP programs is special and
more complicated than the above two.  We will discuss the property in
\S\ref{sec:verify:contract}.

\textcolor{red}{TODO} lemma : if an error state exists in safe state graph, it also
exist in state graph.

\section{Monolithic Model Checking for MiniMP} \label{sec:verify:monolithic}
The model checking technique can be used to verify safety properties
and deadlock freedom of MiniMP programs.  One of the inputs of a
general model checking algorithm for MiniMP is a model of the whole
program, so we call such a model checking algorithm the monolithic
approach.

The general model checking algorithm $\mymath{MC}$ takes a MiniMP
model $\model$ and a positive number $n$ representing the number of
processes, searches all reachable states $\mymath{MC(\model, n)
  \subset G_{\model_{safe}}}$ from an initial state $s_0 \in S_0$,
where $\mymath{nprocs(s) = n}$.  We say a state $s'$ is reachable from
a state $s$ in a state space if and only if there exists a path from
$s$ to $s'$ in the state space.  The model $\mymath{\model_{safe}}$ is
verified as free of safety or deadlock freedom property violation with
$n$ processes if and only if there is no error state found in
$\mymath{MC(\model, n)}$.  Whenever an error state is found, a path
from the initial state to the error state can be provided as a
counter-example.

The monolithic model checking technique can also check functional
correctness of MiniMP programs against function contracts via
translating contracts into program assertions.  But we will not
elaborate such an approach in this paper because 1) the state
explostion is the inevitable problem for monolithic model checking;
and 2) we will introduce a new approach in \S\ref{sec:verify:contract}
which enables modular verification for functional correctness.

\section{Modular Verification using Model Checking and Symbolic Execution} \label{sec:verify:contract}
%% modular:
One of the motivations of applying modular verification to
message-passing programs, such as MiniMP, is to reduce the complexity
of the monolithic verification problem via dividing the problem into a
number of smaller sub-problems.

The basic idea of modular verification with function contracts is that
for a program, one verifies a function satisfying its contract with
the assumption that other functions in the program satisfy their
contracts.  Such verification only depends on the contracts, instead
of the definitions, of other functions, hence the verification of one
function is independent of others.  If all the functions are verified
in such a way, the program is verified.

Applying such an idea to verify a MiniMP program, one will verify each
collective-style or process-local function while assuming that all
other collective-style or process-local functions satisfy their
contracts.  Note that such verification is independent with other
collective-style or process-local functions but still depends on the
functions that are neither collective-style nor process-local.  We
call a collective-style or process-local function a \emph{dividable
function}.  Then \emph{undividable functions} are the functions that
are not dividable functions.  If all dividable functions are verified
in such a way, the MiniMP program is verified.

Although a MiniMP program may contain undividable functions, it is
always able to be divided into a set of dividable functions because
the \texttt{main} function is always a dividable function.  In the
worst case, a MiniMP program can only be divided into a singleton set
of function which makes the modular verification be same as monolithic
verification.  But we believe this will be the rare case, especially
for relatively a large program.  Our belief is based on the basic rule
of thumb of software engineering that a good way of coding is grouping
procedures into functions.

%%focus on collective-style:
The verification approach we are going to introduce is designed for
collective-style functions, but is also appropriate for process-local
functions if one take a process-local function as a special case of
collective-style functions for executions with a single process.  We
will show how does the approach work for process-local function by the
end of this section.  For now, we will only focus on collective-style
functions.

%% model checking and symbolic execution
\subsubsection{The State Space of a Collective-style Function}
Our modular verification approach is based on model checking and
symbolic execution.  Recall that the symbolic execution technique is
about assigning symbols to variables and associating executions with
path conditions.  Let $\mymath{SymExpr}$ be the set of \emph{symbolic
  expressions}, which contains $\dom$ and a set of symbolic constants
$\mymath{Symbol = \{ X_0, X_1, ...\}}$.  Every symbolic constant
represents an arbitrary value in domain $\dom$.  Any operations that
can be applied to values in $\dom$ can also be applied to symbolic
expressions.  Symbolic expressions $\mymath{SymExpr}$ are formed by
the union of $\dom$, $\mymath{Symbol}$ and operations over
$\mymath{\dom \cup Symbol}$.  Let $\textit{State}^S$ be the set of
states where memories map variables to symbolic expressions and the
channals are sequences of symbolic expressions.  Instead of searching
states in the state space of a whole MiniMP model, our approach
searches states in the state space of a function with a contract.

\begin{defn}
  For a function graph with a contract $\mymath{FG'_f}$ in a safe
  MiniMP model $\mymath{M_{safe}}$, a state space of the function
  graph is a tuple:
  \begin{align}
    \mymath{
    G_{FG'_f} = (Q, Q_0, Edge_{f}, \leadsto^S_{f})} \nonumber 
  \end{align}
  , where
  \begin{itemize}
  \item $Q$ is a set of pairs $\mymath{(s, pc)}$, where
    $s \in \textit{State}^S$ and $\mymath{pc}$ is a symbolic
    expression representing a path condition
  \item $Q_0$ is a set of initial pairs
  \item $Edge_f$ is the set of edges in the $FG'_f$
  \item $\mymath{\leadsto^S_f \subseteq \textit{State}^S \times SymExpr
      \times [n] \times Edge_f \times \textit{State}^S \times SymExpr}$ is the
    transition relation
  \end{itemize}
\end{defn}

Let $\mymath{fresh(s)}$ denote a symbolic constant that occurs free in
all the symbolic expressions that all memories in state $s$ can map
to.  We define a procedure $\mymath{havoc(s, p, Var)}$ that assigns
all the variables in the set $\mymath{Var}$ for process $p$ with a set
of unique symbolic constants that occur free in state $s$ as follows:
\begin{itemize}
\item[] $\mymath{havoc(s, p, Var) = }$
\item $s$, if $\mymath{Var = \emptyset}$
\item $\mymath{havoc(\frac{var \rightarrow fresh(s)}{s,
      p}, p, Var - \{var\})}$, otherwise
\end{itemize}

The procedure $\mymath{next^S(s, pc, p, edge)}$ that depends on a
state-path-condition pair $\mymath{(s, pc)}$, a process $p$ and an
edge $edge$ interprets a transitions
$\mymath{(s, pc, p, edge, s', pc')}$:
\begin{itemize}
\item[] $\mymath{next^S((s, pc), p, (l, g, a, l')) = }$
\item $\mymath{\emptyset}$, if $\mymath{toploc(s, p) \not= l}$ or
  $\mymath{pc = 0}$, else
  
\item $\mymath{
    \{(s, pc \wedge \myeval{g}(s, p)) \mid s \in next(s, p, (l, 1, a, l')\}
  }$, if
  \begin{itemize}
  \item[] $\mymath{a = var \texttt{ = } e}$ or
  \item[] $\mymath{a =
      var\texttt{[}e_0\texttt{]} \texttt{ = } e_1}$ or
  \item[] $\mymath{a =
      \texttt{ret } e}$
  \item[] $\mymath{a =
      \texttt{send } e_0 \texttt{ to } e_1}$
  \end{itemize}, else
  
\item
  $\mymath{\{(havoc(topvars(s, p) \cup \{var\}, \frac{\uparrow,
      \downarrow{}top(s, p)[l' / l]}{s, p}, p),\, pc)\}}$, if $\mymath{a = var
    \texttt{ = call } f}$

\item $\mymath{
    \{(s, pc \wedge |comm(s)(\myeval{e}(s, p), p)| > 0) \mid s \in next(s, p, (l, 1, a, l')\}
  }$, if $\mymath{a = \texttt{recv } var \texttt{ from } e}$

\item 
  $\mymath{\{ 
    (dequeue(\frac{\uparrow,\, \downarrow{}top(s, p)[l' / l],\, var_0
      \rightarrow head(\mathit{C}(p', p)),\, var_1 \rightarrow p'}{s,
      p}, p', p),  pc \wedge |comm(s)(p', p)| > 0
    \mid p' \in [n]\}}$ \\
  , if $\mymath{a = \texttt{recv } var_0 \texttt{ from any } var_1}$
\end{itemize}

Correspondingly, we have
\begin{center}
  $\mymath{nextAll^S(Q', Edge) = \bigcup\limits_{(s, pc) \in Q',\, p \in
      np(s),\, edge \in Edge} next^S((s, pc), p, edge)}$
\end{center}

In $\mymath{G_{FG'_f}}$, $Q$ is likely infinite, which comes out of
the well-known problem that loops and recursions may lead the symbolic
execution to infinite exploration.  We will discuss this problem
later.  For now, we will assume $Q$ may be infinite and
$\mymath{Q = nextAll^{S^{+\infty}}(Q_0, Edge_f) \cup Q_0}$.

Let $\mymath{havocAll(s, n)}$ be a procedure that recursively applies
$\mymath{havoc}$ to all visible variables for all processes in $[n]$
on state $s$, i.e. 
\begin{itemize}
\item[]  $\mymath{havocAll(s, n) = }$
\item $\mymath{havoc(s, 0, topvars(s, 0))}$, if $n = 1$
\item $\mymath{havocAll(havoc(s, n-1, topvars(s, n-1)), n-1)}$, otherwise
\end{itemize}

 The set $Q_0$ of
initial pairs is defined by
\begin{center}
  $\mymath{Q_0 = \{(havocAll(s, n), 1) \mid initial(s, n), n > 0\}}$, where
\end{center}
$\mymath{initial(s, n)}$ is a predicate defined as
\begin{align}
  \mymath{initial(s, n)} = \forall{p}.\,
  & |\mymath{stack}(s, p)| = 1~\wedge~\mymath{toploc}(s, p) =
    \mymath{loc}_{f_0}~\wedge~\mymath{comm}(s)
    = \epsilon \nonumber\\
  \text{, for } & p \in [n]  \nonumber
\end{align}

For simplicity, we abuse $\mymath{np}$ with
$\mymath{np((s, pc)) = np(s)}$ for $\mymath{(s, pc) \in Q}$.  The transition
relation $\leadsto^S_f$ is defined as
\begin{center}
$\leadsto^S_f = \{(q, p, edge, q') \mid{} next^S(q, p,
edge) = q',\,f p \in np(q), q, q'\in Q, edge \in
Edge_f\}$
\end{center}

Similar to the concepts of state spaces of MiniMP models, for a
transition $t = (q, p, edge, q') \in \leadsto^S_f$, we use
$\mymath{src^S(t)}$ to denote the \emph{source pair} $q$ and
$\mymath{dest^S(t)}$ to denote the \emph{destination pair} $q'$.  We
call a finite sequence of transitions $\rho = t_0t_1...t_m$ a path in
$\mymath{G_{FG'_f}}$, if $t_i \in \leadsto^S_f,\, 0 \leq i \leq m$ and
$dest(t_i) = src(t_{i+1}),\, 0 \leq i \leq m$.  The notation
$\mymath{States^S(\rho)}$ denotes the set of states in a path $\rho$,
i.e.
$\mymath{States^S(\rho) = \bigcup\limits_{t \in \rho}\{src^S(t),
  dest^S(t)\}}$.  A path $\rho$ is \emph{infeasible} if
$\mymath{\exists{(s, q)}.\, q = 0 \wedge{} (s, q) \in
  States^S(\rho)}$.  A path is \emph{feasible} if it is not
infeasible.  In $G_{FG'_f}$, a path $\pi$ is called an execution if it
starts with $q \in Q_0$ and ends with a $q' \in Q$ such that
$\mymath{\neg{}\exists{t}.\, src^S(t) = q' \wedge t \in \leadsto^S_f}$

\subsubsection{Model Checking for Function Contracts}
In the rest of this section, we will only talk about state space of
function graphs, so there is no ambiguity if we simply refer a pair
$(s, pc) \in Q$ as a state.  When we say something of a state
$(s, pc)$, it means something of $s$ except that the path condition of
a state $(s, pc)$ means the $pc$.

The state space $\mymath{G_{FG'_f}}$ for a function $f$ contains all
possible behaviors of the collective-style function $f$. But the model
checking algorithm introduced in \S\ref{sec:verify:monolithic} cannot
be simply applied to $\mymath{G_{FG'_f}}$ because the search will
likely not terminate due to the aforementioned infinite symbolic
execution problem.  A simple solution is to add bounds to some of the
symbolic constants in the initial state.  This can be done by
assigning formulas to the path condition of the initial state.  Figure
\ref{fig:example:add_bounds} shows an example of that adding bounds to
a symbolic constant makes the reachable states finite from a given
initial state.  Adding bounds to some symbolic constants in the
initial states makes reachable state set finite but limits the
verification result to be within the bounds.  Recall that this is what
many software model checkers do and the result is useful under the
small scope hypothesis.  We will talk about using \emph{loop
  invariants} to reduce the limits in a later chapter.

In general, our approach for verifying one function $f$ is to apply
model checking algorithm to search in the state space of $f$ for error
states which violates the safety property, deadlock freedom or the
function contract $C_f$.  The apporach should guarantee that if it
terminates and finds no error state, the function $f$ satisfies its
contract.  If the approach finds an error state, one may find an path
of the model containing $f$ from an initial state to the error state.
Whether one can find such a path depends on if the pre-condition of
$C_f$ is strong enough for the model.

%% TODO : define the sturcture (G_fg, Spec) for verification


For a state space $G_{FG'_f}$ of a function $f$, we are not interested
in those states that only exist in infeasible paths.  In addition, we
are not interested in the states that only exist in the paths that are
stated as never will happen by the function contracts.  We will
categorize the paths in the latter case as infeasible paths as well
hence the definition of the infeasible path needs to be extended with
respect the sturcture $\mymath{(G_{FG'_f}, Spec)}$.


\textcolor{red}{TODO}  Figure \ref{fig:example:add_bounds}

\textbf{The approaches for verifying functions indepedently}

\textbf{proof}

\textbf{Infinite state space}

%% If one verify every function (including main) using the
%% verification approach, the program is correct, i.e. all functions
%% satisfy their contracts. Since main function satisifies its
%% contract, the program is functionally correct.

%% proof