\contentsline {figure}{\numberline {2.1}{\ignorespaces Inference rules of Hoare calculus.\relax }}{12}{figure.caption.7}
\contentsline {figure}{\numberline {2.2}{\ignorespaces The derivation of a Hoare triple. $X$ and $Y$ are auxiliary variables holding the values of \texttt {x} and \texttt {y}, respectively, at pre-state. The symbol $\mathit {abs}$ represents the absolute value function in the underlying first order logic. \relax }}{13}{figure.caption.8}
\contentsline {figure}{\numberline {2.3}{\ignorespaces The computation of the weakest pre-condition, $\textup {WP}(S, Q)$, for a given statement $S$ and desired post-condition $Q$. \relax }}{13}{figure.caption.9}
\contentsline {figure}{\numberline {2.4}{\ignorespaces A simple C/MPI program. Process 0 sends and process 1 receives a message. The remaining processes perform no operation.\relax }}{21}{figure.caption.10}
\contentsline {figure}{\numberline {4.1}{\ignorespaces The grammar of \textsc {MiniMP}{}. An \texttt {\texttt {\textit {\leavevmode {\color {blue}Identifier}}}} is a character sequences. An \texttt {\texttt {\textit {\leavevmode {\color {blue}IntegerLiteral}}}} is an integer literal. An \texttt {\texttt {\char `\{}{} \texttt {\textit {\leavevmode {\color {blue}List-of-Constant}}} \texttt {\char `\}}{}} is an array literal.\relax }}{33}{figure.caption.11}
\contentsline {figure}{\numberline {4.2}{\ignorespaces A \textsc {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}.\relax }}{35}{figure.caption.12}
\contentsline {figure}{\numberline {4.3}{\ignorespaces A \textsc {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}.\relax }}{36}{figure.caption.13}
\contentsline {figure}{\numberline {4.4}{\ignorespaces A \textsc {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}.\relax }}{36}{figure.caption.14}
\contentsline {figure}{\numberline {4.5}{\ignorespaces The pseudocode definition of the translation process.\relax }}{40}{figure.caption.15}
\contentsline {figure}{\numberline {4.6}{\ignorespaces 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 \textsf {skip}{} 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.\relax }}{41}{figure.caption.16}
\contentsline {figure}{\numberline {4.7}{\ignorespaces \textsc {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 {}$}). \relax }}{45}{figure.caption.17}
\contentsline {figure}{\numberline {4.8}{\ignorespaces The definition of the $n$-processes interpretation function $\mathit {I_n}$ that describes the results of executing a local transition from a state by a process.\relax }}{46}{figure.caption.18}
\contentsline {figure}{\numberline {5.1}{\ignorespaces The program segment of the loop \texttt {\textit {\leavevmode {\color {blue}Statement}}} in the \texttt {bcast} procedure showed in Fig.\ \ref {fig:minimp:example:bcast}.\relax }}{53}{figure.caption.19}
\contentsline {figure}{\numberline {5.2}{\ignorespaces The syntax of \textsc {MiniMP}{} specification language\relax }}{56}{figure.caption.20}
\contentsline {figure}{\numberline {5.3}{\ignorespaces The definition of the $n$-processes specification evaluation function $[\tmspace -\thinmuskip {.1667em}[\mathit {e}]\tmspace -\thinmuskip {.1667em}]^{\textsf {spec}}_n$, which evaluates a contract expression $e$ for a process $p$ at a pre- or a post-state $s$ of a program segment $l{\penalty \@M \mskip 2mu\mathpunct {}\nonscript \mkern -\thinmuskip {:}\mskip 6muplus1mu\relax }C\nobreakspace {}{l'}$ in a path $\rho $.\relax }}{59}{figure.caption.21}
\contentsline {figure}{\numberline {5.4}{\ignorespaces The definition of the event interpretation function $\mathit {I^{\textsf {event}}_{C, \rho }}$ with respect to a path $\rho $ and a program segment $l{\penalty \@M \mskip 2mu\mathpunct {}\nonscript \mkern -\thinmuskip {:}\mskip 6muplus1mu\relax }C\nobreakspace {}{l'}$.\relax }}{60}{figure.caption.22}
\contentsline {figure}{\numberline {5.5}{\ignorespaces A contract of a branch statement that ``broadcasts'' a value.\relax }}{62}{figure.caption.23}
\contentsline {figure}{\numberline {5.6}{\ignorespaces A contract for the branch statement that ``gathers'' values from all processes.\relax }}{63}{figure.caption.24}
\contentsline {figure}{\numberline {5.7}{\ignorespaces A \textsc {MiniMP}{} program in pseudocode where \textit {init} is a procedure that depends on \texttt {PID} and initializes \texttt {dat} elements. Suppose \texttt {\textit {barrier}} is a barrier.\relax }}{65}{figure.caption.25}
\contentsline {figure}{\numberline {6.1}{\ignorespaces Rules for decomposing collective triples\relax }}{75}{figure.caption.26}
\contentsline {figure}{\numberline {6.2}{\ignorespaces A contract for the sequential combination of the two branch statements given by Fig.\ \ref {fig:minimp:spec:gather} and \ref {fig:minimp:spec:bcast}.\relax }}{79}{figure.caption.27}
\contentsline {figure}{\numberline {6.3}{\ignorespaces A $\mathcal {R}$ derivation of a collective triple that specifies a sequential combination of two collective style \textsc {MiniMP}{} statements. \relax }}{80}{figure.caption.28}
\contentsline {figure}{\numberline {7.1}{\ignorespaces The definition of the interpretation for symbolic execution with $n$ processes.\relax }}{94}{figure.caption.29}
\contentsline {figure}{\numberline {7.2}{\ignorespaces The definition of contract violation and deadlock for a prefix $\rho $ of an execution in the state space graph $G$ searched by $\textsc {Mc}(\mathcal {M}, \delimiter "426830A {}\psi ,\tmspace +\thinmuskip {.1667em}\Gamma {}\delimiter "526930B {}\nobreakspace {}C\nobreakspace {}\delimiter "426830A {}\phi ,\tmspace +\thinmuskip {.1667em}\Upsilon {}\delimiter "526930B {}{}, n)$.\relax }}{98}{figure.caption.30}
\contentsline {figure}{\numberline {7.3}{\ignorespaces A collective state (upper right) associated with an execution (below) of a \textsc {MiniMP}{} program (upper left). All processes are collectively at line 6 in the collective state.\relax }}{103}{figure.caption.31}
\contentsline {figure}{\numberline {7.4}{\ignorespaces Conditions of a contract violation of an execution $\pi $ explored by $\textsc {Mc}^{\Delta }(\mathcal {M}, \frac {\textsf {Tri}}{\delimiter "426830A {}\psi ,\tmspace +\thinmuskip {.1667em}\Gamma {}\delimiter "526930B {}\nobreakspace {}C\nobreakspace {}\delimiter "426830A {}\phi ,\tmspace +\thinmuskip {.1667em}\Upsilon {}\delimiter "526930B {}{}}, n)$.\relax }}{107}{figure.caption.32}
\contentsline {figure}{\numberline {7.5}{\ignorespaces A \textsc {MiniMP}{} procedure \texttt {exchange} and its contract.\relax }}{111}{figure.caption.33}
\contentsline {figure}{\numberline {7.6}{\ignorespaces The structure of a collate type object for $n$ processes. \textsf {id} denotes the identifier of the associated procedure, \textsf {tag} indicates whether the collate serves for a collective pre- or post-state. Every $\textsf {slot}_i$ will hold a process state of a process $i$. The \textsf {channels} stores a copy of message channels, which keeps being updated.\relax }}{113}{figure.caption.34}
\contentsline {figure}{\numberline {7.7}{\ignorespaces Collates in states along the on-the-fly exploration of the execution showed in Fig.\ \ref {fig:minimp:example:collective:state}.\relax }}{115}{figure.caption.35}
\contentsline {figure}{\numberline {8.1}{\ignorespaces The layout of the CIVL framework\relax }}{137}{figure.caption.36}
\contentsline {figure}{\numberline {8.2}{\ignorespaces A selected set of CIVL-C primitives\relax }}{138}{figure.caption.37}
\contentsline {figure}{\numberline {8.3}{\ignorespaces A CIVL-C representation of a hierarchical concurrency memory model.\relax }}{139}{figure.caption.38}
\contentsline {figure}{\numberline {8.4}{\ignorespaces The definition of \texttt {MPI\texttt {\char `\_}{}Recv} in the MPI library in CIVL.\relax }}{140}{figure.caption.39}
\contentsline {figure}{\numberline {8.5}{\ignorespaces The general C/MPI to CIVL-C transformation template.\relax }}{143}{figure.caption.40}
\contentsline {figure}{\numberline {9.1}{\ignorespaces An MPI collective-style function that requires any following statement not to send any message with tag 1 to process 0 until process 0 exits it.\relax }}{148}{figure.caption.41}
\contentsline {figure}{\numberline {9.2}{\ignorespaces A sequential C function with an ACSL contract.\relax }}{150}{figure.caption.42}
\contentsline {figure}{\numberline {9.3}{\ignorespaces The syntax of the behaviors of the MPI contract language.\relax }}{151}{figure.caption.43}
\contentsline {figure}{\numberline {9.4}{\ignorespaces The syntax of the expression of the MPI contract language. The \texttt {\textit {\leavevmode {\color {blue}ACSL-Expr}}} stands for the expression syntax of ACSL.\relax }}{152}{figure.caption.44}
\contentsline {figure}{\numberline {9.5}{\ignorespaces A collective-style MPI function \texttt {ring} with a contract.\relax }}{153}{figure.caption.45}
\contentsline {figure}{\numberline {9.6}{\ignorespaces CIVL-C implementation for collate and collate queue\relax }}{157}{figure.caption.46}
\contentsline {figure}{\numberline {9.7}{\ignorespaces A CIVL state of a CIVL-C program transformed from an general MPI program, which contains a function \texttt {f}. The boxes labeled by \textbf {d0, d1, ...} are dyscopes. Arrows between dyscopes denote the ``parent-of'' relation. Boxes under ``p0, p1, p2'' are call stack entries. Dashed arrows mark the referred dyscope of every call stack entry.\relax }}{159}{figure.caption.47}
\contentsline {figure}{\numberline {9.8}{\ignorespaces Merging a snapshot to a state. The snapshot (on the right) was taken from the state in Fig.\ \ref {fig:civl:state} for process p1.\relax }}{160}{figure.caption.48}
\contentsline {figure}{\numberline {9.9}{\ignorespaces The simplified code of the CIVL-C function that will be called every time a send operation was performed by a process in order to check for the free of \textbf {PGV}.\relax }}{163}{figure.caption.49}
\contentsline {figure}{\numberline {9.10}{\ignorespaces Transformation template for generating \texttt {f\texttt {\char `\_}{}driver} from a function \texttt {f} with its contract. The upper shows the original annotated function \texttt {f} and the lower shows the generated \texttt {f\texttt {\char `\_}{}driver}.\relax }}{167}{figure.caption.50}
\contentsline {figure}{\numberline {9.11}{\ignorespaces The transformation template for summarizing \texttt {f} with respect to its contract.\relax }}{169}{figure.caption.51}
\contentsline {figure}{\numberline {10.1}{\ignorespaces Annotating function contracts for all the collective-style functions used by CIVL's implementation of \texttt {MPI\texttt {\char `\_}{}Allreduce}.\relax }}{173}{figure.caption.52}
\contentsline {figure}{\numberline {10.2}{\ignorespaces An \texttt {MPI\texttt {\char `\_}{}Allreduce} implementation based on the recursive doubling algorithm.\relax }}{175}{figure.caption.53}
\contentsline {figure}{\numberline {10.3}{\ignorespaces The data structures that are used in Fig.\ \ref {fig:mpi:dotprod}. Insignificant fields are omitted.\relax }}{176}{figure.caption.54}
\contentsline {figure}{\numberline {10.4}{\ignorespaces A function that computes vector product in parallel using MPI.\relax }}{177}{figure.caption.55}
\contentsline {figure}{\numberline {10.5}{\ignorespaces The definition of the \texttt {matmat} function that collectively performs matrix multiplication.\relax }}{181}{figure.caption.56}
\contentsline {figure}{\numberline {10.6}{\ignorespaces Function contract of the function in the \texttt {OddEvenSort} example.\relax }}{182}{figure.caption.57}