= CIVL: The Concurrency Intermediate Verification Language =

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.

* [https://vsl.cis.udel.edu/trac/civl/wiki/Tour#DiningphilosopherinCIVL-C Dining philosopher in CIVL-C]
* [https://vsl.cis.udel.edu/trac/civl/wiki/Tour#a1-dimensionalwavesimulatorinMPI 1-dimensional wave simulator in MPI]
* [https://vsl.cis.udel.edu/trac/civl/wiki/Tour#DotproductinOpenMP Dot product in OpenMP]


=== Dining philosopher in CIVL-C ===
CIVL-C implementation of dining philosophers, which contains a deadlock. The input file name is [https://vsl.cis.udel.edu/lib/demo/diningBad.cvl diningBad.cvl].

{{{
/* Dining philosophers, standard version, which deadlocks.
 *
 *		civl verify -inputB=4 diningBad.cvl
 * or (if you want to find the minimal counterexample)
 *		civl verify -inputB=4 diningBad.cvl -min
 */
#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() { 
  $elaborate(n);
  $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.

{{{
#ifdef _CIVL
#include <civlc.cvh>
#endif
/* wave1dBad.c: A bad wave1d.c program. It never intiate the ghost
 * cells of u_next to zero which is never been covered when cycling
 * pointers. Runing this mpi program can hardly find the bug because
 * the ghost cells are allocated from memory which will be zero if that
 * memory space is not dirty.
 * To execute: mpicc wave1d.c ; mpiexec -n 4 ./a.out Or
 * replace "4" with however many procs you want to use.  To verify:
 * civl verify wave1d.c
 */
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <math.h>
#include <mpi.h>

#define SQR(x) ((x)*(x))
#define OWNER(index) ((nprocs*(index+1)-1)/nx)

/* MPI message tags */
#define FROMLEFT     1
#define FROMRIGHT    2
#define DATAPASS     3

/* 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 */
$input int _NPROCS_LOWER_BOUND = 1;
$input int _NPROCS_UPPER_BOUND = 4;
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

int nx, height_init, width_init;
int nsteps, wstep;
double c;

#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 */

/* Returns the global index of the first cell owned
 * by the process with given rank */
int firstForProc(int rank) {
  return (rank*nx)/nprocs;      
}

/* Returns the number of cells the given process owns */
int countForProc(int rank) {
  int a = firstForProc(rank);
  int b = firstForProc(rank + 1);

  return b - a;
}

#ifndef _CIVL

/* Some particular initial condition for testing only */
void init(int first, int nxl) {
  int i;
  double e = exp(1.0);

  for(i = 1; i < nxl+1; i++) {
    int idx = first + i - 1;

    if(idx == 1 || idx >= width_init)
      u_prev[i] = 0.0;
    else
      u_prev[i] = height_init * e *
	exp(-1.0/(1-SQR(2.0*(idx-width_init/2.0)/width_init)));
  }
}

#endif

/* 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() {
  int i, j;

#ifndef _CIVL

  nx = 50;
  c = 0.3;
  height_init = 10;
  width_init = 10;
  nsteps = 500;
  wstep = 5;

#endif

  assert(nx >= 2);
  assert(c > 0);
  assert(nsteps >= 1);
  assert(wstep >= 1 && wstep <= nsteps);
  k = c * c;
  printf("Wave1d with nx=%d, c=%f, nsteps=%d, wstep=%d\n", nx, c, nsteps, wstep);

#ifdef _CIVL

  // If in CIVL verification mode and rank is 0,
  // do a sequential run and store result in "oracle" 
  // for comparison later
  if(rank == 0) { 
    // sets constant boundaries for first string and
    // it's virtual previous string
    oracle[0][0] = 0;
    oracle[0][nx + 1] = 0;
    // initialization for first string and
    // it's virtual previous string
    for(i = 1; i < nx + 1; i++) {
      oracle[0][i] = u_init[i - 1];
      oracle[1][i] = u_init[i - 1];
    }
    for(i = 1; i < nsteps; i++){
      oracle[i][0] = 0;
      oracle[i][nx + 1] = 0; 
      // update
      for (j = 1; j < nx + 1; j++)
	oracle[i+1][j] = 2.0*oracle[i][j] - oracle[i-1][j] +
	  k*(oracle[i][j+1] + oracle[i][j-1] -2.0*oracle[i][j]);
    }
  }

#endif

  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) {
  int i;

  for(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
    printf("\n");
  }
}

/* receives data from other processes and wirte frames */
void write_frame (int time) {
  if(rank == 0) {
    double  buf[nx + 2];
    MPI_Status status;

    printf("\n======= Time %d =======\n", time);
    printData(time, first, nxl, &u_curr[1]);
    for(int i=1; i < nprocs; i++) {
      int displ = firstForProc(i);
      int count;

      MPI_Recv(buf, nx, MPI_DOUBLE, i, DATAPASS, MPI_COMM_WORLD, &status);
      MPI_Get_count(&status, MPI_DOUBLE, &count);
      printData(time, displ, count, buf);
    }
    printf("\n");
  } else 
    MPI_Send(&u_curr[1], nxl, MPI_DOUBLE, 0, DATAPASS, MPI_COMM_WORLD);
}

/* 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;


#ifdef _CIVL

  // elaborate nx to concrete value...
  $elaborate(nx);

#endif
  MPI_Init(&argc, &argv);
  MPI_Comm_rank(MPI_COMM_WORLD, &rank);
  MPI_Comm_size(MPI_COMM_WORLD, &nprocs); 
  initialization();
#ifdef _CIVL

  if(nxl != 0) {
    memcpy(&u_curr[1], &u_init[first], sizeof(double) * nxl);
    memcpy(&u_prev[1], &u_curr[1], sizeof(double) * nxl);
  }

#else

  if(nxl != 0) {
    init(first, nxl);
    memcpy(&u_curr[1], &u_prev[1], nxl * sizeof(double));
  }

#endif
  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 detects 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.