The evaluation of our approach for verifying message-passing program
against function contracts is based on the MPI function contract
system described in Chapter \ref{chp:mpi:system}.  We applied our
implementation to a number of C/MPI/CIVL-C collective-style functions,
including functions from CIVL's MPI library, implementations of
advanced algorithms for MPI collective functions and collective-style
functions carved out from MPI scientific computing applications.

Two of the aforementioned collective-style functions are selected to
be presented with details in \S\ref{chp:eval:examples}.  The overall
experimental results and performance are discussed about in
\S\ref{chp:eval:results}.

\section{Running Examples} \label{chp:eval:examples}

Real MPI implementations, such as MPICH
\cite{Thakur:2005:OCC:2747766.2747771}, use advanced algorithms for
MPI collective functions.  And more such algorithms keep being
designed and implemented \cite{jesper2019optimal, KANG2019220}.  An
MPI contract system can be effective for verifying the correctness of
these algorithms since 1) it can verify function implementations in
isolation; and 2) different implementations of one MPI collective
function can share a function contract.  To illustrate such
effectiveness, we show the verification of two
\texttt{MPI\U{}Allgather} implementations in
\S\ref{sec:mpi:eval:allgather}.

The implementation of an MPI collective function, or more generally,
of an MPI collective-style function can be complicated though, their
complex has no effect on the verification of their caller
functions for a contract system.  Thanks to the modular verification
feature of contract systems, the behavior of a call to a contracted
function only depends on its function contract.  We illustrate such an
advantage of our MPI contract system in \S\ref{sec:mpi:eval:dotprod}
by presenting an example that uses the \texttt{MPI\U{}Allgather}
function.

\subsection{Allgather Implementations} \label{sec:mpi:eval:allgather}

\textbf{CIVL's implementation.} In CIVL, simple and deterministic algorithms are used to implement MPI
collective functions.  Figure \ref{fig:mpi:eval:allgather} shows
CIVL's implementation of the \texttt{MPI\U{}Allreduce} function, which
is just a call to the \texttt{MPI\U{}Reduce} followed by a call to the
\texttt{MPI\U{}Bcast}.

Both the \texttt{MPI\U{}Reduce} and \texttt{MPI\U{}Bcast} are
annotated with function contracts.  Therefore, for the purpose of
verifying the functional correctness of the \texttt{MPI\U{}Allreduce}
function, their definitions are not needed.  Since all these functions
are MPI collective functions, they are guaranteed not to interfere
with each other.  So there is no need to specify a requirement or
guarantee for these functions.

To verify \texttt{MPI\U{}Allreduce} with the contracts, the user needs
to specify a bounded number of processes.  The contract system then is
able to verify that \texttt{MPI\U{}Allreduce} satisfies its function
contract for the bounded number of processes and arbitrary message
data, data size, data type and reduction operation.

Next, we briefly explain these contracts.

For the contract of \texttt{MPI\U{}Bcast}, the state-requirement
states that

\begin{enumerate}
\item \texttt{root} must be in between 0 and the size of the
  communicator;
  
\item the type signature (i.e., the product of the \texttt{count} and
  the \texttt{datatype} extent) must be non-negative;

\item all processes must have the same values for \texttt{root} and
  the type signature,  respectively;

\item the pointer \texttt{buf} must point to an allocated memory
  region, of which the size shall not be less than the type signature.
\end{enumerate}
The state-guarantee ensures that eventually all processes will have
the same value in their memory regions referred by their
\texttt{buf}s.  In addition, only those memory regions of the non-root
processes will be modified.  Such a frame condition is expressed with
a behavior named by ``\texttt{nonroot}''.

For the contract of \texttt{MPI\U{}Reduce}, the state-requirement is
similar to the one of \texttt{MPI\U{}Bcast} except that it is stronger
over the values of \texttt{count} and \texttt{datatype}.  It requires
that all processes must have same values for \texttt{root} and
\texttt{datatype}, respectively.  In fact, the author of this
dissertation was not aware of that \texttt{MPI\U{}Reduce} needs a
stronger state-requirement than \texttt{MPI\U{}Bcast} until the
contract system reports an error.  The state-guarantee ensures that 1)
nothing will be modified for all the non-root processes; and 2) the
memory region referred by \texttt{recvbuf} on the root process will
eventually be assigned the result of reduction over all the memory
regions referred by \texttt{sendbuf}s on all the processes.

The contract of \texttt{MPI\U{}Allreduce} is similar to the one of
\texttt{MPI\U{}Reduce} except that \texttt{MPI\U{}Allreduce} ensures
all processes will eventually hold the reduction result.


\begin{figure}
  \begin{programSmall}
\mycomment{/*@ \BSL{}mpi\U{}collective(comm, COL):}\\
\mycomment{\ \ \ \ requires 0 <= root < \BSL{}mpi\U{}comm\U{}size \&\&
  0 <= count * \BSL{}mpi\U{}extent(datatype)}\\
\mycomment{\ \ \ \ \ \ \ \ \ \ \&\& \BSL{}mpi\U{}agree(root) \&\& \BSL{}mpi\U{}agree(count * \BSL{}mpi\U{}extent(datatype))}\\
\mycomment{\ \ \ \ \ \ \ \ \ \ \&\& \BSL{}mpi\U{}valid(buf, count, datatype);}\\
\mycomment{\ \ \ \ ensures \BSL{}mpi\U{}agree(\BSL{}mpi\U{}region(buf, count, datatype));}\\
\mycomment{\ \ \ \ behavior nonroot:}\\
\mycomment{\ \ \ \ \ \ assumes \BSL{}mpi\U{}comm\U{}rank != root;}\\
\mycomment{\ \ \ \ \ \ assigns  \BSL{}mpi\U{}region(buf, count,
  datatype); */}\\
\ccode{int} MPI\U{}Bcast(\ccode{void} * buf, \ccode{int} count, 
MPI\U{}Datatype datatype, \ccode{int} root, \\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ MPI\U{}Comm
              comm);\\ \\
 \mycomment{/*@ \BSL{}mpi\U{}collective(comm, COL):} \\
 \mycomment{\ \ \ \   requires  0 <= count*\BSL{}mpi\U{}extent(datatype)} \\
 \mycomment{\ \ \ \ \ \ \ \ \ \ \&\& \BSL{}mpi\U{}valid(sendbuf, count, datatype)}\\
 \mycomment{\ \ \ \ \ \ \ \ \ \ \&\& \BSL{}mpi\U{}valid(recvbuf, count, datatype)}\\
 \mycomment{\ \ \ \ \ \ \ \ \ \ \&\& \BSL{}mpi\U{}agree(root) \&\& \BSL{}mpi\U{}agree(count) \&\& \BSL{}mpi\U{}agree(datatype);}\\
 \mycomment{\ \ \ \ \ \ \ \ \ \ \&\& 0 <= root < \BSL{}mpi\U{}comm\U{}size;}\\
 \mycomment{\ \ \ \   behavior root:}\\
 \mycomment{\ \ \ \ \ \   assumes \BSL{}mpi\U{}comm\U{}rank == root;}\\
 \mycomment{\ \ \ \ \ \   assigns \BSL{}mpi\U{}region(recvbuf, count, datatype);}\\
  \mycomment{\ \ \ \ \ \  ensures  \BSL{}mpi\U{}equals(\BSL{}mpi\U{}region(recvbuf, count, datatype),}\\
  \mycomment{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
    \BSL{}mpi\U{}reduce(sendbuf, count, datatype, op)); */}\\
\ccode{int} MPI\U{}Reduce(\ccode{void} * sendbuf, \ccode{void} * recvbuf, \ccode{int} count, MPI\U{}Datatype datatype, \\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ MPI\U{}Op op, \ccode{int} root, MPI\U{}Comm comm); \\
\\
\mycomment{/*@ \BSL{}mpi\U{}collective(comm, COL):}\\
\mycomment{\ \ \ \ requires count >= 0 \&\& \BSL{}mpi\U{}valid(sendbuf, count,
  datatype)}\\
\mycomment{\ \ \ \ \ \ \ \ \ \ \&\& \BSL{}mpi\U{}valid(recvbuf, count, datatype)}\\
\mycomment{\ \ \ \ \ \ \ \ \ \ \&\& \BSL{}mpi\U{}agree(count) \&\& \BSL{}mpi\U{}agree(op) \&\& \BSL{}mpi\U{}agree(datatype);}\\
\mycomment{\ \ \ \   assigns  \BSL{}mpi\U{}region(recvbuf, count, datatype);}\\
\mycomment{\ \ \ \   ensures  \BSL{}mpi\U{}equals(\BSL{}mpi\U{}region(recvbuf, count, datatype),}\\
\mycomment{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \BSL{}mpi\U{}reduce(sendbuf, count, datatype, op));*/}\\
\ccode{int} MPI\U{}Allreduce(\ccode{void} * sendbuf, \ccode{void} * recvbuf, \ccode{int} count, \\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ MPI\U{}Datatype datatype, MPI\U{}Op op, MPI\U{}Comm comm) \lb{} \\
\ \  MPI\U{}Reduce(sendbuf, recvbuf, count, datatype, op, 0, comm); \\
\ \  MPI\U{}Bcast(recvbuf, count, datatype, 0, comm); \\
\ \   \ccode{return} 0; \\
\rb{}\\
\end{programSmall}
\caption{Annotating function contracts for all the collective-style
  functions used by CIVL's implementation of
  \texttt{MPI\U{}Allreduce}.}
\label{fig:mpi:eval:allgather}
\end{figure}

\textbf{Recursive Doubling.}  Real MPI implementations use more
optimized algorithms for \texttt{MPI\U{}Allreduce}, such as the
\emph{recursive doubling} algorithm.  Figure
\ref{fig:mpi:eval:recursive-double} is a CIVL-C realization of a
recursive doubling \texttt{MPI\U{}Allreduce} pseudocode given in
\cite{Ruefenacht:2017:GRD:3163938.3164013}.  The function contract of
the \texttt{MPI\U{}Allreduce} in this figure is redundant and hence
omitted.

In this implementation, we used CIVL-C primitives to abstract details
that are irrelevant to the algorithm:

\begin{itemize}
\item The \texttt{\$mpi\U{}malloc} is a helper function written in
  CIVL-C.  It allocates a memory region of the size of the given type
  signature.  In the case of that the value of \texttt{datatype} is
  arbitrary, instead of elaborating all possible concrete choices,
  this function uses an uninterpreted function
  $\mymath{extent(\texttt{datatype})}$ to represent the extent of the
  \texttt{datatype} and allocates a memory region of size
  $\mymath{extent(\texttt{datatype}) * \texttt{count}}$.
  
\item In ACSL, reduction operations can be expressed with different
  constructs according to the reduction operation.  For example,
  summing up all the $n$ elements in an array $a$ can be expressed as
  \texttt{\BSL{}sum(0, $n$-1, \BSL{}lambda int i; $a$[i])} in ACSL.
  However, for the cases where the reduction operation is arbitrary,
  specifying a reduction operation in ACSL will inevitably elaborate
  all possible concrete choices.  However, elaboration will make the
  verification much more expensive.  Hence, we used a CIVL-C system
  function \texttt{\$memapply} to implement the \texttt{reduce}
  function that performs process local reduction operation:
  
  \begin{programNoNum}
  \ccode{void} reduce(\ccode{void} * inout, \ccode{void} * in,
  \ccode{int} count, \ccode{int} size, \\
\ \ \ \ \ \ \ \ \ \ \ \ MPI\U{}Op op) \lb{}\\
\ \  \$memapply(inout, (\$operation)op, in, count, size, inout); \\
\rb{}
\end{programNoNum}

The \texttt{\$memapply} function performs an ``element-wise''
\texttt{\$operation} on two memory regions referred by \texttt{inout}
and \texttt{in}, respectively, and writes the result back to
\texttt{inout}.  Here ``element-wise'' means that the operation is
applied to every pair of \texttt{size $/$ count} bytes memory regions
that are referred by \texttt{(char*)inout + $i$ * (size $/$ count)}
and \texttt{(char*)in + $i$ * (size $/$ count)}, respectively, for
$0 \leq i < \texttt{count}$.

When the \texttt{op} has a non-concrete value, \texttt{\$memapply}
uses an uninterpreted function to represent the general reduction
result.
\end{itemize}

With these abstractions, this function implementation can be verified
by the MPI contract system with the same configuration as the previous
implementation.

\begin{figure}
  \begin{programSmall}
\ccode{void} MPI\U{}Allreduce(\ccode{void} * sendbuf, \ccode{void} *
recvbuf, \ccode{int} count,  \\ 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ MPI\U{}Datatype datatype, MPI\U{}Op op,  MPI\U{}Comm comm) \lb{}\\
\ \  \ccode{int} datasize = sizeofDatatype(datatype) * count; \\
\ \  \ccode{void} * global = \$mpi\U{}malloc(count, datatype); \\
\ \  \ccode{int} pof2, rem, int nprocs, rank, myrank, mask = 1; \\
\\
\ \  MPI\U{}Comm\U{}size(comm, \&nprocs);   MPI\U{}Comm\U{}rank(comm, \&rank);\\
\ \  pof2 = log2(nprocs);  pof2 = pow2(pof2); \\
\ \  rem = nprocs - pof2; \\
\ \  memcpy(global, sendbuf, datasize);\\
\ \ \ccode{if} (rank < 2 * rem)  \lb{} \\
\ \ \ \  \ccode{if} (rank \% 2 == 0) \lb{} \\
\ \ \ \ \ \   MPI\U{}Send(global, count, datatype, rank + 1, 0, comm); \\
\ \ \ \ \ \    myrank = -1; \\
\ \ \ \  \rb{} \ccode{else} \lb{} \\
\ \ \ \ \ \   MPI\U{}Recv(recvbuf, count, datatype, rank - 1, 0, comm, MPI\U{}STATUS\U{}IGNORE);\\
\ \ \ \ \ \   reduce(global, recvbuf, count, datasize, op); \\
\ \ \ \ \ \   myrank = rank / 2;\\
\ \ \ \   \rb{}\\
\ \  \rb{} \ccode{else} \\
\ \ \ \     myrank = rank - rem;\\
\ \ \ccode{if} (myrank != -1)  \\
\ \ \ \  \ccode{while} (mask < pof2) \lb{} \\
\ \ \ \ \ \   \ccode{int} dst, newdst = myrank \char`\^{} mask; \\
\\
\ \ \ \ \ \    \ccode{if} (newdst < rem) \\
\ \ \ \ \ \ \ \ 	dst = newdst * 2 + 1;\\
\ \ \ \ \ \     \ccode{else} \\
\ \ \ \ \ \ \ \	dst = newdst + rem;\\
\ \ \ \ \ \  MPI\U{}Sendrecv(global, count, datatype, dst, 0, \\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ recvbuf, count, datatype, dst, 0, comm, MPI\U{}STATUS\U{}IGNORE);\\
\ \ \ \ \ \      reduce(global, recvbuf, count, datasize, op);\\
\ \ \ \ \ \      mask = mask <{}< 1;\\
\ \ \ \    \rb{}\\
\ \  \ccode{if} (rank < 2 * rem) \\
\ \ \ \   \ccode{if} (rank \% 2 != 0) \\
\ \ \ \ \ \   MPI\U{}Send(global, count, datatype, rank - 1, 0, comm); \\
\ \ \ \  \ccode{else} \\
\ \ \ \ \ \   MPI\U{}Recv(global, count, datatype, rank + 1, 0, comm, MPI\U{}STATUS\U{}IGNORE);\\
\ \  memcpy(recvbuf, global, datasize);\\
\ \  free(global);\\
\rb{}
\end{programSmall}
\caption{An \texttt{MPI\U{}Allreduce} implementation based on the
  recursive doubling algorithm.}
\label{fig:mpi:eval:recursive-double}
\end{figure}
  
\subsection{Parallel Vector Product} \label{sec:mpi:eval:dotprod}

The two \texttt{MPI\U{}Allreduce} implementations presented in
\S\ref{sec:mpi:eval:allgather} have different degrees of
complicatedness.  But the implementation is irrelevant to the
functional correctness of a caller function of
\texttt{MPI\U{}Allreduce} as long as \texttt{MPI\U{}Allreduce} is
annotated with a contract.  We present such a collective-style caller
function to \texttt{MPI\U{}Allreduce} in Fig.\ \ref{fig:mpi:dotprod}.
The data structures used in this figure are showed in Fig.\
\ref{fig:mpi:dotprod:structures}.  This C code was carved out from the
HYPRE \cite{falgout:2002:hypre} open source project.

%% what does this function do ?
The \texttt{hypre\U{}ParVectorInnerProd} function lets every process
computes the vector product of two sequences of elements in parallel
and then sums up the vector products on all the processes.

The collective behavior in the function contract of
\texttt{hypre\U{}ParVectorInnerProd} is associated to the MPI
communicator stored in the structure referred by \texttt{x}.  The
state-requirement states that

\begin{enumerate}
\item the structures referred by \texttt{x} and \texttt{y} have been
  allocated,

\item the \texttt{hypre\U{}Vector}
structures referred by the fields \texttt{local\U{}vector} of
\texttt{*x} and \texttt{*y} have been allocated, 

\item the sequences of elements referred by the fields \texttt{data}
  of \texttt{x->local\U{}vector} and \texttt{y->local\U{}vector} have
  been allocated, and

\item the size of an element sequence must be positive.
\end{enumerate}
The state-guarantee states that 1) nothing will be modified by this
function, and 2) the returned value will equal to the sum over all the
dot products computed by all the processes.

This function relies on the
\texttt{hypre\U{}SeqVectorInnerProd} sequential function to perform
process local dot product operations.  In order to fully verify the
functional correctness of \texttt{hypre\U{}ParVectorInnerProd}, one
must also verify the function \texttt{hypre\U{}SeqVectorInnerProd} independently.
The contract of this sequential function is purely in ACSL and is easy
to understand.  We remark that in order to verify this function for
arbitrary size of the element sequences, we need to annotate the loop
at line 23-24 with a loop invariant.  The loop invariant describes the
property of the loop and will be verified in an inductive way during
the symbolic execution.  Once the loop is verified as satisfying the
loop invariant, the effect of the loop to the program can be directly
derived from the loop invariant.  Detailed description of CIVL's
support on sequential loop invariants can be found in
\cite{10.1007/978-3-030-03421-4_12}.

By verifying \texttt{hypre\U{}SeqVectorInnerProd} and
\texttt{hypre\U{}ParVectorInnerProd} \\
against their contracts
separately, the functional correctness of both functions are thus
verified.  Of course, for \texttt{hypre\U{}ParVectorInnerProd}, the
result is limited for a bounded number of processes.

\begin{figure}[t]
  \begin{minipage}[t][][b]{.45\textwidth}
    \begin{programSmall}
      \ccode{typedef struct} \lb{}\\
      \ \  HYPRE\U{}Complex  *data;\\
      \ \   HYPRE\U{}Int      size; \\
      \ \   HYPRE\U{}Int   num\U{}vectors;   \\
      \ \   ... \\
      \rb{} hypre\U{}Vector;\\
    \end{programSmall}
  \end{minipage}
  \begin{minipage}[t][][b]{.45\textwidth} 
    \begin{programSmall}
      \ccode{typedef struct} hypre\U{}ParVector\U{}struct \lb{}\\
      \ \ MPI\U{}Comm	         comm;\\
      \ \ hypre\U{}Vector	*local\U{}vector; \\
      \ \ ... \\
      \rb{} hypre\U{}ParVector;
    \end{programSmall}
  \end{minipage}
  \caption{The data structures that are used in Fig.\
    \ref{fig:mpi:dotprod}.  Insignificant fields are omitted.}
  \label{fig:mpi:dotprod:structures}
\end{figure}

\begin{figure}
  \begin{programSmall}
\ccode{\#define} hypre\U{}ParVectorComm(vector)  	        ((vector) -> comm)\\
\ccode{\#define} hypre\U{}ParVectorLocalVector(vector)      ((vector) -> local\U{}vector)\\
\ccode{\#define} hypre\U{}VectorData(vector)      ((vector) -> data)\\
\ccode{\#define} hypre\U{}VectorSize(vector)      ((vector) -> size)\\
\ccode{\#define} hypre\U{}VectorNumVectors(vector) ((vector) -> num\U{}vectors)\\
\ccode{\#define} hypre\U{}conj(value) value\\
    \ccode{\#define} SIZE ((x->size)*(x->num\U{}vectors))\\
    \ccode{\#define} PAR\U{}SIZE
    ((x->local\U{}vector->size)*(x->local\U{}vector->num\U{}vectors)) \\
    \ccode{\#define} NPROCS   \BSL{}mpi\U{}comm\U{}size \\
\mycomment{/*@ requires \BSL{}valid(x) \&\& \BSL{}valid(y) \&\& 0 < SIZE}\\
\mycomment{\ \ \ \ \ \ \ \ \ \ \&\& \BSL{}valid(x->data + (0 .. SIZE-1)) \&\& \BSL{}valid(y->data + (0 .. SIZE-1));}\\
\mycomment{\ \ \ \  assigns  \BSL{}nothing;}\\
\mycomment{\ \ \ \  ensures  \BSL{}result == \BSL{}sum(0, SIZE-1, \BSL{}lambda int j;
  y->data[j] * x->data[j]); */}\\
HYPRE\U{}Real  hypre\U{}SeqVectorInnerProd(hypre\U{}Vector *x,
				      hypre\U{}Vector *y) \lb{}\\
\ \   HYPRE\U{}Complex *x\U{}data = hypre\U{}VectorData(x);\\
\ \   HYPRE\U{}Complex *y\U{}data = hypre\U{}VectorData(y);\\
\ \   HYPRE\U{}Int    i, size   = hypre\U{}VectorSize(x);  \\         
\ \   HYPRE\U{}Real     result = 0.0;\\
\ \   size *=hypre\U{}VectorNumVectors(x);\\
\ \ \mycomment{/*@ loop invariant 0 <= i <= size}\\
\ \ \mycomment{\ \ \ \ \ \ \ \ \ \ \ \ \&\& result == \BSL{}sum(0, i-1, \BSL{}lambda int j; y\U{}data[j] * x\U{}data[j]);}\\
\ \  \mycomment{\ \ \ \ loop assigns result, i; */}\\
\ \  \ccode{for} (i = 0; i < size; i++) \\
\ \ \ \  result += hypre\U{}conj(y\U{}data[i]) * x\U{}data[i]; \\
\ \  \ccode{return} result;\\
\rb{}\\
    \\
\mycomment{/*@ \BSL{}mpi\U{}collective(hypre\U{}ParVectorComm(x), COL):}\\
\mycomment{\ \ \ \   requires \BSL{}valid(x) \&\& \BSL{}valid(y) \&\& 0 < PAR\U{}SIZE  \&\&}\\
\mycomment{\ \ \ \ \ \ \ \ \ \ \ \ \   \BSL{}valid(x->local\U{}vector) \&\& \BSL{}valid(y->local\U{}vector) \&\&}\\
\mycomment{\ \ \ \ \ \ \ \ \ \ \ \ \ \BSL{}valid(x->local\U{}vector->data + (0 .. PAR\U{}SIZE-1))  \&\&}\\
\mycomment{\ \ \ \ \ \ \ \ \ \ \ \ \  \BSL{}valid(y->local\U{}vector->data + (0 .. PAR\U{}SIZE-1));}\\
\mycomment{\ \ \ \    assigns \BSL{}nothing;}\\
\mycomment{\ \ \ \    ensures \BSL{}result == \BSL{}sum(0,  NPROCS-1, \BSL{}lambda int k;}\\
\mycomment{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \BSL{}on(k,  \BSL{}sum(0,  PAR\U{}SIZE-1, \BSL{}lambda int t;}\\
\mycomment{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \   x->local\U{}vector->data[t] *
  y->local\U{}vector->data[t]))); */}\\
HYPRE\U{}Real hypre\U{}ParVectorInnerProd(hypre\U{}ParVector *x,
				     hypre\U{}ParVector *y) \lb{} \\
\ \  MPI\U{}Comm      comm    = hypre\U{}ParVectorComm(x);\\
\ \   hypre\U{}Vector *x\U{}local = hypre\U{}ParVectorLocalVector(x);\\
\ \   hypre\U{}Vector *y\U{}local = hypre\U{}ParVectorLocalVector(y);\\
\ \   HYPRE\U{}Real result = 0.0;\\
\ \   HYPRE\U{}Real local\U{}result = hypre\U{}SeqVectorInnerProd(x\U{}local, y\U{}local);\\    
\ \   hypre\U{}MPI\U{}Allreduce(\&local\U{}result, \&result, 1, HYPRE\U{}MPI\U{}REAL,\\
\ \ \ \ \ \ \ \ 		      hypre\U{}MPI\U{}SUM, comm);   \\
\ \  \ccode{return} result;\\
\rb{}
\end{programSmall}
\caption{A function that computes vector product in parallel using
  MPI.}
\label{fig:mpi:dotprod}
\end{figure}

\section{Experiment} \label{chp:eval:results}

We evaluate our MPI contract system implementation by using it to
specify and verify a set of C/MPI/CIVL-C collective-style functions.

This experiment contains two parts.  In the first part, we ignore the
checking of absence assertions in the contracts.  In other words, 1)
the first part assumes that no interference can happen for every
collective-style function; and 2) it does not verify the guarantees of
the verified functions.  In the second part, we enable full validity
verification for a selected subset of the experiments.

For each collective-style function in the experiment, we prepared a
set of negative examples, each of which contains a specific kind of
contract violation, such as state-guarantee violation, too weak
state-requirement to ensure the state-guarantee or a kind of absence
assertion violations.  Our system can precisely report the expect
error for each of these negative examples.
For brevity, we do not show the results
of all the negative examples.

%% why break up into 2 parts
Instead of directly verifying the full validity of every contracted
function, we separated the verification only for state-requirement and
-guarantees in the first part for two reasons.  First, the absence
assertions are introduced for reasoning about the case of
interference.  Most of our examples use only MPI collective functions
and wildcard-free send/receive operations.  They fall into the
category where no interference can happen naturally.  Second, full
validity verification involves checking path predicates (i.e., absence
assertions).  CIVL was originally designed for verifying properties
that can be expressed by state predicates only.  So its sophisticated
POR algorithm is not sound for full validity verification.  In our
contract system implementation, we enforce the soundness by informing
the CIVL model checker to stop applying POR when a statement that may
be visible to the absence assertions is enabled.  This is a coarse
approximation in that the model checker eventually has to explore a
large number of commutative executions.  Therefore, in the second part
of the experiment, examples cannot be scaled to the same level as
themselves in the first part.

%% setting of provers
CIVL uses automated theorem provers to reason about the logic formulas
that are still non-trivial after a series of simplifications applied by
CIVL.  Each prover is assigned a timeout so that it will not run
infinitely in undecidable cases.  A call to a prover is expensive.
Although the longer the timeout, the higher the possibility of that a
prover can eventually solve a formula, CIVL has to waste more time in
waiting for the reasoning of unsolvable formulas.  Therefore, in this
experiment, we carefully set the timeout for different provers.

\begin{enumerate}
\item Z3 and CVC4 are used in a sequence for all kinds of the reasoning
  with a 2 seconds timeout.
\item CVC4 will be invoked only if Z3 is not able to solve a formula
  within 2 seconds.
\item Why3 will only be used for checking assertions and is only
  invoked when neither Z3 nor CVC4 solves a formula within 2 seconds.
  Why3 is assigned a default 5 seconds timeout.  In fact, Why3 itself
  is not an automated theorem prover but a platform that translates
  the input and sends it to various provers including Z3 and CVC4.  We
  use Why3 for two of its advantages over our direct translation to Z3
  and CVC4: 1) in addition to the translation, Why3 introduces extra
  transformations and axioms for specific theories; 2) Why3 supplies
  libraries for rich theories such as permutation and multi-set.
\end{enumerate}
The experiment was run on an iMac with 3.5 GHz Intel Core i7 and 32 GB
1600 MHz DDR3.

%% purely functional correctness run
Table \ref{tab:experimental:result:part:I-1} and
\ref{tab:experimental:result:part:I-2} show the experimental results
of the first part.  

Examples in Table \ref{tab:experimental:result:part:I-1} are the
implementations of MPI collective functions in CIVL's MPI library.
These implementations are all based on simple and intuitive
algorithms.  For example, the implementation of \texttt{bcast} is
letting the root process send messages to all processes in a fixed
order.  Although the implementations are naive, their contracts are
general and conform to the MPI standard.

%% what is concluded from this ? representation of non-trivial
%%data sturcture values matters ?
Reasoning about arbitrary aggregate type objects can be expensive.
Observing the differences in the statistics of \texttt{bcast},
\texttt{gather} and \texttt{gatherv}.  The naive implementation of
\texttt{gather} can be seen as a reverse of the one of \texttt{bcast}:
the root process receives messages from all processes in a fixed
order.  These two examples have very different performances.  For the
runs of them with a same number of processes, the verification of
\texttt{gather} generates almost 9 times more prover calls than the
one of \texttt{bcast}.  This is because the value eventually in the
receiving buffer of the \texttt{gather} function is a partitioned
array, in which each part was sent from a process.  Considering the
fact that both the content and size of each part are arbitrary, the
general representation of such a value has to involve a number of
quantified formulas.  In \texttt{gatherv}, the ``gathered''
partitioned array is even more general in that the order of each part
is arbitrary.  This explains why verifying \texttt{gatherv} takes
twice the time of verifying \texttt{gather}.

%% concluded ? modular is effective
The contract system is effective in re-using verification results.
For example, the \texttt{allgather} example is implemented by
combining \texttt{gather} and \texttt{bcast}.  During the
verification, the behaviors of \texttt{gather} and \texttt{bcast} are
derived from their contracts respectively.  In other words, by
assuming that \texttt{gather} and \texttt{bcast} satisfy their
contracts, the verification results of them are directly re-used.
According to the statistics in the table, it is easier for the
contract system to verify \texttt{allgather} than \texttt{gather}.

%% conclude: contracts are re-usable.
A function contract can be re-used for different implementations.  In
Table \ref{tab:experimental:result:part:I-2}, \texttt{allreduce\U{}dr}
and \texttt{reduceScatter} are implementations of MPI collective
functions based on advanced algorithms.  Implementations are different
though, \texttt{allreduce\U{}dr} and \texttt{allreduce} share the same
function contract.

%% work togather with loop invariants and sequential contracts,

Rest of the examples in Table \ref{tab:experimental:result:part:I-2}
are functions from different MPI scientific computing applications.
In these examples, each process is responsible for performing some
computation locally.  Process-local functions can be specified by pure
ACSL function contracts.  Verifying and re-using pure ACSL contracts
is just a special case of dealing with MPI contracts for our contract
system.  Taking \texttt{diff1dExchange} and \texttt{diff1dIter} as an
example.  The \texttt{diff1dExchange} is the ``ghost cell exchange''
function. The \texttt{diff1dIter} is the loop body of the iterative
computational procedure of a parallel 1d-diffusion solver.  The
\texttt{diff1dIter} is a combination of a call to
\texttt{diff1dExchange} and a call to a process-local computing
function.  The behaviors of both calls are summarized from their
contracts.  The verification result of the process-local function is
not showed in the table since it is irrelevant to our topic.  Similar
for \texttt{diff2dExchange} and \texttt{diff2dIter}.

%% diff1d and diff2d again emphsizes the importance of the logic
%% reasoning
For functions from the 1d-diffusion solver, the contracts have no
specific assumption on the pattern of distribution.  That is, the left
neighbor of a process can be any other process.  Ditto for the right
neighbor.  However, for the functions from the 2d-diffusion solver, we
strengthen the contracts to assume a checkerboard distribution.  This
is the compromise we made to the complexity of proving these functions
for arbitrary parameters.  For this example, there are 2d arrays with
arbitrary contents and sizes, inside which partitions are moving
around.  The general representation we mentioned before for
arbitrarily partitioned arrays is powerful in expressiveness but makes
reasoning difficult.

%% matmat is typical example for collective-style division
The \texttt{matmat} example is a collective matrix multiplication
implementation.  It is a typical example for showing that dividing MPI
programs by collective-style functions are effective.  Figure
\ref{fig:eval:matmat} shows the function definition.  The function
definition can be considered as being composed of three
collective-style functions and a process-local procedure.  Taking the
process local function \texttt{matmat\U{}local}, which computes one
row of the result, as a special case of collective-style functions,
the verification of this function definition is thus divided into four
sub-problems.

\begin{figure}
  \begin{center}
  \begin{programSmall}
\ccode{int} N, M, L, *A, *B, *C, size, rank; \\    
    \ccode{void} matmat() \lb{}\\
\ \  \ccode{int} tmpC[L], tmpA[M]; \\
\\      
\ \  MPI\U{}Bcast(B, M*L, MPI\U{}INT, 0, MPI\U{}COMM\U{}WORLD);\\
\ \  MPI\U{}Scatter(A, M, MPI\U{}INT, tmpA, M, MPI\U{}INT, 0,
MPI\U{}COMM\U{}WORLD); \\
\ \  \ccode{if} (rank != 0) \\
\ \ \ \    memcpy(A, tmpA, M * sizeof(int));\\
\ \   matmat\U{}local(); \\
\ \  memcpy(tmpC, C, L * sizeof(int)); \\
\ \  MPI\U{}Gather(tmpC, L, MPI\U{}INT, C, L, MPI\U{}INT, 0, MPI\U{}COMM\U{}WORLD); \\
\rb{}
\end{programSmall}
\end{center}
\caption{The definition of the \texttt{matmat} function that
  collectively performs matrix multiplication.}
\label{fig:eval:matmat}
\end{figure}


%% odd-even sort is a good example for abstraction
Function contracts sometimes can help the developer to ignore the
details of communication but focus on the correctness of the
algorithm.  For instance, the \texttt{oddEvenSort} example comprises
the loop body of a parallel odd-even sorting algorithm.  The
correctness of this algorithm is not so obvious and parallelism makes
it even harder for developers to prove it.  Figure
\ref{fig:eval:oddEvenSort} shows the function contract of this
example.  Each process holds an element of an unsorted sequence.
Every $i$-th element in the sequence can be expressed as
\texttt{\BSL{}on(i, myvalue)}.  In the contract, the state-guarantee at
line 9-10 expresses the sortedness property; the one at line 11-12
expresses the permutation property.  The contract only describes input
and output of the function while leaves communication details
invisible.  To prove the sortedness and permutation of the complete
algorithm, one can focus on the induction on the contract.
\param{}

\begin{figure}
  \begin{center}
  \begin{programSmall}
\ccode{int} id, n; \mycomment{// id:\ process rank, n:\ sorting array} \\
T myvalue;     \mycomment{// element hold by the process } \\
MPI\U{}Comm comm; \\
\\
\mycomment{/*@ \BSL{}mpi\U{}collective(comm, P2P):} \\
\mycomment{\ \ \ \  requires \BSL{}mpi\U{}agree(i);} \\
\mycomment{\ \ \ \  requires 0 <= i < n \&\& id == \BSL{}mpi\U{}comm\U{}rank \&\& n == \BSL{}mpi\U{}comm\U{}size;}\\
\mycomment{\ \ \ \  assigns  myvalue;}\\
\mycomment{\ \ \ \  ensures  (id \% 2 == 0 \&\& id < n-1 ==> myvalue <=
                                \BSL{}on(id+1,  myvalue))} \\
\mycomment{\ \ \ \  \ \ \ \ || (id \% 2 == 1 \&\& id < n-1 ==> myvalue <= \BSL{}on(id+1, myvalue));}\\
\mycomment{\ \ \ \  ensures  \BSL{}sum(0, n-1, \BSL{}lambda int t;
  \BSL{}on(t, myvalue) == myvalue ?\ 1 :\ 0) ==} \\
\mycomment{\ \ \ \ \ \ \ \ \ \ \BSL{}sum(0, n-1, \BSL{}lambda
  int t;  \BSL{}old(\BSL{}on(t, myvalue)) == myvalue ?\ 1 :\ 0);}\\
\mycomment{*/}\\
\ccode{void} oddEvenParIter(\ccode{int} i); \mycomment{// i is the
  loop identifier}\\
\end{programSmall}
\end{center}
\caption{Function contract of the function in the \texttt{OddEvenSort}
  example.}
\label{fig:eval:oddEvenSort}
\end{figure}

%% run with assuming wildcard exists


%% table of experiments

\begin{table}
  \begin{center}
\begin{small}
  %% name   | mode 1 | np | states | prover calls | timeout | time |
  %% BLANK | mode 2 | np | states | prover calls | timeout | time | DESCRIPTION
  %% BLANK | mode 3 | np | states | prover calls | timeout | time |
  \begin{tabular}{| p{5cm} | r | r | r | r | r |}
    \hline 
    name \& description & \#procs & \#states & \#trans & \#prover  & time(s)\\
    \hline
        \multirow{5}{5cm}{\texttt{bcast:}
    root sends in a roll and the rests do a receive, implemented in
    CIVL's MPI library
    } & 2 & 1, 121 & 3, 500 & 7 & 6 \\
                        & 3 & 3, 057 & 8, 235 & 14 & 8 \\
                        & 4 & 5, 805 & 15, 632 & 23 & 12 \\
                        & 5 & 9, 797 & 26, 608 & 34 & 17 \\
                        & 6 & 15, 545 & 42, 832 & 47 & 25 \\
    \hline
    \multirow{5}{5cm}{\texttt{gather:}
    root receives in a roll and the rests do one send, implemented
    in CIVL's MPI library
    } & 2 & 2, 608 & 7, 246 & 47 & 9 \\
                        & 3 & 6, 791 & 18, 226 & 102 & 16 \\
                        & 4 & 14, 788 & 38, 659 & 187 & 28  \\
                        & 5 & 31, 541 & 79, 997 & 297 & 54  \\
                        & 6 & 71, 850 & 175, 925 & 428 & 123  \\
    \hline
    \multirow{5}{5cm}{\texttt{gatherv:}
    root receives in a roll and the rests do one send, implemented
    in CIVL's MPI library
    } & 2 & 1, 266 & 3, 692 & 41 & 8\\
                        & 3 & 3, 053 & 8, 640 & 85 & 13\\
                        & 4 & 5, 852 & 16, 398 & 140 & 27\\
                        & 5 & 10, 121 & 28, 029 & 215 & 78\\
                        & 6 & 16, 612 & 45, 512 & 310 & 236\\
    \hline
    \multirow{5}{5cm}{\texttt{scatter:}
    root sends in a roll and the rests do one receive, implemented
    in CIVL's MPI library
    } & 2 & 2, 466 & 7, 007 & 43 & 8 \\
                        & 3 & 6, 332 & 17, 438 & 101 & 14 \\
                        & 4 & 13, 509 & 36, 428 & 188 & 27 \\
                        & 5 & 28, 067 & 73, 801 & 275 & 46 \\
                        & 6 & 62, 483 & 158, 481 & 386 & 108 \\
    \hline
    \multirow{5}{5cm}{\texttt{alltoall:}
    each proc performs \#procs sends and receives
    } & 2 & 786 & 2, 038 & 17 & 6\\
                        & 3 & 1, 382 & 3, 424 & 45 & 7\\
                        & 4 & 2, 153 & 5, 111 & 67 & 10\\
                        & 5 & 3, 114 & 7, 135 & 89 & 14 \\
                        & 6 & 4, 287 & 9, 532 & 115 & 19\\
    \hline
    \multirow{5}{5cm}{\texttt{alltoall2}
    each proc collectively calls \texttt{scatter} \#procs times,
    implemented in CIVL's MPI library
    } & 2 & 933 & 2, 986 & 19 & 7\\
                        & 3 & 1, 769 & 5, 905 & 32 & 10\\
                        & 4 & 3, 011 & 10, 351 & 66 & 15\\
                        & 5 & 4, 779 & 16, 972 & 84 & 31 \\
                        & 6 & 7, 174 & 26, 560 & 150 & 69\\
    \hline
    \multirow{5}{5cm}{\texttt{allgather:}
    each proc collectively calls \texttt{gather} then \texttt{bcast},
    implemented in CIVL's MPI library
    } & 2 & 2, 119 & 6, 235 & 23 & 11 \\
                        & 3 & 3, 690 & 10, 699 & 34 & 15 \\
                        & 4 & 5, 794 & 16, 512 & 44 & 21 \\
                        & 5 & 8, 944 & 24, 820 & 55 & 31 \\
                        & 6 & 14, 176 & 37, 915 & 65 & 50 \\
    \hline
    \multirow{5}{5cm}{\texttt{allreduce:}
    each proc collectively calls \texttt{reduce} then \texttt{bcast},
    implemented in CIVL's MPI library
    } & 2 & 841 & 2, 958 & 3 & 6 \\
                        & 3 & 1, 368 & 4, 803 & 3 & 6 \\
                        & 4 & 1, 903 & 6, 763 & 3 & 7 \\
                        & 5 & 2, 446 & 8, 838 & 3 & 9 \\
                        & 6 & 2, 997 & 11, 028 & 3 & 10 \\
    \hline
  \end{tabular}
\end{small}
\end{center}
\caption{The experimental results of verifying CIVL's implementations
  of the MPI collective functions with respect to state-requirements and
  -guarantees.}
\label{tab:experimental:result:part:I-1}
\end{table}

\begin{table}
  \begin{center}
    \begin{small}
      \begin{tabular}{| p{5cm} | r | r | r | r | r |}
        \hline 
        name \& description & \#procs & \#states & \#trans & \#prover  & time(s)\\
        \hline
        \multirow{5}{5cm}{\texttt{allreduce\U{}dr:}
        an implementation of the recursive doubling algorithm given by a
        pseudo code in \cite{Ruefenacht:2017:GRD:3163938.3164013}
        } & 2 & 648 & 1, 904 & 4 & 7\\
                            & 3 & 1, 060 & 3, 006 & 4 & 7\\
                            & 4 & 1, 562 & 4, 349 & 4 & 8\\
                            & 5 & 2, 017 & 5, 615 & 4 & 10\\
                            & 6 & 2, 486 & 6, 942 & 4 & 11\\
        \hline
        \multirow{5}{5cm}{\texttt{reduceScatter:}
        an implementation of an algorithm optimized for
        non-commutative reduction operations \cite{Bernaschi:2002:EIR:1895489.1895529}
        } & 2 & 713 & 1, 905 & 13 & 7\\
                            & 3 & 1, 378 & 3, 163 & 42 & 11\\
                            & 4 & 2, 147 & 4, 679 & 70 & 16\\
                            & 5 & 3, 102 & 6, 489 & 111 & 25\\
                            & 6 & 4, 248 & 8, 629 & 166 & 50\\
        \hline
        \multirow{5}{5cm}{\texttt{diff1dExchange:}
        the exchange ghost cells function in a 1d-diffusion implementation
        } & 2 & 1, 771 & 5, 083 & 19 & 7\\
                            & 3 & 6, 979 & 19, 164 & 40 & 12\\
                            & 4 & 25, 546 & 68, 328 & 69 & 25\\
                            & 5 & 93, 086 & 244, 148 & 102 & 84\\
                            & 6 & 345, 202 & 891, 940 & 135 & 382\\
        \hline 
        \multirow{4}{5cm}{\texttt{diff1dIter:}
        one time step implementation for a 1d-diffusion solver
        } & 2 & 2, 186 & 6, 354 & 58 & 19 \\
                            & 3 & 8, 646 & 23, 677 & 161 & 85 \\
                            & 4 & 31, 492 & 82, 514 & 380 & 275 \\
                            & 5 & 114, 108 & 287, 467 & 829 & 731 \\
        \hline
        \multirow{2}{5cm}{\texttt{diff2dExchange:}
        $n \times{} n$ checkerboard ghost cell exchange 
        } & $2 \times 2$ & 2, 010 & 4, 787 & 52 & 43\\
                            & $3 \times 3$ & 5, 154 & 12, 817 & 135 & 115\\
        & & & & &\\
        \hline
        \multirow{3}{5cm}{\texttt{diff2dIter:}
        one time step for a 2d-diffusion solver with $n \times{} n$
        checkerboard distribution
        } & $2 \times 2$ & 1, 727 & 5, 126 & 66 & 95\\
                            & & & & & \\
                            & & & & & \\
                            & & & & & \\
%                            & 4 & 1717 & 5110 & 25 & +13\\
%                           & 4 & 1720 & 5110 & 33 & +14\\
%                          & 4 & 1716 & 5110 & 25 & +15\\
%                           & 4 & 1717 & 5110 & 33 & +16\\
        \hline
        \multirow{5}{5cm}{\texttt{dotProd:}
        parallel vector product function extracted from \cite{falgout:2002:hypre}
        } & 2 & 712 & 2, 315 & 26 & 39\\
                            & 3 & 1, 127 & 3, 629 & 51 & 82\\
                            & 4 & 1, 546 & 5, 010 & 84 & 141 \\
                            & 5 & 1, 995 & 6, 458 & 125 & 220 \\
                            & 6 & 2, 434 & 7, 973 & 174 & 213 \\
        \hline
        \multirow{5}{5cm}{\texttt{matmat:}
        collective matrix multiplication, each process computes for
        one row
        } & 2 & 1, 155 & 3, 829 & 37 & 35\\
                            & 3 & 1, 849 & 6, 096 & 40 & 41\\
                            & 4 & 2, 551 & 8, 469 & 46 & 49\\
                            & 5 & 3, 261 & 10, 948 & 52 & 57\\
                            & 6 & 3, 979 & 13, 533 & 56 & 64\\
        \hline
        \multirow{5}{5cm}{\texttt{oddEvenSort:}
        one loop iteration in a parallel odd-even sorting implementation
        } & 2 & 1, 115 & 3, 505 & 4 & 6\\
                            & 3 & 2, 141 & 6, 699 & 6 & 8\\
                            & 4 & 3, 947 & 12, 458 & 8 & 12\\
                            & 5 & 6, 320 & 20, 217 & 10 & 13\\
                            & 6 & 10, 713 & 34, 757 & 12 & 19\\
        \hline
      \end{tabular}
    \end{small}
  \end{center}
  \caption{The experimental results of verifying MPI collective-style
    functions with respect to state-requirements and -guarantees.  The
    experiments are under an assumption that no interference can
    happen.}
  \label{tab:experimental:result:part:I-2}
\end{table}

\begin{table}[t]
  \begin{center}
  \begin{tabular}{| l | r | r | r | r | r | r |}
    \hline 
    name & \#procs & \#states & \#seen & \#trans & \#prover  & time(s)\\
    \hline
    \texttt{gather\U{}w} & 2 & 5, 953 & 5 & 19, 597 & 48 & 12\\
         & 3 & 218, 766  & 302 & 764, 096 & 123 & 208 \\
    \hline
    \texttt{allgather} & 2 & 9, 848 & 6 & 32, 855 & 31 & 22 \\
         & 3 & 164, 155 & 93 & 547, 753 & 92 & 378 \\
    \hline
    \texttt{matmat} & 2 & 3, 116 & 1 & 11, 102 & 39 & 37 \\
         & 3 & 23, 254 & 17 & 83, 359 & 48 & 75 \\
         & 4 & 342, 653 & 285 & 1, 229, 132& 110 & 704\\
    \hline
    \texttt{oddEvenSort}
         & 2 & 1, 824 & 0 & 6, 327 & 4 & 6 \\
         & 3 & 8, 706 & 8 & 30, 164 & 6 & 10 \\
         & 4 & 96, 961 & 115 & 338, 889 & 10 & 66 \\
    \hline
    \texttt{diff1dIter} & 2 & 5, 668 & 5 & 19, 745 & 35 & 10 \\
         & 3 & 492, 163 & 567 & 1, 779, 177 & 182 & 505\\
    \hline
    \texttt{diff1dExchange} & 2 & 3, 485 & 3 &  11, 300 & 21 & 8 \\
         & 3 & 114, 173 & 150 & 388, 751 & 66 & 75\\
    \hline
    \texttt{dotProd} & 2 & 1, 711 & 1 & 6, 058 & 6 & 7\\
         & 3 & 7, 127 & 5 & 25, 431 & 12 & 15\\
         & 4 & 36, 450 & 23 & 130, 936 & 18 & 43 \\
         & 5 & 225, 223 & 119 & 811, 950 & 24 & 389 \\
    \hline
  \end{tabular}
\end{center}
\caption{The experimental results of verifying full validity of MPI
  collective-style functions.}
  \label{tab:experimental:result:part:II}
\end{table}


%% verify guarantees
In the second part of the experiment, we enable the contract system to
verify the full validity of the examples listed in Table
\ref{tab:experimental:result:part:II}.  In order to let the experiment
cover all kinds of violations, we implemented a \texttt{gather\U{}w}
function using wildcard receives, which is intended to deliver the
same functionality as \texttt{gather}.  Then we assume that other
examples (i.e., \texttt{allgather} \& \texttt{matmat}) use
\texttt{gather\U{}w} instead of \texttt{gather}.

In \texttt{gather\U{}w}, a root process receives messages from others
in a non-deterministic order with wildcards.  Due to the use of 
wildcard receives, \texttt{gather\U{}w} can be interfered by
statements following itself.  Therefore, the function contract of
\texttt{gather\U{}w} shall include a path-requirement asserting that no
process shall send a message with a specific tag to root after exiting
\texttt{gather\U{}w} until the root process exits.  Otherwise, the
contract system cannot prove the validity of this function with
respect to a function contract.

For the same reason, in \texttt{allgather} and \texttt{matmat}
examples, contracts of the collective functions shall be strong enough
to make sure that the calls to \texttt{gather\U{}w} will never be
interfered.  For example, in \texttt{allgather}, a call to
\texttt{bcast} follows a call to \texttt{gather\U{}w} hence the
contract of \texttt{bcast} shall guarantee that it cannot interfere
\texttt{gather\U{}w}.

For the rest of the examples in Table
\ref{tab:experimental:result:part:II}, interference is impossible
since only deterministic send and receive operations or MPI collective
functions are used.  So for these examples, in addition to what
have been verified in the first part, their guarantees are verified in
the second part.

Most of the examples in the second part can barely be scaled to more
than 3 processes within 1, 000 seconds.  Compare to the corresponding
result in the first part, the full validity verification of an example
has to explore much more executions that are commutative to the ones
already explored in the first part.  In theory, commutative executions
will eventually run into a same state.  This explains why the numbers
of prover calls of two corresponding runs in the first part and the
second part respectively are close though the states they explored
differ significantly.  State-guarantees are barely repeatedly checked
for commutative executions.  For example, the contract system explores
only 3, 947 states for \texttt{oddEvenSort} with 4 processes in the
first part while it explores almost 25 times more states for
\texttt{oddEvenSort} with the same setting in the second part.  The
difference in the number of prover calls is only 2.

We can conclude that the current POR algorithm is sound for full
validity verification but it is insufficient to claim its
effectiveness in performance.  Either better POR algorithm or new
approach for check absence assertions is needed.

%% TODO: sound but too expensive, better POR

