Changes between Version 69 and Version 70 of Next-GenOpenMPTransformation

Timestamp:

03/15/21 19:50:06 (5 years ago)

Author:

wuwenhao

Comment:

--

Next-GenOpenMPTransformation

@@ -10 +10 @@
 2. At a left mover (e.g., unlock, exit_critical), 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(); clean_all(); barrier();
-4. In a $track{..} scope, both read and write operations of shared variables are tracked for checking data race.
-    ($tracked_reads() and $tracked_writes() are functions returning a set containing all shared variables read or written.)
+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 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.,
@@ -37 +49 @@
   $depends_on(/*nothing*/)$atomic{
     $omp_team _omp_team = $omp_team_create($here, _omp_gteam, _omp_tid);
-    $track{ // RS stack: rs0; WS stack: ws0;
+    $track{ // RS stack: rs0:={}; WS stack: ws0:={};
       // Enter parallel region
       A; 
       $yield();
-      $track{ // RS stack: rs0, rs1; WS stack: ws0, ws1;
-        $when(_omp_critical_c->value == 0);
-        $track{ // Ignore race on lock
-           _omp_critical_c->value = 1; // Enter critical block
-        }
-        B;
-        $track{ // Ignore race on lock
-           _omp_critical_c->value = 0; // Exit critical block
-        }
-        $check_data_race(); // 1st check
-      } // RS stack: rs0; WS stack: ws0; empty sets rs1, ws1;
+      $when(_omp_critical_c->value == 0);
+      $track{ // Ignore race on lock
+         _omp_critical_c->value = 1; // Enter critical block
+      }
+      B;
+      $track{ // Ignore race on lock
+         _omp_critical_c->value = 0; // Exit critical block
+      }
+      // RS stack: rs0:={A, B}; WS stack: ws0:={A, B};
+      $check_data_race(); // 1st check
+      $track_clean();
+      // RS stack: rs0:={}; WS stack: ws0:={};
       C;
       $check_data_race(); // 2nd check