OpenMP Analysis Toolkit (OAT)


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.



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

Major Developer:

Dr. Hongyi Ma, Computer Science, University of Wyoming 


Dr. Chunhua Liao, Lawrence Livermore National Laboratory

Dr. Daniel Quinlan, Lawrence Livermore National Laboratory

Dr. Zijiang Yang, Western Michigan University


[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.