\section{The MPI Contract Language} \label{sec:mpi:contract_language}

We designed the contract language for C/MPI based on an existing
specification language ACSL, which is for specifying sequential C
programs.  ACSL provides rich primitives for describing program
behaviors and constructing logic proofs.  An ACSL function contract is
a pair of pre- and post-conditions that are in the form of a C program
annotation.  We extended ACSL with a few primitives for MPI and
concurrency.

\begin{figure}
  \begin{center}
    \begin{program}
    /*@ requires \BSL{}valid(a) \&\& \BSL{}valid(b); \\
    \ \ \ \ assigns \BSL{}nothing;\\
    \ \ \ \ behavior GT: \\
    \ \ \ \ \ \ assumes *a > *b;\\
    \ \ \ \ \ \ ensures \BSL{}result == *a - *b;\\
     \ \  \ \ behavior LTE: \\
    \ \ \ \ \ \ assumes *a <= *b;\\
    \ \ \ \ \ \ ensures \BSL{}result == *b - *a;\\
    */ \\
  \ccode{int} diff(\ccode{int} *a, \ccode{int} *b) \lb{} \\
  \ \ \ccode{if} (*a > *b) \ccode{return} *a - *b; \\
  \ \ \ccode{else} \ccode{return} *b - *a;\\
  \rb{}\\
\end{program}
\end{center}
\caption{A sequential C function with an ACSL contract.}
\label{fig:exmp:pure-acsl}
\end{figure}

\begin{exmp}
  Figure \ref{fig:exmp:pure-acsl} presents a simple example of a C
  function with its ACSL function contract.  The \texttt{requires},
  \texttt{assigns}, \texttt{ensures} clauses also appear in \minimp{}
  specification language and they remain their meanings in ACSL.
  Ditto for \texttt{\BSL{}result}.  The \texttt{\BSL{}nothing}
  expression stands for an empty set of memory location.  A
  \texttt{\BSL{}valid($\textsf{pts}$)} construct asserts that it is
  safe to dereference a pointer in the pointer set $\textsf{pts}$.  A
  \texttt{behavior} that is identified by a \emph{name} specifies a
  pair of pre- and post-conditions under a specific assumption.  The
  \texttt{assumes} clause in a behavior introduces the assumption.
  $\qed$
\end{exmp}

In this section, we mainly describe our extension for MPI to the ACSL.
Original ACSL constructs will be explained when they are involved.

\subsection{Syntax}
The syntax of the MPI contract language is given in Fig.\
\ref{fig:mpi:spec:syntax}.  An MPI function contract is a set of
\emph{behaviors}.  There are two kinds of behaviors in ACSL, the
\emph{default behavior} and \emph{named behaviors}.  The default
behavior is the set of \emph{clauses} before any named behaviors.  A
named behavior starts with the keyword \texttt{behavior} and is
identified by a \emph{name}.  A named behavior also consists of a set
of clauses.

\begin{figure}[h]
  \begin{programNoNum}
    \nonterm{Contract} \ \ \ \ \ \ \ \ \ \ \ := \nonterm{Behaviors} \nonterm{CollectiveBehaviors}\\
    \nonterm{Behaviors} \ \ \ \ \ \ \ \ \ \ := \nonterm{BehaviorBody} \nonterm{NamedBehavior}\textit{*}\\
    \nonterm{CollectiveBehaviors} := \BSL{}mpi\U{}collective
    (\nonterm{Expr}, \nonterm{CollectiveKind}):\ \nonterm{Behaviors}\\
    \nonterm{NamedBehavior}  \ \ \ \ \ \ := behavior
    \nonterm{Identifier} :\ \nonterm{BehaviorBody} \\
    \nonterm{CollectiveKind} \ \ \ \ \ := P2P $\mid$ COL \\
    \nonterm{BehaviorBody} \ \ \ \ \ \ \ := \nonterm{Clause}$^*$\\
  \end{programNoNum}
  \caption{The syntax of the behaviors of the MPI contract
    language.}
  \label{fig:mpi:spec:syntax}
\end{figure}

Our extension adds two higher-level structures to ACSL behaviors:
\emph{local behavior} and \emph{collective behaviors}.  The local
behavior in a function contract is the set of ACSL behaviors before
any collective behavior.  A collective behavior starts with the
keyword \texttt{\BSL{}mpi\U{}collective}, which is followed by two
parameters: an expression of \texttt{MPI\U{}Comm} type and a constant
denoting the \emph{collective kind}.  The former one refers to an MPI
communicator.  The latter one can either be \texttt{P2P}, which stands
for ``point-to-point'', or \texttt{COL}, which stands for
``collective''.  These two parameters together identify a
communication universe.  A collective behavior consists of a set of
ACSL behaviors as well.  

Clauses in the MPI contract language are same as the ones in ACSL.
For expressions, a few new constructs for MPI and concurrency are
added to ACSL.  The syntax of these new expressions is given in
Fig.\ \ref{fig:mpi:contract:expr_syntax}.

Recall the syntax of \minispec{} in \S\ref{sec:minimp:spec:syntax},
\acslon{} is not allowed to be used in absence assertions.  Following
the same spirit, we remark that MPI contract language restricts the
expressions in absence assertions to be process-local, i.e., no
``\texttt{\BSL{}on}'' can appear in an absence assertion.

\begin{figure}
  \begin{programNoNum}
    \nonterm{Expr} \ \ \ \ \ \ :=
    \nonterm{ACSL-Expr} $\mid$ \nonterm{MPIExpr} $\mid$
    \BSL{}on(\nonterm{Expr}, \nonterm{Expr}) \\
    \nonterm{MPIExpr} \ \ \ :=
    \BSL{}mpi\U{}comm\U{}rank $\mid$ \BSL{}mpi\U{}comm\U{}size $\mid$
    \BSL{}mpi\U{}extent(\nonterm{Expr}) \\
    \ \ \ \ \ \ \ \ \ \ \ \ $\mid$
    \BSL{}mpi\U{}offset(\nonterm{Expr},
    \nonterm{Expr}, \nonterm{Expr})
    \\
        \ \ \ \ \ \ \ \ \ \ \ \ $\mid$
    \BSL{}mpi\U{}region(\nonterm{Expr},
    \nonterm{Expr}, \nonterm{Expr})
    \\
        \ \ \ \ \ \ \ \ \ \ \ \ $\mid$
    \BSL{}mpi\U{}valid(\nonterm{Expr},
    \nonterm{Expr}, \nonterm{Expr})
    \\
        \ \ \ \ \ \ \ \ \ \ \ \ $\mid$
        \BSL{}mpi\U{}agree(\nonterm{Expr}) \\
        \ \ \ \ \ \ \ \ \ \ \ \ $\mid$
        \BSL{}mpi\U{}equals(\nonterm{Expr}, \nonterm{Expr}) 
        \\
        \ \ \ \ \ \ \ \ \ \ \ \ $\mid$
        \BSL{}mpi\U{}reduce(\nonterm{Expr}, \nonterm{Expr},
        \nonterm{Expr}, \nonterm{Expr})
        \\
        \ \ \ \ \ \ \ \ \ \ \ \ $\mid$
        \BSL{}absenceof \nonterm{Event} \BSL{}after \nonterm{Event}
        \BSL{}until \nonterm{Event}
        \\
        \nonterm{Event} \ \ \ \ \ :=
        \BSL{}sendto(\nonterm{Expr},
        \nonterm{Expr}) $\mid$ \BSL{}sendfrom(\nonterm{Expr},
        \nonterm{Expr})
        \\
        \ \ \ \ \ \ \ \ \ \ \ \ $\mid$
        \BSL{}enter(\nonterm{Expr}) $\mid$ \BSL{}enter\\
        \ \ \ \ \ \ \ \ \ \ \ \ $\mid$
        \BSL{}exit(\nonterm{Expr}) $\mid$ \BSL{}exit\\
  \end{programNoNum}
  \caption{The syntax of the expression of the MPI contract language.
    The \nonterm{ACSL-Expr} stands for the expression syntax of ACSL.}
  \label{fig:mpi:contract:expr_syntax}
\end{figure}

\begin{figure}
  \begin{center}
 \begin{programSmall}
    \ccode{int} rank, size, data, buf; \\
    \ ...\ \\
    \mycomment{/*@}\\
    \mycomment{\BSL{}mpi\U{}collective(MPI\U{}COMM\U{}WORLD, P2P):}\\
    \mycomment{\ \ requires rank == \BSL{}mpi\U{}comm\U{}rank \&\&
      size == \BSL{}mpi\U{}comm\U{}size;}\\
    \mycomment{\ \ assigns buf;}\\
    \mycomment{\ \ ensures \BSL{}on((rank + 1) \% size, buf) == data \&\&}\\
    \mycomment{\ \ \ \ \ \ \ \ \ \
      \BSL{}absenceof \BSL{}exit \BSL{}after \BSL{}enter \BSL{}until}
    \mycomment{\BSL{}enter((rank + 1) \% size));} \\
    \mycomment{*/}\\
    \ccode{int} ring() \lb{} \\
    \ \  \ccode{int} left = (rank + size - 1) \% size; \\
    \ \  \ccode{int} right = (rank + 1) \% size; \\
   \ \  MPI\U{}Sendrecv(\&data, 1, MPI\U{}INT, left, 0,\\
   \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \&buf, 1, MPI\U{}INT, right,
   0, MPI\U{}COMM\U{}WORLD); \\
    \rb{}
  \end{programSmall}
\end{center}
  \caption{A collective-style MPI function \texttt{ring} with a
    contract.}
  \label{fig:mpi:ring:contract}
\end{figure}

%% meaning of collective behavior
\subsection{Semantics}

A local behavior specifies the \emph{process-local properties}.  A
collective behavior specifies \emph{global properties} of a
collective-style function.  A global property may involve multiple
processes and must be satisfied by all processes.  Absence assertions
in a collective behavior are independent with ones in another
collective behavior if the two collective behaviors are associated
with different communication universes.

Furthermore, there are two implicit assertions in every collective
behavior: 1) a state-requirement asserting that the message channels
in the associated communication universe are all empty and 2) a
post-condition asserting the same property.

The interpretation of a local behavior is based on the process state
of the process that reaches the entry or exit of a contracted
function.  Collective behaviors in theory shall be interpreted in a
similar way as \minimp{} contracts with respect to collective states.
In fact, the interpretation of MPI contracts is simpler: a
state-requirement or -guarantee is still evaluated on corresponding
collective pre- or post-state; a path-requirement or -guarantee is
partially evaluated at the source state of a global transition
representing the entering of the corresponding function by a process.
This simplification is correct because only process-local expressions
are allowed to be used in absence assertions.


%% meaning of the new primitives:
Meanings of the constructs for MPI and concurrency are informally
described as the follows:

\begin{itemize}
\item \texttt{\BSL{}on($\textsf{rank}$, $\textsf{expr}$)} represents
  the value of the expression $\textsf{expr}$ that is evaluated by a
  process of rank $\textsf{rank}$.

\item \texttt{\BSL{}mpi\U{}comm\U{}rank} is a constant that stands for
  the rank of the running process.

\item \texttt{\BSL{}mpi\U{}comm\U{}size} is a constant that stands for
  the size of the communicator.

\item \texttt{\BSL{}mpi\U{}extent($\textsf{datatype}$)} represents the
  bytewise size of the \texttt{MPI\U{}Datatype} $\textsf{datatype}$.

\item \texttt{\BSL{}mpi\U{}offset($\textsf{buf}$, $\textsf{count}$,
    $\textsf{datatype}$)} is such a pointer:
  \begin{center}
    \texttt{(char *)$\textsf{buf}$ + $\textsf{count}$ * \BSL{}mpi\U{}extent($\textsf{datatype}$)}
  \end{center}

\item \texttt{\BSL{}mpi\U{}region($\textsf{buf}$, $\textsf{count}$,
    $\textsf{datatype}$)} represents the value in a memory region
  that spans from the address \texttt{$\textsf{buf}$} to the
  length of \texttt{$\textsf{count}$ *
    \BSL{}mpi\U{}extent($\textsf{datatype}$)} bytes.

\item \texttt{\BSL{}mpi\U{}agree($\textsf{expr}$)} asserts that all
  processes must have the same value for $\textsf{expr}$.

\item \texttt{\BSL{}mpi\U{}valid($\textsf{buf}$, $\textsf{count}$,
    $\textsf{datatype}$)} asserts that the memory region spanning from
  the address \texttt{$\textsf{buf}$} to the length of
  \texttt{$\textsf{count}$ * \BSL{}mpi\U{}extent($\textsf{datatype}$)} bytes
  is accessible.

\item \texttt{\BSL{}mpi\U{}equals($r_0$,
    $r_1$)} asserts that values in the two given memory
  regions $r_0$ and $r_1$ are the same.

\item \texttt{\BSL{}mpi\U{}reduce($\textsf{buf}$, $\textsf{count}$,
    $\textsf{datatype}$, $\textsf{op}$)} represents the reduction
  value of the operation $\textsf{op}$ over
  \begin{align}
    & \texttt{\BSL{}mpi\U{}region(\BSL{}on(0, $\textsf{buf}$), $\textsf{count}$,
      $\textsf{datatype}$)}, \nonumber \\
    & \texttt{\BSL{}mpi\U{}region(\BSL{}on(1, $\textsf{buf}$), $\textsf{count}$,
      $\textsf{datatype}$)}, \nonumber \\
    & ..., \nonumber \\
    & \texttt{\BSL{}mpi\U{}region(\BSL{}on(n-1, $\textsf{buf}$), $\textsf{count}$,
      $\textsf{datatype}$)},  \nonumber 
  \end{align}
  where $\textsf{op}$ has \texttt{MPI\U{}Op} type and $n = $
  \texttt{\BSL{}mpi\U{}comm\U{}size}.

\item \texttt{\BSL{}absenceof $\theta_0$ \BSL{}after $\theta_1$
    \BSL{}until $\theta_2$} represents an absence assertion, where
  $\theta_0$, $\theta_1$ and $\theta_2$ are events.
  
\item \texttt{\BSL{}sendto($\textsf{dest}$, $\textsf{tag}$)} is an
  event representing the transitions that the running process sends a
  message with $\textsf{tag}$ to a process of rank $\textsf{dest}$.

\item \texttt{\BSL{}sendfrom($\textsf{src}$, $\textsf{tag}$)} is an
  event representing the transitions that a process of rank
  $\textsf{src}$ sends a message with $\textsf{tag}$ to the running
  process.

\item \texttt{\BSL{}enter($\textsf{rank}$)} is an event representing
  the transitions that the process of $\textsf{rank}$ enters the
  specified function.  Optionally, \texttt{\BSL{}enter} is a shortcut
  for \\ \texttt{\BSL{}enter(\BSL{}mpi\U{}comm\U{}rank)}.

\item \texttt{\BSL{}exit($\textsf{rank}$)} is an event representing
  the transitions that the process of $\textsf{rank}$ exits the
  specified function.  Optionally, \texttt{\BSL{}exit} is a shortcut
  for \\ \texttt{\BSL{}exit(\BSL{}mpi\U{}comm\U{}rank)}.
  
\end{itemize}
Names of clauses (i.e., state-requirement and -guarantee,
path-requirement and -guarantee) in MPI contract language are
inherited from \minimp{}.  The Restriction \ref{rest:absent:1} on
absence assertions in \minimp{} is also inherited by MPI contract
language with a natural extension.


\begin{exmp}
  The function contract in Fig.\ \ref{fig:mpi:ring:contract} consists
  of a collective behavior that is associated with the point-to-point
  communication universe of the default MPI communicator.  The
  collective behavior requires that for every process, the
  \texttt{rank} and \texttt{size} shall hold the rank of the process
  in \texttt{MPI\U{}COMM\U{}WORLD} and the size of
  \texttt{MPI\U{}COMM\U{}WORLD} respectively.  The contract states
  that no memory location of any process will be modified in
  \texttt{ring} except \texttt{buf}.  The contract ensures that on the
  state where all processes collectively exit \texttt{ring}, for every
  process, the value of \texttt{buf} equals to the value of
  \texttt{data} on its right neighbor.  Finally, \texttt{ring}
  guarantees that a process will not exit \texttt{ring} until its right
  neighbor enters \texttt{ring}. $\qed$
\end{exmp}