When implementing a software model using the one-sided communication of MPI, the developer is required to obey certain rules with respect to memory consistency, process synchronization and operation completion in order to avoid data races and undefined behavior. For a non-trivial application, dealing with different synchronization and memory models that are provided by MPI version 3, manual correctness checks may turn out to be cumbersome. This thesis evaluates the ability to perform a verification of properties specific to the use of one-sided communication of MPI by statically analyzing an LLVM intermediate representation using two different IFDS problem models, powered by a static analysis framework named Phasar.

@mastersthesis{VOOMCCUSAI19,
	author	 = {Marcel Heing-Becker},
	title	 = {{Verification of one-sided MPI communication code using static analysis in LLVM}},
	advisors	 = {Jannek Squar and Michael Kuhn},
	year	 = {2019},
	month	 = {02},
	school	 = {Universität Hamburg},
	howpublished	 = {{Online \url{https://wr.informatik.uni-hamburg.de/_media/research:theses:marcel_heing_becker_verification_of_one_sided_mpi_communication_code_using_static_analysis_in_llvm.pdf}}},
	type	 = {Master's Thesis},
	abstract	 = {When implementing a software model using the one-sided communication of MPI, the developer is required to obey certain rules with respect to memory consistency, process synchronization and operation completion in order to avoid data races and undefined behavior. For a non-trivial application, dealing with different synchronization and memory models that are provided by MPI version 3, manual correctness checks may turn out to be cumbersome. This thesis evaluates the ability to perform a verification of properties specific to the use of one-sided communication of MPI by statically analyzing an LLVM intermediate representation using two different IFDS problem models, powered by a static analysis framework named Phasar.},
}