\section{MPI Function Contract System Implementation} \label{sec:mpi:impl}
%intro: what are needed by a contract system starting from CIVL
%framwork ?
The implementation of the MPI function contract system in CIVL is a
solution to the following 4 problems: 1) CIVL is designed for
verifying complete programs monolithically hence cannot verify
functions separately; 2) the semantics of the contract system has
differences from the semantics of CIVL, e.g., a call to a function
with a contract shall be summarized only from the contract instead of
the function definition; 3) there is no existing primitive in CIVL
that is close to collate or collective states; 4) CIVL does not
support path predicates.

Problem 1 and 2 are tackled by AST-level code transformation, and
problem 3 and 4 are solved by implementing CIVL-C libraries for
collates and absence assertions.  Both the two methods are in keeping
with the philosophy of CIVL, which is to support a small verification
kernel well, and do the rest of the work by customized libraries and
source code transformation.

In the rest of this section, we first describe the collate library in
\S\ref{sec:mpi:impl:collate}, then explain the method of reasoning
about absence assertions in \S\ref{sec:mpi:impl:absence}.  Finally, in
\S\ref{sec:mpi:impl:transform}, we show that how does source code
transformation converts an MPI program to a CIVL-C program, which can
be verified by the common CIVL verifier with respect to the contract
system semantics.


\subsection{Implementing Collates} \label{sec:mpi:impl:collate}

One of the extensions the contract system made to CIVL is a
\texttt{collate} library.  This library provides data types and
functions to realize the collate-based algorithm for constructing
collective states.  Like the MPI library in CIVL, the \texttt{collate}
library hides the details that a collate queue is in fact a shared
object from the clients---MPI processes.  Therefore, conceptually
the \texttt{collate} library introduces no shared object.

In the library, a collate queue is implemented by a data structure,
\texttt{\$gcollator}.  A collate queue is associated with a group of
processes in a communicator.  Each process owns a process-local
handle, \texttt{\$collator}, to the collate queue.  Operations on the
collate queue can only be performed through the handle.  A collate in
the queue is implemented as a data structure,
\texttt{\$gcollate\U{}state}.  Similarly, a process can only access a
collate through a process-local handle, \texttt{\$collate\U{}state}.

The CIVL-C data structure representing the collate queue
\texttt{\$gcollator} (left) and the collate
\texttt{\$gcollate\U{}state} (right) is given in Fig.\
\ref{fig:mpi:impl:data-structure}.  The left data structure is simply
a wrap of a CIVL-C sequence of ``collate''s and two integers, the
number of processes and the number of ``collate''s in queue.  The
right data structure represents a collate.  In a collate, an array
\texttt{status} keeps the track of whether every process have copied
its snapshot to this collate.  If \texttt{status[$p$]} is true,
process $p$ has copied its snapshot to this collate.  The field
\texttt{state} holds the program state that is merged from the
snapshots that have been copied to this collate. The arrays
\texttt{requirements} and \texttt{guarantees} store the corresponding
absence assertions to this collate for each process.  The field
\texttt{isPre} labels the collate for whether it is associated to a
collective pre-state.  The field \texttt{isTarget} labels the collate
for whether it is associated to a collective state of the verifying
function.  Finally, \texttt{id} holds an identifier for the function
associated with this collate.

The \texttt{\$state} is a CIVL-C built-in type representing program
states.  The \texttt{state} field in a collate will keep being updated
via being merged with the snapshots from processes.  Once
\texttt{status[$p$]} is true for every process $p$, the collate is
completed, the \texttt{state} field becomes equivalent to the
collative state to which the collate is associated.

Following the collate management algorithm (described in
\S\ref{subsec:minimp:collate}), an object (collate) of
\texttt{\$gcollate\U{}state} type will be created and enqueued by the
first process that reaches a collective location, i.e., the entry or
exit of a contracted function.  The \texttt{id} field is initialized
during the creation.  When every following process reaches a
collective location and copies its snapshot to the collate, the
process compares its \texttt{id} value with the \texttt{id} in the
collate.  A mismatch means that there is a collective-style function
in the program that is not called by all processes collectively.

The other four fields are used by the absence assertion checking
algorithm, which will be described in the next subsection.

\begin{figure}
  \begin{center}  
    \begin{minipage}[t][][t]{.45\textwidth}
      \begin{program}
        \ccode{struct} \U{}gcollator \lb{} \\
        \ \  \ccode{int} nprocs;  \\
        \ \  \ccode{int} queue\U{}length; \\
        \ \  \$gcollate\U{}state queue[]; \\
\rb{};
      \end{program}
    \end{minipage}
    \begin{minipage}[t][][t]{.45\textwidth}
    \begin{program}
      \ccode{struct} \U{}gcollate\U{}state \lb{} \\
      \ \ \U{}Bool status[]; \\
      \ \ \$state state; \\
      \ \ \U{}Bool requirements[]; \\
      \ \   \U{}Bool guarantees[];   \\
      \ \   \U{}Bool isPre;       \\
      \ \   \U{}Bool isTarget;   \\
      \ \ \ccode{int} id;\\
      \rb{};
    \end{program}
  \end{minipage}
\end{center}
\caption{CIVL-C implementation for collate and collate queue}
\label{fig:mpi:impl:data-structure}
\end{figure}

Around these data structures, the \texttt{collate} library provides a
set of functions for the clients to interact with them.  Among those
functions, there is a pair for processes to copy their snapshots to
proper collates and to free collates collectively:

\begin{itemize}
\item[] \begin{programNoNum}
\textbf{1.}    \$collate\U{}state \$collate\U{}arrives(\$collator c, \$scope
    scope, \\
    \ \ \ \ \ \ \ \ \U{}Bool isPre, \U{}Bool isTarget, 
					  \U{}Bool requirement, \\
    \ \ \ \ \ \ \ \ \U{}Bool guarantee, \ccode{int} id);
  \end{programNoNum}
  
\item[] \begin{programNoNum}
\textbf{2.}    \ccode{void} \$collate\U{}departs(\$collator c, \$collate\U{}state cs);
  \end{programNoNum}
\end{itemize}

When a process reaches a collective location associated with a
collective-style function $g$, the process calls the
\texttt{\$collate\U{}arrives} function to save its snapshot to the
proper collate in a collate queue.  The queue is given by the
\texttt{\$collator} handle.  In addition to the snapshot, the
requirement and guarantee of $g$ of the process are stored in the
collate.  This \texttt{\$collate\U{}arrives} function returns a handle
to the accessed collate.  To free a collate, each process calls
\texttt{\$collate\U{}departs} with a handle to the collate
collectively.  Once all processes have called
\texttt{\$collate\U{}departs} for a collate, the collate will be
freed.

A snapshot of a process is also a \texttt{\$state}.  Initially, the
\texttt{state} field in a collate holds the snapshot of the first
``arrived'' process.  Then, whenever a process ``arrives'', its
snapshot will be merged into the \texttt{state} field.  Here we dig a
little deeper into this state merging process.

In CIVL, a program state is mainly a tree of \emph{dynamic scopes}
(dyscopes) and a group of call stacks.  A dynamic scope is a runtime
instance of a lexical program scope and is assigned a unique ID.  A
call stack belongs to a process.  An entry of a call stack is a
reference to a dyscope.

Figure \ref{fig:civl:state} shows a CIVL state of a CIVL-C program
transformed from a general MPI program.  Recall that the
transformation template is given in Fig.\ \ref{fig:sec:mpi:transform}.
The state belongs to a run with two MPI processes.  Note that in
addition to the two processes that run the
\texttt{\U{}mpi\U{}process}, the state includes a ``root'' process p0
that was spawned initially.  The ``parent-of'' relation in between
dyscopes depends on their lexical scopes.  If a dyscope $d$ is the
parent of another dyscope $d'$, the lexical scope of $d$ is the parent
of the lexical scope of $d'$.  For example, in Fig.\
\ref{fig:civl:state}, \textbf{d0} is a runtime instance of the root
scope $s_0$ and \textbf{d1} is a runtime instance of the lexical scope
$s_1$ of the \texttt{main} function.  So $s_0$ is the parent of $s_1$
and \textbf{d0} is the parent of \textbf{d1}.  For a lexical scope, it
can have multiple runtime instances.

\begin{figure}[t]
  \begin{center}
    \includegraphics[scale=.45]{civl-state}
  \end{center}
  \caption{A CIVL state of a CIVL-C program transformed from an
    general MPI program, which contains a function \texttt{f}.  The
    boxes labeled by \textbf{d0, d1, ...} are dyscopes.  Arrows
    between dyscopes denote the ``parent-of'' relation.  Boxes
    under ``p0, p1, p2'' are call stack entries.  Dashed arrows mark
    the referred dyscope of every call stack entry.}
  \label{fig:civl:state}
\end{figure}

In a snapshot of a process $p$ taken from a state $\omega$, the
dyscope tree contains only the dyscopes reachable by $p$ in $\omega$.
There is only one call stack in the snapshot, which belongs to $p$.

Readers now may recollect the notions of trees, lists and the least
common ancestor $\mymath{lca(t, l)}$ of a tree $t$ and a list $l$ from
Chapter \ref{chp:notation}.

For two dyscopes $d$ and $d'$ in any different dyscope trees, $d$ is
said to be equal to $d'$ iff they have the same ID.  Let
$\mymath{merge(t, l)}$ be a tree, which depends on a tree $t$ and a
list $l$.  The $\mymath{merge(t, l)}$ is obtained by appending a
sub-list $l'$ of $l$ to $\mymath{lca(t, l)}$ in $t$.  Here $l'$ is a
sub-list of $l$ such that the root of $l'$ is the child of
$\mymath{lca(t, l)}$ in $l$.

Note that the \texttt{\$collate\U{}arrives} function also takes a
\texttt{\$scope} parameter, which shall refer to the dyscope where the
process invokes the call to this function.  Let $h$ be the
\texttt{\$scope} parameter, $\omega_c$ be the \texttt{\$state} in the
collate and $\omega_p$ be the snapshot of the process $p$ that calls
\texttt{\$collate\U{}arrives}.  We use $\mymath{tree(\omega)}$ to
denote the dyscope tree of a state $\omega$.

The state merging process can be described by the following steps:

\begin{enumerate}
\item If there is no $\omega_c$, i.e., the process $p$ is the first
  process that ``arrives'' the collate, $\omega_c = \omega_p$;
  Otherwise,
  
\item let $l$ be the list that consists of $h$ and all ancestors of
  $h$ in $\mymath{tree(\omega_p)}$, we have
  $t = \mymath{merge(tree(\omega_c), l)}$;
  
\item repeatedly update $t$ for each non-top call stack entry $e$ in
  the call stack of $p$ in $\omega_p$ by that let $l'$ be the list
  that consists of $d$ and all ancestors of $d$, where $d$ is the
  dyscope referred by $e$, $t = \mymath{merge(t, l')}$;

\item finally, the merged state can be obatined by adding the call
  stack of $p$ in $\omega_p$ to
  $\omega_c[t / \mymath{tree(\omega_c)}]$.
\end{enumerate}

\begin{exmp}
  Figure \ref{fig:state:merge} shows merging a snapshot (on the
  right), which is taken from the state in Fig.\ \ref{fig:civl:state}
  for process p1, to a \emph{partially merged state} (on the left), on
  which processes are re-numbered by their ranks and are at some
  collective locations.  The merging algorithm takes the sub-list of
  the dyscopes in the snapshot that are process-local and appends it
  to dyscope \textbf{d1} in the partially merged state.  The dyscopes,
  as well as the process, from the snapshot will be renamed so that
  their names do not conflict with the ones in the state.
\end{exmp}

  \begin{figure}[t]
    \begin{center}
      \includegraphics[scale=.35]{merging}
    \end{center}
    \caption{Merging a snapshot to a state.  The snapshot (on the
      right) was taken from the state in Fig.\ \ref{fig:civl:state}
      for process p1.}
    \label{fig:state:merge}
  \end{figure}

According to such state merging process, the ``shared'' dyscopes,
i.e., the ones reachable by all processes, are coming from the
snapshot of the first ``arrived'' process.  The MPI communicators
reside in these ``shared'' dyscopes.  Following the collate management
algorihtm, message channels in the MPI communicators in a collate
shall then be updated whenever a process $p$, which has not arrived
the collate, executes a send or a receive operation.

To update the message channels in collates, the \texttt{collate}
library provides a pair of functions:

\begin{itemize}
\item \texttt{\$collate\U{}enqueue(\$collator
    c, \$comm comm, \$message m)}

\item \texttt{\$collate\U{}dequeue(\$collator
    c, \$comm comm, \$message m)}  
\end{itemize}
For every collate that has not ``arrived'' by the running process in
the queue referred by \texttt{c}, the \texttt{\$collate\U{}enqueue}
function enqueues the \texttt{\$message m} to the proper message
channel of the communicator referred by \texttt{comm} residing in the
merged state of the collate.  Recall that the source and destination
information of a \texttt{\$message} are encoded in itself.  Vice versa
for the \texttt{\$collate\U{}dequeue} function.

\subsection{Implementing Absence
  Assertions} \label{sec:mpi:impl:absence} Absence assertions in the
MPI contract language are translated to CIVL-C \emph{abstract
  functions}.  An abstract function is a mathematical uninterpreted
function.

\begin{itemize}
\item \texttt{\mygammaMPI{p}{t}} is translated to an boolean abstract
  function \texttt{\mygammaCIVL{p}{t}};
\item \texttt{\myguarantyMPI{p}{t}{q}} is translated to an boolean
  abstract function \texttt{\myguarantyCIVL{p}{t}{q}};
\item  \texttt{\mywaitsforMPI{p}} is translated to an boolean abstract
  function \texttt{\mywaitsforCIVL{p}}.
\end{itemize}

We define these abstract functions in a CIVL-C library,
\texttt{absence\U{}assertion.cvh}, which is another extension to CIVL.
In addition to these abstract functions, the library provides a set of
functions for reasoning about the absence assertions.  For example,
there is an \texttt{\$aa\U{}not\U{}exists(\U{}Bool set, \U{}Bool
  absence)} function.  It takes two boolean expressions: \texttt{set}
is the conjunction of a set of absence assertions and \texttt{absence}
is a single absence assertion.  The function returns true iff the
\texttt{absence} assertion is not an element of the \texttt{set}.  For
instance, if
\begin{align}
  \texttt{set} =&~
                   \forall{i, t}.\,  0 \leq i < n \Rightarrow{}
                   \texttt{\myguarantyCIVL{i}{t}{r}} \wedge{}
                   \texttt{\mywaitsforCIVL{p}} \nonumber \\
  \texttt{absence} = &
                       \texttt{ \myguarantyCIVL{a}{b}{c}}, \nonumber
\end{align}
the function returns
$(\forall{i}.\, 0 \leq i < n \Rightarrow{} i \not= a) \vee r \not= c$.

Absence assertions are checked for the freedom of the errors defined
in Fig.\ \ref{fig:minimp:mono:error} and
\ref{fig:modular:verify:error} when processes reach specific
locations.  We use the CIVL-C function \texttt{check\U{}guarantee}
that checks the freedom of \textbf{$\Upsilon$-violation} as an
example.  Figure \ref{fig:mpi:imple:check:upsilon} shows the
simplified CIVL-C code of this \texttt{check\U{}guarantee} function.
The function is executed immediately after a process performs a send
operation.  At line 6-10, the code searches the collate of the
collective pre-state of the verifying function by iterating the given
collate queue.  By the collate management algorithm, the search will
succeed because the goal collate will not be freed until all processes
have reached the end of the verifying function.  Line 16-20 checks for
each process $q$ that has not entered the verifying function, if the
guarantee of the function of the running process (identified by
\texttt{place} in the communicator) contains
\begin{center}
  \texttt{\myguarantyMPI{\texttt{dest}}{\texttt{tag}}{q}},
\end{center}
the guarantee is violated.


\begin{figure}[t]
  \begin{small}
  \begin{program}
    \ccode{void} check\U{}guarantee(\ccode{int} place, \ccode{int} dest, \ccode{int} tag, \ccode{int} nprocs, \\
    \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \$collator c)  \lb{} \\
    \ \   \$collate\U{}state cs; \\
    \ \  \ccode{int} queue\U{}size = \$collate\U{}queue\U{}size(c, place); \\
    \\
    \ \   \ccode{for} (\ccode{int} i = 0; i < queue\U{}size; i++)  \lb{} \\
    \ \ \ \    cs = \$collate\U{}get\U{}in\U{}queue(c, i); \\
    \ \ \ \    \ccode{if} (\$collate\U{}state\U{}is\U{}pre(cs) \&\& \$collate\U{}state\U{}is\U{}target(cs)) \\
    \ \ \ \ \ \      \ccode{break};       \\
    \ \ \rb{} \\
    \ \ \textcolor{red}{// cs must have hold the handle to the collate
      for the collective} \\
    \ \ \textcolor{red}{// pre-state of the verifying function.}\\
    \ \   \U{}Bool element;\\
    \ \ \U{}Bool set = \$collate\U{}get\U{}guarantee(cs, place);\textcolor{red}{// get my guarantee}  \\
    \\
    \ \   \ccode{for} (\ccode{int} i = 0; i < nprocs; i++) \\
    \ \ \ \  \ccode{if} (!\$collate\U{}arrived(cs, i))  \lb{} \\
    \ \ \ \ \ \ element = \$absent\U{}sendto(dest, tag, i); \\
    \ \ \ \ \ \ \$assert(\$aa\U{}not\U{}exists(element, set),\\
    \ \ \ \ \ \ \ "the guarantee
    of the verifying function is violated!"); \\
    \ \ \ \     \rb{}\\
    \rb{}
  \end{program}
  \end{small}
  \caption{The simplified code of the CIVL-C function that will be
    called everytime a send operation was performed by a process in
    order to check for the free of \textbf{$\Upsilon$-violation}.}
  \label{fig:mpi:imple:check:upsilon}
\end{figure}


\subsection{Transformation} \label{sec:mpi:impl:transform}

A \emph{contract transformer} was developed and added to CIVL for
transforming a C/MPI/CIVL-C program along with ACSL function contracts
to a pure CIVL-C program.  The transformer takes a parameter $f$,
which is the name of the verifying function, and then transforms all
the annotated functions in the original program in two ways:

\begin{enumerate}
\item For the function $f$, the transformer renames $f$ to
  $f\texttt{\U{}origin}$ and creates a new function
  $f\texttt{\U{}driver}$.  The $f\texttt{\U{}driver}$ initializes all
  the variables with respect to the state-requirement of $f$, then calls
  $f\texttt{\U{}origin}$ to launch the exploration of the original
  function body.  The state-guarantee of $f$ is checked after the
  control returns from $f\texttt{\U{}origin}$.
  
\item For every annotated function $g$ (including $f$), the
  transformer replaces the definition of $g$ with CIVL-C code that 1)
  asserts the state-requirement of $g$; 2) refreshes the objects
  specified in \texttt{assigns} clauses; 3) assumes the
  state-guarantee of $g$.
\end{enumerate}
Note that the verifying function $f$ will be transformed in both of
the ways.  This results in three different functions that all
originate from $f$: $f\texttt{\U{}driver}$, $f\texttt{\U{}origin}$ and
the $f$ with new body.

The transformation relies on a number of basic CIVL-C primitives, as
well as helper libraries that provide contract-specific data types and
functions.  A selected set of such primitives are listed below:

\begin{itemize}
   
\item \texttt{\$value\U{}at(\emph{expr}, \emph{state}, \emph{pid})}
  is an expression that represents the evaluation of
  \texttt{\emph{expr}} on \texttt{\emph{state}} by the process of
  \texttt{\emph{pid}}.  The \texttt{\BSL{}on}, as well as the
  \texttt{\BSL{}old} construct from ACSL, will be translated to this
  expression.  The ACSL \texttt{\BSL{}old} construct is same as the
  \texttt{old} in MiniMP specification language.
  
\item \texttt{\$run \emph{stmt}} is a CIVL-C statement that creates
  a new process to execute \emph{stmt}. 
  
\item \texttt{\$with(\emph{state}) \emph{stmt}} is a CIVL-C
  statement that executes the given \texttt{\emph{stmt}} starting from
  the given \texttt{\emph{state}}.
  
\item \texttt{\$havoc(\emph{pointer})} ``refreshes'' an object by
  assigning a unique and unconstrained symbolic constant to the
  object referred by the \texttt{\emph{pointer}}.
  
\item \texttt{\$mem} is a type representing a set of memory
  locations.

\item \texttt{\$mem\U{}havoc(\emph{m})} assigns a unique and
  unconstrained symbolic constant to every object in the memory
  locations in \texttt{\emph{m}}.
  
\item \texttt{\$mem\U{}contains(\emph{m0}, \emph{m1})} returns true
  iff every element in the memory location set \texttt{\emph{m1}} is
  also an element of the memory location set \texttt{\emph{m0}}.

\item \texttt{\$write\U{}set\U{}push()} informs the verifier to
  start to save all the memory locations that are modified during the
  execution.  This is implemented by pushing a new empty memory
  location set to a stack that is maintained by every process.  The
  stack is called the \emph{write set stack}.  During the execution, a
  write operation that is performed by a process $p$ on a memory
  location $m$ will cause $m$ be added into the top entry of the write
  set stack of $p$ unless the stack is empty.

\item \texttt{\$write\U{}set\U{}pop()} pops and returns the top
  entry of the write set stack of the executing processes.  When the
  write set stack is empty, the verifier will not save any memory
  location.

\item \texttt{\$mpi\U{}snapshot(\emph{comm}, \emph{scope},
    \emph{isPre}, \emph{isTarget}, \emph{requirement},
    \emph{guarantee}, \emph{function-identifier})} is a helper
  function for the transformer that wraps the
  \texttt{\$collate\U{}arrives} function.  In addition to a call to
  \texttt{\$collate\U{}arrives}, this function contains CIVL-C code
  that checks absence assertion violation and performs POR.  
  Dually, there is
  \texttt{\$mpi\U{}unsnapshot(\emph{collate\U{}state})}.

  We remark that the \texttt{\emph{comm}} parameter is of
  \texttt{MPI\U{}Comm} type.  In our extended implementation for MPI
  contracts, an MPI communicator was extended with an extra field
  holding a collate queue (i.e., a \texttt{\$gcollator}).  This is be
  in consistent with the theory that a collate queue is associated
  with a communication universe.  As a consequence,  collate queues
  that are in different MPI communicators are naturally independent.
\end{itemize}

All the MPI specific constructs in the MPI contract language are
translated to special CIVL system functions.  A system function in
CIVL is a function that is implemented in the language that writes
CIVL, i.e., Java 8 \cite{java8}, instead of CIVL-C.  For example, the
\texttt{\BSL{}mpi\U{}agree($e$)} expression in contract will be
translated to a call to the system function
\texttt{\$mpi\U{}agree($e$)}.  The system function returns true iff
every process evaluates $e$ to a same value at the current state.


\textbf{Driver Function Generation.}
For a given verifying function \texttt{f}, \texttt{f} must be assigned
a function contract.  The transformer moves the original body of
\texttt{f} to the new function \texttt{f\U{}origin}.  Then generates a
new function \texttt{f\U{}driver} with respect to the contract.
Figure \ref{fig:mpi:impl:transform:driver} summarizes the idea of
generating \texttt{f\U{}driver} with a template.

In the template, the pseudo code above the horizontal line is the
original verifying function \texttt{f} with its contract.  The
\texttt{T, T1, T2} and \texttt{T3} represent arbitrary types. The
$\psi$ and $\phi$ are boolean expressions.  The $\Delta$ represents a
list of lvalue expressions.  The $\Gamma$ and $\Upsilon$ are sets of
absence assertions.

The pseudocode below the line is the generated \texttt{f\U{}driver}
function.  The MPI communicator \texttt{comm} associated to the
collective behavior in the contract is initialized by duplicating the
\texttt{MPI\U{}COMM\U{}WORLD} (line 4).  Two variables
\texttt{\$mpi\U{}comm\U{}rank} and \texttt{\$mpi\U{}comm\U{}size} are
created to replace the constants \texttt{\BSL{}mpi\U{}comm\U{}rank}
and \texttt{\BSL{}mpi\U{}comm\U{}size} in the contract respectively.
Formal parameters are declared as local variables. These local
variables, as well as the global variables, are initialized by
unconstrained symbolic constants (line 8).

For a pointer type formal parameter $v$, one cannot assume that $v$
can be safely dereferenced unless the contract ``requires''
\texttt{\BSL{}valid($v$)}.  For such $v$, a unique object $o$ of the
referrenced type of $v$ will be declared and ``refreshed''.  The
expression \texttt{\BSL{}valid($v$)} in the state-requirement is then
replaced by \texttt{$v$ == \&$o$}.

We remark that such a transformation for \texttt{\BSL{}valid}
expressions in state-requirements is only sound under an assumption
that there is no \emph{pointer aliasing}, i.e., a pointer type formal
parameter is assumed not to refer to a program variable or an object
referred by another pointer unless it is explicited expressed in the
state-requirement.

A state-requirement is \texttt{\$assume}d in a pair of barriers so
that the state from which this \texttt{\$assume} statement is executed
will be equivalent to a collective pre-state of \texttt{f}.  Similar
for the case of \texttt{\$assert}-ing a state-guarantee.

Although for \texttt{f}, the collective pre- and post-state do not
need collates to be constructed, there are still
\texttt{\$mpi\U{}snapshot} calls.  This is because that these two
calls represent the events of entering and exiting the function
\texttt{f} respectively.  In addition, the created collective pre-state of
\texttt{f} will be used to evaluate the \texttt{\BSL{}old} expressions
in the state-guarantee.

The call to the \texttt{f\U{}origin} is surrounded by a pair of
\texttt{\$write\U{}set\U{}push} and \texttt{\$write\U{}set\U{}pop}.
By doing so, any memory location that is modified during the execution
of the original function body will be saved in \texttt{m} (line 17).
Then the validity of the frame condition can be verified by testing if
\texttt{m} is a subset of $\Delta$.

Finally, the collates created by calls to \texttt{\$mpi\U{}snapshot}
will be collectively ``destroyed'' through the calls to
\texttt{\$mpi\U{}unsnapshot} (line 26-27).

\begin{figure}
  \begin{program}
    T3 g, ...\ ; \\
    \mycomment{/*@ \ \BSL{}mpi\U{}collective(comm, $\mymath{kind}$):}\\
    \mycomment{\ \ \ \ \ \ requires $\bigwedge{\Gamma}$;}\\
    \mycomment{\ \ \ \ \ \ requires $\psi$;}\\
    \mycomment{\ \ \ \ \ \ assigns $\Delta$;}\\
    \mycomment{\ \ \ \ \ \ ensures $\phi$;}\\
    \mycomment{\ \ \ \ \ \ ensures $\bigwedge{\Upsilon}$; */}\\
    T f(T1 a, T2 * b, ...\ ) \lb{} 
     ...\ 
    \rb{}
  \end{program}
  
  \rule{\textwidth}{.5pt}
  
  \begin{program}
    \ccode{void} f\U{}driver() \lb{} \\
    \ \ \ccode{int} \$mpi\U{}comm\U{}rank, \$mpi\U{}comm\U{}size;\\
    \ \ MPI\U{}Comm comm; \\
    \ \ MPI\U{}Comm\U{}dup(MPI\U{}COMM\U{}WORLD, \&comm); \\
    \ \ MPI\U{}Comm\U{}rank(comm, \&\$mpi\U{}comm\U{}rank); \\
    \ \ MPI\U{}Comm\U{}size(comm, \&\$mpi\U{}comm\U{}size);\\
    \ \ T1 a, T2 *b, T2 b\U{}obj ...\ ; \\
    \ \ \$havoc(\&g); \$havoc(\&a); \$havoc(\&b); \$havoc(\&b\U{}obj);
    ...\; \\
     \ \ MPI\U{}Barrier(comm); \\
     \ \ \$assume($\psi$); \\
     \ \ MPI\U{}Barrier(comm); \\
    \ \ \$collate\U{}state \U{}cs\U{}pre = \$mpi\U{}snapshot(comm,
    \$here, \$true,  \$true,  \\
    \ \ \ \ $\bigwedge{}\Gamma$,  $\bigwedge{}\Upsilon$, ''f'');\\    
    \\
    \ \ \$write\U{}set\U{}push(); \\
    \ \ T \$result = f\U{}origin(comm, a, b, ...\ );\\
    \ \ \$mem m = \$write\U{}set\U{}pop();\\
    \ \ \$assert(\$mem\U{}contains($\Delta$, m));\\
    \\
    \ \ \$collate\U{}state \U{}cs\U{}post = \$mpi\U{}snapshot(comm,
    \$here, \$false, \$true, \\
    \ \ \ \  $\bigwedge{}\Gamma$,  $\bigwedge{}\Upsilon$, ''f''); \\
    \ \ MPI\U{}Barrier(comm);\\
    \ \ \$state* \U{}s\U{}pre = \$collate\U{}get\U{}state(\U{}cs\U{}pre);\\
    \ \ \$assert($\phi$); \\
    \ \ MPI\U{}Barrier(comm);\\
    \ \ \$mpi\U{}unsnapshot(\U{}cs\U{}pre);\\
    \ \ \$mpi\U{}unsnapshot(\U{}cs\U{}post); \\
    \rb{}
  \end{program}
  \caption{Transformation template for generating \texttt{f\U{}driver}
    from a function \texttt{f} with its contract. The upper shows the
    original annotated function \texttt{f} and the lower shows the
    generated \texttt{f\U{}driver}.}
  \label{fig:mpi:impl:transform:driver}
\end{figure}


\textbf{Summarizing Function Behavior From Contract.}  For every
contracted function, including the verifying function, its' original
function body will be replaced by the transformer with a CIVL-C code
that summarizes the function from the function contract.  The template
for generating such a new function body from a contract is given in
Fig.\ \ref{fig:mpi:impl:transform:callee}.

In this template, a pair of collective pre- and post-state of the
function \texttt{f} are created through calls to
\texttt{\$mpi\U{}snapshot}.  The state-requirement and -guarantee will
be evaluated on these two states, respectively, once they are
completed.  For each MPI process, it shall not wait at the location
until a collective state is completed because if doing so, the
semantics of the program gets changed.  Therefore, an MPI process will
``fork'' a new ``deamon'' process that will asynchronously waits for
the completion of a collective state and then evaluates the
state-requirement or -guarantee on the state.  The ``deamon'' process
is created by the \texttt{\$run} statement (line 10 and 21).  The
``deamon'' process will be blocked by the \texttt{\$when} statement
(line 11 and 22), in which the guard is a system function
\texttt{\$collate\U{}complete($c$)} that returns true iff the collate
referred by $c$ is completed.  Once the guard evaluates to true, the
``deamon'' process asserts (or assumes) the state-requirement (or the
state-guarantee) from the completed collective state.  The collective
state is given by a pointer, which points to the \texttt{\$state}
object in a collate (line 9 and 20).  The ``deamon'' process
terminates automatically after the assertion (or assumption).

In addition to asserting the state-requirement and assuming the
state-guarantee, the objects listed in \texttt{assigns} clauses will
be ``refreshed'' by the \texttt{\$havoc} calls.

A special variable \texttt{\$result} is created to represent the
returned value of \texttt{f}.  The expression \texttt{\BSL{}result} in
the contract will be replaced by \texttt{\$result}.

The running process will be blocked (at line 24) if it has to wait for
some other processes $p$ that have not ``entered'' this function.
Recall that the entering-function event is represented by the
transition that an MPI process marks itself on the collate associated
to the collective pre-state.  This realizes the guarantees in the
contract of the form: \texttt{\mywaitsforMPI{$\mymath{p}$}}.

\begin{figure}
  \begin{program}
    T3 g, ...\ ;\\
    T f(MPI\U{}Comm comm, T1 a, T2 *b, ...\ ) \lb{} \\
    \ \ \ccode{int} \$mpi\U{}comm\U{}rank, \$mpi\U{}comm\U{}size;\\
    \ \ MPI\U{}Comm\U{}rank(comm, \&\$mpi\U{}comm\U{}rank); \\
    \ \ MPI\U{}Comm\U{}size(comm, \&\$mpi\U{}comm\U{}size); \\
\\
  \ \ \$collate\U{}state \U{}cs\U{}pre = \$mpi\U{}snapshot(comm,
  \$here, \$true, \$false, \\
  \ \ \ \ $\bigwedge{}\Gamma$, $\bigwedge{}\Upsilon$, ''f''); \\
  \ \ \$state* \U{}s\U{}pre =
  \$collate\U{}get\U{}state(\U{}cs\U{}pre); \\
  \ \ \$run \\
  \ \ \ \ \$when (\$collate\U{}complete(\U{}cs\U{}pre))  \\
  \ \ \ \ \ \  \$with (*\U{}s\U{}pre) \$assert($\psi$); \\
  \\
  \ \ T \$result; \\
  \ \  $\mymath{\forall{d \in \Delta}.\, }$
  \$havoc(\&$d$);\\
  \ \ \$havoc(\&\$result);\\
\\
  \ \ \$collate\U{}state \U{}cs\U{}post = \$mpi\U{}snapshot(comm,
  \$here, \$false, \$false, \\
  \ \ \ \ $\bigwedge{}\Gamma$, $\bigwedge{}\Upsilon$, ''f''); \\
  \ \ \$state* \U{}s\U{}post =
  \$collate\U{}get\U{}state(\U{}cs\U{}post); \\
  \ \ \$run \\
  \ \ \ \ \$when (\$collate\U{}complete(\U{}cs\U{}post)) \\
  \ \ \ \ \ \  \$with (*\U{}s\U{}post) \$assume($\phi$);\\
  \ \ \$when(\$collate\U{}arrived(\U{}cs\U{}pre, $\mymath{p}$)); \\
  \ \ \$mpi\U{}unsnapshot(\U{}cs\U{}pre);\\
  \ \ \$mpi\U{}unsnapshot(\U{}cs\U{}post);\\
\rb{}
\end{program}
\caption{The transformation template for summarizing \texttt{f} with
  respect to its contract.}
\label{fig:mpi:impl:transform:callee}
\end{figure}

\begin{comment}
\begin{exmp}
  For the function \texttt{ring} given in Fig.\ \ref{}, we present the
  \texttt{ring\U{}driver} function in Fig.\
  \ref{exmp:mpi:contract:ring} and the transformed \texttt{ring}
  function in Fig.\ \ref{exmp:mpi:impl:ring-driver}. $\qed$
\end{exmp}


\begin{figure}
  \begin{program}
    \ccode{int} rank, size;\\
    ...\ \\
    \ccode{void} ring\U{}driver() \lb{}\\
    \ \   \ccode{int} \$mpi\U{}comm\U{}rank, \$mpi\U{}comm\U{}size; \\
    \ \   MPI\U{}Comm comm;\\
    \ \   MPI\U{}Comm\U{}dup(MPI\U{}COMM\U{}WORLD, comm);\\
    \ \   MPI\U{}Comm\U{}rank(comm, \&\$mpi\U{}comm\U{}rank); \\
    \ \ MPI\U{}Comm\U{}size(comm,   \&\$mpi\U{}comm\U{}size);  \\
    \\
    \ \  \$havoc(\&rank); \$havoc(\&size);\\
    \ \  MPI\U{}Barrier(comm);\\
    \ \ \$assume(rank == \$mpi\U{}comm\U{}rank \&\& size ==
    \$mpi\U{}comm\U{}size);\\
    \ \  MPI\U{}Barrier(comm);\\
    \ \ \$collate\U{}state \U{}cs \U{}pre =
    \$mpi\U{}snapshot(comm, \$here, 1, 1, 1, 1, \\
    \ \ \ \ ''ring'');\\
    \\
    \ \  \$write\U{}set\U{}push();\\
    \ \ ring\U{}origin();\\
    \ \ \$mem m = \$write\U{}pop\U{}push();\\
    \ \ \$assert(\$mem\U{}contains((\$mem)\&buf, m));\\
    \\
    \ \ \$collate\U{}state \U{}cs \U{}post =
    \$mpi\U{}snapshot(comm, \$here, 0, 1, 1, \\
    \ \ \ \ \$abent\U{}exit((rank + 1) \% size), ''ring'');\\
    \ \  MPI\U{}Barrier(comm);\\
    \ \ \$state * \U{}s\U{}post = \$collate\U{}get\U{}state(\U{}cs\U{}post);\\
    \ \ \$assert(\$value\U{}at(buf, *\$state\U{}post, (rank + 1) \%
    size) == data);\\
        \ \  MPI\U{}Barrier(comm);\\
    \ \ \$mpi\U{}unsnapshot(\U{}cs\U{}pre); \\
    \ \ \$mpi\U{}unsnapshot(\U{}cs\U{}post);\\
    \rb{}\\
  \end{program}
  \caption{The \texttt{ring\U{}driver} function created by the
    contract transformer.  This function verifies that whether
    \texttt{ring} satisfies its function contract.}
  \label{exmp:mpi:impl:ring-driver}
\end{figure}

  
\begin{figure}
  \begin{program}
    \ccode{int} ring() \lb{}  \\
    \ \   \ccode{int} \$mpi\U{}comm\U{}rank, \$mpi\U{}comm\U{}size; \\
    \ \   MPI\U{}Comm\U{}rank(comm, \&\$mpi\U{}comm\U{}rank); \\
    \ \ MPI\U{}Comm\U{}size(comm,
    \&\$mpi\U{}comm\U{}size);   \\
    \ \ \$collate\U{}state \U{}cs\U{}pre =
    \$mpi\U{}snapshot(comm, \$here, 1, 0, 1, 1, \\
    \ \ \ \ ''ring''); \\
    \ \ \$state* \U{}s\U{}pre =
    \$collate\U{}get\U{}state(\U{}cs\U{}pre);\\
    \ \ \$run \$when (\$collate\U{}complete(\U{}cs\U{}pre)) \\
    \ \ \ \  \$with (*\U{}s\U{}pre) \\
    \ \ \ \ \ \ \$assert(rank == \$mpi\U{}comm\U{}rank \&\& size ==
    \$mpi\U{}comm\U{}size);\\
    \ \ \$havoc(\&buf); \\ \\
    \ \ \$collate\U{}state \U{}cs\U{}post = \$mpi\U{}snapshot(comm,
    \$here, 0, 0, 1, \\
    \ \ \ \ \$absent\U{}exit((rank + 1) \% size), ''ring''); \\
    \ \ \$state* \U{}s\U{}post =
    \$collate\U{}get\U{}state(\U{}cs\U{}post);\\
    \ \ \$run \$when (\$collate\U{}complete(\U{}cs\U{}post)) \\
    \ \ \ \  \$with (*\U{}s\U{}post) \\
    \ \ \ \ \ \ \$assume(\$value\U{}at(buf, \$state\U{}null, (rank +
    1) \% size) == data);\\
    \ \ \$when (\$collate\U{}arrived(
    \U{}cs\U{}pre, (rank + 1) \% size,)); \\
    \ \ \$mpi\U{}unsnapshot(\U{}cs\U{}pre); \\
    \ \ \$mpi\U{}unsnapshot(\U{}cs\U{}post); \\
    \rb{}\\
  \end{program}
  \caption{The \texttt{ring} function after transformation.  The
    original function body is replaced with CIVL-C code that
    summarizes the behavior of \texttt{ring} with respect to its
    contract.}
  \label{exmp:mpi:impl:ring}
\end{figure}
\end{comment}