Authors:  Hongyi Ma, Liqiang Wang, University of Wyoming
                Chunhua Liao, Daniel Quinlan, Lawrence Livermore National Laboratory
                Zijiang Yang, Western Michigan University

As one of the popular parallel programming models, OpenMP has been widely used in scientific applications in recent years to facilitate shared-memory parallelism. The increasing availability of multicore devices has permitted more and more sequential programs to be parallelized using OpenMP. Unfortunately, it is a daunting task to develop correct OpenMP programs. Concurrency errors, such as data races and deadlocks, are tricky to detect using traditional testing techniques. This paper presents an OpenMP Analysis Toolkit (OAT) to detect data races and deadlocks using SMT-solver based symbolic analysis, which can approximately simulate the real execution of an OpenMP program with different schedulings. Hence, our symbolic analysis is more accurate than traditional static analysis, and more efficient and scalable than runtime analysis tools. We conducted experiments on real-world OpenMP benchmarks and student homework assignments by comparing our OAT tool with two commercial runtime tools (Intel Thread Checker and Sun Thread Analyzer) for checking multithreaded programs. Our experiments show that our symbolic analysis tool is more efficient and scalable than the two commercial tools. Our tool OAT is as accurate as Sun Thread Analyzer, and both are more precise than Intel Thread Checker for checking concurrency errors in OpenMP programs.

This is a joint work between the University of Wyoming and Lawrence Livermore National Laboratory.