| Version 8 (modified by , 8 years ago) ( diff ) |
|---|
CIVL: The Concurrency Intermediate Verification Language
The following demonstrate some of CIVL's capabilities. This is a small sample; see the CIVL manual for the full story.
Dining philosopher in CIVL-C
CIVL-C implementation of dining philosophers, which contains a deadlock. The input file name is 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 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 wave1d.c by adding statements to initialize u_next[0] and u_next[nxl+1] to zero, yielding wave1d_fix.c. Then CIVL is applied again to verify the fix. In fact, the erroneous 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 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 dotProduct_critical_fix.c, which is verified by CIVL successfully.
Note:
See TracWiki
for help on using the wiki.
