Changes between Version 74 and Version 75 of Next-GenOpenMPTransformation

Timestamp:

11/19/21 13:56:01 (4 years ago)

Author:

wuwenhao

Comment:

Add transformation for atomic operations

Next-GenOpenMPTransformation

@@ -811 +811 @@
 === Translating `atomic` ===
 
-In general, reads and writes to shared variables will be processed using the protocols described above.  However if the operation occurs within an omp atomic construct, it is translated differently.
-
-TODO: need to look up the rules on the different flavors of atomics.
-
-If sequentially consistent atomic...
-
-If non-sequentially consistent atomic...
+In general, the memory location protected by the atomic construct will be isolated by interacting with local intermediate variables, so that data race on other memory locations not protected by this atomic construct can be checked by CIVL. 
+The local intermediate variable is named based on the protected variable identifier, the kind of atomic construct and a counter ID (for separating distinct atomic constructs, which have same `atomic-clause` for a same variable).
+Currently, CIVL only support sequentially consistent atomic operations and will NOT handle non-sequentially consistent ones. 
+
+==== `read` ====
+
+{{{
+#pragma omp atomic read
+  v = x; // int type
+}}}
+
+=>
+
+{{{
+int $x_read$0;
+$track{ // Will not collect this read on x for checking data race
+  $x_read = x;
+}
+v = $x_read$0;
+}}}
+
+==== `write` ====
+
+{{{
+#pragma omp atomic write
+  x = EXPR; // int type
+}}}
+
+=>
+
+{{{
+int $x_write$0 = EXPR;
+$track{ // Will not collect this write on x for checking data race
+  x = $x_write$0;
+}
+}}}
+
+==== `update` ====
+
+{{{
+#pragma omp atomic update
+  x = x BIN_OP EXPR; // int type
+}}}
+
+=>
+
+{{{
+int $x_update$0 = EXPR;
+$track { // Will not collect this update on x for checking data race
+  x = x BIN_OP $x_update$0;
+}
+}}}
+
+(All update expression statement can be concluded in this form.) 
+
+==== `capture` ====
+
+{{{
+#pragma omp atomic capture
+{
+  v = x; // int type
+  x = x BIN_OP EXPR; // int type
+}
+}}}
+
+=>
+
+{{{
+int $x_capture$0;
+int $x_capture_delta$0 = EXPR;
+$track { // R/W operations on x will not be collected.
+  $x_capture$0 = x;
+  x = x BIN_OP $x_capture_delta$0;
+}
+v = $x_capture$0;
+}}}
+
+(The order of the assignment statement of `$x_capture` and the update 
+expression statement is corresponding to the order in source code.)
 
 ([https://vsl.cis.udel.edu/trac/civl/wiki/Next-GenOpenMPTransformation#OpenMPConstructs back to top])