\contentsline {prefacesection}{List of Tables}{ix}{chapter*.4}
\contentsline {prefacesection}{List of Figures}{x}{chapter*.5}
\contentsline {prefacesection}{Abstract}{xv}{chapter*.6}
\contentsline {part}{Part\ \numberline {I}\uppercase {$\nobreakspace {}$Preliminaries}}{1}{part.1}
\contentsline {chapter}{\numberline {1}Introduction}{2}{chapter.1}
\contentsline {section}{\numberline {1.1}Motivation}{2}{section.1.1}
\contentsline {section}{\numberline {1.2}Contributions}{5}{section.1.2}
\contentsline {subsection}{\numberline {1.2.1}A contract theory for message-passing programs}{5}{subsection.1.2.1}
\contentsline {subsection}{\numberline {1.2.2}A method for verifying collective contracts}{6}{subsection.1.2.2}
\contentsline {subsection}{\numberline {1.2.3}An MPI Specification Language}{7}{subsection.1.2.3}
\contentsline {subsection}{\numberline {1.2.4}A Prototype MPI Contract-Based Verification Tool}{8}{subsection.1.2.4}
\contentsline {section}{\numberline {1.3}Outline}{8}{section.1.3}
\contentsline {chapter}{\numberline {2}Background \& Related Work}{10}{chapter.2}
\contentsline {section}{\numberline {2.1}Hoare Logic}{10}{section.2.1}
\contentsline {section}{\numberline {2.2}Formal Methods For Concurrency}{14}{section.2.2}
\contentsline {section}{\numberline {2.3}Model Checking}{17}{section.2.3}
\contentsline {section}{\numberline {2.4}Symbolic Execution}{18}{section.2.4}
\contentsline {section}{\numberline {2.5}MPI}{19}{section.2.5}
\contentsline {section}{\numberline {2.6}Model Checkers for MPI}{21}{section.2.6}
\contentsline {section}{\numberline {2.7}Static Analysis and Runtime Verification for MPI}{24}{section.2.7}
\contentsline {subsection}{\numberline {2.7.1}MPI Static Analyzers}{24}{subsection.2.7.1}
\contentsline {subsection}{\numberline {2.7.2}MPI Runtime Verification}{26}{subsection.2.7.2}
\contentsline {section}{\numberline {2.8}Deductive Verification for MPI}{27}{section.2.8}
\contentsline {chapter}{\numberline {3}Notation}{29}{chapter.3}
\contentsline {part}{Part\ \numberline {II}\uppercase {$\nobreakspace {}$Theory}}{31}{part.2}
\contentsline {chapter}{\numberline {4}The MiniMP Programming Language}{32}{chapter.4}
\contentsline {section}{\numberline {4.1}Syntax}{32}{section.4.1}
\contentsline {section}{\numberline {4.2}The \textsc {MiniMP}{} Model}{35}{section.4.2}
\contentsline {section}{\numberline {4.3}Semantics}{41}{section.4.3}
\contentsline {subsection}{\numberline {4.3.1}Process States and Global States}{41}{subsection.4.3.1}
\contentsline {subsection}{\numberline {4.3.2}Interpretation}{44}{subsection.4.3.2}
\contentsline {subsection}{\numberline {4.3.3}State Space Graph}{47}{subsection.4.3.3}
\contentsline {subsection}{\numberline {4.3.4}Actions}{49}{subsection.4.3.4}
\contentsline {chapter}{\numberline {5}The Specification Language for MiniMP}{51}{chapter.5}
\contentsline {section}{\numberline {5.1}Program Segment}{51}{section.5.1}
\contentsline {section}{\numberline {5.2}Path Predicate}{55}{section.5.2}
\contentsline {section}{\numberline {5.3}Syntax of The \textsc {MiniMP}{} Specification Language}{55}{section.5.3}
\contentsline {section}{\numberline {5.4}Semantics of The \textsc {MiniMP}{} Contracts}{58}{section.5.4}
\contentsline {section}{\numberline {5.5}The Collective Triple}{62}{section.5.5}
\contentsline {subsection}{\numberline {5.5.1}The Intuition in Collective Triple}{64}{subsection.5.5.1}
\contentsline {subsection}{\numberline {5.5.2}Interference}{67}{subsection.5.5.2}
\contentsline {subsection}{\numberline {5.5.3}The Validity of A Collective Triple}{69}{subsection.5.5.3}
\contentsline {chapter}{\numberline {6}A Inference System for MiniMP}{70}{chapter.6}
\contentsline {section}{\numberline {6.1}Rules for Decomposing Collective Triples}{70}{section.6.1}
\contentsline {section}{\numberline {6.2}The Adaptation Problem}{77}{section.6.2}
\contentsline {section}{\numberline {6.3}An Derivation Example}{78}{section.6.3}
\contentsline {section}{\numberline {6.4}Extending the Entering/Exiting Notation}{79}{section.6.4}
\contentsline {section}{\numberline {6.5}Soundness}{81}{section.6.5}
\contentsline {chapter}{\numberline {7}A Verification System for MiniMP}{93}{chapter.7}
\contentsline {section}{\numberline {7.1}Symbolic Execution and Model Checking for \textsc {MiniMP}{}}{93}{section.7.1}
\contentsline {section}{\numberline {7.2}Composite and Modular Verification for \textsc {MiniMP}{}}{98}{section.7.2}
\contentsline {subsection}{\numberline {7.2.1}Collective States}{99}{subsection.7.2.1}
\contentsline {subsection}{\numberline {7.2.2}The Composite and Modular Verification Algorithm}{102}{subsection.7.2.2}
\contentsline {section}{\numberline {7.3}Procedure Contract System for \textsc {MiniMP}{}}{108}{section.7.3}
\contentsline {subsection}{\numberline {7.3.1}Formal Parameters and Return Value}{109}{subsection.7.3.1}
\contentsline {subsection}{\numberline {7.3.2}On The Fly Model Checking with Collective States}{111}{subsection.7.3.2}
\contentsline {subsection}{\numberline {7.3.3}Absence Assertion Verification and Partial Order Reduction}{114}{subsection.7.3.3}
\contentsline {subsection}{\numberline {7.3.4}Infinite Reachable States}{119}{subsection.7.3.4}
\contentsline {section}{\numberline {7.4}Soundness}{120}{section.7.4}
\contentsline {subsection}{\numberline {7.4.1}Soundness of The Monolithic Algorithm}{120}{subsection.7.4.1}
\contentsline {subsection}{\numberline {7.4.2}Soundness of The Composite And Modular Algorithm }{122}{subsection.7.4.2}
\contentsline {part}{Part\ \numberline {III}\uppercase {$\nobreakspace {}$Practice}}{135}{part.3}
\contentsline {chapter}{\numberline {8}Modeling C/MPI Programs in The CIVL Framework}{136}{chapter.8}
\contentsline {section}{\numberline {8.1}CIVL: The Concurrency Intermediate Verification Language}{136}{section.8.1}
\contentsline {section}{\numberline {8.2}Modeling MPI with Transformation and Libraries}{138}{section.8.2}
\contentsline {subsection}{\numberline {8.2.1}The MPI Library}{139}{subsection.8.2.1}
\contentsline {subsection}{\numberline {8.2.2}AST-Level Code Transformation}{142}{subsection.8.2.2}
\contentsline {subsection}{\numberline {8.2.3}MPI Program Properties}{144}{subsection.8.2.3}
\contentsline {chapter}{\numberline {9}Verifying C/MPI Programs with Function Contracts}{146}{chapter.9}
\contentsline {section}{\numberline {9.1}Bring Function Contracts From \textsc {MiniMP}{} To MPI}{146}{section.9.1}
\contentsline {section}{\numberline {9.2}The MPI Contract Language}{150}{section.9.2}
\contentsline {subsection}{\numberline {9.2.1}Syntax}{151}{subsection.9.2.1}
\contentsline {subsection}{\numberline {9.2.2}Semantics}{152}{subsection.9.2.2}
\contentsline {section}{\numberline {9.3}MPI Function Contract System Implementation}{155}{section.9.3}
\contentsline {subsection}{\numberline {9.3.1}Implementing Collates}{155}{subsection.9.3.1}
\contentsline {subsection}{\numberline {9.3.2}Implementing Absence Assertions}{161}{subsection.9.3.2}
\contentsline {subsection}{\numberline {9.3.3}Transformation}{162}{subsection.9.3.3}
\contentsline {chapter}{\numberline {10}Evaluation}{170}{chapter.10}
\contentsline {section}{\numberline {10.1}Running Examples}{170}{section.10.1}
\contentsline {subsection}{\numberline {10.1.1}Allgather Implementations}{171}{subsection.10.1.1}
\contentsline {subsection}{\numberline {10.1.2}Parallel Vector Product}{174}{subsection.10.1.2}
\contentsline {section}{\numberline {10.2}Experiment}{178}{section.10.2}
\contentsline {chapter}{\numberline {11}Summary and Future Work}{187}{chapter.11}
\contentsline {section}{\numberline {11.1}Dissertation Summary}{187}{section.11.1}
\contentsline {section}{\numberline {11.2}Future Work}{189}{section.11.2}
\contentsline {chapter}{\uppercase {Bibliography}}{191}{chapter*.61}