Changes between Initial Version and Version 1 of OpenMP-Transformation-Introduction

Timestamp:

12/02/21 15:59:26 (4 years ago)

Author:

wuwenhao

Comment:

Create this page for NextGen Omp Trans Sec.1 Intro

OpenMP-Transformation-Introduction

@@ +1 @@
+= 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]