The function contract approach introduced in Part II for \minimp{} is
an instance of the ``divide and conquer'' methodology that has several
advantages over monolithic model checking approaches. First, it
divides a large problem into a number of smaller independent problems.
Since each smaller problem is much easier to be solved, there is a
potential that the ``divide and conquer'' approach can help mitigate
the state explosion problem.  Second, a function contract, which
serves as a specification of a function, enables the verifier to cover
the most general cases of the function with respect to the
specification.  Whereas whether a function can be throughly verified
by a monolithic approach depends on how is the function called in a
program.  Finally, writing function contracts encourage developers to
pay more attention to specifications and documents.

Based on the MPI model described in Chapter \ref{chp:mpi:model}, our
discussion in this chapter will focus on implementing a function
contract system for MPI in CIVL.  The rest of the chapter is
structured as follows: \S\ref{sec:mpi:minimp2mpi} discusses about the
challenges in applying the function contract approach to MPI programs
and sketches the solutions; \S\ref{sec:mpi:contract_language}
introduces the contract language for C/MPI programs;
\S\ref{sec:mpi:impl} describes a source code transformation based
implementation for the MPI contract system.

\section{Bring Function Contracts From \minimp{} To MPI} \label{sec:mpi:minimp2mpi}

In Part II, we have discussed about the contract approach for
message-passing programs around a toy language, \minimp{}.  Applying
the approach to C/MPI programs would face many new challenges because
of the complexity of both MPI and C.  In the rest of this section, we
briefly talk about these challenges and their solutions.

\textbf{Multi-Communication Universes.} A \minimp{} program only involves
a single communication universe that includes all the processes
launched at the beginning.  However, MPI programs can have multiple
communication universes.  A communicator conceptually contains two,
one for point-to-point and the other for collective communication.
Besides, communicators can be dynamically created.  A process can
participate in different communicators.  Different communicators can
have different sizes.  A collective-style function in an MPI program
may involve multiple communicators.  Hence \minimp{}'s specification
language cannot be proper for MPI since the constants \texttt{PID} and
\texttt{NPROCS} have different values in different communication universes.

Consequently, the reasoning of the contracts must be sensitive to
communication universes. For example, given two consecutive calls to
collective-style functions \texttt{$f$();$g$()}, a guarantee 
\begin{center}
\texttt{\acslguarantee{p}{q}{r}}
\end{center}
of $g$ does not make $g$ satisfy the requirement 
\begin{center}
\texttt{\acslgamma{p}{q}{r}}
\end{center}
of $f$, if the contracts are describing behaviors for two different
communication universes.

The challenge of multiple communication universes demands that
communications in different universes shall be reasoned independently.
Within a single universe, the theory for \minimp{} is still applicable to
MPI.

\textbf{Message Tags.} In MPI, messages in point-to-point
communication are always labeled with an integer tag.  When a process
sends or receives a message, it must specify a tag for the message.
When receiving a message, one can specify \texttt{MPI\U{}ANY\U{}TAG}
for the message tag.  A receive operation on a specific message
channel with \texttt{MPI\U{}ANY\U{}TAG} will get the earliest message
in it (i.e., the head of the FIFO queue).

The existence of the message tags makes the communication in MPI more
flexible while the reasoning of the communication more complicated.
The \minimp{} specification language has no notion for message tags hence
it cannot specify absence assertion precisely in many cases.

Therefore, to specify MPI programs, the absence assertions need to be
extended with message tags.


\begin{figure}
    \begin{program}
      \ccode{void} f() \lb{}\\
      \ \ \ccode{if} (rank == 0) \\
    \ \ \ \ \ccode{for} (\ccode{int} i = 1; i < size; i++) \\
    \ \ \ \ \ \ MPI\U{}Recv(\&buf, 1, MPI\U{}INT,
    MPI\U{}ANY\U{}SOURCE, 1, MPI\U{}COMM\U{}WORLD); \\
    \ \ \ccode{else} \\
    \ \ \ \ MPI\U{}Send(\&value, 1, MPI\U{}INT, 0, 1, MPI\U{}COMM\U{}WORLD);\\
    \rb\\
  \end{program}
  \caption{An MPI collective-style function that requires any
    following statement not to send any message with tag 1 to process
    0 until process 0 exits it.}
  \label{fig:mpi:exmp:tag}
\end{figure}

\begin{exmp}
  Considering the collective-style function in Fig.\
  \ref{fig:mpi:exmp:tag}, process 0 uses the wildcard receive to
  gather messages from the rests.  In order to prevent this function
  being interfered by following statements, the function contract must
  have a strong enough requirement stating that no process shall send
  a message to process 0 after it exits \texttt{f} until process 0
  exits \texttt{f}.  But this requirement is too strong.  In fact,
  \texttt{f} only requires that no process shall send a message tagged
  by 1 to process 0.  The \minimp{} specification language has no notion
  of message tags hence cannot specify such a precise requirement for
  \texttt{f}.  $\qed$
\end{exmp}


\textbf{The complexity of the C/MPI APIs.}  The MPI library provides a
large number of functions and datatypes.  It will not be a surprise
that MPI has more complicated APIs than the communication operations
of \minimp{}.  This dissertation only focuses on a subset of them:
blocking point-to-point and collective communication functions.  For
this subset, the complexity of the APIs is mainly attributed to MPI's
unique type system and the relatively lower-level features in C (i.e.,
pointer and memory management).  We use an MPI collective function
\texttt{MPI\U{}Bcast} as an example to illustrate these two aspects.

The \texttt{MPI\U{}Bcast} has the following signature:

\begin{center}
\begin{programNoNum}
  int MPI\U{}Bcast(void * buf, int count, MPI\U{}Datatype 
    datatype, int root, \\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ MPI\U{}Comm comm).
\end{programNoNum}
\end{center}

\texttt{MPI\U{}Bcast} must be called collectively by all
processes, among which a process is designated to be the ``root''.
The ``root'' process broadcasts a message to all other processes.
Every non-``root'' process receives the message.  This function has
five formal parameters:
\begin{itemize}
\item \texttt{buf} is a pointer to the memory location where, for the
  ``root'' process, the sending data occupies, and for the
  non-``root'' processes, the receiving data will be saved.

\item \texttt{count} and \texttt{datatype} together specify the
  expected \emph{type signature} of the data in the message. All
  processes must agree on the type signature.  A type signature
  determines the bytewise size of the data, i.e., the product of the
  \texttt{count} and the extent of the \texttt{datatype}.  The
  \texttt{MPI\U{}Datatype} is an enumeration, in which most
  enumerators refer to language specific data types, such as that
  \texttt{MPI\U{}INT} refers to \texttt{int} in C.
  
\item \texttt{root} specifies the rank of the process that will be the
  ``root'' process.
  
\item \texttt{comm} specifies the communicator that is associated with
  this operation.
\end{itemize}

In C, one cannot access data through a \texttt{void} pointer such as
the \texttt{buf} in our example.  The \texttt{buf} must be converted
to a pointer to a non-void $T$ type before being used to access the
data.  The $T$ can be determined by elaborating different cases of the
\texttt{datatype}.  However, elaboration is quite expensive when the
value of the \texttt{datatype} is arbitrary.  Moreover, under the
weakest assumption, the data referred by \texttt{buf} is also
arbitrary.  One needs to find a representation for the arbitrary data
of arbitrary type in CIVL.

To deal with such complexity, we use an uninterpreted function
$\mymath{extent(datatype)}$ to represent the bytewise extent of a
$\mymath{datatype}$.  A simple theory for the $\mymath{extent}$
function is that for an \texttt{MPI\U{}Datatype} $d$ and a C type $t$,
$\mymath{extent(d) == \texttt{sizeof}(t)}$ if and only if $d$ corresponds to
$t$.

Then an arbitrary data, of which the size is given by a pair of
\texttt{MPI\U{}Datatype} $d$ and count $c$ can be represented as an arbitrary
\texttt{char} array of length $\mymath{extent}(d) \times{} c$.

\textbf{The Complexity of C language}. Finally, C language itself is a
complicated language, which has various powerful but also error-prone
features such as multi-level pointers, type casting, memory
allocation, etc.  A contract system for C/MPI programs must first be
able to specify and verify C programs.

We introduce the contract language for C/MPI programs in the next
section.  The language is an extension of an existing specification
language for sequential C programs.  Hence instead of designing a
contract language for C programs from scratch, we choose to add MPI
features to a mature specification language.