Changes between Version 7 and Version 8 of OpenMP-Transformation-Introduction

Timestamp:

07/10/22 03:23:46 (4 years ago)

Author:

wuwenhao

Comment:

--

OpenMP-Transformation-Introduction

@@ -49 +49 @@
 
 {{{
-void $check_data_race($mem *rs, $mem *ws, int n, int tid) {
+void $update_memsets($mem *rs, $mem *ws, int tid) {
   rs[tid] = $tracked_reads();
   ws[tid] = $tracked_writes();
+}
+}}}
+
+{{{
+void $check_data_race($mem *rs, $mem *ws, int tid, int nthreads) {
   $assert(
     $forall (int j: 0 .. nthreads - 1) (j != tid) ==> 
@@ -59 +64 @@
 }
 }}}
+
+{{{
+void $lock(lock_t l) {
+  $track{ // Ignore race on lock
+    $when(l->value == 0);
+    l->value = 1; // Enter critical block
+  }
+}
+
+void $unlock(lock_t l) {
+  $track{ // Ignore race on lock
+    l->value = 0; // Exit critical block
+  }
+}
+}}}
+
 {{{
 // Init parallel region env.
@@ -76 +97 @@
     $track{ 
       // Enter parallel region
-// local memset stacks: rs:={{}}; ws:={{}};
       A; 
-// local memset stacks: rs:={{A}}; ws:={{A}};
-// update global memsets RS[tid] and WS[tid] in $yield
-// global memses: RS[tid]:={A}; WS[tid]:={A};
+
+      $update_memsets(&RS, &WS, tid);
       $yield();
-// local memset stacks: rs:={{A}, {}}; ws:={{A}, {}};
-
-      $when(critical_c->value == 0);
-      $track{ // Ignore race on lock
-         critical_c->value = 1; // Enter critical block
-      }
+
+      $lock(&critical_c);
       B;
-// local memset stacks: rs:={{A}, {B}}; ws:={{A}, {B}};
-      $track{ // Ignore race on lock
-         critical_c->value = 0; // Exit critical block
-      }
-// update global memsets RS[tid] and WS[tid] in $check_data_race
-// global memses: RS[tid]:={A}U{B}; WS[tid]:={A}U{B};
-      $check_data_race(&RS, &WS, nthreads, tid); // 1st check
+      $unlock(critical_c);
+
+      $update_memsets(&RS, &WS, tid);
+      $check_data_race(&RS, &WS, tid, nthreads); // 1st check
       $track_clean();
-// local memset stacks: rs:={{}}; ws:={{}};
 
       C;
-// local memset stacks: rs:={{C}}; ws:={{C}};
-// update global memsets RS[tid] and WS[tid] in $check_data_race
-// global memses: RS[tid]:={C}; WS[tid]:={C};
-      $check_data_race(&rs, &ws, nthreads, tid); // 2nd check
+
+      $update_memsets(&RS, &WS, tid);
+      $check_data_race(&rs, &ws, tid, nthreads); // 2nd check
     } // RS stack: <empty>; WS stack: <empty>; empty sets rs0, ws0;
   } // end $atomic