| Version 2 (modified by , 8 years ago) ( diff ) |
|---|
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 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 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 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 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 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 dotProduct_critical_fix.c, which is verified by CIVL successfully.
