ompVerify is a static analysis tool that is developed by CAIRN and Mélange (Colorado State University) that verifies OpenMP programs. The tool is based on polyhedral analyses that is actively used for automatic parallelization. In this tool, we use the same analysis techniques for verification of already parallelized programs. The tool is capable of reasoning at the instance/element-wise level, enabling more precise verification. The analysis is currently based on the well known omega test by Pugh et al.
The type of errors that is detected by ompVerify are data races and unsafe reads from shared variables. Both of these errors can be very easily introduced by misplacing parallel loops, or forgetting to mark some variables to be private.
The tool is integrated into the Eclipse IDE and its CDT (C/C++ Development Tooling) to verify C/C++ programs with OpenMP pragmas, aiming to provide real-time static verification for OpenMP programmers.
The ompVerify tool is open-source and can be installed as a regular GeCoS feature through the standard installation process. The feature to install is called ompVerify and belongs to the Extra category.
The ompVerify feature provides a wizard to demonstrate what can be achieved with the tool:
The example contains just a simple C source file called omp.c. This C source file contains several functions with loops and openMP pragmas illustrating how the tool can be used.