Changes between Version 24 and Version 25 of Next-GenOpenMPTransformation

Timestamp:

05/20/19 20:08:04 (7 years ago)

Author:

ziqing

Comment:

--

Next-GenOpenMPTransformation

@@ -153 +153 @@
   * The OpenMP simplifier sequentializes the program which will be checked by CIVL.  Any possible array out-of-bound error will be caught by CIVL.
 
-* Example 2 : ( `DRB014-outofbounds-orig-yes.c` from DataRaceBench v1.2.0 )
+* Example 2 : ( `DRB014-outofbounds-orig-yes.c` from  [https://github.com/LLNL/dataracebench/releases/tag/v1.2.0 DataRaceBench v1.2.0] )
 {{{
 #include <stdio.h>
@@ -180 +180 @@
 int main()
 {
-  int a[50],i;
-
-  a[0] = 1;
+  int a[10],i;
+
 #pragma omp parallel for
-  for(i=1; i<49; i++)
+  for(i=0; i<10; i++)
     {
       int c;
 
-      c = i + 10;
-      a[i + c] = a[i + c];
+      c = i % 2;
+      a[i + c] = 0;
     }
 }
@@ -195 +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
+  * CIVL reports PROVABLE errors:
+  {{{
+Thread 1 can not safely write to memory location &<d5>a[0], because thread 0 has
+written to that memory location and hasn't flushed yet.
+
+Violation 0 encountered at depth 64:
+CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
+at OpenMPTransformer "_omp_a_shared, &(_om" inserted by OpenMPTransformer.a_sharedWriteCall before civlc.cvh:105.14-20 "$malloc"
+Assertion: false
+ -> false
+. . .
+Call stacks:
+process 0:
+  main at OpenMPTransformer "$parfor (int _omp_ti" inserted by OpenMPTransformer.parallelPragma before civlc.cvh:105.14-20 "$malloc"
+process 1:
+  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
+  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
+  $omp_barrier_and_flush at civl-omp.cvl:322.2-14 "$barrier_call" called from
+  _par_proc0 at OpenMPTransformer "_omp_team" inserted by OpenMPTransformer.barrierAndFlushCall before civlc.cvh:105.14-20 "$malloc"
+process 2:
+  $omp_write at civl-omp.cvl:247.4-10 "$assert" called from
+  _par_proc0 at OpenMPTransformer "_omp_a_shared, &(_om" inserted by OpenMPTransformer.a_sharedWriteCall before civlc.cvh:105.14-20 "$malloc"
+process 3:
+  $omp_arrive_loop at civl-omp.cvl:405.2-8 "$atomic" called from
+  _par_proc0 at OpenMPTransformer "_omp_team, 0, ($doma" inserted by OpenMPTransformer.myItersDeclaration before civlc.cvh:105.14-20 "$malloc"
+
+Logging new entry 0, writing trace to CIVLREP/testOmp5_0.trace
+Terminating search after finding 1 violation.
+
+  }}}
 
 == Capture Read / Write at Runtime ==