Changes between Version 22 and Version 23 of Next-GenOpenMPTransformation

Timestamp:

05/20/19 20:00:05 (7 years ago)

Author:

ziqing

Comment:

--

Next-GenOpenMPTransformation

@@ -152 +152 @@
   * The OpenMP simplifier can determine that no data race will happen in the parallel region as long as no array out-of-bound error happens in it.
   * 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 )
+{{{
+#include <stdio.h>
+int main(int argc, char* argv[])
+{
+  int i,j;
+  int n=10, m=10;
+  double b[n][m];
+#pragma omp parallel for private(j)
+  for (i=1;i<n;i++)
+    for (j=0;j<m;j++) // Note there will be out of bound access                                                               
+      b[i][j]=b[i][j-1];
+
+  printf ("b[50][50]=%f\n",b[50][50]);
+
+  return 0;
+}
+}}}
+  * OpenMP Simplifier proves that `b[i][j]` and `b[i][j-1]` that accessed by different threads which hold different values of `i` will have no data race as long as no array out-of-bound error happens.
+  * OpenMP Simplifier sequentializes the OpenMP program while the verification condition for array out-of-bound freedom will be checked by CIVL by default.
+  * The CIVL back-end runs the sequentialized program and detects the array out-of-bound access.
+
+Example 3
+{{{
+#include <omp.h>
+int main()
+{
+  int a[50],i;
+
+  a[0] = 1;
+#pragma omp parallel for
+  for(i=1; i<49; i++)
+    {
+      int c;
+
+      c = i + 10;
+      a[i + c] = a[i + c];
+    }
+}
+}}}
+  * 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
 
 == Capture Read / Write at Runtime ==