Documentation

A video demonstration:

 

1) As first step, the user needs to change some parameters in the program.
1a) Change the default kernel call to an intrinsic function of ESBMC-GPU.

 Original Code Modified Code
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
#include < cuda.h >
#define tid threadIdx.x
#define N 1024

__device__ inline void inlined(int *A, int offset) {
int temp = A[tid + offset];
A[tid] += temp;
}

__global__ void inline_test(int *A, int offset) {
inlined(A, offset);
}

int main( ) {
int *a;
int *dev_a;
int size = N*sizeof(int);

cudaMalloc((void**)&dev_a, size);

a = (int*)malloc(N*size);

for (int i = 0; i < N; i++)
a[i] = i;

cudaMemcpy(dev_a,a,size, cudaMemcpyHostToDevice);

inline_test<<<1,N>>>(dev_a, 2);

cudaMemcpy(a,dev_a,size,cudaMemcpyDeviceToHost);
free(a);
cudaFree(dev_a);
return 0;
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
#include < cuda.h >
#define tid threadIdx.x
#define N 2

__device__ inline void inlined(int *A, int offset) {
int temp = A[tid + offset];
A[tid] += temp;
}

__global__ void inline_test(int *A, int offset) {
inlined(A, offset);
}

int main( ) {
int *a;
int *dev_a;
int size = N*sizeof(int);

cudaMalloc((void**)&dev_a, size);

a = (int*)malloc(N*size);

for (int i = 0; i < N; i++)
a[i] = i;

cudaMemcpy(dev_a,a,size, cudaMemcpyHostToDevice);

ESBMC_verify_kernel_intt(inline_test, 1, N, dev_a, 2);

cudaMemcpy(a,dev_a,size,cudaMemcpyDeviceToHost);
free(a);
cudaFree(dev_a);
return 0;
}

Note that the kernel call is replaced by an ESBMC-GPU intrinsic function, called ESBMC_verify_kernel(). This function takes as argument the kernel to be verified, the number of blocks, the number of threads, and the kernel parameters. In this particular case, one can observe that line 28 of the original code is modified. Additionally, line 3 is also modified in order to define the number of threads to 2.

2) Check file.cu using ESBMC-GPU.

To run ESBMC-GPU, which is available on the download webpage, the user must type the following command:

$ ./esbmc-gpu main.cu -I libraries/ – – force-malloc-success – – data-races-check


where -I points to the ESBMC-GPU libraries, – – force-malloc-success which considers that there is always enough memory available in the device, and – – data-race-check to check for data race conditions to avoid that multiple threads perform unsynchronized accesses to the shared variable.

3) Possible expected results.

VERIFICATION SUCCESSFUL ~ There is no property violation up to the bound k.
VERIFICATION FAILED ~ The property is violated and a counterexample is provided.

4) Inspect verification results (counterexample).

 

In this example, the result is VERIFICATION FAILED, i.e., ESBMC-GPU detects a data race condition.

#Additional flags for ESBMC-GPU verification
Here are some additional flags used by ESBMC-GPU. Note that all ESBMC-GPU flags are available via command line ./esbmc – – help.

FlagObjective
--no-assertions ignore assertions
--no-bounds-check do not do array bounds check
--no-div-by-zero-checkdo not do division by zero check
--no-pointer-checkdo not do pointer check
--memory-leak-checkenable memory leak check check
--overflow-check enable arithmetic over- and underflow check
--deadlock-checkenable global and local deadlock check with mutex
--data-races-checkenable data races check
--lock-order-checkenable for lock acquisition ordering check
--atomicity-checkenable atomicity check at visible assignments
--memlimitconfigure memory limit, of form "100m" or "2g"
--timeoutconfigure time limit, integer followed by {s,m,h}
--force-malloc-successconsiders that there is always enough memory available in the device
-DGPU_threads=nrdefines the total number of threads by kernel. This flag is used only for ESBMC-GPU v1.0