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