The OpenMP Analysis Toolkit (OAT) is able to automatically detect data races and deadlocks accurately and efficiently. It includes a novel encoding algorithm specialized for OpenMP programs.  In particular, we encode every parallel code region of an OpenMP program into formulae suitable for off-the-shelf SMT-solvers such as Yices. By interpreting the solution reported by Yices, we are able to reproduce a feasible execution trace that reveals the errors. This evidence-based approach not only improves the accuracy of error detection, but is also very useful in debugging programs and fixing problems.

PI:

Dr. Liqiang Wang, Computer Science, University of Wyoming, University of Central Florida

Major Developer:

Dr. Hongyi Ma, Computer Science, University of Wyoming 

Collaborators:

Dr. Chunhua Liao, Lawrence Livermore National Laboratory

Dr. Daniel Quinlan, Lawrence Livermore National Laboratory

Dr. Zijiang Yang, Western Michigan University

Publications:

[1] Hongyi Ma*, Steve R. Diersen, Liqiang Wang, Chunhua Liao, Daniel Quinlan, and Zijiang Yang. Symbolic Analysis of Concurrency Errors in OpenMP Programs. In the 42nd International Conference on Parallel Processing (ICPP-2013). October 1-4, 2013, Lyon, France. IEEE Press.

[2] Hongyi Ma*, Liqiang Wang, and Krishanthan Krishnamoorthy*. Detecting Thread-Safety Violations in Hybrid OpenMP/MPI Programs. In the 2015 IEEE International Conference on Cluster Computing (CLUSTER 2015), Sept. 2015. Chicago, USA. IEEE Press.

Source Code Download.