OpenMP Program Verification Based On Bounded Model Checking

With the rapid development and wide application of software,parallel programs are becoming more and more popular in some important fields such as weather forecasting and oil exploration.Currently,OpenMP has become the most widely used parallel programming language.Due to the non-determinism of the execution order among threads,OpenMP is more error-prone than traditional serial programs,and program errors are difficult to reproduce,which brings great difficulties to the debugging of the program.Moreover,the related OpenMP program verification technology and verification tools are still immature.These factors make the correctness of the OpenMP programs difficult to guarantee,which seriously hinders the development of OpenMP programs.In order to better guarantee the correctness of the OpenMP program,this paper studied how to apply the efficient verification technologies,such as the bounded model checking used by Yogar-CBMC which is an efficient Pthreads program verification tool,to the verification of OpenMP program.Firstly,by studying the characteristics of OpenMP programs and the efficient verification techniques used by Yogar-CBMC,this paper proposed a method that convert OpenMP programs into lower-level Pthreads programs,then use Yogar-CBMC to verify it.Then,the semantics of OpenMP directives are converted based on the Pthreads program,and the OpenMP program is converted into an equivalent Pthreads program.By modifying the open source OpenMP compiler OMPi and rewriting the corresponding Pthreads runtime library,this paper implemented the function of automatically converting the OpenMP program into a streamlined Pthreads program,and then uses Yogar-CBMC to directly verify the converted Pthreads program,extending Yogar-CBMC to support for OpenMP program verification.As a result,the efficient verification techniques used in Yogar-CBMC,such as bounded model checking,abstraction refinement and graph based analysis,are applied to OpenMP program verification,which enables efficient verification of OpenMP programs.