%\input{model_example} \section{CIVL: The Concurrency Intermediate Verification Language} \label{sec:civl} The CIVL verification framework consists of a front-end, an intermediate verification language CIVL-C and a back-end verifier for CIVL-C programs. Figure \ref{fig:civl:layout} shows the layout of the CIVL framework. CIVL is designed with idea that using CIVL-C to represent various concurrent programming languages and letting the back-end verifier focuses only on dealing with the CIVL-C language. The front-end automatically translates programs written in different concurrent programming languages to CIVL-C programs. The back-end verifier uses model checking and symbolic execution techniques for verifying CIVL-C programs. The reasoning of symbolic expressions is carried out by automated theorem provers \cite{barrett-etal:2011:cvc4, Z3Prover, filliatre:2013:why3}. \begin{figure} \begin{center} \includegraphics[scale=.7]{civl-framework} \end{center} \caption{The layout of the CIVL framework} \label{fig:civl:layout} \end{figure} The CIVL-C language is an extension of the sequential part of C11 \cite{iso:2011:c11} with a large number of primitives for concurrency and specification. In addition, CIVL-C allows nested function definitions, which plays an important role in representing different concurrency models. We list a selected set of CIVL-C primitives in Fig.\ \ref{fig:civlc:primitives}. Every CIVL-C primitive starts with a \texttt{\$} sign. Fig.\ \ref{fig:mpi:model:civlc} shows a simple CIVL-C example that utilizes these primitives. \begin{figure}[t] \begin{itemize} \item \texttt{\$proc:} a type representing a process \item \texttt{\$spawn \textit{stmt}:} spawns a new process to execute a statement and returns immediately a \texttt{\$proc} object representing the new process. \item \texttt{\$parfor (int \textit{i} :\ \textit{domain}) \textit{stmt}:} spawns a set of processes, each of which corresponds to an integer in an integral domain and executes the given statement, and waits until all processes terminate. \item \texttt{\$when (\textit{expr}) \textit{stmt}:} executes the given statement once the guard \textit{expr} evaluates to true; blocks the execution otherwise. \item \texttt{\$choose\U{}int (\textit{n}):} non-deterministically returns an integer in between 0 and \texttt{\textit{n}}-1. \item \texttt{\$input:} a type specifier that specifies a variable to be a program input, which is non-writable and will be initialized by an arbitrary value by default. \item \texttt{\$output:} a type specifier that specifies a variable to be a program output, which shall not be read by the original program but will be compared against a specification. \item \texttt{\$assume (\textit{expr}):} informs the verifier to ignore the current execution path unless \textit{expr} evaluates to true. \item \texttt{\$assert (\textit{expr}):} asserts that \textit{expr} evaluates to true. \end{itemize} \caption{A selected set of CIVL-C primitives} \label{fig:civlc:primitives} \end{figure} The program in Fig.\ \ref{fig:mpi:model:civlc} represents a hierarchical concurrency model. The \texttt{\$parfor} at line 20 spawns 5 ``processes'', each of which executes the \texttt{proc} function with a unique \texttt{pid}. Each ``process'' spawns 5 ``threads'' to read the \texttt{\$input} variable and \texttt{compute} in parallel (line 11). Each ``thread'' executes the \texttt{thread} function with a different \texttt{tid}. The \texttt{thread} function is defined inside the scope of the \texttt{proc} function so that ``process''-local variables \texttt{pid} and \texttt{result} are also visible to each ``thread'' (line 9). Every ``process'' sums up the results of its ``threads'' to a global variable \texttt{sum} that is shared by all processes. The access to \texttt{sum} is protected by a \texttt{lock}. Each ``process'' attempts to acquire the \texttt{lock} by waiting until it is 0. The evaluation of the \texttt{\$when} guard (i.e., \texttt{!lock}) and the execution of the first statement following \texttt{\$when} (i.e., \texttt{lock = 1}) is uninterruptible. The ``process'' eventually releases the \texttt{lock} by setting it back to 0. \begin{figure}[t] \begin{center} \begin{program} \$input \ccode{int} IN[5];\\\\ \ccode{int} compute(\ccode{int} x, \ccode{int} y) \lb{}\ ...\ \rb{}\\\\ \ccode{int} sum, lock = 0; \\ \ccode{void} proc(\ccode{int} pid) \lb{} \\ \ \ \ccode{int} result[5]; \\ \\ \ \ \ccode{void} thread(\ccode{int} tid) \lb{}result[tid] = compute(IN[pid], tid);\rb{}\\ \\ \ \ \$parfor (\ccode{int} i :\ 0\ ..\ 4) thread(i);\\ \ \ \$when (!lock) \lb{} \\ \ \ \ \ lock = 1; \\ \ \ \ \ \ccode{for} (\ccode{int} i = 0; i < 5; i++) sum += result[i];\\ \ \ \ \ lock = 0;\\ \ \ \rb{} \ \ ...\ \\ \rb{}\\ \\ \ccode{int} main() \lb{} \\ \ \ \$parfor(\ccode{int} i :\ 0\ ..\ 4) proc(i); \\ \ \ \$assert (sum == ...\ );\\ \rb{}\\ \end{program} \end{center} \caption{A CIVL-C representation of a hierarchical concurrency memory model.} \label{fig:mpi:model:civlc} \end{figure} Finally, the \texttt{\$assert} statement (line 21) checks for the correctness of the computation. In CIVL-C, first order logic quantifiers, \texttt{\${}forall} and \texttt{\${}exists}, can be used in the boolean expressions in \texttt{\$assert} or \texttt{\$assume} primitives. \section{Modeling MPI with Transformation and Libraries} \label{sec:civl:mpi-support} The support of MPI in CIVL is a combination of 1) customized MPI library implementation written in CIVL-C; and 2) a code transformer that takes in C/MPI programs and outputs pure CIVL-C programs. \subsection{The MPI Library} CIVL's MPI library implementation covers a subset of the MPI constructs, including standard point-to-point communication functions, all blocking collective functions and other constructs such as \texttt{MPI\U{}Comm\U{}dup} and \texttt{MPI\U{}Init\U{}thread}. Every MPI construct was carefully modeled by CIVL-C code with the help of the core libraries in CIVL. The most important core library provided by CIVL for the MPI library is the \texttt{comm} library. It consists of a set of basic primitives for communication in a message-passing manner. Here we use the CIVL-C implementation of the \texttt{MPI\U{}Recv} function as an example to demonstrate how does CIVL model MPI. Fig.\ \ref{fig:mpi:model:MPI_Recv} presents CIVL's definition of \texttt{MPI\U{}Recv}, which is the standard point-to-point receive operation in MPI. \begin{figure} \begin{center} \begin{program} \ccode{int} \$mpi\U{}recv(\ccode{void} *buf, \ccode{int} count, MPI\U{}Datatype datatype, \ccode{int} src,\\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ccode{int} tag, MPI\U{}Comm comm, MPI\U{}Status *status) \lb{} \\ \ \ \textcolor{blue}{\$message} in;\\ \ \ \ccode{int} place = \ccommplace{}(comm.p2p); \\ \ \ \ccode{int} nprocs = \ccommsize{}(comm.p2p); \\ \\ \ \ \cassert{}((src >= 0 \&\& src < nprocs) || src == MPI\U{}ANY\U{}SOURCE, \\ \ \ \ \ \ \ \ \ \ \ "Illegal MPI message receive source \%{}d.\BSL{}n", src)\\ \ \ \cassert(tag == -2 || tag >= 0, \\ \ \ \ \ \ \ \ \ \ \ "Illegal MPI message receive tag \%{}d.\BSL{}n", tag); \\ \ \ \celaborate(src);\\ \ \ in = \ccommdequeue(comm.p2p, src, tag); \\ \\ \ \ \ccode{int} size = count*sizeofDatatype(datatype); \\ \\ \ \ \cmessageunpack(in, buf, size); \\ \ \ \ccode{if} (status != MPI\U{}STATUS\U{}IGNORE) \lb{}\\ \ \ \ \ status->size = \cmessagesize{}(in); \\ \ \ \ \ status->MPI\U{}SOURCE = \cmessagesource{}(in); \\ \ \ \ \ status->MPI\U{}TAG = \cmessagetag{}(in); \\ \ \ \ \ status->MPI\U{}ERROR = 0; \\ \ \ \rb{} \\ \ \ \ccode{return} 0; \\ \rb{}\\ \\ \ccode{int} MPI\U{}Recv(\ccode{void} *buf, \ccode{int} count, MPI\U{}Datatype datatype, \ccode{int} src, \\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ccode{int} tag, MPI\U{}Comm comm, MPI\U{}Status *status) \lb{} \\ \ \ \cassert(\U{}mpi\U{}state == \U{}MPI\U{}INIT, "MPI\U{}Recv() cannot be invoked " \\ \ \ \ \ "without MPI\U{}Init() being called before.\BSL{}n"); \\ \ \ \ccode{return} \$mpi\U{}recv(buf, count, datatype, src, tag, comm, status); \\ \rb{} \end{program} \end{center} \caption{The definition of \texttt{MPI\U{}Recv} in the MPI library in CIVL.} \label{fig:mpi:model:MPI_Recv} \end{figure} The function is defined at line 26--31. The argument \texttt{buf} points to a memory location where the received data will be saved when the function returns. The expected size of the message data is given by \texttt{count} and \texttt{datatype}. The argument \texttt{src} specifies the rank of the sender, \texttt{tag} specifies the message tag and \texttt{comm} specifies the MPI communicator. The \texttt{status} can be a pointer to a \texttt{MPI\U{}Status} object which will be filled after the function returns or a constant \texttt{MPI\U{}STATUS\U{}IGNORE} for opting out the returned information. In this function, the implementation first checks whether \texttt{MPI\U{}Init} has been called then calls \texttt{\$mpi\U{}recv} to deliver the main functionality. The \texttt{\$mpi\U{}recv} function is built upon the \texttt{comm} library: \begin{itemize} \item \texttt{\$comm:} a type representing a reference to a communication universe. A communication universe mainly consists of a group of $n$ processes and $n^2$ message channels. Each message channel is identified by an ordered pair $(i, j)$, $0 \leq i,j < n$, which means that the message channel buffers messages sent from process $i$ to $j$. An MPI communicator is implemented in CIVL as two communication universes, one for point-to-point communication and the other for collective communication. Therefore, the \texttt{MPI\U{}Comm} type is implemented as a structure including two \texttt{\$comm} fields, namely \texttt{p2p} and \texttt{col}, respectively. \item The pair of \texttt{\$comm\U{}place} and \texttt{\$comm\U{}size} functions are the ``getters'' that return the $\mymath{pid}$ of the running process and the size of the communication universe, respectively, through a \texttt{\$comm} reference. \item The function \texttt{\$comm\U{}dequeue(\$comm c, int src, int tag)} dequeues a message from the message channel of the communication universe referred by \texttt{c}. The message channel is identified by the ordered pair $(\mymath{pid}, \texttt{src})$, where $\mymath{pid}$ is the ID the process in the communication universe. The message is tagged by \texttt{tag}. If there is no message matching the \texttt{tag} in the given channel, this function blocks the execution. The value of \texttt{tag} can be a constant pre-defined in MPI library, \texttt{MPI\U{}ANY\U{}TAG}, which matches any message tag. \item Messages are represented by a \texttt{\$message} type. In addition to the data, a message includes meta information such as IDs of the sender and receiver, message tag and data size. \item A number of ``getter'' functions are provided for reading information from messages, e.g.\ \texttt{\$message\U{}unpack} reads the message data and \texttt{\$message\U{}source} reads the ID of the sender from a message. \end{itemize} With this infrastructure provided by the \texttt{comm} library, the \texttt{\$mpi\U{}recv} can be implemented with straightforward CIVL-C code as showed from line 1-24. To model the functionality of the MPI functions, CIVL's implementation uses simple algorithms. Recall that CIVL is a symbolic execution tool, so the values of variables are not necessarily concrete. But the \texttt{\$comm\U{}dequeue} function requires the \texttt{src} to be concrete. To solve this problem, the \texttt{\$elaborate(src)} statement was inserted at line 11 to inform the verifier to elaborate different concrete cases of the value of \texttt{src}. \subsection{AST-Level Code Transformation} In addition to the MPI library, CIVL applies an \emph{Abstract Syntax Tree} (AST) level code transformer to automatically convert an C/MPI program to an equivalent CIVL-C program. The transformation approach can be generalized as a template, showed in Fig.\ \ref{fig:sec:mpi:transform}. \begin{figure} \textbf{\textit{a generic MPI program:}}\\ \begin{program} \ccode{int} main(\ccode{int} argc, \ccode{char} * argv[]) \lb{} \\ \ \ \textcolor{red}{\textit{[body of} main \textit{function]}} \\ \rb{} \end{program} \hrulefill \textbf{\textit{the CIVL-C program after translation:}}\\ \begin{program} \cinput\ \inttype\ {\civlU}mpi{\civlU}nprocs; \\ \cinput\ \inttype\ {\civlU}mpi{\civlU}nprocs{\civlU}lo = 1,\ {\civlU}mpi{\civlU}nprocs{\civlU}hi,\ {\civlU}civl{\civlU}argc;\\ \cinput\ \cchar\ {\civlU}civl{\civlU}argv[{\civlU}civl{\civlU}argc][];\\ \cscope\ \civlU{}mpi\civlU{}root = \chere;\\ \cassume({\civlU}mpi{\civlU}nprocs{\civlU}lo <= {\civlU}mpi{\civlU}nprocs \&\& \\ \ \ \ \ \ \ \ \ {\civlU}mpi{\civlU}nprocs <= {\civlU}mpi{\civlU}nprocs{\civlU}hi);\\ % \cassume(0 < {\civlU}civl{\civlU}argc);\\ \cmpigcomm\ {\civlU}mpi{\civlU}gcomm{\civlU}world, {\civlU}mpi{\civlU}gcomms[]; \textcolor{red}{\emph{// global communicators:}}\\ \void\ {\civlU}mpi{\civlU}process(\inttype\ {\civlU}mpi{\civlU}rank)\ \lb\\ \ \ MPI\U{}Comm\ \MPICOMMWORLD \ =\ \cmpicommcreate(\chere, {\civlU}mpi{\civlU}gcomm,\\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\civlU}mpi{\civlU}rank);\\ \ \ \textcolor{red}{\textit{[more definitions of MPI functions]}}\\ \ \ \textcolor{red}{\textit{[insert original source code here, but rename main \civlU{}civl\civlU{}main]}}\\ \ \ {\civlU}civl{\civlU}main({\civlU}civl{\civlU}argc, \\ \ \ \ \ \ \ \ \ \ \ \ \ \ (\cchar\ *\ [{\civlU}civl{\civlU}argc])\clambda\ (\inttype\ i)\ {\civlU}civl{\civlU}argv[i]); \\ \ \ \cmpicommdestroy(\MPICOMMWORLD);\\ \rb\\ \inttype\ main()\ \lb \\ \ \ {\civlU}mpi{\civlU}gcomm{\civlU}world = \cmpigcommcreate(\civlU{}mpi\civlU{}root, \ {\civlU}mpi{\civlU}nprocs); \\ \ \ \cseqinit(\&{\civlU}mpi{\civlU}gcomms, 1, \&{\civlU}mpi{\civlU}gcomm{\civlU}world);\\ \ \ \cparfor\ (\inttype\ i:\ 0\ ..\ {\civlU}mpi{\civlU}nprocs - 1)\ {\civlU}mpi{\civlU}process(i);\\ \ \ \cmpigcommdestroy({\civlU}mpi{\civlU}gcomm{\civlU}world);\\ \rb \end{program} \caption{The general C/MPI to CIVL-C transformation template.} \label{fig:sec:mpi:transform} \end{figure} For an MPI program, every process runs a copy of it and has no shared storage. Recall that processes in CIVL-C are spawned with statements. And a variable is shared by two processes, if the variable is visible to the definitions of both the processes. One of the most notable changes made by the transformer is that the whole original program, as well as the inlined libraries, is wrapped by a function that will be executed by a process. By doing so, there is no variable in the original program that is shared by processes. In our template in Fig.\ \ref{fig:sec:mpi:transform}, the function is named \texttt{\U{}mpi\U{}process} (line 8-16) for the meaning of that it will be executed by every ``MPI process''. The original \texttt{main} function is renamed to \texttt{\U{}civl\U{}main} (line 13). The transformer creates a new \texttt{main} function that is responsible for creating a set of processes to execute the \texttt{\U{}mpi\U{}process}. Without affecting the message-passing concurrency model, the transformer creates a set of global variables, including \texttt{\$input}s and data structures representing the communication environment. The number of processes, as well as its bounds, are defined as \texttt{\$input} variables: \texttt{\U{}mpi\U{}nprocs}, \texttt{\U{}mpi\U{}nprocs\U{}lo} and \texttt{\U{}mpi\U{}nprocs\U{}hi}. Usually the user only needs to give a concrete value to the upper bound variable from the command line. The lower bound is by default one. The original program arguments are also transformed to \texttt{\$input} variables: \texttt{\U{}civl\U{}argv} and \texttt{\U{}civl\U{}argc}. Other than the \texttt{\$input} variables, MPI communicators are declared globally. The \texttt{\$mpi\U{}gcomm} type represents an MPI communicator. The \texttt{\U{}mpi\U{}gcomm\U{}world} variable represents the default communicator, which is referred by \texttt{MPI\U{}COMM\U{}WORLD}. In addition, there is a \emph{sequence} \texttt{\U{}mpi\U{}gcomms} that manages dynamically created communicators. A sequence is a CIVL-C primitive that performs as a dynamically re-sizable array. A sequence of $T$ type variable is declared as an incomplete array of $T$. A sequence must be initialized by \texttt{\$seq\U{}init} (e.g., line 19) before use. The creation of the default communicator is done by the new \texttt{main} function. Each process is responsible for creating its process-local \texttt{MPI\U{}Comm} reference to the default communicator. All these global variables are created by the transformer hence they are invisible to the original program. There is no direct access from the original code to any global variable. Indirect accesses to global data structures, such as buffering a sending message into a message channel, are all operated through specific handles. These handles guarantee that ``MPI processes'' cannot be aware of the existence of any global variable. \subsection{MPI Program Properties} \label{sec:civl:mpi:quality} We discuss about the quality of the MPI model in CIVL in terms of the properties of an original MPI program that are preserved by the transformed CIVL-C program. These properties include a wide range of standard C properties that CIVL can verify for an MPI program such as assertion violation, improper pointer dereferencing or out-of-bound array access, division by zero, memory leak, etc. One of the most common errors in MPI programs is deadlock. There are two kinds of deadlocks: \emph{absolute deadlock} and \emph{potential deadlock}. Absolute deadlocks are caused by the existence of unmatched send and receive operations. Potential deadlocks include absolute deadlocks. In addition, potential deadlocks also contain deadlocks caused by the short of message buffer. Potential deadlocks are hard to re-produce because buffer sizes can vary in different runs. CIVL can verify the freedom of both kinds of deadlocks. Other MPI specific properties that can be verified by CIVL include: the freedom of receive buffer overflow, incompatible message and receive types, inconsistency of collective calls. The functional correctness of an MPI program can be specified as either assertions or a separate sequential program, which is simple, trusted and functionally equivalent to the MPI program. For the latter manner, CIVL is able to check the functional equivalence between two programs, which is carried out by assuming the two programs have exact same inputs and verifying that they always produce the exact same outputs.