\section{Correctness of MiniMP Programs} \label{sec:correct-minimp}
In this section, we discuss the properties about correctness of MiniMP
programs.  Intuitively, a program is considered correct if nothing bad
will happen in any execution of it and it produces the correct result.
For MiniMP programs, programmers will also want to make sure that it
will always terminate.  The properties that are about nothing bad
happens in executions are called \emph{safety properties}.  We say a
program is functionally correct if it produces the correct result.
Whether a program will always terminate belongs to the termination
problem.

For MiniMP programs, safety properties can be violated if an
evaluation results in the undefined value---\textbf{UNDEF}. For
example, during the execution of a program, if such an expression
\texttt{1/0} is evaluated, it reuslts in \textbf{UNDEF} and the
program is considered incorrect.  

If a MiniMP program will not terminate, it must be one of the two
situations:
\begin{enumerate}
\item there is a deadlock, i.e. the program runs into a state where at
  least one process has not terminated and there is no transition can
  depart from the state.
\item there is an infinite loop or recursion.
\end{enumerate}

Deadlock is a common error in parallel programs.  We give the
following as an example that a MiniMP program will always run into a
deadlock:
\begin{center}
  \begin{program}
    \ccode{int} main() \lb{}\\
    \ \ \ccode{int} x;\\
    \ \ recv(x, 0); \\
    \rb{}
  \end{program}
\end{center}
A transition associated with a \texttt{recv} action can depart from a
state only if the corresponding communication channel is not empty.
Since there is no \texttt{send} statement in this example,
communication channels are always empty, any run of this example will
end with a state $s$ where all processes are at the location before
the \texttt{recv} action while no transition can depart from $s$.   

In some programming areas, such as reactive systems, programs are
designed to run until interruptions and written with infinite loops.
But MiniMP is not belong to these areas hence infinite loops or
recursions are considered errors.  A MiniMP program may run into an
infinite loop or recursion if and only if the state space of the
program has infinite states or contains cycles.  For example,
executing the \texttt{while(true) x++;} loop from a state $s_0$ will
result in an infinite path $s_0s_1...$.  For another example, after
the second time executing the \texttt{while(true) x = 0;} loop from a
state $s$ will always result in the same state $s$, which forms a
cycle.

We categorize the safety properties and properties about termination
as \emph{standard properties}.  These properties are specified by the
programming language itself.  One can decide if there is a standard
property violation in a program without knowing the purpose of the
program.

%% what is correct is defined in semantics of contracts, here we show
%% some examples that violate the contract and point out that wildcard
%% can be error-prone.
Unlike the standard properties, functional correctness is
user-specified.  Functional correctness states the purpose of a
program or a function.  For MiniMP programs, their functional
correctness is specified as function contracts by the users.  A
function contract can be seen as a specification of a MiniMP function.
Function contract of a \texttt{main} function can be seen as a
specification of a whole MiniMP program.  

A MiniMP function $f$ is functionally correct if and only if $f$
satisfies its function contract, i.e. $FG'_f \models C_f$.  For any
caller to $f$, it the caller fails to satisfy the pre-condition of
$f$, the caller function is functionally incorrect.

Finally, we want to point out that using a wildcard receive statement
in a collective-style function can be error-prone.  Consider the
following \texttt{max} function:
\begin{center}
  \begin{program}
    \ccode{int} max(\ccode{int} val) \\
assigns \BSL{}nothing;\\
collective:\\
\ \ ensures !(val > \BSL{result}@0); \\
\ \ behavior root: \\
\ \ \ \ assume PID == 0; \\
\ \ \ \ waitsfor 1 ..\ NPROCS-1; \\
\ \ behavior nonroot: \\
\ \ \ \ assume PID != 0; \\
\ \ \ \ waitsfor \BSL{}nothing; \\
\lb{} \\
\ \ \ccode{int} max = val; \\
\ \    \ccode{if} (PID == 0) \lb{} \\
\ \ \ \ \ccode{int} recved = 1; \\
\ \ \ \ \ccode{while} (recved < NPROCS) \lb{} \\
\ \ \ \ \ \ \ccode{int} src; \\
\ \ \ \ \ \ recv(any src, val); \\
\ \ \ \ \ \ \ccode{if} (val > max) \lb{} \\
\ \ \ \ \ \ \ \ max = val; \\
\ \ \ \ \ \ \rb{}\\
\ \ \ \ recved = recved + 1; \\
\ \ \ \ \rb{} \\
\ \    \rb{} \ccode{else} \lb{} \\
\ \ \ \ send(0, val);\\
\ \    \rb{}\\
\ \ \ccode{return} max;\\
\rb{}
  \end{program}
\end{center}
This \texttt{max} function was intended to be a collective-style
function and hence was assigned a function contract.  However,
\texttt{max} is not a collective-style function hence it cannot
satisfy the function contract.  Suppose \texttt{max} is called in such
a program:
\begin{center}
  \begin{programContinue}{27}
    \ccode{int} main() \lb{} \\
\ \    \ccode{int} m; \\
\ \    m = max(PID); \\
\ \    m = max(PID);\\
\rb{}
  \end{programContinue}
\end{center}
We can find an execution $\pi$ of the program above with 3 processes
such that
\begin{align}
  &
  \mymath{coState(loc_{0_\texttt{max}}, \pi, 1) \not= \xi} \nonumber \\
  \wedge~ & (\forall{p, p'}.\,\mymath{comm(coState(loc_{0_\texttt{max}}, \pi, 1))(p, p') = \epsilon}, 
  \text{for } 0 \leq p, p' < 3) \nonumber \\
  \wedge~ & \mymath{coState(loc_{{ret}_\texttt{max}}, \pi, 1) \not= \xi}  \nonumber \\
  \wedge~ & (\exists{p, p'}.\,\mymath{comm(coState(loc_{{ret}_\texttt{max}}, \pi, 1))(p, p') \not= \epsilon}, 
  \text{for } 0 \leq p, p' < 3)\nonumber
\end{align}, which makes \texttt{max} fail to satisfy the conditions for collective-style functions.  
Here we show a prefix of such an $\pi$:
\begin{align}
  &t_0 : (s_0, 1, 30, \texttt{true}, \texttt{call max}, 12, s_1) \nonumber \\
  &t_1 : (s_1, 1, 12, \texttt{true}, \texttt{max = val}, 13, s_2) \nonumber \\
  &t_2 : (s_2, 1, 13, \texttt{!(PID == 0)}, \texttt{send val to 0}, 26, s_3) \nonumber \\
  &t_3 : (s_3, 1, 26, \texttt{true}, \texttt{ret max}, 31, s_4) \nonumber \\
  &t_4 : (s_4, 1, 31, \texttt{true}, \texttt{call max}, 12, s_5) \nonumber \\
  &t_5 : (s_5, 1, 12, \texttt{true}, \texttt{max = val}, 13, s_6) \nonumber \\
  &t_6 : (s_6, 1, 13, \texttt{!(PID == 0)}, \texttt{send val to 0}, 26, s_7) \nonumber \\
  &t_7 : (s_7, 0, 30, \texttt{true)}, \texttt{call max}, 12, s_8) \nonumber \\
  &t_8 : (s_8, 0, 12, \texttt{true)}, \texttt{max = val}, 13, s_9) \nonumber \\
  &t_9 : (s_9, 0, 13, \texttt{PID == 0}, \texttt{recved = 1}, 15, s_{10}) \nonumber \\
  &t_{10} : (s_{10}, 0, 15, \texttt{recved < NPROCS}, \texttt{recv val from any src}, 18, s_{11}) \nonumber \\
  &t_{11} : (s_{11}, 0, 18, \texttt{val > max}, \texttt{max = val}, 21, s_{12}) \nonumber \\
  &t_{12} : (s_{12}, 0, 21, \texttt{true}, \texttt{recved = recved + 1}, 15, s_{13}) \nonumber \\
  &t_{13} : (s_{13}, 0, 15, \texttt{recved < NPROCS}, \texttt{recv val from any src}, 18, s_{14}) \nonumber\\
  & ... \nonumber
\end{align}
In this execution $\pi$, process 1 completes two send statements in
two different calls to \texttt{max} before process 0 and process 2
entering the first \texttt{max} call.  Because of the wildcard receive
statement, process 0 can receive messages from any process.  In $\pi$,
process 0 consecutively receives the 2 messages sent by process 1.
This is where an unexpected error occurs, process 0 in the first call
to \texttt{max} receives a message sent by process 1 from its second
call to \texttt{max}.  Eventually, the collective post-state, where
all 3 processes are first time at the exit of \texttt{max}, will have
a non-empty communication channel.  Hence function \texttt{max} is not
a collective-style function, so it will not satisfy the collective
function contract.

The wildcard receive statement introduces non-determinism into
programs.  Non-determinism is one of the challenges for programmers to
write correct parallel programs.  The next chapter will introduce
approaches for verifying the correctness of MiniMP programs.  We will
mainly focus on the functional correctness of collective-style
functions.  We will also show how to verify the safety properties and
free of deadlock for MiniMP programs.

\begin{lema}
  \textcolor{red}{TODO:} ``a collective-style function satisfies a function contract
  must make sure that in every execution of every model, every
  collective pre-state has empty message channels''
\end{lema}

\begin{lema}
  \textcolor{red}{TODO:} ``a non collective-style function will never satisfies a function contract''
\end{lema}

\begin{lema}
  \textcolor{red}{TODO:} ``a collective-style function satisfies a
  function contract'' implies ``every message sent by one of
  the collective instances must be received by one of the same group
  of collective instances''
\end{lema}

\textcolor{red}{TODO:}  how to prove ``every message sent by one of
  the collective instances must be received by one of the same group
  of collective instances'' ?