Analysis And Verification Of MPI Programs Based On Symbolic Execution

Software dependability is of great importance for modern computing systems.Message Passing Interface(MPI)has been the mainstream framework for parallel programs.A significant part of parallel programs were written with MPI,many of which are developed in dozens of person-years.Because of the large scale of MPI applications and the high cost of building and maintaining super computers,the assurance of the quality of MPI softwares draws more and more attention.And the analysis and verification of MPI programs becomes a key part of developing large scale parallel programs to improve dependability.Bugs of MPI programs can be input-related.Hence the bugs of MPI programs appear “sometimes”,i.e.,a bug may appear in some runs and disappear in the rest runs,depending on the input.Techniques without input space coverage such as testing,correctness checking and dynamic verification may miss such input-related bugs.Symbolic execution is a constraint solving based program analysis technique originally introduced in the 1970 s,which can explore the state space of a program systematically.Symbolic execution can be employed to bug finding,automatic testing and automatic verification of programs.The basic idea of this thesis is to employ symbolic execution to analyze MPI programs.However,as a general technique of program analysis,symbolic execution faces challenges when analyzing MPI programs with complexity and non-determinism being its inherent qualities: it can not provide both non-determinism coverage and input coverage;another problem is the scalability challenge,especially analyzing big MPI programs.In this thesis,we focus on these two challenges,aiming to improve the dependability of MPI programs.The main contributions of this thesis are listed as follows:1.Symbolic execution of synchronous MPI programs.Most existing error detection methods for MPI programs can not provide both input coverage and non-determinism coverage,which leads to missing errors.To achieve high performance,MPI allows so called “wildcard” receives,i.e.,allowing a wildcard value for tags or sources of receives,which can match many possiblesends,depending on the runtime choices made by the MPI library.This brings much non-determinism.In this thesis,we employ symbolic execution to ensure input coverage,and propose a method named lazy-matching to ensure non-determinism coverage for blocking MPI programs with wildcard receives.We propose a on-the-fly scheduler to avoid exploring interleavings blindly.We have proved that no deadlock would be missed when using this scheduler.The results of the experiments on benchmarks show that our method can find deadlocks and runtime errors efficiently.2.Symbolic execution of asynchronous MPI programs.When developing MPI programs,the overlap of communication and computation is commonly used to improve the performance,and the overlap is achieved by using non-blocking calls.However,when analyzing MPI programs with nonblocking calls,the method for synchronous MPI programs faces problems.To cover both input space and non-determinism space,we extend the lazy-matching method,with the main idea of delaying the matches of wildcard receives as much as possible.On the other hand,as a major challenge of symbolic execution,the path explosion problem becomes more severe when analyzing MPI programs: theoretically,the path number is exponential with process number of an MPI program,the number of the sends any wildcard receive may match and number of branches in the program.In this thesis,we propose a deadlock oriented guiding method,which encodes the guiding problem into a deadlock model checking problem,and guides the symbolic executor to find deadlocks quickly according to the result of model checking.3.Detecting MPI buffer errors.Using non-blocking MPI calls leads to buffer errors frequently.In this thesis,we propose a symbolic execution based method to detect the input-related buffer errors in MPI programs.Using the aforementioned methods of the symbolic execution of MPI programs,we can systematically check each path of an MPI program with respect to the critical property of message buffers.To avoid the significant overhead brought by buffer error checking at each memory access,two optimizations are proposed to improve the efficiency by reducing the times of buffer error checking.Besides,according to the symbolic execution methods of synchronous and asynchronous MPI programs,we have implemented a symbolic execution platform named MPISE.MPISE works on source code level,and provides the ability of detecting deadlocks,buffer errors and runtime errors of MPI programs.MPISE has several advantages such as providing the coverage of both input space and non-determinism,supporting nonblocking calls and no need to modify the analyzed source code.In addition,we have employed MPISE to analyze a MPI program up to 80 k LOC successfully.