Changes between Version 26 and Version 27 of Next-GenOpenMPTransformation

Timestamp:

05/20/19 20:14:03 (7 years ago)

Author:

ziqing

Comment:

--

Next-GenOpenMPTransformation

@@ -194 +194 @@
 }}}
   * OpenMP Simplifier cannot prove data-race freedom for this program.
-  * OpenMP2CIVL Transformer will transform this program to a equivalent CIVL-C program for model checking
+  * OpenMP2CIVL Transformer will transform this program to a equivalent CIVL-C program for model checking. Here is the code snippet for the CIVL-C program after transformation:
+  {{{
+int main() {
+  int  a[10];
+  {
+    {
+      int _elab_i = 0;
+      for (; _elab_i < _omp_num_threads; _elab_i = _elab_i + 1)
+        ;
+    }
+    int $sef$0 = $choose_int(_omp_num_threads);
+    int _omp_nthreads = 1 + $sef$0;
+    $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);
+    $omp_gshared _omp_a_gshared = $omp_gshared_create(_omp_gteam, &(a));
+    $parfor (int _omp_tid: _omp_dom) {
+      $omp_team _omp_team = $omp_team_create($here, _omp_gteam, _omp_tid);
+      int  _omp_a_local[10];
+      int  _omp_a_status[10];
+      $omp_shared _omp_a_shared = $omp_shared_create(_omp_team, _omp_a_gshared, &(_omp_a_local), &(_omp_a_status));
+      {
+        $range _omp_r1 = 1 .. 10 - 1 # 1;
+        $domain(1) _omp_loop_domain = ($domain){_omp_r1};
+        $domain $sef$1 = $omp_arrive_loop(_omp_team, 0, ($domain)_omp_loop_domain, 2);
+        $domain(1) _omp_my_iters = ($domain(1))$sef$1;
+        $for (int _omp_i_private: _omp_my_iters) {
+          int c;
+          c = _omp_i_private % 2;
+          int _omp_write0;
+          _omp_write0 = 0;
+          $omp_write(_omp_a_shared, &(_omp_a_local[c]), &(_omp_write0));
+        }
+      }
+      $omp_barrier_and_flush(_omp_team);
+      $omp_shared_destroy(_omp_a_shared);
+      $omp_team_destroy(_omp_team);
+    }
+    $omp_gshared_destroy(_omp_a_gshared);
+    $omp_gteam_destroy(_omp_gteam);
+  }
+}
+  }}}
   * CIVL reports PROVABLE errors:
   {{{