1 of 1

Verification of OpenMP SIMD using CIVL

1

Scientific Achievement

Efforts to model OpenMP’s SIMD clause within the CIVL verifier identified ambiguities in the OpenMP specification. CIVL can be used to help resolve those ambiguities.

Significance and Impact

Discussion with the OpenMP committee led the committee to revisit the definitions in the specification and ultimately conclude that the current description, based on the undefined notion of “lexical forward dependency”, needs to be revised to accurately capture the expected behavior of compilers and the conditions under which the SIMD clause can be safely used.

Is this a correct use of the OpenMP SIMD directive? The answer depends on whether the OpenMP implementation is expected to force all SIMD lanes to complete the reads of A[i+2] before any begins the write to A[i]. By default, CIVL imposes no restrictions on the lanes and will reveal data races in this code.

Technical Approach

  • CIVL converts parallel C or Fortran programs using MPI or OpenMP, or CUDA-C, to the Concurrency Intermediate Verification Language for verification by symbolic execution and model checking.
  • CIVL has been extended to allow a user to specify, using annotations, the dependencies within an OpenMP SIMD loop.

PI(s): Jan Hückelheim, Stephen F. Siegel

Collaborating Institutions: Argonne National Laboratory, University of Delaware

ASCR Program: SciDAC

ASCR PM: Kalyan Perumalla (SciDAC RAPIDS2)

#pragma omp simd

for (int i=0; i<N-2; i++) {

int a;

a = A[i+2];

A[i] = a;

}

#pragma omp simd

for (int i=0; i<N-2; i++) {

int a;

#pragma civl depend source(A)

a = A[i+2];

#pragma civl depend target(A)

A[i] = a;

}

The pragmas above direct CIVL to preserve the dependency. This code verifies successfully. CIVIL identified the need to revise OpenMP SIMD specification.