Changes between Version 71 and Version 72 of Next-GenOpenMPTransformation

Timestamp:

03/17/21 10:45:37 (5 years ago)

Author:

wuwenhao

Comment:

--

Next-GenOpenMPTransformation

@@ -42 +42 @@
 
 {{{
+void $check_data_race($mem *rs, $mem *ws, int n, int tid) {
+  $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 _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);
+$mem rs[_omp_nthreads], ws[_omp_nthreads];
+for(..) {
+  ws[i] = empty;
+  rs[i] = empty;
+}
 $for (int _omp_tid: _omp_dom) {
   $depends_on(/*nothing*/)$atomic{
@@ -62 +76 @@
       }
       // RS stack: rs0:={A, B}; WS stack: ws0:={A, B};
-      $check_data_race(); // 1st check
+      $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(); // 2nd check
+      $check_data_race(&rs, &ws, nthreads, tid); // 2nd check
     } // RS stack: <empty>; WS stack: <empty>; empty sets rs0, ws0;
   } // end $atomic