\section{Related Work} \label{sec:related}
This dissertation is closely related to the existing verification work
of MPI programs.

%%%% Model checkers CIVL, ISP, DMAPI, ...
Many automated formal verification tools for MPI are based on model
checking.  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 from the
matches that the MPI wildcard receive operations can make.  ISP and
DAMPI are able to check deadlock freedom or free of assertion
violation.

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, dynamic model checkers can
only verify MPI programs for a concrete setting, 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.
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 different paths of an MPI
program.  Once a violation-free path is explored, a
\emph{Communication Sequential Process} (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 possible
interleaves 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 executed path is deadlock free regardless of the possible
interleaves or MPI communication matches that can happen along itself.
MOPPER cannot deal with multi-path programs.  A multi-path program
contains branches that depend on program inputs.  It means that
multiple runs of the same program with different inputs may have
different paths.  MOPPER generates SAT formulas from only one
execution so it does not guarantee to cover all possible paths.
HERMES generates SAT formulas for all the paths that are explored by
symbolic execution hence it is sound for multi-path 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 much
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 general representation for multiple such
APIs.  Although CIVL can hardly run as fast as MPI-Spin, it can deal
with programs using not only different concurrency APIs but also the
combinations of them.


A common challenge that these 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.  Therefore, model checking based tools for monolithic
verification cannot be scaled to verify large codebases with realistic
configurations.

%%%% 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.


%% and \cite{christakis:2011:detection} for Erlang
%% and PPCFG\cite{huchant2019multivalued} detect deadlock caused by
%% collective mis-order. Anomaly \cite{ye:2018:detecting} detection

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
point-to-point 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, of which the code size is
as large as tens of thousands of lines.

Besides 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:2007:erlang} message-passing programs.  The
message-passing model in Erlang is very similar to the conceptual
model of MPI used in this dissertation.  The analyzer corresponds CFGs
of functions to a \emph{communication graph}, where a vertex is a
process and a directed edge corresponds to a message channel for the
two connected processes.  It is able to detect errors such as deadlock
caused by a receive without a matching send or a potential deadlock
caused by a send without a matching receive. The analysis is
approximated.


To represent message-passing concurrent
programs, extensions (e.g.,
pCFG\cite{Bronevetsky:2009:CSD:1545006.1545049},
MPI-ICFG\cite{Strout:2006:DAM:1156433.1157634},
PPCFG\cite{huchant2019multivalued}) are made to CFG.


\cite{christakis:2011:detection} for Erlang
Anomaly \cite{ye:2018:detecting} detection
PPCFG\cite{huchant2019multivalued} detect deadlock caused by
collective mis-order.  Soundness is not guaranteed for all cases.

%% disadvantage:
Without dynamic
information, static analysis is approximate.  So these tools may
produce false alarms and may not claim the soundness.

%%%% Runtime
There are runtime verification tools, such as Marmot
\cite{krammer2004marmot} and its successor MUST
\cite{Hilbrich:2012:MRE:2388996.2389037}.  They detect MPI errors by
taking the use of runtime information.  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
deadlock can happen in alternative executions.  MUST do not report
false alarm but its error checking depends on runtime executions.


All the related work described so far falls into the category of
automated approaches.  A common feature of the work under this
category is that automated tools require little effort from users and
usually verify (resp.\ detect) a set of pre-defined properties (resp.\
errors).  Some tools accept customized assertions or temporal logic
formulas.  But in general, verification against a specification is not
well supported by the automated tools.

%%%% Type-based verification, ParTypes, Future-based, Frama-C
In contrast to automated approaches, deductive verification approaches
can formally verify that if a program satisfies a specification but
require the user to provide the specification.  The specification is
usually written in a formal language so that it can be understood by
the verification tools.

\partypes{} \cite{Lopez:2015:PVM:2814270.2814302} verifies an MPI
program with a \emph{protocol}.  The protocol language ensures that a
\emph{well-formed} protocol defines a \emph{mismatch-free}
communication behavior.  Hence if an MPI program conforms to a
well-formed protocol, the program is guaranteed to be deadlock free for
arbitrary inputs and number of processes.  The satisfaction of the
program to the protocol is eventually checked by the VCC
\cite{cohen-etal:2009:vcc} verifier.  However, the protocol language
cannot express the functional correctness of a program.  Furthermore,
\partypes{} cannot deal with the wildcard receive operation.  The
matches of the MPI communication operations supported by \partypes{}
in an MPI program are deterministic.

In \cite{oortwijn2016future}, Oortwijn et al.\ present their
preliminary 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.  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 a fixed number of processes with process algebra.

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 function
contracts and a global invariant.  The global invariant is strong
enough to imply both functional and communication correctness of the
program.  The deductive reasoning is done automatically by Frama-C.
It shows that the global invariant is preserved at any interleaving
point of the program.







