\section{Motivation} Message-passing is used pervasively in high-performance computing (HPC). This is expected to continue for the foreseeable future. For example, a recent survey found that 93\% of the applications being developed under the U.S.\ Department of Energy's Exascale Computing Project are currently using or plan to use the Message Passing Interface \cite{bernholdt-etal:2018:mpi_exascale}.\footnote{Table 4, Question 20, ``Do you expect the exascale version of your program to use MPI?''. Based on the 77 projects which responded to the survey, out of a total of 97 active projects. For the reported result, ``application'' includes application and software technology projects.} %(MPI, \cite{mpi-forum:2015:mpi31}) These applications are run on the world's most powerful supercomputers---machines which are extremely expensive to build, operate, and maintain. Time on these machines is very valuable, and the machines consume an enormous amount of energy. Time spent debugging at scale, or re-running programs after a defect was discovered at scale, wastes these resources. Moreover, HPC projects deal with issues of fundamental importance to science, engineering, and society more generally. They include applications to predict earthquake damage \cite{johansen:2017:earthquake}, model the global climate \cite{drake:2005:overview}, perform atomic-level simulations of chemical and biological systems \cite{valiev:2010:nwchem}, and to investigate the electronic structure of molecules \cite{mathuriya:2017:embracingquantum}, among many others. These programs inform both profound scientific conclusions and decisions of the utmost importance to society. For all of these reasons, it is imperative to develop effective methods for verifying correctness of message-passing HPC programs. Indeed, there is a growing consensus in the HPC community that better methods are needed to verify the correctness of HPC applications \cite{gopalakrishnan-etal:2017:correctness}. % you can cite many more things here about the correctness crisis % (DOI: 10.1109/MCSE.2017.3421558) ... %% various meanings of correctness There are many aspects to the correctness of a program. A programming language, such as C, imposes certain \emph{generic} correctness requirements that apply to all programs in that language. For example, any correct C program should not use an array index that lies outside the bounds of the array, dereference a null pointer, or invoke \texttt{free} on a pointer that was not returned by an earlier call to \texttt{malloc}. The use of concurrency APIs, such as MPI, imposes further generic requirements; for example, a correct MPI program should not deadlock, or have processes in a communicator invoke collective operations in different orders. While the work of this dissertation does apply to these generic properties, the focus is more on \emph{program-specific} correctness properties. These properties assert that a program---or an individual procedure within a program---should behave in the intended way, and should compute what the developer expects. By their very nature, program-specific properties require the developer to \emph{specify} intended behavior. While there are many different approaches to specifying programs, one of the most influential is the \emph{code contract}. This approach was introduced by Bertrand Meyer \cite{Meyer:1992:ADC} and realized in the Eiffel programming language \cite{Meyer:1988:eiffel}, and has since spread to many contexts. Larch \cite{vandevoorde:1994:specializedprocedures} was one of the early specification languages and was applicable to multiple programming languages, the Java Model Langauge \cite{leavens:1999:jml} was developed to specify Java programs and has been extremely influential, Spark \cite{spark} is a highly successful specification language for Ada \cite{ada2012}, and ACSL \cite{ACSL:Reference} is a specification language for C that is used with the Frama-C analysis platform. The most fundamental kind of code contract is the \emph{procedure contract}. A procedure contract consists primarily of a pair of \emph{pre-} and \emph{post-conditions}. These conditions specify a relation between the input and the output of the procedure. The contract asserts that \emph{if} the pre-condition holds when the procedure is called, \emph{then} the post-condition will hold when the procedure returns. This fundamental semantic idea originated in Hoare logic \cite{hoare:1969:axiomatic}, but is extended in several ways to deal with procedure calls, side effects, and other complexities that arise in real programming languages. The contract approach enables modular and composite verification of programs. For every procedure in a program, one verifies whether it satisfies its contract under the assumption that all other procedures satisfy their contracts. By doing so, the verification problem is decomposed into a number of smaller and independent sub-problems. This sort of decomposition, or something like it, is the only way that verification has any chance of scaling to software of the considerable size and complexity seen in modern HPC. There are many different ways to ``verify'' that a procedure satisfies its contracts. These include the automatic insertion of assertions for runtime checks, and automatic generation of test cases. Such approaches cannot verify with certainty, but only provide varying degrees of evidence for the likelihood that a contract holds. The most rigorous approach to contract verification is \emph{deductive reasoning}, which works by generating verification conditions that are individual theorems, which, if proved, imply a contract holds. Advances in automated theorem proving have eliminated much of the human effort previously required to discharge the proof obligations, but even the best tools still require significant manual guidance in the form of invariants, lemmas, and various ``hints'' for the theorem provers. This methodology has been realized in many contract verification tools, e.g., \cite{barnett:2006:boogie,gordon:1989:mechanizing,leino:1999:checkingjava, dannenberg:1982:formal, cuoq:2011:wp, filliatre:2013:why3, leino:2010:dafny, ball:2010:towards, barnett:2005:specsharp, beckert:2007:KeY}. A common point of the majority of these tools is that they are only suitable for sequential programs. There has been some work extending the ideas for shared-memory concurrent programs (e.g., \cite{cohen-etal:2009:vcc, blom:2017:vercors, amani:2017:complex}), but almost nothing for message-passing parallelism. In fact, it is not obvious that procedure contracts are suitable for reasoning about message-passing programs. First, in a message-passing parallel program, the behavior of a procedure depends not only on its inputs but also on the behaviors of other processes that run in parallel. Second, there is not a clear notion of pre- or post-state because processes can enter and exit a given procedure at different times. Nevertheless, the need to ``divide and conquer'' the verification task is as evident for message-passing programs as it is for sequential programs. \section{Contributions} \subsection{A contract theory for message-passing programs} The first contribution of this dissertation is to cope with the problems above by developing a \emph{theory of contracts} for message-passing programs. The basic idea of this theory is to use a contract to specify the collective behavior of a procedure that is executed by all processes collectively. We call such procedures the \emph{collective-style procedures}. This theory is applicable to programs containing non-collective-style procedures, it simply does not provide a way to decompose the specification/verification task for such procedures. In other words, if a collective-style procedure $f$ calls some non-collective-style procedure $g$, then $f$ and $g$ will be specified and verified as a unit: the user will write a contract for $f$ (but not write one for $g$) and the verification of $f$'s contract will require the definitions of both $f$ and $g$. Obviously, this approach is only useful to the extent that there are many collective-style procedures in real message-passing programs. We contend that such procedures are ubiquitous. For starters, all of the official MPI collective functions are collective-style, and the MPI collectives are widely used. As the ECP teams responded in \cite{bernholdt-etal:2018:mpi_exascale}, 80\% of them use MPI collective functions in their current applications and this percentage increases to 82\% for exascale version of their applications. Furthermore, we have examined source code in two large, state-of-the-art MPI applications: the Monte Carlo particle transport code OpenMC \cite{romano-etal:2015:openmc}, and a module (\texttt{parcsr\U{}ls}) in the algebraic multigrid solver AMG \cite{yang-etal:2017:amg}. OpenMC consists of over 24 thousand lines of C++ code, and the AMG module is over 35 thousand lines of C code. Through a combination of static analysis and manual inspection, we confirmed that every function in these codes either involves no MPI communication (in which case the usual sequential contract techniques can be applied) or is collective-style. % For OpenMC, we confirmed that every direct call to an MPI % communication function belongs to a collective-style function. For % the part of code in AMG, we confirmed that every direct call to MPI % point-to-point communication functions belongs to a collective-style % function. \subsection{A method for verifying collective contracts} The second contribution of this dissertation is a method for automatically verifying that a collective-style function satisfies its contract. As explained above, deductive reasoning is typically used for this sort of verification in the case of sequential programs. The main advantage of deductive reasoning is that it can perform \emph{complete verification} for an arbitrary configuration of a program. But it costs the user's effort in specifying every single function and loop in the program with a contract and a \emph{loop invariant}, respectively, and possibly additional annotations specifying theories, lemmas, and so on. % Finding appropriate loop % invariants is a notoriously difficult process. Instead of deductive reasoning, our method is based on model checking \cite{clarke:2000:modelchecking} and symbolic execution \cite{king:1976:symbolic}. The main advantage of this method is that it requires no invariants or annotations beyond the procedure contracts, and given those it is completely automated. Furthermore, in order to verify that a procedure $f$ satisfies its contract, it is not necessary to have contracts for all procedures called by $f$. The called procedures without contracts will effectively be executed when verifying $f$. This enables a very incremental approach to the specification and verification work. The cost is that our method performs \emph{bounded verification}---it requires small bounds to be placed on the number of processes, and possibly on other parameters. If the verification succeeds, it is theoretically possible that a contract could be violated with a larger number of processes. The effectiveness of this approach relies on the \emph{Small Scope Hypothesis} \cite{Jackson:2006:SAL}, which posits that almost all defects can be found by exhaustively exploring all possible behaviors in all small configurations of a system. Both the contract theory and the verification method will be formulated in this dissertation using a ``toy'' message-passing language, which we call MiniMP. Using a simple language with a mathematically precise semantics is the best way to elucidate the essential ideas, and also allows us to state and prove precise statements about the soundness of the verification method. % Considering the fact that the MPI standard in real world contains too % much complexity, e.g., multiple communicators, various data types and % C void pointers, the simplicity of MiniMP allows us to illustrate the % ideas and prove their soundness with mathematical precisions. \subsection{An MPI Specification Language} The simple MiniMP language leaves out many of the ``accidental'' complexities of C and MPI. These includes pointers and pointer arithmetic, specifying buffers through \code{void*} pointers and byte-counts, use of multiple communicators, representing types and reduction operations as values, and so on. A practical specification language for message-passing programs must deal with all these issues. As the third contribution of this dissertation, we present such a specification language for C/MPI programs. The language extends the existing ACSL language for sequential C. It adds new ``MPI-aware'' primitives which realize many of the central concepts that arise informally in the MPI Standard. These include the notion of a \emph{region} of memory specified by a \code{void*} pointer and size (i.e., a buffer); a predicate for asserting that two buffers contain the same typed values; predicates that compare memory across different processes, and so on. The contract system supports a significant subset of MPI, including standard mode blocking point-to-point communication, the wildcards \texttt{MPI\U{}ANY\U{}SOURCE} and \texttt{MPI\U{}ANY\U{}TAG}, all blocking collective communication, all kinds of pre-defined MPI data types and operations, and multiple communicators. We believe this new specification language has significant practical potential, even without a corresponding verification tool. For example, it could be used to make formally precise the semantics of the MPI collective functions, which are currently described using only natural language in the MPI Standard. It could also be used by programmers simply to document the intended behavior of their code. The language is sufficiently intuitive and readable that it can be easily understood by programmers who are not experts in formal verification. \subsection{A Prototype MPI Contract-Based Verification Tool} The fourth contribution of this dissertation is an actual verification tool for C/MPI programs specified using the language described above. The prototype tool implements the theoretical verification approach, based on model checking and symbolic execution, described in Section \ref{fillmein}. The tool was developed using a general verification framework, CIVL \cite{siegel-etal:2015:civl_sc}. The framework is based on an intermediate verification language, CIVL-C, which provides a small set of generic concurrency primitives on top of standard C. We have added an automatic transformer which consumes a C/MPI program with contracts and produces a CIVL-C program. The CIVL-C program contains assertions and assumptions, in such a way that if all assertions hold on all executions, then the original contract must hold. This prototype implementation was evaluated with a number of simple C/MPI programs, including MPI collective implementations used by CIVL itself, advanced MPI collective algorithms and typical MPI computational applications. \begin{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% A program is considered \emph{reliable}, if it always behave as expected. The expectation to a program is called the \emph{specification} of the program. A program is reliable if it \emph{satisfies} its specification. A specification describes the \emph{properties} of a program without ambiguity. For example, a common property for message-passing parallel programs is deadlock freedom; free of invalid pointer dereferencing is a common C program property. %% hard to debug and test, verification approaches are more effective: The behaviors of a message-passing programs is asynchronous and nondeterministic, so traditional software testing methods can hardly cover all possible behaviors of a message-passing program \cite{Pervez:2010:FMA:1712067.1712069, godefroid2008concurrency}. The research work in recent decades \cite{vakkalanka2008dynamic, Yu:2018:CSE:3183440.3190336, khanna2018dynamic, siegel2011tass, Luo:2017:VMP:3127024.3127032, Strout:2006:DAM:1156433.1157634} shows that static analysis and formal verification approaches are effective in finding bugs in message-passing concurrent systems. These approaches can roughly be divided into two kinds: \emph{automated} and \emph{deductive}. Automated analysis and verification approaches require little effort from the user side and is able to check a set of pre-defined \emph{standard} properties for a message-passing program. For example, the ISP \cite{vakkalanka2008dynamic} model checker, which uses the model checking \cite{Clarke:2000:MC:332656} technique, takes a message-passing program as an input and verifies whether the program is free of deadlock or assertion violation. Message-passing applications usually have large codebases, hence automated approaches are attractive to developers. In contrast, deductive verification approaches \cite{luo2018towards, Lopez:2015:PVM:2814270.2814302, oortwijn2016future} require the user to provide a specification for the verifying program. The specification usually is written in a specific programming language so that it can be understood by computers. By writing a specification, the user is able to express rich and customized properties. A deductive verification tool performs parametric verification for a program against its specification in a composite and modular way. Both kinds of the verification approaches have their disadvantages. Automated approaches are mainly based on finite-state searching or static analysis techniques. The former technique requires the program parameters to be bounded in small scopes. The latter technique produces false positives. For deductive approaches, the human effort that needs to be made is not only excessive but also requiring expert knowledge. %% what does this dissertation do ? The main contribution of this dissertation is the attempt to combine these two kinds of approaches to verify message-passing programs. In summary, our approach is to divide a message-passing program into a set of \emph{collective-style} procedures. The division is done via assigning each collective-style procedure a specification. By verifying the satisfaction to the specification for each \emph{collective-style} procedure independently, the whole program is thus verified. The verification of each procedure is based on automated approaches. %% the advantage of the combinatorial approach ? Our approach has three main advantages. First, it enables composite and modular verification. Verifying each of the divided procedures is a much smaller problem than the verification of the whole program. During the verification of a single procedure, all other procedures will be assumed being verified and their verification results will be re-used. Second, instead of dividing a message-passing program into arbitrary procedures, the collective-style based division allows the user to pay more attention to the inputs and outputs of procedures than the interaction among processes. All the non-collective style procedures are automatically executed during the verification. Finally, encoding specifications in a programming language encourages the developers to document and be careful with their code. This approach is implemented in a general verification framework, CIVL \cite{siegel-etal:2015:civl_sc}. The implementation is evaluated with MPI programs. MPI, the Message-Passing Interface, is the \emph{de-facto} standard of message-passing programming in HPC. In order to specify properties for MPI programs, we extended and designed a \emph{contract language} for C/MPI programs from an existing specification language for sequential C programs. This language is another contribution of this dissertation. \end{comment} \section{Outline} The dissertation is composed of three parts. Part I includes chapters for preliminary information. Chapter \ref{chp:background-related} introduces background knowledge and related work. Chapter \ref{chp:notation} presents general notation that will be used throughout the document. In Part II, we describe a theory of message-passing contracts and their verification using the simple MiniMP language. The syntax and semantics of the language proper are formally described in Chapter \ref{chp:minimp}. In Chapter \ref{chp:minimp:spec}, we present a specification language for MiniMP and show how the correctness of a MiniMP program can be expressed using this specification language. Chapter \ref{chp:minimp:rules} presents an inference system, which consists of four rules, for reasoning about MiniMP programs with specifications. Chapter \ref{chp:minimp:system} presents a system based on that inference system for verifying MiniMP programs, using model checking and symbolic execution techniques. Part III focuses on bringing the theoretical approach to practice. Chapter \ref{chp:mpi:model} gives an overview of the CIVL framework, on which a contract system for verifying C/MPI programs will be built. In Chapter \ref{chp:mpi:system}, we introduce our \emph{MPI contract language} and the implementation of an C/MPI contract system. Chapter \ref{chp:mpi:eval} presents our evaluation of the contract language and system. It also includes a discussion of the experimental results. Finally, we conclude this dissertation in Chapter \ref{chp:conclusion}.