User Tools

Site Tools


ompverify

ompVerify

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.

Screenshots

Try it !

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:

  1. In the Eclipse main menu, click on File → New → Example…
  2. Search for the Gecos/Polyhedral entry and choose the example called Scop highligther example
  3. Select a project name in the wizard dialog and click on finish

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.

Reference

  • V. Basupalli, Tomofumi Yuki, Sanjay V. Rajopadhye, Antoine Morvan, Steven Derrien, Patrice Quinton, David Wonnacott, ompVerify: Polyhedral Analysis for the OpenMP Programmer. International Workshop on openMP (IWOMP), 2011
ompverify.txt · Last modified: 2016/03/04 21:26 by sderrien