Changes between Initial Version and Version 1 of Tour

Timestamp:

08/31/18 17:51:30 (8 years ago)

Author:

wuwenhao

Comment:

--

Tour

@@ +1 @@
+= CIVL: The Concurrency Intermediate Verification Language =
+
+== Abstract ==
+'''CIVL: Concurrency Intermediate Verification Language''' is a framework for the verification of multiple concurrent C dialects and libraries, such as OpenMP, MPI, Pthreads, CUDA, etc. 
+It contains transformers to transform programs of such language or libraries into CIVL-C program, which is a dialect of C with concurrent extension, and uses symbolic execution to model check the programs. 
+CIVL-C language is designed to capture the common features of concurrency so that could be used to describe a large number of concurrent dialects or libraries. 
+CIVL is open source, and is designed to be flexible to be extended for verifying more concurrent languages and libraries.
+
+Properties that CIVL checks include: deadlock, memory leak, array index-out-of bound, invalid pointer dereference, user-specified assertions, and functional equivalence.
+
+CIVL is also able to verify hybrid concurrent programs, i.e., programs containing more than one dialects or librabries, such as MPI-OpenMP, MPI-Pthreads, etc.
+
+== Examples ==
+The following demonstrate some of CIVL's capabilities. This is a small sample; see the [https://vsl.cis.udel.edu/lib/sw/civl/civl-manual.pdf CIVL manual] for the full story.
+* Dining philosopher in CIVL-C
+* 1-dimensional wave simulator in MPI
+* Dot product in OpenMP
+
+
+=== Dining philosopher in CIVL-C ===
+CIVL-C implementation of dining philosopher, which contains a deadlock. Suppose the file name is [https://vsl.cis.udel.edu/lib/demo/diningBad.cvl diningBad.cvl].
+
+{{{
+#include <civlc.cvh>
+
+$input int B = 4; // upper bound on number of philosophers
+$input int n;     // number of philosophers
+$assume(2<=n && n<=B);
+
+_Bool forks[n]; // Each fork will be on the table ($true) or in a hand ($false).
+
+void dine(int id) {
+  int left = id;
+  int right = (id + 1) % n;
+
+  while (1) {
+    $when (forks[left]) forks[left] = $false;
+    $when (forks[right]) forks[right] = $false;
+    forks[right] = $true;
+    forks[left] = $true;
+  }
+}
+
+void main() { 
+  $for(int i: 0 .. n-1)
+    forks[i] = $true;
+  $parfor(int i: 0 .. n-1)
+    dine(i);
+}
+}}}
+
+'''Command''': civl verify -inputB=4 diningBad.cvl
+
+The above command triggers CIVL to verify the CIVL-C program for dining philosophers, with the upper bound of number of philosophers being 4. As shown by the output below, CIVL detects a deadlock violation of the program at depth 79, i.e., after 78 trace steps.
+
+'''Output''':
+{{{
+CIVL v1.17.1+ of 2018-07-30 -- http://vsl.cis.udel.edu/civl
+
+Violation 0 encountered at depth 21:
+CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
+at diningBad.cvl:31.11-11
+            dine(i);
+
+A deadlock is possible:
+  Path condition: true
+  Enabling predicate: false
+process p0 (id=0): false
+process p1 (id=1): false
+process p2 (id=2): false
+
+Call stacks:
+process 0:
+  main at diningBad.cvl:31.11 ";"
+process 1:
+  dine at diningBad.cvl:21.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:31.4-7 "dine"
+process 2:
+  dine at diningBad.cvl:21.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:31.4-7 "dine"
+
+Logging new entry 0, writing trace to CIVLREP/diningBad_0.trace
+Terminating search after finding 1 violation.
+
+=== Source files ===
+diningBad.cvl  (diningBad.cvl)
+
+
+=== Command ===
+civl verify -inputB=4 diningBad.cvl 
+
+=== Stats ===
+   time (s)            : 1.36
+   memory (bytes)      : 268435456
+   max process count   : 3
+   states              : 32
+   states saved        : 26
+   state matches       : 1
+   transitions         : 30
+   trace steps         : 21
+   valid calls         : 104
+   provers             : cvc4, z3
+   prover calls        : 3
+
+=== Result ===
+The program MAY NOT be correct.  See CIVLREP/diningBad_log.txt
+}}}
+
+Now that we know there is a violation, we probably want to find a minimal one. We can use the option "-min" for the verification, as shown by the following command.
+
+'''Command''': civl verify -inputB=4 -min diningBad.cvl
+
+As shown in the following output, CIVL keeps reducing the search depth until it finds the minimal counterexample at depth 23, which is much smaller and is the case when there are two philosophers.
+
+'''Output''':
+{{{
+CIVL v1.17.1+ of 2018-07-30 -- http://vsl.cis.udel.edu/civl
+
+Violation 0 encountered at depth 21:
+CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
+at diningBad.cvl:31.11-11
+            dine(i);
+
+A deadlock is possible:
+  Path condition: true
+  Enabling predicate: false
+process p0 (id=0): false
+process p1 (id=1): false
+process p2 (id=2): false
+
+Call stacks:
+process 0:
+  main at diningBad.cvl:31.11 ";"
+process 1:
+  dine at diningBad.cvl:21.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:31.4-7 "dine"
+process 2:
+  dine at diningBad.cvl:21.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:31.4-7 "dine"
+
+Logging new entry 0, writing trace to CIVLREP/diningBad_0.trace
+Restricting search depth to 20
+
+Violation 1 encountered at depth 16:
+CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
+at diningBad.cvl:31.11-11
+            dine(i);
+
+A deadlock is possible:
+  Path condition: true
+  Enabling predicate: false
+process p0 (id=0): false
+process p1 (id=1): false
+process p2 (id=2): false
+
+Call stacks:
+process 0:
+  main at diningBad.cvl:31.11 ";"
+process 1:
+  dine at diningBad.cvl:21.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:31.4-7 "dine"
+process 2:
+  dine at diningBad.cvl:21.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:31.4-7 "dine"
+
+New log entry is equivalent to previously encountered entry 0
+Length of new trace (16) is less than length of old (21): replacing old with new...
+Restricting search depth to 15
+
+=== Source files ===
+diningBad.cvl  (diningBad.cvl)
+
+
+=== Command ===
+civl verify -inputB=4 -min diningBad.cvl 
+
+=== Stats ===
+   time (s)            : 1.11
+   memory (bytes)      : 268435456
+   max process count   : 5
+   states              : 76
+   states saved        : 62
+   state matches       : 2
+   transitions         : 73
+   trace steps         : 51
+   valid calls         : 256
+   provers             : cvc4, z3
+   prover calls        : 3
+
+=== Result ===
+The program MAY NOT be correct.  See CIVLREP/diningBad_log.txt
+}}}
+
+Now CIVL finds the minimal counterexample and we can use CIVL to reproduce it via the "replay" command.
+
+'''Command''': civl replay -showTransitions diningBad.cvl
+
+'''Output''':
+{{{
+CIVL v1.17.1+ of 2018-07-30 -- http://vsl.cis.udel.edu/civl
+
+Initial state:
+
+State (id=9)
+| Path condition
+| | true
+| Dynamic scopes
+| | dyscope d0 (parent=NULL, static=1)
+| | | variables
+| | | | B = NULL
+| | | | n = NULL
+| | | | forks = NULL
+| Process states
+| | process 0
+| | | call stack
+| | | | Frame[function=main, location=0, diningBad.cvl:9.15 "4", dyscope=d0]
+
+Executed by p0 from State (id=9)
+  0->1: B=4 at diningBad.cvl:9.0-15 "$input int B = 4"
+  1->2: n=InitialValue(n) [n:=X_n] at diningBad.cvl:10.0-11 "$input int n"
+  2->3: $assume((2<=X_n)&&(X_n<=4)) at diningBad.cvl:11.0-20 "$assume(2<=n && n ... )"
+  3->4: forks=InitialValue(forks) [forks:=(boolean[X_n]) ($lambda i: int. false)] at diningBad.cvl:13.0-13 "_Bool forks[n]"
+--> State (id=18)
+
+Step 1: Executed by p0 from State (id=18)
+  4->5: $elaborate_domain(($domain(1))(0..X_n-1#1)) [$assume(0==(X_n - 2))] at diningBad.cvl:28.14-21 "0 .. n-1"
+--> State (id=22)
+
+Step 2: Executed by p0 from State (id=22)
+  5->6: LOOP_BODY_ENTER (guard: ($domain(1))(0..1#1) has next for (NULL)) at diningBad.cvl:28.14-21 "0 .. n-1"
+  6->7: NEXT of (NULL) in ($domain(1))(0..1#1) [i:=0] at diningBad.cvl:28.2-5 "$for"
+--> State (id=26)
+
+Step 3: Executed by p0 from State (id=26)
+  7->5: forks[0]=true at diningBad.cvl:29.4-civlc.cvh:10.14 "forks[i] = 1"
+--> State (id=29)
+
+Step 4: Executed by p0 from State (id=29)
+  5->6: LOOP_BODY_ENTER (guard: ($domain(1))(0..1#1) has next for (0)) at diningBad.cvl:28.14-21 "0 .. n-1"
+  6->7: NEXT of (0) in ($domain(1))(0..1#1) [i:=1] at diningBad.cvl:28.2-5 "$for"
+--> State (id=33)
+
+Step 5: Executed by p0 from State (id=33)
+  7->5: forks[1]=true at diningBad.cvl:29.4-civlc.cvh:10.14 "forks[i] = 1"
+--> State (id=36)
+
+Step 6: Executed by p0 from State (id=36)
+  5->8: LOOP_BODY_EXIT (guard: !($domain(1))(0..1#1) has next for (1)) at diningBad.cvl:28.14-21 "0 .. n-1"
+--> State (id=38)
+
+Step 7: Executed by p0 from State (id=38)
+  8->9: $elaborate_domain(($domain(1))(0..1#1)) [$assume(true)] at diningBad.cvl:30.17-24 "0 .. n-1"
+  9->10: $parfor(i0: ($domain(1))(0..1#1)) $spawn _par_proc0(i0) at diningBad.cvl:30.2-8 "$parfor"
+  10->11: _civl_ir1=0 at diningBad.cvl:31.11 ";"
+--> State (id=52)
+
+Step 8: Executed by p0 from State (id=52)
+  11->12: LOOP_BODY_ENTER (guard: 0<2) at diningBad.cvl:31.11 ";"
+--> State (id=54)
+
+Step 9: Executed by p1 from State (id=54)
+  23->15: dine(0) at diningBad.cvl:31.4-10 "dine(i)"
+  15->16: left=0 at diningBad.cvl:16.2-14 "int left = id"
+  16->17: right=(0+1)%2 [right:=1] at diningBad.cvl:17.2-25 "int right = (id  ... n"
+--> State (id=61)
+
+Step 10: Executed by p1 from State (id=61)
+  17->18: LOOP_BODY_ENTER (guard: 1!=0) at diningBad.cvl:19.9 "1"
+--> State (id=63)
+
+Step 11: Executed by p2 from State (id=63)
+  23->15: dine(1) at diningBad.cvl:31.4-10 "dine(i)"
+  15->16: left=1 at diningBad.cvl:16.2-14 "int left = id"
+  16->17: right=(1+1)%2 [right:=0] at diningBad.cvl:17.2-25 "int right = (id  ... n"
+--> State (id=70)
+
+Step 12: Executed by p2 from State (id=70)
+  17->18: LOOP_BODY_ENTER (guard: 1!=0) at diningBad.cvl:19.9 "1"
+--> State (id=72)
+
+Step 13: Executed by p1 from State (id=72)
+  18->19: forks[0]=false at diningBad.cvl:20.24-civlc.cvh:12.15 "forks[left] = 0"
+--> State (id=75)
+
+Step 14: Executed by p2 from State (id=75)
+  18->19: forks[1]=false at diningBad.cvl:20.24-civlc.cvh:12.15 "forks[left] = 0"
+--> State (id=78)
+
+Step 15: 
+State (id=78)
+| Path condition
+| | true
+| Dynamic scopes
+| | dyscope d0 (parent=NULL, static=1)
+| | | variables
+| | | | B = 4
+| | | | n = 2
+| | | | forks = {[0]=false, [1]=false}
+| | dyscope d1 (parent=d0, static=4)
+| | | variables
+| | | | i = 1
+| | | | __LiteralDomain_counter0__ = NULL
+| | dyscope d2 (parent=d0, static=7)
+| | | variables
+| | | | _dom_size0 = 2
+| | | | _par_procs0 = {[0]=p1, [1]=p2}
+| | dyscope d3 (parent=d0, static=8)
+| | | variables
+| | | | i = 0
+| | dyscope d4 (parent=d0, static=8)
+| | | variables
+| | | | i = 1
+| | dyscope d5 (parent=d2, static=9)
+| | | variables
+| | | | _civl_ir1 = 0
+| | dyscope d6 (parent=d5, static=10)
+| | | variables
+| | dyscope d7 (parent=d0, static=3)
+| | | variables
+| | | | id = 0
+| | dyscope d8 (parent=d7, static=12)
+| | | variables
+| | | | left = 0
+| | | | right = 1
+| | dyscope d9 (parent=d0, static=3)
+| | | variables
+| | | | id = 1
+| | dyscope d10 (parent=d9, static=12)
+| | | variables
+| | | | left = 1
+| | | | right = 0
+| Process states
+| | process 0
+| | | call stack
+| | | | Frame[function=main, location=12, diningBad.cvl:31.11 ";", dyscope=d6]
+| | process 1
+| | | call stack
+| | | | Frame[function=dine, location=19, diningBad.cvl:21.4-8 "$when", dyscope=d8]
+| | | | Frame[function=_par_proc0, location=23, diningBad.cvl:31.4-7 "dine", dyscope=d3]
+| | process 2
+| | | call stack
+| | | | Frame[function=dine, location=19, diningBad.cvl:21.4-8 "$when", dyscope=d10]
+| | | | Frame[function=_par_proc0, location=23, diningBad.cvl:31.4-7 "dine", dyscope=d4]
+
+Violation of Deadlock found in (id=78):
+A deadlock is possible:
+  Path condition: true
+  Enabling predicate: false
+process p0 (id=0): false
+process p1 (id=1): false
+process p2 (id=2): false
+
+Trace ends after 15 trace steps.
+Violation(s) found.
+
+=== Source files ===
+diningBad.cvl  (diningBad.cvl)
+
+
+=== Command ===
+civl replay -showTransitions diningBad.cvl 
+
+=== Stats ===
+   time (s)            : 1.01
+   memory (bytes)      : 268435456
+   max process count   : 3
+   states              : 27
+   valid calls         : 98
+   provers             : cvc4, z3
+   prover calls        : 3
+
+}}}
+
+
+=== 1-dimensional wave simulator in MPI ===
+MPI implementation of 1d-wave simulator, which has a bug. The file name of this program is [https://vsl.cis.udel.edu/lib/demo/wave1d.c wave1d.c]. 
+Some additional CIVL-C code has been inserted to specify the intended behavior of the program; 
+in the full source, this extra code is within preprocessor directives #ifdef _CIVL ... #endif 
+which cause the extra code to be ignored during normal compilation but used by CIVL. 
+The program starts with the string in some arbitrary initial position specified by the input variable u_init . 
+The variable oracle keeps the result of a sequential run of the simulator at every time step, 
+and at every time step of the parallel run an assertion is checked to see if the parallel result agrees with the sequential one.
+
+{{{
+/* Input parameters */
+#ifdef _CIVL
+$input int NXB = 5;               /* upper bound on nx */
+$input int nx;                    /* number of discrete points including endpoints */
+$assume(2 <= nx && nx <= NXB);     /* setting bounds */
+$input double c;                  /* physical constant to do with string */
+$assume(c > 0.0);       
+$input int NSTEPSB = 5;        
+$input int nsteps;                /* number of time steps */
+$assume(0 < nsteps && nsteps <= NSTEPSB);
+$input int wstep = 1;             /* number of time steps between printing */
+double oracle[nsteps + 1][nx + 2];/* result of sequential run at every time step */
+$input double u_init[nx];         /* arbitrary initial position of string */
+...
+#else
+...
+#endif
+
+/* Global varibales */
+double *u_prev, *u_curr, *u_next;
+double k;
+int nprocs, nxl, rank;
+int first;                       /* global index of first cell owned by this process */
+int left, right;                 /* ranks of left neighbor and right neighbor */
+...
+/* Update cells owned by processes */
+void update() {
+  int i;
+  double *tmp;
+
+  for (i = 1; i < nxl + 1; i++){
+    u_next[i] = 2.0*u_curr[i] - u_prev[i] +
+      k*(u_curr[i+1] + u_curr[i-1] -2.0*u_curr[i]);
+  }
+  //cycle pointers:
+  tmp = u_prev;
+  u_prev = u_curr;
+  u_curr = u_next;
+  u_next = tmp;
+}
+
+/* Initialization function, initializes all parameters and data array.
+ * In CIVL mode, process 0 runs the complete problem sequentially to
+ * create the oracle which will be compared with the results of the
+ * parallel run.
+ */
+void initialization() {
+  ...
+  nxl = countForProc(rank);
+  first = firstForProc(rank);
+  u_prev = (double *)malloc((nxl + 2) * sizeof(double));
+  assert(u_prev);
+  u_curr = (double *)malloc((nxl + 2) * sizeof(double));
+  assert(u_curr);
+  u_next = (double *)malloc((nxl + 2) * sizeof(double));
+  assert(u_next);
+  // sets constant boundaries
+  u_prev[0] = 0;
+  u_curr[0] = 0;
+  //u_next[0] = 0;
+  u_prev[nxl + 1] = 0;
+  u_curr[nxl + 1] = 0;
+  //u_next[nxl + 1] = 0;
+  // skip processes which are allocated no cells
+  if(first != 0 && nxl != 0)
+    left = OWNER(first - 1);
+  else 
+    left = MPI_PROC_NULL;
+  if(first + nxl < nx && nxl != 0)
+    right = OWNER(first + nxl);
+  else
+    right = MPI_PROC_NULL;
+}
+
+...
+/* Print out the value of data cells; 
+   Do comparison in CIVL mode */
+void printData (int time, int first, int length, double * buf) {
+  for(int i = 0; i < length; i++){
+    printf("u_curr[%d]=%8.8f   ", first + i, buf[i]);
+#ifdef _CIVL
+
+     $assert((oracle[time + 1][first + i + 1] == buf[i]), \
+    "Error: disagreement at time %d position %d: saw %lf, expected %lf", \
+    time, first + i, buf[i], oracle[time + 1][first + i + 1]);
+#endif
+  }
+}
+...
+
+/* Exchanging ghost cells */
+void exchange(){
+  MPI_Sendrecv(&u_curr[1], 1, MPI_DOUBLE, left, FROMRIGHT, &u_curr[nxl+1], 1, MPI_DOUBLE, 
+               right, FROMRIGHT, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
+  MPI_Sendrecv(&u_curr[nxl], 1, MPI_DOUBLE, right, FROMLEFT, &u_curr[0], 1, 
+               MPI_DOUBLE, left, FROMLEFT, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
+}
+
+int main(int argc, char * argv[]) {
+  int iter;
+
+  MPI_Init(&argc, &argv);
+  MPI_Comm_rank(MPI_COMM_WORLD, &rank);
+  MPI_Comm_size(MPI_COMM_WORLD, &nprocs); 
+  initialization();
+  ...
+  for(iter = 0; iter < nsteps; iter++) {
+    if(iter % wstep == 0)
+      write_frame(iter);
+    if(nxl != 0){
+      exchange();
+      update();
+    }
+  }
+  free(u_curr);
+  free(u_prev);
+  free(u_next);
+  MPI_Finalize(); 
+  return 0;
+}               
+
+}}}
+
+With the upper bound of the size of initial vector being 5, and the bound of number of steps of the computation being 5, 
+and the number of processes is restricted to be in the range [1, 4], 
+CIVL finds a violation of the assertion of the program in a few seconds. The violation is at depth 1082.
+
+'''Command''': civl verify -enablePrintf=false -input_mpi_nprocs=4 wave1d.c
+
+'''Output''':
+{{{
+CIVL v1.17.1+ of 2018-07-30 -- http://vsl.cis.udel.edu/civl
+
+Violation 0 encountered at depth 820:
+CIVL execution violation in p1 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
+at wave1d.c:199.4-201.61
+            $assert((oracle[time + 1][first + i + 1] == buf[i]), \
+            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+        ...
+            time, first + i, buf[i], oracle[time + 1][first + i + 1]);
+            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Assertion: (((oracle)[(time+1)])[((first+i)+1)]==*((buf+i)))
+ -> -2*(((((X_u_init[1]+((-1/2)*X_u_init[2])+((-1/2)*X_u_init[0]))*(X_c^2))+((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2))+((-1/2)*X_u_init[1])+X_u_init[0])*(X_c^2))+(-1*((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2)))+((-1/2)*X_u_init[0]))==*(&<d5>heap.malloc6[0][1]+0)
+ -> (-2*(((((X_u_init[1]+((-1/2)*X_u_init[2])+((-1/2)*X_u_init[0]))*(X_c^2))+((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2))+((-1/2)*X_u_init[1])+X_u_init[0])*(X_c^2))+(-1*((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2)))+((-1/2)*X_u_init[0])))==(-2*(((((X_u_init[1]+((-1/2)*X_u_init[2])+((-1/2)*X_u_init[0]))*(X_c^2))+((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2))+((-1/2)*Hp1s5f8o0[0])+((-1/2)*X_u_init[1])+X_u_init[0])*(X_c^2))+(-1*((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2)))+((-1/2)*X_u_init[0])))
+ -> (0==((X_u_init[1] + (-1/2)*X_u_init[2] + (-1/2)*X_u_init[0])*(X_c^2) + (X_u_init[1] - 2*X_u_init[0])*(X_c^2) + (-1/2)*Hp1s5f8o0[0] + (-1/2)*X_u_init[1] + X_u_init[0] - 1*((X_u_init[1] + (-1/2)*X_u_init[2] + (-1/2)*X_u_init[0])*(X_c^2) + (X_u_init[1] - 2*X_u_init[0])*(X_c^2) + (-1/2)*X_u_init[1] + X_u_init[0])))||(0==X_c)
+
+Input:
+  ...
+  nx=5
+  c=X_c
+  nsteps=5
+  wstep=1
+  u_init=X_u_init
+  _mpi_nprocs=4
+  _mpi_nprocs_lo=1
+  ...
+Context:
+  forall _t : dynamicType . (0 <= CIVL_SIZEOF(_t) - 1)
+  0<X_c
+  0<=(SIZEOF_REAL-1)
+  0<=(X__civl_argc-1)
+  0<=(X__mpi_nprocs_hi-4)
+Call stacks:
+process 0:
+  main at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before wave1d.c:237.13-16 "argc"
+process 1:
+  printData at wave1d.c:199.4-10 "$assert" called from
+  write_frame at wave1d.c:215.4-12 "printData" called from
+  _civl_main at wave1d.c:268.6-16 "write_frame" called from
+  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before wave1d.c:237.13-16 "argc" called from
+  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before wave1d.c:237.13-16 "argc"
+process 2:
+  $mpi_sendrecv at civl-mpi.cvl:272.6-18 "$comm_dequeue" called from
+  MPI_Sendrecv at mpi.cvl:134.2-14 "$mpi_sendrecv" called from
+  exchange at wave1d.c:233.2-13 "MPI_Sendrecv" called from
+  _civl_main at wave1d.c:270.6-13 "exchange" called from
+  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before wave1d.c:237.13-16 "argc" called from
+  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before wave1d.c:237.13-16 "argc"
+process 3:
+  $mpi_sendrecv at civl-mpi.cvl:272.6-18 "$comm_dequeue" called from
+  MPI_Sendrecv at mpi.cvl:134.2-14 "$mpi_sendrecv" called from
+  exchange at wave1d.c:231.2-13 "MPI_Sendrecv" called from
+  _civl_main at wave1d.c:270.6-13 "exchange" called from
+  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before wave1d.c:237.13-16 "argc" called from
+  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before wave1d.c:237.13-16 "argc"
+process 4:
+  $mpi_send at civl-mpi.cvl:223.2-7 "return" called from
+  MPI_Send at mpi.cvl:90.9-17 "$mpi_send" called from
+  write_frame at wave1d.c:226.4-11 "MPI_Send" called from
+  _civl_main at wave1d.c:268.6-16 "write_frame" called from
+  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before wave1d.c:237.13-16 "argc" called from
+  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before wave1d.c:237.13-16 "argc"
+
+Logging new entry 0, writing trace to CIVLREP/wave1d_0.trace
+Terminating search after finding 1 violation.
+
+=== Source files ===
+wave1d.c  (wave1d.c)
+
+=== Command ===
+civl verify -enablePrintf=false -input_mpi_nprocs=4 wave1d.c 
+
+=== Stats ===
+   time (s)            : 6.98
+   memory (bytes)      : 581959680
+   max process count   : 5
+   states              : 2058
+   states saved        : 1231
+   state matches       : 0
+   transitions         : 2057
+   trace steps         : 819
+   valid calls         : 8903
+   provers             : cvc4, z3
+   prover calls        : 36
+
+=== Result ===
+The program MAY NOT be correct.  See CIVLREP/wave1d_log.txt
+}}}
+
+With "-min" option enabled, CIVL finds a minimal counterexample at depth 660 after 19.08 seconds. 
+With the help of the counterexample, one can be guided to fix [https://vsl.cis.udel.edu/lib/demo/wave1d.c wave1d.c] by adding statements to initialize u_next![0] and u_next[nxl+1] to zero, 
+yielding [https://vsl.cis.udel.edu/lib/demo/wave1d_fix.c wave1d_fix.c]. Then CIVL is applied again to verify the fix. 
+In fact, the erroneous [https://vsl.cis.udel.edu/lib/demo/wave1d.c wave1d.c] had been used for two years in a parallel computing course taught by one of us (Dr. Siegel), 
+but the defect was never noticed, apparently because the allocated memory was almost always initialized with 0s, something which is certainly not guaranteed by the C Standard.
+
+=== Dot product in OpenMP ===
+Now let's look at a simple OpenMP program [https://vsl.cis.udel.edu/lib/demo/dotProduct_critical.c dotProduct_critical.c] that performs the dot product of two vectors. 
+The program is originally used as an example program for a parallel programming course.
+
+{{{
+#include <omp.h>
+...             
+#define N 100
+
+int main (int argc, char *argv[]) {
+  double a[N], b[N];
+  double localsum, sum = 0.0;
+  int i, tid, nthreads;
+  
+#pragma omp parallel shared(a,b,sum) private(i, localsum)
+  {
+    /* Get thread number */
+    tid = omp_get_thread_num();
+    
+    /* Only master thread does this */
+#pragma omp master
+    {
+      nthreads = omp_get_num_threads();
+      printf("Number of threads = %d\n", nthreads);
+    }
+
+    /* Initialization */
+#pragma omp for
+    for (i=0; i < N; i++)
+      a[i] = b[i] = (double)i;
+
+    localsum = 0.0;
+
+    /* Compute the local sums of all products */
+#pragma omp for
+    for (i=0; i < N; i++)
+      localsum = localsum + (a[i] * b[i]);
+
+#pragma omp critical
+    sum = sum+localsum;
+
+  }  /* End of parallel region */
+
+  printf("   Sum = %2.1f\n",sum);
+
+#ifdef _CIVL
+  assert(sum==328350);
+#endif
+  exit(0);
+}
+}}}
+
+CIVL transforms an OpenMP program to be purely CIVL-C before it performs verification on it, during which an input variable THREAD_MAX is introduced as the upper bound of the number of threads. To verify an OpenMP program, one needs to specify the value of THREAD_MAX . Here, we use 3 as THREAD_MAX for verification.
+
+'''Command''': civl verify -min -inputTHREAD_MAX=3 -enablePrintf=false dotProduct_critical.c
+
+'''Output''':
+{{{
+CIVL v1.17.1+ of 2018-07-30 -- http://vsl.cis.udel.edu/civl
+
+Violation 0 encountered at depth 1355:
+CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
+at OpenMPTransformer "_omp_tid_shared, &(_" inserted by OpenMPTransformer.tid_sharedWriteCall before civlc.cvh:31.22-27 "$scope" included from civl-stdio.cvh:3
+Assertion: (otherTid<0)
+ -> 0<0
+ -> false
+
+Input:
+  _omp_thread_max=3
+Context:
+  forall _t : dynamicType . (0 <= CIVL_SIZEOF(_t) - 1)
+Call stacks:
+process 0:
+  ...
+process 1:
+  ...
+process 2:
+  $omp_write at civl-omp.cvl:238.2-8 "$assert" called from
+  _par_proc0 at OpenMPTransformer "_omp_tid_shared, &(_" inserted by OpenMPTransformer.tid_sharedWriteCall before civlc.cvh:31.22-27 "$scope" included from civl-stdio.cvh:3
+
+Logging new entry 0, writing trace to CIVLREP/dotProduct_critical_0.trace
+Restricting search depth to 1354
+
+  ...
+
+Violation 203 encountered at depth 38:
+CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
+
+  ...
+
+=== Source files ===
+dotProduct_critical.c  (dotProduct_critical.c)
+
+
+=== Command ===
+civl verify -min -input_omp_thread_max=3 -enablePrintf=false dotProduct_critical.c 
+
+=== Stats ===
+   time (s)            : 6.23
+   memory (bytes)      : 322961408
+   max process count   : 4
+   states              : 31425
+   states saved        : 15725
+   state matches       : 0
+   transitions         : 31625
+   trace steps         : 11264
+   valid calls         : 29990
+   provers             : cvc4, z3
+   prover calls        : 2
+
+=== Result ===
+The program MAY NOT be correct.  See CIVLREP/dotProduct_critical_log.txt
+}}}
+
+As shown by the above output, wihtin 10 seconds, CIVL dectecs a race condition and finds the minimal counterexample at depth 38 after detecting 204 violations, 
+which is much smaller than the first violation which is at depth 1355. 
+With the help of trace provided by CIVL replay for the minimal counterexample, one is guided to fix the error by adding the variable tid to the private list of the parallel construct, 
+yielding [https://vsl.cis.udel.edu/lib/demo/dotProduct_critical_fix.c dotProduct_critical_fix.c], which is verified by CIVL successfully.
+