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