wiki:Next-GenOpenMPTransformation

Version 28 (modified by siegel, 7 years ago) ( diff )

--

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.

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.

The Current Approach For Model Checking OpenMP Programs

  • Example: 
    #include <omp.h>
int main()
{
  int a[10],i;

#pragma omp parallel for
  for(i=0; i<10; i++)
    {
      int c;

      c = i % 2;
      a[i + c] = 0;
    }
}
    • 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. Here is the code snippet for the CIVL-C program after transformation: 
      int main() {
  int  a[10];
  {
    {
      int _elab_i = 0;
      for (; _elab_i < _omp_num_threads; _elab_i = _elab_i + 1)
        ;
    }
    int $sef$0 = $choose_int(_omp_num_threads);
    int _omp_nthreads = 1 + $sef$0;
    $range _omp_thread_range = 0 .. _omp_nthreads - 1;
    $domain(1) _omp_dom = ($domain){_omp_thread_range};
    $omp_gteam _omp_gteam = $omp_gteam_create($here, _omp_nthreads);
    $omp_gshared _omp_a_gshared = $omp_gshared_create(_omp_gteam, &(a));
    $parfor (int _omp_tid: _omp_dom) {
      $omp_team _omp_team = $omp_team_create($here, _omp_gteam, _omp_tid);
      int  _omp_a_local[10];
      int  _omp_a_status[10];
      $omp_shared _omp_a_shared = $omp_shared_create(_omp_team, _omp_a_gshared, &(_omp_a_local), &(_omp_a_status));
      {
        $range _omp_r1 = 1 .. 10 - 1 # 1;
        $domain(1) _omp_loop_domain = ($domain){_omp_r1};
        $domain $sef$1 = $omp_arrive_loop(_omp_team, 0, ($domain)_omp_loop_domain, 2);
        $domain(1) _omp_my_iters = ($domain(1))$sef$1;
        $for (int _omp_i_private: _omp_my_iters) {
          int c;
          c = _omp_i_private % 2;
          int _omp_write0;
          _omp_write0 = 0;
          $omp_write(_omp_a_shared, &(_omp_a_local[c]), &(_omp_write0));
        }
      }
      $omp_barrier_and_flush(_omp_team);
      $omp_shared_destroy(_omp_a_shared);
      $omp_team_destroy(_omp_team);
    }
    $omp_gshared_destroy(_omp_a_gshared);
    $omp_gteam_destroy(_omp_gteam);
  }
}
    • CIVL reports PROVABLE errors: 
      Thread 1 can not safely write to memory location &<d5>a[0], because thread 0 has
written to that memory location and hasn't flushed yet.

Violation 0 encountered at depth 64:
CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at OpenMPTransformer "_omp_a_shared, &(_om" inserted by OpenMPTransformer.a_sharedWriteCall before civlc.cvh:105.14-20 "$malloc"
Assertion: false
 -> false
. . .
Call stacks:
process 0:
  main at OpenMPTransformer "$parfor (int _omp_ti" inserted by OpenMPTransformer.parallelPragma before civlc.cvh:105.14-20 "$malloc"
process 1:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  $omp_barrier_and_flush at civl-omp.cvl:322.2-14 "$barrier_call" called from
  _par_proc0 at OpenMPTransformer "_omp_team" inserted by OpenMPTransformer.barrierAndFlushCall before civlc.cvh:105.14-20 "$malloc"
process 2:
  $omp_write at civl-omp.cvl:247.4-10 "$assert" called from
  _par_proc0 at OpenMPTransformer "_omp_a_shared, &(_om" inserted by OpenMPTransformer.a_sharedWriteCall before civlc.cvh:105.14-20 "$malloc"
process 3:
  $omp_arrive_loop at civl-omp.cvl:405.2-8 "$atomic" called from
  _par_proc0 at OpenMPTransformer "_omp_team, 0, ($doma" inserted by OpenMPTransformer.myItersDeclaration before civlc.cvh:105.14-20 "$malloc"

Logging new entry 0, writing trace to CIVLREP/testOmp5_0.trace
Terminating search after finding 1 violation.

The New Approach for Model Checking OpenMP programs

  • Using CIVL's new infrastructure that captures reads / writes 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

Transformation Details

Support Types

  • $omp_gteam: global team object, represents a team of threads executing in a parallel region. A handle type. This is where all the state needed to correctly execute a parallel region will be stored. This includes a global barrier and a worksharing queue (incomplete array-of-$omp_work_record) for every thread. Definition: 
    typedef struct OMP_gteam {
  $scope scope;
  int nthreads;
  _Bool init[];
  $omp_work_record work[][];
  $gbarrier gbarrier;
} * $omp_gteam;
  • $omp_team: local object belonging to a single thread and referencing the global team object. A handle type. It also includes a local barrier. Definition: 
    typedef struct OMP_team {
  $omp_gteam gteam;
  $scope scope;
  int tid;
  $barrier barrier;
} * $omp_team;
  • $omp_work_record: the worksharing information that a thread needs for executing a worksharing region. It contains the kind of the worksharing region, the location of the region, the status of the region and the subdomain (iterations/sections/task assigned to the thread). 
    typedef struct OMP_work_record {
  int kind; // loop, barrier, sections, or single
  int location; // location in model of construct
  _Bool arrived; // has this thread arrived yet?
  $domain loop_dom;// full loop domain; null if not loop
  $domain subdomain; // tasks this thread must do
} $omp_work_record;

Support Functions

Team creation and destruction

  • $omp_gteam $omp_gteam_create($scope scope, int nthreads)
    • creates new global team object, allocating object in heap in the specified scope. Number of threads that will be in the team is nthreads.
  • void $omp_gteam_destroy($omp_gteam gteam)
    • destroys the global team object. All shared objects associated to the team must have been destroyed before calling this function.
  • $omp_team $omp_team_create($scope scope, $omp_gteam gteam, int tid)
    • creates new local team object for a specific thread.
  • void $omp_team_destroy($omp_team team)
    • destroys the local team object

Other

  • void $omp_apply_assoc(void * x, $operation op, void * y)
    • translation of x = x op y
  • void $omp_flush_all($omp_team)
    • performs an OpenMP flush operation on all shared objects. This is the default in OpenMP if no argument is specified for a flush construct.
Note: See TracWiki for help on using the wiki.