%%%%%%%%%%% 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}