%%%%%%%%%%% Expression grammar %%%%%%%%%%%%%%%
In this chapter, we introduce a ``toy'' message-passing programming
language---\minimp{} for the purpose of focusing on message-passing
only.  Real programming languages have too much complexities, such as
pointers and memory allocations in C language, that are essentially
irrelevant to the theory of our approach.

\minimp{} contains a minimal set of basic primitives that are common
in most of the imperative programming languages, such as C or Java.
There are procedures in \minimp{} because this dissertation is about
decomposing a program into procedures.  Procedure parameters are all
pass by value.  There are also arrays since they play one of the most
important roles in many algorithms.  To keep the syntax of \minimp{}
simple, this language is dynamically typed.


For message-passing, \minimp{} provides the basic send and receive
operations.  Unlike MPI, in \minimp{}, messages have no tag and there
is a single communication universe for all processes.  \minimp{} does
allow the use of wildcards in receive operations.

\minimp{} will be used to illustrate the idea of our approaches
through Part \ref{part:2} of this dissertation.  The syntax of
\minimp{} is given in \S\ref{sec:minimp:syntax}.  We describe an
abstract representation, called the ``\minimp{} model'', of this
language in \S\ref{sec:minimp:model}.  The semantics of \minimp{} is
then defined using the \minimp{} model in
\S\ref{sec:minimp:semantics}.

\section{Syntax} \label{sec:minimp:syntax}
\begin{figure}[h]
  \scalebox{.9}{
    \begin{programNoNum}
      \nonterm{List-of-T} \ \ \ \ \synxdef{} \nonterm{T} \biglp{},
      \nonterm{T}\bigrp{}\regxstar{} $\synxbar$ \\
      \nonterm{Constant} \ \ \ \ \ \synxdef{} true $\synxbar$ false $\synxbar$
      \nonterm{IntegerLiteral} $\synxbar$
      $\synxdots{}$   \\
      \nonterm{UnOp} \ \ \ \ \ \ \ \ \ \synxdef{} \texttt{-} $\synxbar$ \texttt{!\
      }$\synxbar$ $\synxdots{}$ \\
      \nonterm{BinOp} \ \ \ \ \ \ \ \ \synxdef{} \texttt{+} $\synxbar$ \texttt{-}
      $\synxbar$ \texttt{*} $\synxbar$ \texttt{/}
      $\synxbar$ \texttt{==} $\synxbar$ \texttt{!=} $\synxbar$ \&\&
      $\synxbar$ || $\synxbar$ ==>  $\synxbar$ 
      $\synxdots{}$ \\
      \nonterm{Expr} \ \ \ \ \ \ \ \ \ \synxdef{} PID $\synxbar$ NPROCS $\synxbar$
      \nonterm{Constant} $\synxbar$ \char`(~\nonterm{Expr} \char`){}
      $\synxbar$ \nonterm{LExpr} $\synxbar$
      len ( \nonterm{LExpr} ) \\
      \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $\synxbar$ \nonterm{UnOp}
      \nonterm{Expr} $\synxbar$ \nonterm{Expr} \nonterm{BinOp}
      \nonterm{Expr}
      $\synxbar$ \ccode{new} [ \nonterm{Expr} ] $\synxbar$
      \lb{} \nonterm{List-of-Expr} \rb{}
      \\
      \nonterm{LExpr} \ \ \ \ \ \ \ \ \synxdef{} \nonterm{Identifier} $\synxbar$
      \nonterm{LExpr} [
      \nonterm{Expr} ] \\
      \nonterm{Statement} \ \ \ \ \synxdef{} \nonterm{LExpr} =
      \nonterm{Expr} ; \\
      \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $\synxbar$ if ( \nonterm{Expr} ) \nonterm{Statement} \biglp{}\ccode{else} \nonterm{Statement}\bigrp{}\regxques{} \\
      \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $\synxbar$ \biglp{}\nonterm{LExpr}
      =\bigrp{}\regxques{}~\nonterm{Identifier}
      ( \nonterm{List-of-Expr} ) ;\\
        
    \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ $\synxbar$ \ccode{while} ( \nonterm{Expr} ) \nonterm{Statement}\\
    \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ $\synxbar$ \ccode{send} \nonterm{Expr} \ccode{to}
    \nonterm{Expr}  ; \\
    \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $\synxbar$ \ccode{recv} \nonterm{LExpr} \ccode{from}
    \nonterm{Expr}  ; \\
    \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $\synxbar$ \ccode{recv}  \nonterm{LExpr} \ccode{from}  \ccode{any} \nonterm{LExpr}  ;\\
    \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ $\synxbar$ \ccode{return} \nonterm{Expr} ;\\
    \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ $\synxbar$ \lb{} \nonterm{Statement}\regxstar{} \rb \\
    \nonterm{Procedure} \ \ \ \ \synxdef{} \ccode{fun}
    \nonterm{Identifier}~( \nonterm{List-of-Identifier} ) \\
    \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \lb{} \biglp{}\ccode{var} \nonterm{List-of-Identifier}\bigrp{}\regxques{}~;
    \nonterm{Statement}\regxstar{} \rb
    \\
    \nonterm{Program} \ \ \ \ \ \ \synxdef{}
    \biglp{}\ccode{var} \nonterm{List-of-Identifier}\bigrp{}\regxques{}~;~\nonterm{Procedure}\regxplus{}
  \end{programNoNum}
  }
  \caption{The grammar of \minimp{}.  An \texttt{\nonterm{Identifier}} is a
    character sequences.  An \texttt{\nonterm{IntegerLiteral}} is an integer
    literal. An \texttt{\lb{} \nonterm{List-of-Constant} \rb{}} is an array literal.}
  \label{fig:minimp:syntax}
\end{figure}


Figure \ref{fig:minimp:syntax} shows the grammar of \minimp{}.  The
grammar is defined to be general in a way that it is actually
parameterized.  We leave $\synxdots$ in the definitions of
\nonterm{Constant}, unary operator \nonterm{UnOp}, and binary operator
\nonterm{BinOp} for marking that these non-terminals are extend-able.
Extending the grammar with any other kind of constants (e.g., real
number literals), unary operators (e.g., increment) or binary
operators (e.g., logical exclusive or) results in a new \minimp{}
language and the theory introduced in this dissertation is still
applicable to every such \minimp{} language.  For this dissertation,
$\synxdots$ can be ignored since Fig.\ \ref{fig:minimp:syntax}
contains all the primitives that we will use.


We use the word \emph{procedure} for the \minimp{} construct, and the
word \emph{function} for a mathematical function.  A \minimp{}
procedure can return a value, and may modify global variables.  A
\minimp{} program consists of procedures and sets of variables.  There
must be an ``entry'' \texttt{main} procedure.  Variables declared
outside of any procedure are called \emph{global variables}.
Variables declared inside the procedures are called \emph{local
  variables}.

A \minimp{} program is executed by specifying a number of processes,
each of which executes a separate copy of the program starting from
the \texttt{main} procedure. (This is similar to the usual usage of
MPI.)  There is no variable that is shared by multiple processes.
Each process is assigned a unique ID.  The IDs are consecutive
integers $0, \ldots{}, n-1$, where $n$ is the number of processes.  A
process can access its own ID and the total number of processes
through pre-defined constants \texttt{PID} and \texttt{NPROCS},
respectively.  Processes interact through the \emph{communication}
statements: the \texttt{\send{$\mymath{expr}$}{$\mymath{dest}$}} and
\texttt{\recv{$\mymath{expr}$}{$\mymath{src}$}} is a pair of basic
statements for sending a value to or receiving a value from a specific
process; in addition, \minimp{} provides a wildcard receive statement
\texttt{\recvany{$\mymath{expr}$}{$\mymath{src}$}}, which receives a
value from ``\texttt{\ccode{any}}'' possible sender in a nondeterministic way.
The actual sender's ID will be assigned to $\mymath{src}$.

In \minimp{}, an array is a finite sequence of values.  The expression
\texttt{\ccode{new} [$m$]} returns a new array of length $m$, in which
every element has an ``undefined'' value.  Array elements can be
accessed through the subscript expression \texttt{$a$[$i$]}, with an
array $a$ and an index $i$.  The expression \texttt{\ccode{len}($a$)}
represents the length of an array $a$.  The binary operation
\texttt{==>} stands for logical implication.

Other kinds of expressions and statements in Fig.\
\ref{fig:minimp:syntax} are common in many imperative languages, like
C or Java.

\begin{exmp}
  Figure \ref{fig:minimp:example:bcast} shows a \minimp{} program that
  uses a \texttt{bcast} procedure.  In this procedure, process
  \texttt{root} sends a variable \texttt{dat} to all other processes.
  Every other process receives the variable from process \texttt{root}.
  The received variable is returned. $\qed$
\end{exmp}

\begin{exmp}
  Figure \ref{fig:minimp:example:gather} shows a \minimp{} program
  that uses a \texttt{gather} procedure.  In this procedure, process
  \texttt{root} receives values from other processes in a
  nondeterministic way.  The received value will be stored in an
  element of the array \texttt{dat} with the index being equal to
  sender's ID.  Every other process simply sends a value to process
  \texttt{root}.  On the process 0, the array holding values gathered
  from all processes will be returned.  On all other processes, the
  returned value is ``undefined''.  $\qed$
\end{exmp}

\begin{exmp}
  Figure \ref{fig:minimp:example:scatter} shows a \minimp{} program
  that uses a \texttt{scatter} procedure.  In the \texttt{scatter}
  procedure, the process \texttt{root} sends every $i$-th element in
  an array to the process $i$.  Every other process simply receives a
  message from the process \texttt{root}.  Eventually, the process
  \texttt{root} returns the \texttt{root}-th element in the array
  \texttt{buf}, and every other process returns its received value.
  $\qed$
\end{exmp}

%% Examples bcast, gather, scatter
\begin{figure}
  \centering
    \begin{minipage}[t][][b]{.45\textwidth}
    \begin{program}
    \ccode{fun} bcast(dat, root)~\lb~\\
    ~~\ccode{var} i;~\\
    ~~\ccode{if}~(PID~==~root)~\lb\\
    ~~~~i~=~0;\\
    ~~~~\ccode{while} (i < NPROCS) \lb{}\\
    ~~~~~~\ccode{if} (i != root) \\
    ~~~~~~~~\send{dat}{i};\\
    ~~~~~~i = i + 1;\\
    ~~~~\rb{}\\
    ~~\rb~\ccode{else}\\
    ~~~~\recv{dat}{root};\\
    ~~\ccode{return} dat;\\
    \rb\\
  \end{program}
\end{minipage}
\begin{minipage}[t][][b]{.45\textwidth}
  \begin{programContinue}{13}
    \ccode{fun} main() \lb{}\\
    \ \  \ccode{var} buf;\\
    \ \  \ccode{if} (PID == 0) \lb{} \\
    \ \ \ \ buf = 0;\\
    \ \ \rb{}\\
    \ \  buf = bcast(buf, 0);\\
    \ \  \ccode{return} buf;\\
    \rb{}
\end{programContinue}
\end{minipage}
\caption{A \minimp{} program in which the \texttt{main} procedure
  (right) uses the \texttt{bcast} procedure (left).  By the end of an
  execution of this program, each process will have value ``$0$'' in
  its variable \texttt{buf}.}
  \label{fig:minimp:example:bcast}
\end{figure}

\begin{figure}
  \centering
    \begin{minipage}[t][][b]{.45\textwidth}
      \begin{program}
    \ccode{fun} gather(val, root)~\lb~\\
    ~~\ccode{var} i, y, dat;\\
    ~~\ccode{if}~(PID~==~root)~\lb\\
    ~~~~i~=~0; \\
    ~~~~dat = \ccode{new} [NPROCS];\\
    ~~~~dat[root] = val;\\
    ~~~~\ccode{while} (i < NPROCS) \lb{}\\
    ~~~~~~\ccode{if} (i != root) \lb{}\\
    ~~~~~~~~\recvany{val}{y};\\
    ~~~~~~~~dat[y] = val;\\
    ~~~~~~\rb{}\\
    ~~~~~~i = i + 1; \\
    ~~~~\rb{}\\
    ~~\rb~\ccode{else} \\
    ~~~~\send{val}{root};\\
    ~~\ccode{return} dat;\\
    \rb\\
  \end{program}
\end{minipage}
  \begin{minipage}[t][][b]{.45\textwidth}
  \begin{programContinue}{17}
  \ccode{fun} main() \lb{}\\
\ \  \ccode{var} buf, result;\\
\ \  buf = PID;\\
\ \  result = gather(buf, 0);\\
\ \  \ccode{return} result;\\
\rb{}
\end{programContinue}
\end{minipage}
\caption{A \minimp{} program in which the \texttt{main} procedure
  (right) uses the \texttt{gather} procedure (left). By the end of an
  execution of this program with $n$ processes, the process 0 will
  have a sequence of values ``$012\ldots{}(n-1)$'' in its variable
  \texttt{result}.}
  \label{fig:minimp:example:gather}
\end{figure}


\begin{figure}
  \centering
  \begin{minipage}[t][][b]{.45\textwidth}
      \begin{program} 
\ccode{fun} scatter(buf, root) \lb{} \\
\ \  \ccode{var} i, result; \\
\ \  \ccode{if} (PID == root) \lb{} \\
\ \ \ \    i = 0;\\
\ \ \ \    \ccode{while} (i < NPROCS) \lb{}\\
\ \ \ \ \ \   \ccode{if} (i == PID) \\
\ \ \ \ \ \ \ \    result = buf[i];\\
\ \ \ \ \ \    \ccode{else} \\
\ \ \ \ \ \ \ \    \send{buf[i]}{i}; \\
\ \ \ \ \ \      i = i + 1;\\
\ \ \ \  \rb{}\\
\ \  \rb{} \ccode{else} \\
\ \ \ \  \recv{result}{root};\\
\ \  \ccode{return} result;\\
\rb{}
\end{program}
\end{minipage}
\begin{minipage}[t][][b]{.45\textwidth}
\begin{programContinue}{14}
\ccode{fun} main() \lb{}\\
\ \  \ccode{var} buf, result, i;\\
\ \  \ccode{if} (PID == 0) \lb{} \\
\ \ \ \    buf = \ccode{new} [NPROCS];\\
\ \ \ \    i = 0; \\
\ \ \ \   \ccode{while} (i < NPROCS) \lb{}\\
\ \ \ \ \ \      buf[i] = i; \\
\ \ \ \ \  \      i = i + 1; \\
\ \ \ \   \rb{}\\
\ \ \rb{}\\
\ \  result = scatter(buf, 0);\\
\ \  \ccode{return} result;\\
\rb{}
\end{programContinue}
\end{minipage}
\caption{A \minimp{} program where the \texttt{main} procedure (right)
  uses a \texttt{scatter} procedure (left). By the end of an execution
  of this program, the process $i$ will have value ``$i$'' in its
  variable \texttt{result}.}
  \label{fig:minimp:example:scatter}
\end{figure}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MODEL: PROGRAM LOCATIONS and ATOMIC STATMENTS
\section{The \minimp{} Model} \label{sec:minimp:model}

In this section, we define an \emph{abstract representation} for a
generic \minimp{} program.  We call such an abstract representation a
\minimp{} \emph{model}.  A \minimp{} model accurately represents a
\minimp{} program while minimizing the information that is needed for
execution.

\begin{defn}
  A \emph{\minimp{} vocabulary} is a tuple
  $\mymath{\vocab{} = (\myprocedure{}, \var, \globvar{}, \locvar{})}$, where
  
  \begin{itemize}
  \item $\mymath{\myprocedure{}}$ is a set of \emph{procedure names},
  \item $\mymath{\var}$ is a set of \emph{variables},
  \item $\mymath{\globvar{} \subseteq \var}$ is the set of \emph{global
      variables}, and
  \item $\mymath{\locvar{}: \myprocedure{} \rightarrow{} \powerset{(\var)} }$ is a
    function which, given a procedure name, returns the set of
    \emph{local variables} for that procedure
  \end{itemize}
  such that
  
  \begin{itemize}
  \item $\mymath{\forall f \in \myprocedure{}, \locvar{}(f)\cap
      \globvar{} = \emptyset}$,
    and 
  \item $\mymath{\forall f, g \in \myprocedure{}, f\neq g \Rightarrow{}
      \locvar{}(f) \cap \locvar{}(g)=\emptyset}$.   $\qed$
  \end{itemize}
\end{defn}

%% DEFINE EXPRESSIONS OVER VOCABULARY
\begin{defn}
  Given a vocabulary
  $\mymath{\vocab{} = (\myprocedure{}, \var, \globvar{}, \locvar{})}$,
  the set of program expressions over $\var$ is denoted
  $\exprv_{\vocab{}}$, and the set of program expressions of boolean
  type over $\var$ is denoted $\bexprv_{\vocab{}}$. $\qed$
  \label{defn:expr-and-bexpr}
\end{defn}

%% DEFINE ATOMIC ACTION
We next define the atomic statements that will be used to label
transitions in a program graph representation.

\begin{defn}
  Given a vocabulary
  $\mymath{\vocab{} = (\myprocedure{}, \var, \globvar{}, \locvar{})}$,
  the set of \emph{atomic statements} over $\vocab{}$, denoted
  $\stmt{}$, consists of elements of the following forms:
  
  \begin{enumerate}
  \item  \myskipstmt{}
  \item \myrettostmt{$e$}{$x$}
  \item \texttt{$x$ = $e$} 
  \item  \texttt{\send{$e_0$}{$e_1$}}
  \item   \texttt{\recv{$e_0$}{$e_1$}} 
  \item   \texttt{\recvany{$e_0$}{$e_1$}} 
  \item   \texttt{$\mymath{id}$ ($e$, $\ldots{}$)} 
  \end{enumerate}
  with $x, e, e_0, e_ 1\in \exprv_{\vocab{}}$ and
  $id \in \myprocedure{}$.  Besides, $x$ must be an expression such
  that it is allowed to be at the left-hand side of an assignment by
  the \minimp{} grammar.  The \myskipstmt{} statement is simply a
  no-op.  The \myrettostmt{$e$}{$x$} statement assigns the returned
  value from the last call to $x$.  Atomic statements 3--7 are
  \minimp{} program statements.  Remark that the statement 7 means
  that the entering from a call site to the starting location of a
  called procedure is atomic.  The execution of the whole body of a
  called procedure is not atomic.  $\qed$
\end{defn}

Procedures in a \minimp{} program is modeled as \emph{procedure
  graphs}.
  \begin{defn}
    Let
    $\mymath{\vocab{} = (\myprocedure{}, \var, \globvar{},
      \locvar{})}$ be a vocabulary, and let $f \in \myprocedure{}$.  A
    procedure graph for $f$ is a tuple
  \begin{center}
    $\mymath{(\myloc{}, l_{0}, T)}$,
  \end{center}
  where 
  \begin{itemize}
  \item $\mymath{\myloc{}}$ is  a set of \emph{program locations},
  \item $\mymath{l_{0}}$ is the \emph{start location}, and
  \item $\mymath{T \subseteq \myloc{} \times \bexprv_{\vocab{}} \times \myloc{}
      \times \stmt}$ is a set of \emph{local transitions}.
  \end{itemize}
  Let $(l, \phi, l', a) \in T$.  The location $l$ is called the
  \emph{origin} of the transition, $l'$ is the \emph{target}.  The
  boolean expression $\phi$ is the \emph{guard} of the transition, and
  $a$ is the atomic statement of the transition.  The variables
  that occur in $\phi$ and $a$ must belong to
  $\mymath{\globvar{} \cup \locvar{}(f)}$.  $\qed$
  \label{defn:function-graph}
\end{defn}

Local transitions that model conditional statements or
\texttt{\ccode{recv}} statements have non-trivial guards.  For
example, a \texttt{\ccode{recv}} statement shall block the execution
if there is no message that has been sent to but not received by the
receiver.  To express guards of \texttt{\ccode{recv}} statement, we
extend the definition of $\bexprv{_\vocab{}}$ (given in Def.\
\ref{defn:expr-and-bexpr}) with new elements of the two forms:
$\myemptyguard(\mymath{src})$ and $\myallemptyguard$.
When these two kinds of boolean expressions are used in guards of
local transitions,

\begin{enumerate}
\item $\myemptyguard(\mymath{src})$ means that the message channel
  from $\mymath{src}$ to the process associated with the local
  transition is empty; and

\item $\myallemptyguard$ means that the message channels from all
  processes to the process associated with the local transition is
  empty.
\end{enumerate}

Suppose there is a state $s$ where a process $p$ is at a location $l$.
If there is a local transition $(l, \phi, l', a)$ such that the guard
$\phi$ is true at $s$ for $p$, $p$ can execute the statement $a$ in
one step.  The execution of $a$ by $p$ from $s$ leads to a new state
where $p$ is at the location $l'$.

We next describe how to translate a procedure in a \minimp{} program
to a procedure graph.

We need a translation process that has such properties: (1) the
translation result of a \nonterm{Statement} in the body of a procedure
$f$ must represent a sub-graph of the procedure graph of $f$; and (2)
the translation result must have a unique pair of entry and exit
locations.  Figure \ref{fig:minimp:translation} shows such a
translation process $\transT{(l, S)}$ using a pseudocode.  The
$\transT{}$ takes an entry location $l$ and a \nonterm{Statement} $S$,
and returns a pair $(l', T)$ where $l'$ is the exit location and $T$
is a set of local transitions.  In Fig.\ \ref{fig:minimp:translation},
integers are used to represent locations.

\begin{figure}
  \begin{algorithm}[H]
    \KwIn{\textsf{integer $l$}, \nonterm{Statement} $S$}
    \KwOut{\textnormal{ordered pair} (\textsf{integer $l$}, \textsf{transition-set }$R$)}
     \Begin(\textsf{$\transT(l, S)$}){
       $R \leftarrow{} \emptyset$;\\
       \uIf{\textup{$S$ is an assignment, a return, or a
         \texttt{\ccode{send}} statement}}{
         \texttt{$R \leftarrow{} \{(l, \texttt{true}, S,
          l + 1)\}$}\; $l \leftarrow{} l + 1$
       }
       \uElseIf{\textup{$S$ is
         \texttt{\recv{$e_0$}{$e_1$}}}}{
         \texttt{$R \leftarrow{} \{(l, \texttt{!}\myemptyguard{}(e_1), S,
        l + 1)\}$}\; $l \leftarrow{} l + 1$
     }
     \uElseIf{\textup{$S$ is \texttt{\recvany{$e_0$}{$e_1$}}}}{
       \texttt{$R \leftarrow{}
         \{(l, \texttt{!}\myallemptyguard{}, S,
        l + 1)\}$}\; $l \leftarrow{} l + 1$
     }
     \uElseIf{\textup{$S$ is $x$ = $f$($\ldots{}$)}}{
       let $e$ be the return expression of $f$ in
       $R \leftarrow{} \{ (l, \texttt{true}, f
       \texttt{($\ldots{}$)}, l + 1), (l + 1,
       \texttt{true}, \myrettostmt{e}{x}, l + 2)
       \}$\; $l \leftarrow{} l + 2$
     }
     \uElseIf{\textup{$S$ is \texttt{\lb{}$S_0 \ldots{} S_{n-1}$\rb{}}}}{
       \ForEach{$i : 0 \texttt{ ..\ } n-1$}{
                   \texttt{$(l, R_2) \leftarrow{} \transT{}(l, S_i)$}\;
                   \texttt{$R \leftarrow{} R_2 \cup{} R$}
       }
     }
     \uElseIf{\textup{$S$ is \texttt{if ($e$) $S_0$ else
         $S_1$}}}{
     $\textsf{entry} \leftarrow{} l$\;
       \texttt{$R \leftarrow{}
         \{(\textsf{entry}, e, \myskipstmt{}, l + 1)\}$}\;
       $(l, R_2) \leftarrow{} \transT{}(l + 1, S_0)$\;
       $R \leftarrow{} R_2 \cup{} R$\;
       $\textsf{exit}_0 \leftarrow{} l$\;
       $R \leftarrow{} R \cup{} (\textsf{entry},
         \texttt{!}e, \myskipstmt{}, l + 1)$\;
       $(l, R_2) \leftarrow{} \transT{}(l + 1, S_1)$\;
       $R \leftarrow{} R_2 \cup{} R$\;
       $\textsf{exit}_1 \leftarrow{} l$\;
       $R \leftarrow{} R \cup{} \{ (\textsf{exit}_0, \texttt{true},
         \myskipstmt{}, l+ 1), (\textsf{exit}_1,
         \texttt{true}, \myskipstmt{}, l + 1)
         \}$\;
       $l \leftarrow{} l + 1$
       }
       \ElseIf{\textup{$S$ is \texttt{while ($e$) $S_0$}}}{
         $\textsf{entry} \leftarrow{} l$\;
         \texttt{$R \leftarrow{}  \{(\textsf{entry}, e, \myskipstmt{},
          l + 1)\}$}\;
         $(l, R_2) \leftarrow{} \transT{}(l + 1, S_0)$\;
         $R \leftarrow{} R_2 \cup{} R$\;
         \texttt{$R \leftarrow{} R \cup{} \{(l, \texttt{true}, \myskipstmt{}, \textsf{entry}), (\textsf{entry}, \texttt{!}e, \myskipstmt{},
          l + 1)\}$}\;
        $l \leftarrow{} l + 1$
         }
         $\textbf{return } (l, R)$
       }
\end{algorithm}

\caption{The pseudocode definition of the translation
  process.}
\label{fig:minimp:translation}
\end{figure}

Note a \texttt{\recv{$v$}{$e$}} statement is guarded by
\texttt{!$\myemptyguard$}$(e)$, and a \texttt{\recvany{$v_0$}{$v_1$}}
statement is guarded by \texttt{!$\myallemptyguard$}.

Given a \minimp{} procedure $f$, a procedure graph of $f$ can be
constructed as
$\mymath{(\myloc{}, l_0, \transT{}(l_0,
  \texttt{\lb{}$S_0S_1\ldots{}$\rb{}}))}$, where
\texttt{\lb{}$S_0S_1\ldots{}$\rb{}} is the body of $f$, $l_0$ is the
entry location, and $\myloc{}$ is the set of the locations used in
$\mymath{\transT{}(l_0, \texttt{\lb{}$S_0S_1\ldots{}$\rb{}})}$.

%% EXAMPLE
\begin{exmp}
  We present the procedure graph of the \texttt{bcast} procedure in
  Fig.\ \ref{fig:minimp:example:bcast} as an example here:
  $ (\{0,\cdots{}{12}\}, 0, T)$, where
\begin{center}
  \begin{enumerate}
%  \item $\mymath{Loc_{\texttt{bcast}} = \{0,\, 1,\, 2,\, 3,\,
 %     4,\, 5, 6, 7\}}$
  \item[] $\mymath{T = \{}$\\
    \begin{tabular}{ll}
      $(0,\, \textcolor{red}{\texttt{PID == root}},\, \myskipstmt{},\, 1),\,
      $ &
      $(1,\, \textcolor{red}{\texttt{true}},\, \texttt{i = 0},\, 2),\, $   \\
      $(2,\, \textcolor{red}{\texttt{i < NPROCS}},\, \myskipstmt{},\, 3),$
         &
      $(3,\, \textcolor{red}{\texttt{i != root}},\, \myskipstmt{},\, 4),$ \\
      $(4,\, \textcolor{red}{\texttt{true}},\, \texttt{\send{dat}{i}},\, 5),$ &
      $(5,\, \textcolor{red}{\texttt{true}},\, \myskipstmt{},\, 7),$
         \\
      $(3,\, \textcolor{red}{\texttt{i == root}},\,
           \myskipstmt{},\, 6),$ &
      $(6,\, \textcolor{red}{\texttt{true}},\, \myskipstmt{},\,
      7),$\\
      $(7,\, \textcolor{red}{\texttt{true}},\, \texttt{i = i + 1},\,
                8),$&
      $(8,\, \textcolor{red}{\texttt{true}},\, \myskipstmt{},\,
      2),$ \\
       $(2,\, \textcolor{red}{\texttt{i >= NPROCS}},\, \myskipstmt{},\,
      9),$&
       $(0,\, \textcolor{red}{\texttt{PID != root}},\, \myskipstmt{},\,
      {10}),$\\               
      $({10},\, \textcolor{red}{\texttt{!\myemptyguard{}(root)}},\, \texttt{\recv{dat}{root}},\,
      {11}),$&
      $(9,\, \textcolor{red}{\texttt{true}},\, \myskipstmt{},\,
                  {12}),$ \\
            $({11},\, \textcolor{red}{\texttt{true}},\, \myskipstmt{},\,
      {12}),$ &                  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%          
    \end{tabular}\\    
    $\}$
  \end{enumerate}
\end{center}
Figure \ref{fig:exmp:func-graph} visualizes this procedure graph.
$\qed$
\end{exmp}

\begin{figure}
  \centering
  
  \usetikzlibrary{shapes.geometric, arrows}
  \tikzstyle{loc} = [rectangle, minimum width=.7cm, minimum
  height=.7cm,text centered, draw=black]
    \tikzstyle{end} = [rectangle, minimum width=.7cm, minimum
    height=.7cm,text centered, draw=black, thick]
  \tikzstyle{arrow} = [thick,->,>=stealth]
  \begin{tikzpicture}[node distance=2cm]
    \node (l0) [end] {$0$};    
    \node (l1) [loc, right of=l0, xshift=1cm] {$1$};
    \node (l2) [loc, right of=l1, xshift=.6cm] {$2$};
    \node (l3) [loc, right of=l2, xshift=1cm] {$3$};
    \node (l4) [loc, right of=l3, xshift=1cm] {$4$};
    \node (l5) [loc, below of=l4, yshift=-.5cm] {$5$};
    \node (l6) [loc, below of=l3, yshift=-.5cm] {$6$};
    \node (l7) [loc, below of=l5, yshift=-.5cm] {$7$};
    \node (l8) [loc, below of=l6, yshift=-.5cm] {$8$};
    \node (l9) [loc, below of=l2, yshift=-.5cm] {$9$};
    \node (l10) [loc, below of=l1, yshift=-.5cm] {${10}$};
    \node (l11) [loc, below of=l10, yshift=-.5cm] {${11}$};
    \node (l12) [end, below of=l9, yshift=-.5cm] {${12}$};
    %% arrows
    \draw [arrow] (l0) -- node[anchor=south]{\footnotesize
      \textcolor{red}{\texttt{PID == root}}}
    node[anchor=south, yshift=-.55cm]{\footnotesize \texttt{\myactskip}}
    (l1);

    \draw [arrow] (l1) -- node[anchor=south]{\footnotesize
      \textcolor{red}{\texttt{true}}}
    node[anchor=south, yshift=-.5cm]{\footnotesize \texttt{i = 0}} (l2);

    \draw [arrow] (l2) -- node[anchor=south]{\footnotesize
      \textcolor{red}{\texttt{i < NPROCS}}}
    node[anchor=south, yshift=-.55cm]{\footnotesize \texttt{\myactskip{}}}
    (l3);

    \draw [arrow] (l3) -- node[anchor=south]{\footnotesize
      \textcolor{red}{\texttt{i != root}}}
        node[anchor=south, yshift=-.55cm]{\footnotesize \texttt{\myactskip{}}}
    (l4);

    \draw [arrow] (l4) -- node[anchor=east, yshift=.3cm]{\footnotesize \textcolor{red}{
      \texttt{true}}} node[anchor=east,
    yshift=-.25cm]{\footnotesize \texttt{\send{dat}{i}}} (l5);

    \draw [arrow] (l5) --
    node[anchor=east, yshift=.3cm]{\footnotesize \textcolor{red}{
      \texttt{true}}} node[anchor=east,
    yshift=-.25cm]{\footnotesize \texttt{\myactskip{}}}
    (l7);

    \draw [arrow] (l3) -- node[anchor=east, yshift=.3cm]{\footnotesize
      \textcolor{red}{\texttt{i == root}}}
     node[anchor=east,
    yshift=-.25cm]{\footnotesize \texttt{\myactskip{}}}
    (l6);

    \draw [arrow] (l6) --
    node[anchor=east, yshift=.05cm]{\footnotesize \textcolor{red}{
      \texttt{true}}} node[anchor=east,
    yshift=-.5cm]{\footnotesize \texttt{\myactskip{}}}
    (l7);

    \draw [arrow] (l7) --
    node[anchor=south]{\footnotesize
      \textcolor{red}{\texttt{true}}}
    node[anchor=south, yshift=-.55cm]{\footnotesize \texttt{i = i + 1}} (l8);

    \draw [arrow] (l8) --
node[anchor=east, yshift=.05cm]{\footnotesize \textcolor{red}{
      \texttt{true}}} node[anchor=east,
    yshift=-.5cm]{\footnotesize \texttt{\myactskip{}}}
    (l2);

    \draw [arrow] (l2) -- node[anchor=east, yshift=.3cm]{\footnotesize
      \textcolor{red}{\texttt{i >= NPROCS}}}
    node[anchor=east, yshift=-.25cm]{\footnotesize $\myactskip$} (l9);

    \draw [arrow] (l0) -- node[anchor=east]{\footnotesize \textcolor{red}{\texttt{PID
          !=root}}}
    node[anchor=east, yshift=-.55cm]{\footnotesize $\myactskip$}
    (l10);

    \draw [arrow] (l10) --
    node[anchor=east]{\footnotesize \textcolor{red}{\texttt{!}\myemptyguard{}(root)}}
    node[anchor=east, yshift=-.5cm]{\footnotesize \texttt{\recv{dat}{root}}}
    (l11);

    \draw [arrow] (l9) --
node[anchor=east, yshift=.3cm]{\footnotesize
      \textcolor{red}{\texttt{true}}}
     node[anchor=east,
    yshift=-.25cm]{\footnotesize \texttt{\myactskip{}}}
    (l12);

    \draw [arrow] (l11) --
    node[anchor=south]{\footnotesize
      \textcolor{red}{\texttt{true}}}
    node[anchor=south,
    yshift=-.55cm]{\footnotesize \texttt{\myactskip{}}}
    (l12);
  \end{tikzpicture}
  
  \caption{Procedure graph of the \texttt{bcast} procedure in Fig.\
    \ref{fig:minimp:example:bcast}.  Boxes are program locations.
    Arrows are labeled by an atomic statement and a guard (in red).
    Trivial statement \myskipstmt{} and trivial guard \texttt{true}
    are omitted.
    Two boxes, including the arrow that connects them, represent a
    local transition.  The bold boxes $0$ and ${12}$ are the sole
    entry and exit, respectively.}
  \label{fig:exmp:func-graph}
\end{figure}

%%%%%%%%%% MINIMP PROGRAM MODEL %%%%%%%%%%%%%% 
\begin{defn}
  A \minimp{} model $\model$ over a vocabulary $(\myprocedure, \var,
  \globvar, \locvar)$ is a tuple:
  \begin{center}
    $\model = \mymath{(\texttt{main}, \myprocGraphFunc{})}$,
  \end{center}
  where 
  \begin{itemize}
  \item $\texttt{main} \in \myprocedure$:  the \texttt{main} procedure
  \item $\mymath{\myprocGraphFunc}$ is a function that maps from
    $\myprocedure$ to procedure graphs. $\qed$
  \end{itemize} 
  \label{defn:model}
\end{defn}

A \minimp{} model can be converted from a \minimp{} program by
converting every procedure in the program to a procedure graph using
the well-defined translation process described above.

\section{Semantics} \label{sec:minimp:semantics}
\subsection{Process States and Global States}
In a state of a \minimp{} program, variables hold values corresponding
to a domain.

\begin{defn}
  The \emph{domain} $\dom$ that contains a special value $\myundef{}$
  that stands for undefined values, integers, boolean values and
  sequences of values are defined recursively by
\begin{align}
  &  \domtmp_0 = \{\myundef{}\} \cup{} \mathbb{Z} \cup \mathbb{B} \cup \ldots{} ,\,\,
    \nonumber \\
  &  \domtmp_{i+1} = \domtmp_{i}^* 
    \text{ for } i \geq 0, \text{ and} \nonumber \\
  & \dom = \domtmp_0 \cup \domtmp_1 \cup \domtmp_2 \cup
    \ldots{}\,\, . \qed{} \nonumber
\end{align}
\label{defn:domain}
\end{defn}

Recall that \minimp{} is extend-able, therefore the base values in a
domain must at least include $\myundef$, $\mathbb{Z}$ and $\mathbb{B}$,
and more is possible.  In Def.\ \ref{defn:domain}, $\dom_i$ is the set
of values of $i$-dimensional arrays, $i \geq 0$.

%%%%%%%%% FRAME

A \emph{frame} is an entry in a process's call stack.  It stores
information about the current procedure for that process: the location
within the procedure's program graph, and the values of the
procedure's local variables.

\begin{defn}
  Let $(\myprocedure, \var, \globvar, \locvar)$ be a vocabulary,
  $\dom$ be a domain, and
  $\model{} = (\texttt{main}, \myprocGraphFunc)$ be a \minimp{} model.
  A \emph{frame} of a procedure $f$ in $\model$ is a tuple:
  \begin{center}
    $(l, \mymem{})$,
  \end{center}
  where
  \begin{itemize}
  \item $\mymath{l}$ is a location in $\myprocGraphFunc{}(f)$.
  \item $\mymath{\mymem{}}\colon{} \mymath{\locvar{}(f)
      \rightarrow{} \dom}$ is a \emph{local
      memory}.
  \end{itemize}
  Let $\myframes_{f, \model}$ be the set of all frames of $f$ in
  $\model$.  Let $\myframes_\model$ be the set of all frames of all
  procedures in $\model$.  $\qed$
\end{defn}

The state of a single process is called a \emph{process state}.
\begin{defn}
  Given a vocabulary $(\myprocedure, \var, \globvar, \locvar)$, a domain
  $\dom$, and a \minimp{} model $\model$.  A \emph{process state} is a
  pair:
  \begin{center}
    $\mymath{\myprocState{} = (\mystack, \mygmem)}$,
  \end{center}
  where
\begin{enumerate}
\item $\mymath{\mystack \in \myframes_{\model}^*}$ is the call stack,
  which is a sequence of frames.
  \item $\mymath{\mygmem}\colon{} \mymath{\globvar \rightarrow \dom}$ is a
    \emph{global memory}. $\qed$
  \end{enumerate}
\end{defn}

In a process state, the last element of its $\mymath{stack}$ is the
top of the call stack.  The current location of a process in a state
is the location in the top of the call stack.

%%%%%%%% GLOABL STATES:

Let $n$ be a positive integer.  Recall that $\nprocs{n}$ is the set of
all integers between $0$ and $n-1$, inclusive.  Now we define a
\emph{state} of a \minimp{} program with $n$ processes, each of which
is identified by a unique integer in $\nprocs{n}$.

\begin{defn}
  Let $(\myprocedure, \var, \globvar, \locvar)$ be a vocabulary,
  $\dom$ be a domain, and $n$ be a positive integer.  A \emph{state}
  with $n$ processes is an $(n + 1)$-ary tuple:
  \begin{center}
    $\mymath{\mystate_n = (\myprocState_0, ..., \myprocState_{n-1}, \mychan)}$, 
    \end{center}
    where
    \begin{itemize}
    \item $\mymath{\myprocState_i}$ is the process state of process $i$.
    \item
      $\mymath{\mychan\colon{} \nprocs{n} \times \nprocs{n} \rightarrow{}
        \dom{}^*}$ is the channel function that maps ordered pairs of
      integers to sequences of values.
    \end{itemize}
    Let $\mystates_n$ be the set of states with $n$ processes.  We may
    simplify $\mystates_n$ to $\mystates$ when $n$ is understood in
    the context.  $\qed$
  \end{defn}
  
  Given an ordered pair of integers $(i, j)$, the value sequence
  $\mychan{}(i, j)$ represents the \emph{message channel} from process
  $i$ to $j$.

  
%%%%%%%%%% SEMANTICS OF EXPRESSION and Transition system
%\subsection{Expression Evaluation}
%%%%%%%%%%%  HELPER NOTATIONS

  We introduce the following shortcut notations for the sake of
  brevity in the rest of this dissertation.  Let $p \in \nprocs{n}$.

\begin{itemize}
\item $\mymath{\myprocState{}_p(s)}$: the process state of
process $p$ of a state $s$ \label{page:notation:procState}
  
\item $\mymath{\mystack(s, p)}$: the stack on the process state of
  the process $p$ in a state $s$  \label{page:notation:stack}
  
\item $\mymath{\mytop(s, p)}$: the \emph{top frame} in
  $\mymath{\mystack(s, p)}$, i.e., $\mytail{(\mystack(s, p))}$
  \label{page:notation:top}
  
\item $\mymath{\mytoploc(s, p)}$: the location of the frame
  $\mymath{\mytop(s, p)}$  \label{page:notation:toploc}
  
\item $\mymath{\mymem(s, p)}$: the union of the local memory of
  $\mymath{\mytop(s, p)}$ and the global memory of
  $\mymath{\myprocState_p(s)}$ \label{page:notation:mem}  
  
\item $\mymath{\mychan(s)}$: the channel function in 
  state $s$ \label{page:notation:comm}

\item $s[l:=l']_p$: the state obtained by changing the ``current
  location'' (i.e., the location in the top frame) of process $p$ to
  $l'$ from $s$.
  
\item $s\downarrow{_p}f$ (\textbf{push frame}) denotes the state
  obtained by appending a new frame $f$ to $\mymath{\mystack(s, p)}$,
  i.e.,
   \begin{align}
     s\downarrow{_p}f =~& \text{let } a = \mystack{}(s, p) \text{ in } \nonumber \\
                      &    \text{let } b =
                        \myprocState{_p}(s)[\textsf{stack}:=a \circ{} f] \text{ in } 
                     s[\myprocState{_p}:=b].     
     \nonumber
   \end{align} \label{page:notation:push}

 \item $s\uparrow{_p}$ (\textbf{pop frame}) denotes the state obtained
   by removing the last frame in $\mymath{\mystack(s, p)}$, i.e.,
   \begin{align}
     s\uparrow{_p} =~& \text{let } a = \myprocState{_p}(s)[\textsf{stack}:=\xi] \text{ in }
                     s[\myprocState{_p}:=a], \text{ where } \nonumber
     \\
     & \xi\colon{} \myframes_\model^* \text{ is defined
                       by }
     \exists{f \in
     \myframes{_\model}}.\, \mystack{}(s, p) = \xi \circ{} f. 
                       \nonumber 
   \end{align} \label{page:notation:pop}
   
 \item $\mymath{s[\textsf{var} := \textsf{val}]_p}$
   (\textbf{assign}) denotes the state obtained by assigning a value
   $\textsf{val}$ to a variable $\textsf{var}$ at a state $s$ for a
   process $p$.  It is either the case that only the local memory of
   $\mystack{(s, p)}$ or only the global memory in $\myprocState_p(s)$
   is changed from $s$ to
   $\mymath{s[\textsf{var} := \textsf{val}]_p}$ 
   such that
   \begin{align}
     \mymem{}(s[\textsf{var} := \textsf{val}]_p, p)(\textsf{var}) = \textsf{val}. \nonumber
   \end{align} \label{page:notation:assign}
   
 \item $s[\enque{(p, q)}{\textsf{val}}]$ (\textbf{enqueue}) denotes the state obtained
   by appending a value $\textsf{val}$ on the channel identified by
   the ordered pair $(p, q)$, i.e.,
   \begin{align}
   s[\enque{(p, q)}{\textsf{val}}] =~& \text{let } a = \mychan{(s)}(p,
                                       q)  \text{ in } \nonumber \\
                                     & \text{let } b = \mychan{(s)}[(p,
                                       q) \mapsto a \circ{}
                                       \textsf{val}]  \text{ in }
     s[\mychan{}:=b]. \nonumber
   \end{align}
   \label{page:notation:enque}

 \item $s[\deque{(p, q)}{\textsf{var}}]$ (\textbf{dequeue}) denotes
   the state obtained by removing the first element from the channel
   identified by the ordered pair $(p, q)$, and then saving the
   removed element in $\textsf{var}$.  That is,
   \begin{align}
     s[\deque{(p, q)}{\textsf{var}}]  =~&
                                          \text{let } a = \mychan{(s)}(p, q)  \text{ in } \nonumber \\
                                        &\text{let } b = \mychan{(s)}[(p, q) \mapsto \xi]  \text{ in }
                                          s[\mychan{}:=b][\textsf{var} := \textsf{val}]_q, \text{ where }
                                          \nonumber \\
                                        &\xi \colon{} \dom^* \text{ and } \textsf{val} \colon{} \dom \text{ is
                                          defined by }
                                          a = \textsf{val} \circ{} \xi. \nonumber
   \end{align}
   \label{page:notation:deque}
 \end{itemize}
 The notations \texttt{!}  and \texttt{?} are borrowed from CSP
 \cite{Hoare:1985:CSP:3921}.

\subsection{Interpretation}
To describe behaviors of a \minimp{} program, one needs to describe
how an expression is evaluated and how a local transition alters a
state.

\begin{defn}
  Given a vocabulary $\vocab{}$ and a domain $\dom$, the
  \emph{$n$-processes evaluation function}
  $\mymath{\myeval{e}_n: \mystates_{n} \times \nprocs{n} \rightarrow
    \dom{}}$ evaluates an expression $e \in \exprv{}_{\vocab{}}$ for a
  process at a state.  The definition of $\myeval{e}_n$ is given in
  Fig.\ \ref{fig:minimp:eval:semantics}.  $\qed$
\end{defn}

The evaluation function is complete.  For undefined cases, such as
reading an uninitialized variable, an out-of-bound array access,
division by zero, the function returns $\myundef{}$.  For brevity, we
may simplify $\myeval{~}_n$ to $\myeval{~}$ when the number of
processes is understood.

\begin{figure}
  \centering
    \fbox{
    \parbox{.75\textwidth}{
  \begin{tabular}{r c l l}
  $\myeval{c}_n(s, p)$ & $ = $ & $\mymath{c}$, where $\mymath{c}
    \in \dom{}$\vspace{.2cm} \\
  $\myeval{\texttt{PID}}_n(s, p)$ & $ = $ & $\mymath{p}$\vspace{.2cm} \\

  $\myeval{\texttt{NPROCS}}_n(s, p)$ & $ = $ & $\mymath{n}$\vspace{.2cm} \\

  $\myeval{v}_n(s, p)$ & $ = $ & $\mymath{\mymem{}(s, p)(v)}$ \vspace{.2cm} \\ 

  $\mymath{\myeval{v\texttt{[}e\texttt{]}}_n(s, p)}$ & $ = $ & $\mymath{
      \myeval{v}_n(s, p)(\myeval{e}_n(s, p))}$ \vspace{.2cm} \\

    $\myeval{\texttt{len($e$)}}_n(s, p)$ & $ = $ &
                                                $\mymath{
                                                     |\myeval{e}_n(s,
                                                   p)|}$\\[\myskip]

    $\myeval{\texttt{new [$e$]}}_n(s, p)$ & $ = $ &
                                                   $\xi$ s.t.\  let $m =
                                                    \myeval{e}_n(s, p)$
                                                    in $|\xi| = m \wedge{} $
    \\

    & & $\xi[i] = \myundef{}$ for $0 \leq{} i < m$ \\[\myskip]
    
  $\myeval{e_0~ \textsf{bop}~ e_1}_n(s, p)$ & $ = $ &
                                                    $\mymath{\myeval{e_0}_n(s,
                                                    p)~\textsf{bop}~\myeval{e_1}_n(s,
                                                    p)}$\vspace{.2cm} \\
    $\myeval{\textsf{uop}~e}_n(s, p)$ & $ = $ &
                                                $\mymath{\textsf{uop}~\myeval{e}_n(s,
                                                p)}$\\[\myskip]

    $\myeval{\myemptyguard{}(e)}_n(s, p)$ & $ = $ & \textbf{T}, if 
                                                    $\mymath{\mychan{(s)}(p,
                                                    \myeval{e}_n(s,
                                                    p)) =
                                                    \epsilon}$\\[\myskip]
    $\myeval{\myallemptyguard{}}_n(s, p)$ & $ = $ & \textbf{T}, if 
                                                    $\forall{q\in\nprocs{n}}.\,\mymath{\mychan{(s)}(p,
                                                    q) =
                                                    \epsilon}$\\[\myskip]
        
    $\myundef{}$, & & \text{in any undefined case} \\
\end{tabular}
}}
\caption{\minimp{} expression evaluation, where $s$ is a state, $p$ is
  a process, $v$ is a variable, $e, e_0, e_1$ are expressions.  The
  \textsf{bop} stands for a binary operator (e.g., \texttt{+, -,
    $\ldots{}$}).  The \textsf{uop} stands for a unary operator (e.g.,
  \texttt{!, -, $\ldots{}$}). }
\label{fig:minimp:eval:semantics}
\end{figure}

%%%%%%%%%%% Next States

\begin{defn}
  Given a vocabulary and a $n$-processes evaluation function
  $\myeval{~}$, the \emph{$n$-processes interpretation function}
  $I_n: \mystates{} \times{} \nprocs{n} \times T \rightarrow{}
  2^{\mystates{}}$ describes the states, each of which is a possible
  result of executing a local transition $(l, g, a, l') \in T$ from a
  state $s \in \mystates{}$ by a process $p \in \nprocs{n}$.  The
  definition of $\mymath{I_n(s, p, (l, g, a, l'))}$ is given in Fig.\
  \ref{fig:minimp:interpretation}. $\qed$
\end{defn}

When the number of processes in understood in a context, we may
simplify $I_n$ to $I$.

\begin{figure}
      \fbox{
    \parbox{.97\textwidth}{  
  \[
    \begin{array}{rll}
    &\mymath{I_n(s, p, (l, g, a, l'))} =  & \vspace{.4cm}\\  

     &\emptyset, & \text{if }  \mymath{\myeval{g}(s, p)=\textbf{F}} \vee{} \mytoploc(s, p)\not=l
                  \vspace{.2cm}\\

    \text{or,}& \{s[l:=l']_p\}, & \text{if }  a \text{ is } \myskipstmt{} \vspace{.4cm}\\

   \text{or,}& \text{let }
               \mymath{s' = s[l:=l']_p} \text{ in } \\
      & 
     \{s'[v := \myeval{e}(s, p)]_p\}, & \text{if } a \text{ is
                                                  } v \texttt{ = } e \vspace{.4cm}\\

                                                 %% 
      \text{or,} & \text{let } s' = s[l:=l']_p \text{ in } & \\
      & \text{let } \textsf{idx} = \myeval{e_0}(s, p) \text{ in } & \\
      & \text{let }  \textsf{val}= \myeval{e_1}(s, p) \text{ in } & \\
      & \text{let } \textsf{arrval} = \myeval{v}(s, p)[\textsf{idx} \mapsto{} \textsf{val}] \text{ in } \\
      & \{s'[v := \textsf{arrval}]_p\}, & \text{if } a \text{ is }
                                               v\texttt{[$e_0$]
                                               = }e_1 \vspace{.4cm}\\
                                               %%
      \text{or,} & \multicolumn{2}{l}{\text{Suppose } \alpha_0,\ldots{}, \alpha_{n-1}
                   \text{ are parameters of } f,  
       \text{and }l_0\text{ is the start location of } f,} \vspace{.2cm}\\ 
      & \text{let }\beta_i = \myeval{e_i}(s, p) \text{ for
        } 0 \leq{} i < n \text{ in}\\
      & \text{let } \textsf{fr}
       = (l_0, \mymem) \text{ in }\\
     & \{\mymath{(s\downarrow{_p}\textsf{fr})[~\alpha_0 := \beta_0]_p[\ldots][\alpha_{n-1} := \beta_{n-1}]_p}\}, & \text{if } a \text{
                                                 is
                                                                        }\texttt{$f(e_0,\ldots{}, e_{n-1})$}                                                \vspace{.4cm}\\
      %%
      \text{or,} & \text{let } \textsf{val} = \myeval{e}(s, p) \text{
                   in }\vspace{.2cm}\\ 
      & \{
        (s\uparrow{_p})[x := \textsf{val}]_p\}, & \text{if } a \text{
                                                  is } \myrettostmt{$e$}{$x$}  \vspace{.4cm}\\
                 %%
      \text{or,} & \text{let } \mymath{s' = s[l:=l']_p} \text{ in}\\
      &  \text{let } \textsf{val} = \myeval{e_0}(s, p) \text{ in} \\
      & \text{let } \textsf{dest} = \myeval{e_1}(s, p) \text{ in }
       \{ s'[\enque{(p, \textsf{dest})}{\textsf{val}}] \}, & \text{if }
                                                       a = \texttt{\send{$e_0$}{$e_1$}} \vspace{.4cm}\\

                                                        %%
      \text{or,} &   \text{let } \mymath{s' = s[l:=l']_p} \text{ in} \\
       & \text{let } \textsf{src} = \myeval{e}(s, p) \text{ in} \\
      & \{(s'[\deque{(\textsf{src}, p)}{v}])\}, & \text{if } a \text{ is } \texttt{\recv{$v$}{$e$}} \vspace{.4cm}\\

                     %%
     \text{or,} & \text{let } \mymath{s' = s[l:=l']_p} \text{ in }\\      
      &\{s'' \in \mystates{} \mid{} \\
      &~~\exists{q \in \nprocs{n}}.\, s'' =  s'[\deque{(q,
       p)}{v_0}][v_1 :=  q]_p \wedge{} \\
      &~~|\mychan(s')(q, p)| > 0&
 \text{if } a = \texttt{\recvany{$v_0$}{$v_1$}}      \\
      &\},  &
    \end{array}
  \]
  }}
\caption{The definition of the $n$-processes interpretation function
  $\mymath{I_n}$ that describes the results of executing a local
  transition from a state by a process.}
\label{fig:minimp:interpretation}
\end{figure}

We briefly explain Fig.\ \ref{fig:minimp:interpretation},

\begin{itemize}
\item A local transition cannot be executed by a process from a state
  $s$, if the guard evaluates to \texttt{false} at $s$, or the
  location of the process at $s$ does not match the origin of
  the local transition.

\item An execution of a local transition alters the current location
  of the running process.  If the local transition is associated with
  the \myskipstmt{} statement, nothing else will be changed by the
  execution.

\item If a local transition is associated with an assignment,
  either the local memory of the top entry in the call stack, or the
  global memory, of the running process will be updated after an
  execution.

\item If a local transition is associated with a call, a new frame
  will be pushed onto the call stack of the running process, and the
  results of evaluating the actual arguments will be assigned to the
  formal parameters, after an execution.

\item If a local transition is associated with a
  \myrettostmt{$e$}{$x$} action, an execution of it includes the
  following three sub-steps that will be done together in one atomic
  step: $e$ will first be evaluated, and then the top frame of the
  running process will be popped, finally the value of $e$ is assigned
  to $x$.

\item If a local transition is associated with a \texttt{\ccode{send}}
  statement, after an execution, the sending value will be appended to
  the message channel identified by the ordered pair $(p, q)$, where $p$
  is the sender and $q$ is the receiver.

\item It a local transition is associated with a
  \texttt{\recv{$v$}{$src$}} statement, after an
  execution, the first element in the message channel identified by
  $(p, q)$ is removed and is assigned to $v$, where $p$ is
  the sender and $q$ is the receiver.
  

\item If a local transition is associated with a wildcard
  \texttt{\recvany{$v$}{$src$}} statement, an execution
  nondeterministically selects a message channel among those that are
  non-empty and are identified by $(p, q)$ for some sender
  $p \in \nprocs{n}$ and the receiver $q$.  With the selected message
  channel, the execution alters the state as if a deterministic
  \texttt{\code{recv}} is performed on that channel.
\end{itemize}


\subsection{State Space Graph}

\begin{defn}
  Let $I_n$ be an $n$-processes interpretation,  $S$ be a set of
  states and $T$ be a set of local transitions.
  We define
\[
 \mynexts_n(S, T) = \bigcup\limits_{s \in S, t \in T, p \in
   \nprocs{n}} I_n(s, p, t). \qed
\]
\end{defn}

\begin{defn}
Denoted by $\mynexts_n^i(S, T)$, the repeated $i$ applications of
$\mynexts_n$ for $i \geq 0$ is defined by

\begin{itemize}
\item[] $\mynexts_n^0(S, T) = \mynexts_n(S, T)$,
\item[] $\mynexts_n^{i+1}(S, T) = \mynexts_n(\mynexts_n^i(S, T), T)$. $\qed$
\end{itemize}
\end{defn}

We say a state $s$ is \emph{reachable} from a set of states $S$ over a
set of local transitions $T$, if there is a non-negative $i$ such that
$\mymath{s \in \mynexts_n^i(S, T)}$.  \label{page:term:reachable}

%%%%%%%%%%%  STATE SPACE
The behaviors of a \minimp{} model are described by a \emph{state
  space graph}.
\begin{defn}
  Let $\vocab{}$ be a vocabulary, $\model$ be a \minimp{} model, and
  $T$ be the union of local transitions of procedures in $\model$.
  Given an positive integer $n$, a finite \emph{state space graph}
  $\mymath{G}$ of $\model$ with $n$ processes is a tuple:
\begin{center}
  $\mymath{G}$ = ($s_0$, $S$, 
  $\mymath{\leadsto}$),
\end{center}
where 
\begin{itemize}
  
\item $s_0$ is the initial state where
  
  \begin{itemize}
  \item variables are all assigned $\myundef{}$ and message channels are
    all empty;
  \item   every process has only one
  frame associated with \texttt{main} in its call stack; and
\item every process is at the entry location of \texttt{main}.
  \end{itemize} 
  
\item $\mymath{S}$ is the set of states that are reachable from $s_0$
  over $T$.
  
\item
  $\leadsto_{\model}\colon{} \mystates \times \nprocs{n} \times \stmt{}
  \times \mystates$ is the \emph{global transition relation} defined by
  \begin{center}
    $\mymath{\{(s, p, \alpha, s') \mid s' \in I(s,
      p, \alpha), s \in S, p \in \nprocs{n}, \alpha \in
      T\} }$. $\qed$
  \end{center}
\end{itemize}
\end{defn}

For a global transition $\mymath{t = (s, p, \alpha, s')}$, we call $s$
the \emph{source state}, denoted $\mysrc(t)$, and $s'$ the
\emph{destination state}, denoted $\mydest(t)$.  We use
$\myproc{}(t)$ to denote the process of $t$.


If taking states as vertices and global transitions as directed edges,
a state space graph $G$ is a directed graph.

\begin{defn}
  Let $G$ be a state space graph.  A path $\rho$ in $G$ is a finite
  sequence of transitions $\mymath{t_0t_1t_2...t_{m-1}}$ such that for
  any pair $\mymath{t_it_{i+1}, 0 \leq i < m-1}$, in $\rho$,
  $\mysrc(t_{i+1}) = \mydest(t_i)$. $\qed$
\end{defn}

\begin{defn}
  Given a path $\rho$, $\mypathtrans(\rho)$ denotes the set of
  transitions in $\rho$ and $\mypathstates(\rho)$ denotes the set of
  states in a path $\rho$, i.e.
  $\mymath{\mypathstates(\rho) = \bigcup\limits_{t \in
      \mypathtrans(\rho)} \{\mysrc(t), \mydest(t)\}}$.  $\qed$
\end{defn}

\begin{defn}
  Let $G = (s_0, S, \leadsto)$ be a state space graph.  An
  \emph{execution} $\pi$ in $G$ is a path such that the the first
  state $\mymath{\mysrc(\myhead(\pi))}$ is $s_0$ and there is no
  transition emanating from the last state of $\pi$, formally,
  $\forall{t \in \leadsto}.\, \mymath{\mysrc(t) \not=
    \mydest(\mytail(\pi))}. \qed$
\end{defn}

We are interested in acyclic executions.  Paths that contain cycles
mean that there are infinite loops or recursions, but we only care
about programs that will eventually terminate.  Therefore, a path
containing a cycle is considered an erroneous path.  An error-free
path is acyclic.

\subsection{Actions}

In the rest of this dissertation, for a global transition $t$, instead
of referring to the atomic statement associated to $t$, we will refer
to the \emph{action} of $t$.  An action is a dynamic instance of an
atomic statement in that (1) an action comprises only concrete values
(i.e., constants) and \emph{l-values} while an atomic statement
comprises expressions; (2) there is no action corresponding to the
wildcard receive statement.

\begin{defn}
  Given a vocabulary $(\myprocedure, \var, \globvar, \locvar)$ and a
  domain $\dom$, an expression $e$ is said an \emph{l-value} if it has
  one of the following forms:

  \begin{enumerate}
  \item $v$, for $v \in \var$
  \item $v[c]$, where $v$ is an l-value and $c \in \dom$. $\qed$
  \end{enumerate}
\end{defn}

\begin{defn}
  Let $v$ be an l-value, $c, \textsf{src}$ and $\textsf{dest}$ be
  constants. An \emph{action} is one of the following forms:

  \begin{enumerate}
  \item $\myactskip$,
  \item $\myactassign{v}{c}$,
  \item $\myactsend{$c$}{\textsf{dest}}$, and
  \item $\myactrecv{$v$}{\textsf{src}}$. $\qed$
  \end{enumerate}
\end{defn}

\begin{defn}
  Given a vocabulary, a domain and a \minimp{} model, we have an
  $n$-processes evaluation function $\myeval{~}$ and an $n$-processes
  interpretation function $I$.  Denoted by $\myact{}(t)$, the
  \emph{action} of a transition $t = (s, p, \alpha, s')$ is defined by
  \begin{center}
  \begin{align}
   &\text{let } \textsf{lv}(x) = 
    \begin{cases}
      x, & \text{if } x \in \var{}\\
      \textsf{lv}(x')\textsf{[$\myeval{i}(s, p)$]}, & \text{if } x
      \text{ matches the form } x'\texttt{[$i$]} 
    \end{cases}   \text{ in }\nonumber \\
    %%
    %%
    &1.\ \myact{}(t) = \myactassign{\textsf{lv}(x)}{\myeval{e}(s, p)}, \text{ if }
                                                                        \alpha{} \text{
                                                                        is labeled
                                                                        }\texttt{$x$ =
                                                                        $e$} \nonumber
    \\
    &2.\ \myact{}(t) = \myactsend{$\myeval{e_0}(s, p)$}{$\myeval{e_1}(s,
      p)$}, \text {if }\alpha\text{ is labeled }
              \texttt{\send{$e_0$}{$e_1$}} \nonumber\\
              %% 
              %% 
    &3.\ \myact{}(t) = \myactrecv{$\textsf{lv}(x)$}{$\myeval{e}(s, p)$}, 
                                                                     \text{
      if }\alpha\text{ is labeled } \texttt{\recv{$x$}{$e$}} \nonumber
    \\
    %%
    %%
   &4.\ \myact{}(t) = \myactrecv{$\textsf{lv}(x)$}{$q$},  \text{ if
                                                           }\alpha\text{
                                                           is labeled
                                                           }
                                                           \texttt{\recvany{$x$}{$x'$}},
     \text{ where}
    \nonumber \\
  & \text{$q$ is the sender s.t.\ $\mychan{(s)}(q, p)$ is the only
    message channel changed from $s$ to $s'$.} \nonumber
  \end{align}
  \end{center}
  We leave other cases of $t$ that are obvious to readers out here.  $\qed$
\end{defn}
Note an action is deterministic.

\label{page:term:state-space}



