The Sequentially Consistent Subset of OpenMP

OpenMP programs that:

• Do not use non-sequentially consistent atomic directives;
• Do not rely on the accuracy of a false result from omp_test_lock and omp_test_nest_lock; and
• Correctly avoid data races as required in Section 1.4.1 on page 23 (OpenMP spec 5.0) (​spec)

The relaxed consistency model is invisible for such programs, and any explicit flush operations in such programs are redundant.

OpenMP Constructs

• parallel
  • private(list)
  • firstprivate(list)
  • copyin(list)
  • shared(list)
  • default(none|shared)
  • num_threads(n)
  • reduction(op:list)

• sections
  • private(list)
  • firstprivate(list)
  • lastprivate(list)
  • reduction(op:list)
  • nowait

• section

• single
  • private(list)
  • firstprivate(list)
  • copyprivate(list)
  • nowait

• for
  • private(list)
  • firstprivate(list)
  • lastprivate(list)
  • reduction
  • schedule
  • collapse
  • nowait

• simd
  • safelen(n)
  • linear(n)
  • aligned(n)
  • private
  • lastprivate
  • reduction
  • collaplse

• for simd
  • safelen(n)
  • linear(n)
  • aligned(n)
  • private
  • lastprivate
  • reduction
  • collapse
  • firstprivate
  • nowait
  • schedule

• declare simd
  • simdlen(n)
  • linear
  • aligned(n)
  • uniform
  • inbranch
  • notinbranch

• barrier

• critical
  • [name]

• atomic
  • read | write | update | capture
  • seq_cst

• master

OpenMP Types

• omp_lock_t

OpenMP Functions

• omp_get_num_threads()
• omp_get_thread_num()
• omp_get_wtime()

OpenMP Functions

• omp_init_lock
• omp_destroy_lock
• omp_set_lock
• omp_unset_lock
• omp_test_lock

Plan

• We are going to get rid of the current OMP2CIVL transformer and come up a new transformer that assumes given OpenMP programs are sequentially consistent
• We are gong to improve the current OmpSimplifier using pointer alias analysis
• Note that an atomic construct without seq_cst is outside of the sequentially consistent subset of the language, we need a way to deal with that.

Notes

• Currently, the simplifier is not aware of the cases that out-of-bound access on multiple dimensional arrays can raise data race. For example,

  int a[10][5];
  #pragma omp parallel for 
  for (int i = 0; i < 5; i++)
    for (int j = 1; j < 10; j++)
      a[i][j] = a[i][j-1] // a[0][4] and a[1][-1] refer to the same element
  

The current simplifier will incorrectly sequentialize the example above without realizing the fact that this example is sequentializable if and only if no "logical" out-of-bound happens during the execution. A fix for the simplifier could be sequentializing the example with inserted assertion for making sure that there is no "logical" out-of-bound error.

Related

• Static Analysis

OpenMP Simplifier

• We improve the existing OpenMP simplifier with the informations provided by the Static Analysis.
• Example 1: (DRB067-restrictpointer1-orig-no.c from ​DataRaceBench v1.2.0)

  #include <stdlib.h>
  typedef double real8;
  
  void foo(real8 * restrict newSxx, real8 * restrict newSyy, int length)
  {
    int i;
  
  #pragma omp parallel for private (i) firstprivate (length)
    for (i = 0; i <= length - 1; i += 1) {
      newSxx[i] = 0.0;
      newSyy[i] = 0.0;
    }
  }
  
  int main()
  {
    int length=10;
    real8* newSxx = malloc (length* sizeof (real8));
    real8* newSyy = malloc (length* sizeof (real8));
  
    foo(newSxx, newSyy, length);
  
    free (newSxx);
    free (newSyy);
    return 0;
  }
  

  • The OpenMP simplifier analyzes the parallel region with points-to informations about the two pointer argument newSxx and newSyy from static analysis.
  • The OpenMP simplifier can determine that no data race will happen in the parallel region as long as no array out-of-bound error happens in it.
  • The OpenMP simplifier sequentializes the program which will be checked by CIVL. Any possible array out-of-bound error will be caught by CIVL.

• Example 2 : ( DRB014-outofbounds-orig-yes.c from DataRaceBench v1.2.0 )

  #include <stdio.h>
  int main(int argc, char* argv[])
  {
    int i,j;
    int n=10, m=10;
    double b[n][m];
  #pragma omp parallel for private(j)
    for (i=1;i<n;i++)
      for (j=0;j<m;j++) // Note there will be out of bound access                                                               
        b[i][j]=b[i][j-1];
  
    printf ("b[50][50]=%f\n",b[50][50]);
  
    return 0;
  }
  

  • OpenMP Simplifier proves that b[i][j] and b[i][j-1] that accessed by different threads which hold different values of i will have no data race as long as no array out-of-bound error happens.
  • OpenMP Simplifier sequentializes the OpenMP program while the verification condition for array out-of-bound freedom will be checked by CIVL by default.
  • The CIVL back-end runs the sequentialized program and detects the array out-of-bound access.

• Example 3

  #include <omp.h>
  int main()
  {
    int a[50],i;
  
    a[0] = 1;
  #pragma omp parallel for
    for(i=1; i<49; i++)
      {
        int c;
  
        c = i + 10;
        a[i + c] = a[i + c];
      }
  }
  

  • OpenMP Simplifier cannot prove data-race freedom for this program.
  • OpenMP2CIVL Transformer will transform this program to a equivalent CIVL-C program for model checking

Capture Read / Write at Runtime

• If the OpenMP Simplifier fails to sequentialize a program, transform the OpenMP program to the following form for model checking:

  $mem writes[nthreads], reads[nthreads];
  $parfor (int tid:0..nthreads-1) {
    $write_set_push();
    $read_set_push();
    block1;
    // barrier
    writes[tid] = $write_set_pop();                                                                                                                
    reads[tid] = $read_set_pop();
    // check for dataraces (collective operation)                                                                            
    $write_set_push();
    $read_set_push();
    // barrier                                                                                                                  
    stmt2;
    // barrier
    writes[tid] = $write_set_pop();                                                                                                                
    reads[tid] = $read_set_pop();                                                                                                                 
    // check for dataraces (collective operation)
  }
  

• Functions for managing $mem objects can be found in mem.cvh