Changes between Version 73 and Version 74 of Next-GenOpenMPTransformation

Timestamp:

03/31/21 10:36:23 (5 years ago)

Author:

wuwenhao

Comment:

--

Next-GenOpenMPTransformation

@@ -43 +43 @@
 {{{
 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) ==> 
@@ -48 +50 @@
       $mem_disjoint(...)
   );
-  rs[tid] = $mem_empty(); 
-  ws[tid] = $mem_empty(); 
 }
 }}}
@@ -82 +82 @@
       $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;
@@ -90 +92 @@
 }}}
 
-We denotes Ax as thread x executes statement A. 
-Assuming there are two threads 0 and 1, 
-the first $check_data_race()  checks races between:
-
-A0,A1; A0,B1;  A1,B0; B0,C1; B1,C0;
-
-Then, the second $check_data_race() checks races between:
-
-A0,C1; A1,C0; C0,C1;
-
-Races between B0 and B1 are disabled, because B is in critical block.
+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. 
+