In this chapter, we give a summary on background and related research
work.  The background knowledge includes an introduction to classical
Hoare style verification approaches for sequential
(\S\ref{sec:background:hoarelogic}) and concurrent programs
(\S\ref{sec:background:formal4concurrency}), two semiformal
verification approaches: model checking
(\S\ref{sec:background:modelchecking}) and symbolic execution
(\S\ref{sec:background:symexe}), and the MPI standard
(\S\ref{sec:background:mpi}).  The state-of-the-art verification tools
for message-passing parallel programs, as well as their relations to
this dissertation, are described in the second part.  The second part
consists of three sections: \S\ref{sec:related:modelcheckers} talks
about automated model checkers; \S\ref{sec:related:staticanalyzer}
gives an overview on other automated tools, including static analyzers
and runtime verifiers; finally, existing deductive verification tools
are briefly described in \S\ref{sec:related:deductive}.


%% HOARE LOGIC
\section{Hoare Logic} \label{sec:background:hoarelogic}

\emph{Hoare logic} \cite{hoare:1969:axiomatic} provides a proof system
for deriving safety properties of sequential programs.  It is the
basis for deductive verification.

The key notion in Hoare logic is the \emph{Hoare triple},
$\{P\}~S~\{Q\}$, where $S$ is a program statement, and $P$ and $Q$ are
logic formulas.  The formula $P$ is called a \emph{pre-condition}, and
$Q$ is called a \emph{post-condition}.  The Hoare triple is
\emph{valid} if the following holds: whenever $S$ is executed from a
state in which $P$ holds, if $S$ terminates then $Q$ will hold in the
resulting state.

Hoare's original paper uses a simple ``while'' programming language
which has assignments, while loops, if and if-else statements, and
sequential composition (\code{;}).  A set of inference rules are
defined for reasoning about Hoare triples over this language.  This
rule set is called the \emph{Hoare calculus}.   Each inference rule
has a set of premises---Hoare triples assumed to hold---and a 
conclusion---the Hoare triple which one can conclude holds given
that the premises do.
% Every inference rule also formally describes the semantics
% of a statement kind.
% SFS: which statement kind does the consequence rule describe?

Fig.\ \ref{fig:intro:hoare:rules} shows the inference rules in Hoare
calculus.  The rules are presented in the standard syntax where the
premises appear above the horizontal line and the conclusion below the
line.

The \emph{skip} rule shows that a pre-condition will be preserved by a
no-op.

The \emph{assignment} rule has no premise.  It states that the
post-condition $Q$ of the assignment \texttt{$a$ := $e$} can be
ensured, if the pre-condition is obtained by substituting $a$ with
expression $e$ in $Q$.

The \emph{sequence} rule states that if there is a condition that can
serve as the post-condition of a statement $S_0$ as well as the
pre-condition of another statement $S_1$, a Hoare triple for the
composite statement $S_0\texttt{;}S_1$ can be inferred.

The \emph{consequence} rule introduces a \emph{side condition}, which
is a logical formula over the pre- and post-conditions of two Hoare
triples.  The rule states that for a statement $S$, one triple can be
inferred from the other if the side condition is valid.

The \emph{conditional} rule expresses that a Hoare triple of a
conditional statement can be inferred from Hoare triples corresponding
to the two branches.

The \emph{loop} rule states that a Hoare triple of a while-loop can be
inferred with a condition $I$, if $I$ is an invariant of the loop
body.  This is the rule that makes proving programs with Hoare logic
hard.  The problem is that there are an infinity of loop invariants
$I$ (i.e., formulas $I$ for which the premise of the loop rule is
valid), but there is no algorithm to find just the right loop
invariant to make a proof go through.  Most program verification
systems based on deductive reasoning require the user to provide the
loop invariants.  This requires intuition about the program and
experience.

\newcommand{\ds}{\displaystyle}
\newcommand{\iskip}{1.5em}

\begin{figure}
  \[
    \begin{array}{rll}      
      \ds\frac{}{ \{P\}~\texttt{skip}~\{P\} }
      & \text{(skip)} &\\[\iskip]      
      \ds\frac{}{ \{Q[e / a]\}~a\texttt{ := }e~\{Q\} }
      & \text{(assignment)} &\\[\iskip]
      \ds\frac{\{P\}~S_0~\{R\},\,\{R\}~S_1~\{Q\}}%
      {\{P\}~S_0\texttt{;}S_1~\{Q\}}
      & \text{(sequence)} & \\[\iskip]
      \ds\frac{\{P'\}~S~\{Q'\}}{\{P\}~S~\{Q\}}
      & \text{(consequence)}
                            &
                              \text{if $P \Rightarrow P' 
                              \wedge{} Q' \Rightarrow{} Q$}\\[\iskip]
      \ds\frac{ \{P \wedge{} C\}~S_0~\{Q\},\, \{P \wedge{}
      \neg{}C\}~S_1~\{Q\}}%
      {\{P\}~\texttt{if } C \texttt{ then }S_0\texttt{ else }S_1~\{Q\}}
      & \text{(cond)} & \\[\iskip]
      \ds\frac{
        \{C\wedge{}I\}~S~\{I\}}%
      {\{I\}~\texttt{while }C\texttt{ do}~S~\{\neg{}C \wedge{} I\}} & \text{(loop)}
    \end{array}
  \]
  \caption{Inference rules of Hoare calculus.}
  \label{fig:intro:hoare:rules}
\end{figure}

%%% verification condition generation
Given appropriate loop invariants for each loop, the proof process of
applying Hoare calculus to Hoare triples can be automated with the
\emph{verification condition generation} (VCG)
\cite{barnett:2006:boogie,gordon:1989:mechanizing,leino:1999:checkingjava}
technique.  Given a Hoare triple, the VCG algorithm automatically
computes a set of formulas in the underlying logic with the property
that the validity of the formulas implies the existence of a Hoare
logic derivation of the triple.  The key step in the VCG algorithm is
the computation of the \emph{weakest pre-condition} (WP) of the
statement with respect to the post-condition. Most of the deductive
verification tools for sequential programs are based on VCG.

\begin{exmp}
  Figure \ref{fig:intro:hoare:derive} shows a derivation for a Hoare
  triple of a \emph{while} program using Hoare calculus.  In this
  figure, auxiliary variables $X$ and $Y$ are used to represent the
  values of \texttt{x} and \texttt{y} at the pre-state, respectively.
  Auxiliary variables are not part of a program, hence they will
  retain their values in the post-state.  The VCG computation for this
  example is given in Fig.\ \ref{fig:intro:hoare:wp}.  Note that the
  term $abs(\texttt{x})$ in the code stands for the absolute value of
  \texttt{x}.  By VCG, the validity of the Hoare triple is represented
  by the following condition:
  \[
  \begin{array}{ll}
    & (\texttt{x} = X \wedge{} \texttt{y} = Y) \Rightarrow{}
    \mymath{\textup{WP}}(\texttt{if x >= 0 then y = x
      else y = -x},~~\texttt{y} = abs(\texttt{x})) \\[\iskip]
    \text{i.e.,} &(\texttt{x} = X \wedge{} \texttt{y} = Y) \Rightarrow{} true
  \end{array}
\]
This verification condition is obviously $\mymath{true}$ hence the
Hoare triple is valid.  $\qed$
\end{exmp}

\begin{figure}[t]
  \centering
\begin{small}
    \fbox{
    \parbox{.96\textwidth}{
\[\begin{array}{lll}
\hspace{-.2cm}    & \{\texttt{x} = X \wedge{} \texttt{y} = Y\}~~  
    \texttt{if x>=0 then y = x else y = -x} 
    ~~\{\texttt{y} = abs(\texttt{x})\} & \hspace{-.2cm}\text{(cond 1, 2)}\\[\myskip]
    
\hspace{-.2cm}    1 & \{\texttt{x} = X \wedge{} \texttt{y} = Y \wedge{} X \geq 0\}~~
    \texttt{y = x} ~~\{\texttt{y} = abs(\texttt{x})\} & \hspace{-.2cm}\text{(conseq 1.1)}\\[\myskip]

    %%% 1.1
\hspace{-.2cm}    1.1 & \{\texttt{x} = \mymath{abs(}\texttt{x})\}~~ \texttt{y = x} ~~\{\texttt{y} =
                        abs(\texttt{x})\} &
                                            \hspace{-.2cm}\text{(assign)}\\[\myskip]

\hspace{-.2cm}    2 & \{\texttt{x} = X \wedge{} \texttt{y} = Y \wedge{} X < 0\}~~
    \texttt{y = -x} ~~\{\texttt{y} = abs(\texttt{x})\} & \hspace{-.2cm}\text{(conseq 1.2)}\\[\myskip]

    %%% 1.2
\hspace{-.2cm}    1.2 & \{-\texttt{x} = \mymath{abs(}\texttt{x})\}~~
                        \texttt{y = -x} ~~\{\texttt{y} =
                        abs(\texttt{x})\} &
                                            \hspace{-.2cm}\text{(assign)}
  \end{array}\]}}
\end{small}
\caption{The derivation of a Hoare triple.  $X$ and $Y$ are auxiliary
  variables holding the values of \texttt{x} and \texttt{y},
  respectively, at pre-state.  The symbol $\mymath{abs}$ represents
  the absolute value function in the underlying first order logic.  }
          \label{fig:intro:hoare:derive}
\end{figure}

\begin{figure}[t]
  \centering
    \fbox{
    \parbox{.96\textwidth}{
  \[
  \begin{array}{lrll}
  \multicolumn{3}{l}{\mymath{\textup{WP}}(\texttt{if x>=0 then y = x
    else y = -x},~~\texttt{x} = abs(\texttt{y}))} & (\text{cond})\\[\myskip]    

 \hspace{1cm} & = & \texttt{x} \geq{} 0 \Rightarrow{} \mymath{\textup{WP}}(\texttt{y = x},~~\texttt{x} =
   abs(\texttt{y}))~~\wedge{}&  \text{(assign)}\\

 \hspace{1cm}  & & \texttt{x} < 0 \Rightarrow{} \mymath{\textup{WP}}(\texttt{y = -x},~~\texttt{x} =
    abs(\texttt{y})) &  \text{(assign)}\\[\myskip]

 \hspace{1cm}  & = & (\texttt{x} \geq{} 0 \Rightarrow{} \texttt{x} =
    abs(\texttt{x}))~~\wedge{}~~(\texttt{x} < 0 \Rightarrow{} \texttt{x} =
    abs(\texttt{-x})) \\ [\myskip]
 \hspace{1cm}  & = & true & 
  \end{array}
  \]
}}
      \caption{The computation of the weakest pre-condition,
        $\textup{WP}(S, Q)$, for a given statement $S$ and desired
        post-condition $Q$. }
          \label{fig:intro:hoare:wp}
\end{figure}


\emph{Design by Contract}$^{\small{\texttt{TM}}}$
\cite{Meyer:1992:ADC} (DbC) is a methodology developed by Bertrand
Meyer for software correctness\footnote{The term was trademarked and
  the trademark is now owned by Eiffel Software.}.  The idea of an
important part of DbC is to use pre- and post-conditions to document,
as well as check the correctness of, program procedures.  A pair of a
pre- and post-conditions for a procedure is called a \emph{procedure
  contract}.  Procedure contracts are built-in constructs in the
Eiffel \cite{Meyer:1988:eiffel} programming language.  They can be
checked as assertions during runtime executions.

Procedure contracts is also absorbed by many programming languages for
playing the role of specifications.  Why3 \cite{filliatre:2013:why3}
and Boogie \cite{barnett:2006:boogie} are verification programming
languages with rich built-in specification constructs, including
procedure contracts.  Both of them at the same time also refer to the
deductive verifiers that can prove the functional correctness of Why3
and Boogie programs, respectively, against procedure contracts and
other kinds of specifications.  There are other programming languages
adopt the idea of procedure contracts.  For example, ACSL, JML
\cite{Gosling:2014:JLS:2636997} and Spec\#
\cite{barnett:2005:specsharp} are specification languages for C, Java
and C\#, respectively.  Spark \cite{Barnes:2012:SPA} is a dialect of
Ada for describing specifications.  Dafny \cite{leino:2010:dafny} is a
programming language with built-in primitives for specification.

A number of tools are developed for verifying programs with respect to
procedure contracts and other kinds of specifications.  Such as the
static verifiers powered by Boogie, including HAVOC
\cite{lahiri2012security, ball:2010:towards}, the Spec\# verifier and
the Dafny verifier.  Spark-2014 \cite{spark} and Frama-C
\cite{cuoq2012framac} with its plug-in WP \cite{cuoq:2011:wp} are the
verification tools using Why3.


\section{Formal Methods For Concurrency}
\label{sec:background:formal4concurrency} Hoare's original logic is not
suitable for specifying and proving concurrent programs. A Hoare
triple describes a statement in terms of its input and output.
However, in a concurrent program, the behavior of a process executing
a statement depends on not only the input but also the behaviors of
other processes that run in parallel.  Besides, Hoare logic cannot
describe \emph{liveness properties}, which are crucial for concurrent
programs.

Owicki and Gries \cite{Owicki1976}, Lamport \cite{lamport:1980:hoare}
and Takaoka \cite{Takaoka:1994:PPV:326619.326811} introduced
extensions to the original Hoare logic for proving properties of
concurrent programs.

%% Owicki & Gries:
Owicki and Gries introduced a new technique in \cite{Owicki1976} based
on Hoare logic for proving \emph{safety properties} of concurrent
programs.  In their work, concurrency is enabled by two general
statements: (1) \texttt{cobegin $S_0$ // $...$ // $S_n$ coend} means
that each statement $S_i$, $0 \leq i \leq n$, is executed by a
separate process and all these processes are run in parallel; (2)
\texttt{await $B$ then $S$} means that the process has to stop at $S$
unless $B$ is true and once $B$ is true, the process executes $S$ in
an atomic step.  Formal semantics for these two statements are defined
with new Hoare-style rules.  Then for a concurrent program $S$ that
consists of the extended set of statements, the validity of
$\{P\}~S~\{Q\}$ can be derived using the rules.

The key idea in this work is the semantics of the \texttt{cobegin ...\
  coend} statement,
\begin{align}
  \frac{\{P_1\}S_1\{Q_1\},  \{P_2\}S_2\{Q_2\},  ...\ \text{ are
  interference-free}}
  {\{P_1\wedge{}P_2\wedge{}...\ \}~ \texttt{cobegin}~S_1 \texttt{ // }
  S_2 \texttt{ // } ...\ \texttt{coend}
  ~\{Q_1\wedge{}Q_2\wedge{}...\ \} }\nonumber
\end{align}
which is straightforward except for the term ``interference-free.''

Given a \texttt{cobegin} $S_1$ \texttt{ // } $\ldots{}$ \texttt{ // }
$S_{m}$ \texttt{coend} statement.  Suppose there are Hoare logic
derivations for $\{P_i\}~S_i~\{Q_i\}$, for $1 \leq i \leq m$.  For
each sub-statement $S'$ of $S_i$, there is an assertion immediately
precedes $S'$ in the derivation, denoted $\textsf{pre}(S')$.  A
sub-statement $T$ of $S_j$, $1 \leq j \leq m$, is said to not
\emph{interfere} $\{P_i\}~S_i~\{Q_i\}$, if both of the following hold:

\begin{enumerate}
\item $T$ preserves $\textsf{pre}(S')$ for every sub-statement $S'$ in $S_i$.
\item $T$ preserves the post-condition $Q_i$ of $S_i$.
\end{enumerate}

To prove the correctness of the \texttt{cobegin} statement, one must
show that every atomic sub-statement of $S_i$ cannot interfere
$S_j$, for $1 \leq i \neq j \leq m$.  Usually, in order to prevent a
triple $\{P\}~S~\{Q\}$ from being interfered, the user needs to weaken
$P$ to accept the behaviors of other parallel statements.

% Lamport: concurrent hoare logic:
Lamport \cite{lamport:1980:hoare} generalizes Hoare logic by refining
the meaning of the triple $\{P\}~S~\{Q\}$ so that (1) $P$ must be
strong enough to guarantee that $Q$ will hold upon termination even if
the execution starts from any location inside $S$; and (2) $P$ must
remain true as long as the control is in $S$, where $S$ is a
concurrent program composed of sequential statements as well as the
\texttt{cobegin} statement used by Owicki and Gries.
There are three predicates that refer to program locations with
respect to a statement $S$: immediately before $S$, inside $S$ and
immediately after $S$.  For a sub-statement $S$ in a \texttt{cobegin}
structure, a strong enough pre-condition usually takes program
locations of different processes into consideration.

% Directed graph based proof technique:
Takaoka \cite{Takaoka:1994:PPV:326619.326811} proves a triple
$\{P\}~S~\{Q\}$ for a parallel program $S$ by analyzing a program
graph representing $S$, where vertices are sets of locations of
running processes and arrows bridging vertices are labeled by program
statements.  In addition, each vertex has an associated assertion.
Initial locations are attached with pre-conditions and final locations
are attached with post-conditions.  Then for every arrow, the
assertion of the destination vertex can be derived from the assertion
of the source vertex with respect to the statement labeling the arrow.
The rules for the assertion derivation are defined in Hoare style.
The triple $\{P\}~S~\{Q\}$ is valid iff such a graph is successfully
constructed.  In Takaoka's work, parallel programs contain
synchronizing statements.  A process $p$ can ``wait for'' another
process $q$ by executing \texttt{call} until $q$ executes
\texttt{accept}.  A similar program-graph-based analysis was done by
Newton \cite{Newton1975} earlier.  In \cite{Newton1975}, program
locations can be used to express properties in assertions though the
parallel programs have no synchronizing statement.


A more intuitive approach \cite{Ashcroft:1975:PAP:1739967.1740302} was
investigated earlier by Ashcroft.  Compared to the Hoare-style based
approaches described above, many researchers, including
Lamport\footnote{Leslie Lamport comments on his publication number 23:
  ``Ashcroft got it right.  Owicki and Gries and I just messed things
  up.  It took me quite a while to figure this out.''  He comments on
  his publication number 40: ``I think Ashcroft was right; one should
  simply reason about a single global invariant, and not do this kind
  of decomposition based on program structure.'' from
  \url{http://lamport.azurewebsites.net/pubs/pubs.html\#proving}},
believe that Ashcroft's approach is a better way to prove correctness
of concurrent programs.  In \cite{Ashcroft:1975:PAP:1739967.1740302},
safety properties of a concurrent program are expressed as a
\emph{global invariant}, i.e., an assertion that is supposed to hold
at any location of the program.  The proof is constructed by showing
that every atomic step in the program preserves the invariant.

A liveness property claims that a desired event must eventually occur
during an infinite execution of a program.  Liveness properties
involve the concept ``eventually''.  \emph{Temporal logic}, which
extends the ordinary logic with temporal operators such as
``henceforth'' and ``eventually'', is widely used to express liveness
properties.  There are different techniques for proving liveness
properties.  The \emph{well-founded set} approach was originally
applied by Floyd \cite{Floyd1993} and later adapted by Manna and
Puneli in \cite{Manna:1984:APP:2731.2734}.  Other examples include the
\emph{proof lattice} approach \cite{Owicki:1982:PLP:357172.357178} and
the \emph{rely-guarantee} approach
\cite{Stark:1985:PTR:646823.706907}.

Modern tools for verifying concurrent programs in an axiomatic way
include VCC \cite{cohen-etal:2009:vcc}, COMPLEX
\cite{amani:2017:complex}, KeY
\cite{beckert:2007:KeY}, Chalice \cite{leino:2009:verification}
and VeriFast \cite{Jacobs:2010:QTV:1947873.1947902}.  VCC is a static
verifier for concurrent C programs.  The user of VCC needs to annotate
invariants and other specifications for programs.  COMPLEX is a
verification framework that targets general imperative programming
languages.  It is based on the aforementioned proof system proposed by
Owicki and Gries.  KeY verifies Java programs against their
specifications written in JML \cite{Gosling:2014:JLS:2636997}.  It
generalizes Hoare logic for Java to the \emph{first order Java Dynamic
  Logic}.  Chalice uses a permission based approach to reason about
multi-threaded concurrent programs.  VeriFast utilizes separation
logic \cite{reynolds2002separation} for verifying multi-threaded C and
Java programs.

Most of the extensions to Hoare logic for coping with concurrency
problems target the shared-memory concurrency.  To the best of the
author's knowledge, only very few such efforts were contributed to the
message-passing concurrency.

%% MODEL CHECKING
\section{Model Checking} \label{sec:background:modelchecking} Unlike
the deductive verification techniques described in the previous two
sections that can verify infinite state systems, model checking
\cite{clarke:2000:modelchecking} is a technique for verifying finite
state systems.  Although the technique is restricted to finite state
systems, model checking has the benefit of being performed
automatically.  In addition, model checking is widely used for
hardware verification because many hardware systems have a finite
number of states.  Furthermore, one can convert an infinite state
system to a finite state system through a combination of abstraction
and restriction.  For example, to apply model checking to a
message-passing concurrent system, one can (1) abstract the actual
complex communication protocols to simple message channels
\cite{Siegel:2005:MWM:1065944.1065957, 10.1007/978-3-540-30579-8_27,
  siegel2007verifying}, and (2) bound the number of processes or the
size of the message channels.  In many cases, errors in systems can be
found by model checkers with small bounds on program parameters.


Transforming a system to a \emph{finite state model} is the first step
of using model checking.  The second step is to give a specification,
which is commonly in the form of temporal logic assertions.

A model checker verifies the satisfaction of a finite state model to a
specification by searching all reachable states in the finite state
space of the model.  A state space is usually structured as a directed
graph, where a node is a state and an edge is a transition which
alters a state in an atomic step.

Model checking is effective for verifying properties of concurrent
systems.  A concurrent systems can be abstracted to an
\emph{interleaving model}. In an interleaving model, the real-world
asynchronous executions are represented by nondeterministic choices
on atomic transitions. For example, the parallel execution of two
atomic commands $a$ and $b$ can be modeled as a nondeterministic
choice over two transition sequences: $a$ followed by $b$ or $b$
followed by $a$.

A challenge in model checking is the state explosion
problem. Typically, the number of states grows exponentially when the
number of components in a concurrent system increases.  Hence, many
model checkers can only scale to programs whose inputs are bounded
with small concrete values. But model checking is still widely used to
solve real problems for two reasons.  First, there is a belief in the
\emph{Small Scope Hypothesis} \cite{Jackson:2006:SAL}, which states
that most bugs can be found by exploring all possible program
executions with inputs, the number of processes/threads, and other
program parameters being bounded in small scopes.  Second, many
sophisticated \emph{reduction} techniques allow model checkers to only
search in a sub-space of the full state space without loss of
soundness.  For example, using the \emph{partial-order reduction}
(POR) technique \cite{godefroid:1993:refining,
  10.1007/BFb0013032,Valmari1992}, a model checker usually only needs
to explore one among a number of commutative transitions.

%% SYMBOLIC EXECUTION
\section{Symbolic Execution} \label{sec:background:symexe}
Symbolic execution is an approach for
testing and analyzing programs \cite{king:1976:symbolic}. It replaces
the concrete program inputs with symbols, each of which represents a
set of concrete values.  During the symbolic execution, a boolean
formula, the \emph{path condition} (PC), is maintained.  PC denotes
the condition under which an execution path is feasible.  Symbols are
also known as \emph{symbolic constants}.  Expressions over constants
and symbolic constants are called \emph{symbolic expressions}.  In
symbolic execution, PC and variable values are all symbolic
expressions.


Symbolic execution is able to explore all possible paths of a program
that a concrete execution may take unless there are an infinite number
of them.  Different paths are generated from the different choices
that a concrete execution can make at branches.  During the
exploration of each path, PC initially is assigned the $\mymath{true}$
value and gets updated at each branch.  The updated value is a
conjunction of the old PC value and the branch condition corresponding
to the choice made in the path.  Once PC becomes unsatisfiable, the
path being explored is infeasible and will be ignored immediately.
Automated theorem provers \cite{Z3Prover, barrett-etal:2011:cvc4,
  alt-ergo} are used to reason about symbolic expressions during the
exploration.

\begin{exmp}

Considering the following C code:

\begin{center}
  \begin{programNoNum}
\ccode{if}~(x~>=~0)\\
~~y~=~x;\\
\ccode{else}\\
~~y~=~-x;\\
\end{programNoNum}
\end{center}

Suppose the variable \texttt{x} holds a symbolic expression $X$.  A
symbolic execution engine will explore two paths for this code
snippet: one path leads to a result where the variable \texttt{y} has
value $X$ and its PC becomes $X \ge 0$; the other path leads to a
result where the variable \texttt{y} has value $-X$ and its PC becomes
$X < 0$. $\qed$
\label{exmp:intro:symexe}
\end{exmp}

%% MPI
\section{MPI} \label{sec:background:mpi} The Message-Passing Interface
(MPI) standard specifies a library for writing message-passing
parallel programs in C/C++ and Fortran.  This library includes a large
number of functions, constants, and data types.  For an MPI program,
every process has its private storage but shares nothing with others.
Communication among processes is carried out by transferring data
using different MPI functions.  By far the most common way that it is
done, an MPI program is written, compiled, and linked to generate an
executable file. The program is executed by instantiating a number of
processes, each of which runs a copy of the executable.

In MPI programs, a \emph{communicator} is an abstraction of a
``communication universe'' for processes.  A communicator comprises an
ordered group of $n$ ($1 \leq{} n$) processes.  Processes are
identified by $0, 1, ..., n-1$.  The numerical identifier of a process
in a communicator is called the \emph{rank} of the process.  A process
may belong to multiple communicators and is assigned different
identifiers in each of them.  But there is a default communicator,
named \texttt{MPI\U{}COMM\U{}WORLD}, 
which contains all processes that are invoked when a program is
launched.  The rank of a process in the default communicator can be
used as the unique ID.  By branching on process ranks, different
processes may behave differently even though they run the same
program.

Communication operations are performed through communicators.
Conceptually, a communicator includes a set of message channels.
Every message channel can be identified by an ordered pair $(i, j)$
($0 \leq i, j < n$).  In general, a channel behaves like a
First-In-First-Out (FIFO) queue for buffering messages that were sent
from a process $i$ but have not been received by process $j$.  When a
process receives an message with a specific \emph{message tag}, it
attempts to pull out the first message matched the tag in the
corresponding channel.  If a wildcard message tag
(\texttt{MPI\U{}ANY\U{}TAG}) is used for the receive operation, the
message channel behaves in exact FIFO order, i.e., the first message
in the channel will be dequeued.

In MPI, communication can be nondeterministic.  A process can perform
a receive operation without specifying an exact sender by using the
pre-defined constant \texttt{MPI\U{}ANY\U{}SOURCE} as the source
argument.  Such a receive operation is called a \emph{wildcard
  receive}.  Conceptually, a wildcard receive performed by process $i$
nondeterministically chooses an integer $j$ ($0 \leq j < n$) for which
channel $(j, i)$ contains a matching message.  It then dequeues the
first such message from the channel.

\begin{exmp}
  Figure \ref{fig:mpi:simple} is a simple C/MPI program.  Constructs
  defined in the MPI library all start with an ``\texttt{MPI\U{}}''
  prefix.  \texttt{MPI\U{}COMM\U{}WORLD} is the constant that refers
  to the default communicator.  The \texttt{MPI\U{}Init} function
  initiates the message-passing environment.  Every process can obtain
  its rank in a communicator by calling \texttt{MPI\U{}Comm\U{}rank}.
  The \texttt{MPI\U{}Finalize} function terminates the environment.

  In this example, the process of rank 0 sends a message to the
  process of rank 1.  The point-to-point (P2P) communication is
  carried out by a pair of standard P2P send and receive functions:

\begin{figure}[t]
  \begin{program}
    \ccode{\#include}~<mpi.h>\\
    \ccode{int}~main(\ccode{int}~argc,~\ccode{char}~*argv[])~\lb~\\
    ~~\ccode{int}~rank,~dat~=~0;~\\
    ~~MPI\civlU{}Init(\&argc,~\&argv);~\\
    ~~MPI\civlU{}Comm\civlU{}rank(MPI\civlU{}COMM\civlU{}WORLD,~\&rank);
\mycomment{//gets the rank of this
  process}\\
~~\ccode{if}~(rank~==~0)~\\
~~~~MPI\civlU{}Send(\&dat,~1,~MPI\civlU{}INT,~1,~0,~MPI\civlU{}COMM\civlU{}WORLD);\\
~~\ccode{else~if}~(rank~==~1)\\
~~~~MPI\civlU{}Recv(\&dat,~1,~MPI\civlU{}INT,~0,~0,~MPI\civlU{}COMM\civlU{}WORLD,
MPI\civlU{}STATUS\civlU{}IGNORE);\\
~~MPI\civlU{}Finalize();\\
\rb\\
\end{program}
\caption{A simple C/MPI program. Process 0 sends and process 1
  receives a message. The remaining processes perform no operation.}
\label{fig:mpi:simple}
\end{figure}
\end{exmp}

\begin{enumerate}
  \item the \texttt{MPI\U{}Send} function (at line 7) sends the data,
  which is stored in \texttt{dat} and of the size of one
  \texttt{MPI\U{}INT}, to the process of rank 1 in the default communicator
  with a tag 0.
  
\item the \texttt{MPI\U{}Recv} function (at line 9) receives the
  message tagged by 0, in which the data is expected to be no larger
  than the size of one \texttt{MPI\U{}INT} and will be saved in
  \texttt{dat}, from the process of rank 0 in the default
  communicator.
\end{enumerate}

No communication action is performed by any other process. $\qed$

\section{Model Checkers for MPI} \label{sec:related:modelcheckers} 
%%%% Model checkers CIVL, ISP, DMAPI, ...
Many automated formal verification tools for MPI are based on model
checking \cite{clarke:2000:modelchecking}.  ISP
\cite{vakkalanka2008dynamic} and DAMPI
\cite{Vo:2010:SDD:1884643.1884681} are dynamic MPI model checkers.
They actually execute the MPI program being verified but exhaustively
rearrange different schedules so that eventually all possible
schedules will be covered.  These schedules differ in the matches of
MPI send and receive operations, as well as the choices made at a
nondeterministic point (e.g. wildcard receive or
\texttt{MPI\U{}Test}).
ISP and DAMPI support a wide range of MPI
primitives, including blocking and non-blocking point-to-point
communications as well as collective communications.  They are able to
check deadlock freedom and other safety properties for MPI programs.

The advantage of such dynamic model checking approaches is that each
schedule can be explored almost as fast as running the parallel
program in a sequential way.  Nevertheless, these model checkers can
only verify a program for a single concrete setting at a time, i.e.,
both the number of processes and the program inputs have to be
concrete.


The model checking technique can be combined with symbolic execution
\cite{king:1976:symbolic}.  With symbolic execution, a model checker
can verify an MPI program for arbitrary program inputs.
MPI-SV\cite{Yu:2018:CSE:3183440.3190336} uses a symbolic execution
engine to explore paths of an MPI program by letting processes execute
in a \emph{round-robin} manner.  These paths cover all possible
choices that processes can make at different branches while contain a
small amount of interleavings of processes.  Once a violation-free
path is explored, a \emph{Communicating Sequential Processes} (CSP)
\cite{Hoare:1985:CSP:3921} model will be generated from the path.  The
model is then fed to a CSP model checker, which explores all
alternative interleavings and nondeterministic choices that could be
made along the path.  MPI-SV verifies MPI programs for deadlock
freedom and user-customized properties expressed in temporal logic.

MOPPER \cite{Forejt:2017:PPA:3133234.3095075} and HERMES
\cite{khanna2018dynamic} are similar to MPI-SV.  They generate SAT
formulas from an execution of an MPI program.  The SAT formulas encode
the deadlock freedom problem.  If all the SAT formulas are proved
valid, the corresponding path is free of deadlock regardless of the
possible interleavings or MPI communication matches that can happen
along that path.

MOPPER generates SAT formulas from only one execution so it does not
guarantee to cover all possible paths.  It means that MOPPER cannot
deal with multi-path programs.  A multi-path MPI program contains
branches that depend on program inputs or wildcard receives.  For a
multi-path MPI program, two different runs may result in different
paths.

HERMES generates SAT formulas for all the paths that are explored by a
symbolic execution engine hence it is sound for multi-path programs.

MPI-SV, MOPPER and HERMES leverage the symbolic execution technique to
cover all possible choices that processes can make at different
branches.  But none of them utilizes symbolic execution for verifying
functional correctness of MPI programs.

Other tools such as MPI-Spin\cite{siegel2007verifying}, TASS
\cite{siegel2011tass}, and CIVL \cite{Luo:2017:VMP:3127024.3127032}
combine model checking and symbolic execution by having symbolic
expressions as values in states.  In addition, a path condition is
associated to each state, which is a boolean symbolic expression.  The
model checker ignores a state if its path condition is unsatisfiable.
Automated theorem provers are used to reason about the symbolic
expressions.  MPI-Spin provides libraries in the \emph{Promela}
language for MPI primitives and symbolic operations.  To use MPI-Spin,
the user needs to write a model for an MPI program in Promela with the
provided libraries.  Properties of the program can be customized in
temporal logic.  The model is eventually checked by the Spin model
checker \cite{holzmann1997spin}.

CIVL uses an intermediate verification language, CIVL-C, to model
various concurrency APIs, including MPI.  MPI programs are
automatically translated to CIVL-C programs and then sent to a CIVL-C
verifier.  TASS is the predecessor of CIVL.

The Spin model checker has been highly optimized to the Promela
language.  So for an MPI program, MPI-Spin is able to explore many
more states than CIVL within the same amount of time.  There is less
chance for the CIVL verifier to be optimized for a specific
concurrency API due to its generality to multiple such APIs.
Although CIVL cannot run as fast as MPI-Spin, CIVL outperformed
MPI-Spin in same cases \cite{Luo:2017:VMP:3127024.3127032} due to
CIVL's effective POR algorithm.  Moreover, CIVL can deal with programs
using not only different concurrency APIs but also the combinations of
them.

Because of the use of symbolic expressions, program inputs can be as
general as unconstrained symbols, and program outputs are consequently
expressions over those symbols.  By asserting on the outputs,
functional correctness of programs can be verified.  One disadvantage
of such an approach is that operations on symbolic expressions are more
expensive than operations on concrete values.

A common challenge that model checkers confront is state explosion.
Typically, the number of states in the state space of a program grows
exponentially with the number of processes.  In addition, model
checkers require the state space to be finite.  So the number of
processes as well as some of the program inputs have to be bounded.
Model checking based tools for monolithic verification usually cannot
be scaled to verify large codebases with realistic configurations.
Therefore, we propose a composite and modular approach in this
dissertation.  One of the motivations of our approach is to divide the
verification problem of an MPI program into a number of smaller and
independent sub-problems.



\section{Static Analysis and Runtime Verification for
  MPI} \label{sec:related:staticanalyzer}
\subsection{MPI Static Analyzers}
%%%% Static analysis: MPI-Checker, pCFG, MPI-IXFG, PARCOACH
Compared to model checkers, static analysis tools reason about
programs for arbitrary inputs and usually have better scalability.  A
common limitation to static analysis approaches is that the analyzed
result is not always exact because of lack of dynamic information.
Moreover, static analysis tool developers often face the tradeoff
between precision and efficiency.

MPI-Checker \cite{Droste:2015:MSA:2833157.2833159} is a static
analyzer for MPI programs that was built on the Clang Static Analysis
\cite{clangstaticanalyzer} framework.  It can check various
MPI-specific errors with a close to zero false positive rate, such as
deadlock caused by communication mismatch, invalid type of arguments
to MPI calls and incorrect message buffer referencing.  The analysis
is performed on an \emph{Abstract Syntax Tree} (AST) of an MPI
program.  MPI-Checker was applied to MPI applications, some of which
have tens of thousands of lines of code.

In addition to the AST, the \emph{Control-Flow Graph} (CFG) is a
typical abstraction of a program where static analyzers perform
\emph{data-flow analysis}.  In \cite{christakis:2011:detection}, the
authors propose an analysis approach on CFG for Erlang
\cite{armstrong:2013:programming} message-passing programs.  The
message-passing model in Erlang is very similar to the conceptual
model of MPI used in this dissertation.  Analysis is performed on a
\emph{communication graph}, where a vertex is the CFG of a function
that may be run by a separate process at runtime, and a directed edge
corresponds to a message channel for the two connected processes.
This analyzer is able to detect message-passing related errors such as
deadlock caused by a receive without a matching send, or potential
deadlock caused by a send without a matching receive.  The analysis is
approximated, i.e., neither the detection of all deadlocks nor the
freedom of false alarms can be guaranteed.

The concept of CFG has been extended for representing concurrent
programs.  The PARCOACH \cite{huchant2019multivalued} static analyzer
relies on Parallel Program Control Flow Graphs to detect
\emph{collective errors} of parallel programs using concurrency APIs
such as MPI.  A collective error in MPI programs is a mismatch of MPI
collective functions.  PARCOACH is efficient in analyzing large HPC
applications but may produce false positives and false negatives.  To
avoid false positives or false negatives, studies
\cite{Bronevetsky:2009:CSD:1545006.1545049,
  Strout:2006:DAM:1156433.1157634} have been made toward improving the
precision of static analysis for message-passing via extending CFGs.

Authors of \cite{ye:2018:detecting} combines the static analysis and
symbolic execution approaches for detecting \emph{anomalies}
\cite{board:1993:ieee}.  An anomaly is a suspicious code that does not
meet the expected coding style.  Most anomalies are true program
defects.  Other cases include coding-style violations or inelegant
code.  For MPI programs, anomalies can reveal true MPI defects
including deadlock caused by communication call mismatch, message
buffer type mismatch and simultaneous accesses to a same message
buffer.  This approach first performs static analysis to a whole MPI
program and collects MPI-related control flow information.  Then,
symbolic execution is only performed to program segments specified by
users.  The biggest advantage of this approach is that the
\emph{partially} applied symbolic execution largely increases the
precision of the analysis while mitigating the \emph{path explosion
  problem}.  Another advantage is that the symbolic execution task on
each code segment is independent hence there is a potential to
parallelize these tasks.  One disadvantage of this approach is that an
anomaly is not equivalent to a defect so that false alarms will be
reported.

In general, static analyzers may report both false positives and false
negatives.  Most of the static analyzers detect a set of pre-defined
errors but cannot check the functional correctness of programs.

Many static analysis approaches are not monolithic.  For example,
\cite{ye:2018:detecting} applies symbolic execution to program
segments instead of a whole program.  Our composite and modular
verification approach performs model checking and symbolic execution
to program segments as well.  Unlike \cite{ye:2018:detecting}, our
approach does not include a static analysis prephase, hence we have to
assume a weaker condition at the beginning of every symbolic
execution, compared to \cite{ye:2018:detecting}.  For example, we
assume that a pointer value can be arbitrary while
\cite{ye:2018:detecting} has a concrete set of candidate pointers.  We
will explore the possibility of combining static analysis with our
approach in the future.

\subsection{MPI Runtime Verification}
%%%% Runtime
There are runtime verification tools, such as Marmot
\cite{krammer2004marmot} and its successor MUST
\cite{Hilbrich:2012:MRE:2388996.2389037}.  MUST intercepts MPI calls
during the execution of an MPI program and collects the state of MPI
communication operations.  After the execution, the tool studies the
\emph{wait-for} dependencies among processes and determines if
MPI-related errors, such as deadlock or message type mismatch, can
happen in alternative executions.  Compared to the actually observed
execution, alternative executions may have different interleavings,
different matches for MPI wildcard receives or different results
returned from \texttt{MPI\U{}Test}.  Runtime verification tools, such
as MUST, are generally more scalable than static analysis based tools.
Besides, this kind of tools benefit from dynamic information, so it
does not report a false alarm.  However, based on the observed runtime
executions, there is no guarantee that all analyzed alternative
executions are complete.  Therefore, a runtime verification tool may
miss a defect if the defect is not revealed in the executions to which
it is applied.

Runtime verifiers are efficient in catching a large number of program
defects but may miss corner cases.  Besides, they cannot verify the
functional correctness of a program.

\section{Deductive Verification for MPI} \label{sec:related:deductive}
The related work described in previous sections all have a certain
degree of automation: no human effort is required during the
verification and little knowledge about verification is needed.  On
the other hand, these approaches face limitations.  First, they have
to balance between precision and scalability.  In addition, these
approaches verify programs only against a set of pre-defined
properties (e.g., deadlock or runtime error freedom).  Some tools
accept customized assertions or temporal logic formulas.  But in
general, verification against a user-defined specification is not well
supported.

%%%% Type-based verification, ParTypes, Future-based, Frama-C
In contrast, deductive verification approaches can formally verify the
conformance of a program to a specification for arbitrary program
inputs.  The user is responsible for providing a specification and
usually is required to interact with the verification tools to guide
the verification.


\partypes{} \cite{Lopez:2015:PVM:2814270.2814302} verifies an MPI
program with a \emph{protocol}.  A protocol consists of vectors of
\emph{term types}.  A subset of MPI operations, such as standard send
and receive functions and collective functions, can be represented by
term types.  \emph{Well-formed} term types are deadlock-free.  Whether
a protocol is well-formed is decidable and will be proved by SMT
solvers.

VCC \cite{cohen-etal:2009:vcc} is the underlying theorem prover used
by \partypes{}.  To verify the conformance of an MPI program to a
protocol, \partypes{} translates the protocol to VCC contracts and
then feeds both the program and the contracts to the VCC verifier.  In
addition to a protocol, the user needs to annotate branches in the
program to inform the verifier about the control flow.

\partypes{}'s protocol language cannot express the functional
correctness of a program.  Furthermore, \partypes{} cannot deal with
\texttt{MPI\U{}ANY\U{}SOURCE}.  The subset of MPI supported in
\partypes{} is deterministic, i.e., given the same inputs, the way
that the send and receive operations are matched is always the same.
In this dissertation, we will show that our approach becomes much more
efficient if we assume that an MPI program is free of wildcard
receives.

In \cite{oortwijn2016future}, Oortwijn et al.\ present their work for
specifying and verifying MPI programs modularly.  They use process
algebra \cite{bergstra2001handbook} terms, which are named
\emph{futures}, to model MPI operations.  The user can use futures to
``predict'' (or specify) the communication behavior of each procedure
in an MPI program for arbitrary inputs.  Whether a procedure conforms
to its futures is proved by Hoare style reasoning.  The global
communication correctness is carried out by a model checker in the
mCRL2 \cite{Cranen:2013:OMT:2450387.2450410} tool set, which reasons
about all the futures for an arbitrary number of processes.  The current
state of this work is preliminary: only a limited set of MPI
primitives are supported, including standard send and receive
operations and a few collective operations.  Receiving from ``any''
source is supported.

Compared to this ``future-based'' contracts, our approach attempts to
minimize the communication details involved in contracts and
encourages the user to pay more attention on expressing the functional
correctness properties.

A different preliminary work for message-passing deductive
verification is done by Luo et al.\ \cite{luo2018towards}.  The
authors verify a simple message-passing program with contracts and a
global invariant.  The approach used in this work was originally
proposed by Ashcroft in \cite{Ashcroft:1975:PAP:1739967.1740302}.  The
verification is complete, i.e., both termination and functional
correctness of the program is proved for arbitrary inputs and number
of processes.  The cost of such completeness is a significant amount
of user effort.  The user has to provide a global invariant, function
contracts, and loop invariants to the program.  Figuring out a proper
global invariant is hard.  The deductive reasoning, which shows the
global invariant is preserved by every program statement, is done by
Frama-C/WP.  Although the tool is automated, authors spent much time
in manually guiding the proof with intermediate assertions.

Being different from Frama-C/WP, which is based on VCG techniques, our
approach uses model checking and symbolic execution, hence it has a
higher degree of automation: contracts on functions and loops are
optional.  For the code that has no contract, it will just be simply
executed.


