= 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) ([https://www.openmp.org/wp-content/uploads/OpenMP-API-Specification-5.0.pdf 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. 

----
[https://vsl.cis.udel.edu/trac/civl/wiki/Next-GenOpenMPTransformation Back: Index]

[https://vsl.cis.udel.edu/trac/civl/wiki/OpenMP-Transformation-Supported-Features Next: Supported OpenMP Features]