1 OpenMP Transformation Introduction

1.1 The Sequentially Consistent Subset of OpenMP

The current domain for OpenMP program verification focuses on sequentially consistent 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.

1.2 Overview of OpenMP Transformation

1.2.1 Data Race Detection by Analyzing Read/Write Operations

Basic Transformation Pattern

1. At a right mover (e.g. lock, enter_critical, enter_atomic), we do yield and push.
2. At a left mover (e.g., unlock, exit_critical, exit_atomic), we do check and then clean (pop).

(Note that it only clean whats in between a pair of right mover and left mover.)

3. A barrier is transformed as: barrier() ; $check_data_race(); $track_clean(); barrier();
4. Read and write operations are tracked in $atomic scope and functions/primitives of tracking read/write operations are:
   • $track{ . . . . . . . . . . . . . . . . creates a new pair of read/write sets for tracking.
   • } // end of $track scope . . removes read/write sets currently used for tracking.
   • $track_empty(); . . . . . . . . . . empties read/write sets currently used for tracking.
   • $tracked_reads(); . . . . . . . . returns a set of tracked shared variables read by its caller process.
   • $tracked_writes(); . . . . . . . returns a set of tracked shared variables written by its caller process.
5. $check_data_race asserts that:

     $forall (int i, j: 0 .. nthreads - 1) (i != j) ==> 
       $mem_disjoint(
         writes[i], 
         $mem_union(reads[j], writes[j])
       );
   

E.g.,

#pragma omp parallel shared(s)
{
  A;
  #pragma omp critical(c)
  {
    B;
  }
  C;
}

==>

void $check_data_race($mem *rs, $mem *ws, int n, int tid) {
  rs[tid] = $tracked_reads();
  ws[tid] = $tracked_writes();
  $assert(
    $forall (int j: 0 .. nthreads - 1) (j != tid) ==> 
      $mem_disjoint(ws[tid], $mem_union(rs[j], ws[j])) &&
      $mem_disjoint(...)
  );
}

// Init parallel region env.
$range thread_range = 0 .. nthreads - 1;
$domain(1) dom = ($domain){thread_range};
$omp_gteam gteam = $omp_gteam_create($here, nthreads);
$mem rs[nthreads], ws[nthreads]; // read sets and write sets.
for(int i=0; i<nthreads; i++) {
  ws[i] = $mem_empty();
  rs[i] = $mem_empty();
}

// Transformed parallel region
$for (int tid: dom) {
  $depends_on(/*nothing*/)$atomic{
    $omp_team team = $omp_team_create($here, gteam, tid);
    $track{ // RS stack: rs0:={}; WS stack: ws0:={};
      // Enter parallel region
      A; 
      $yield();
      $when(critical_c->value == 0);
      $track{ // Ignore race on lock
         critical_c->value = 1; // Enter critical block
      }
      B;
      $track{ // Ignore race on lock
         critical_c->value = 0; // Exit critical block
      }
      // RS stack: rs0:={A, B}; WS stack: ws0:={A, B};
      $check_data_race(&rs, &ws, nthreads, tid); // 1st check
      $track_clean();
      rs[tid] = $mem_empty(); 
      ws[tid] = $mem_empty(); 
      // RS stack: rs0:={}; WS stack: ws0:={};
      C;
      $check_data_race(&rs, &ws, nthreads, tid); // 2nd check
    } // RS stack: <empty>; WS stack: <empty>; empty sets rs0, ws0;
  } // end $atomic
} // end $for

We denotes that thread x executes statement A as Ax. Assuming there are two threads 0 and 1, two traces shall be explored:

Trace1: A0y0 A1y1 B0cdr0C0cdr0 B1cdr1C1cdr1;

Trace2: A0y0 A1y1 B1cdr1C1cdr1 B0cdr0C0cdr0;

For the first trace, cdr0 following B0 checks data races between

A0 and A1; B0 and A1;

Then, w/r sets on thread 0 is cleaned.

The second cdr0 following C0 checks data races between

C0 and A1;

An implicit barrier is placed at the end after the second cdr0, thus thread 1 starts executing its remaining part. The first cdr1 checks data races between

C0 and A1; C0 and B1;

Then, tracked sets on both A1 and B1 are cleaned.

Finally, the last cdr1 in the first trace checks data races between

C0 and C1;

The second trace will complete checking by performing checks between

B1 and A0 C1 and A0 C1 and B0

Because B is protected by critical section, races between B0 and B1 are not checked. As a result, all required pairs are checked.

Back: Index

Next: Supported OpenMP Features