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:
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.
| Flag | Objective |
|---|---|
| --no-assertions | ignore assertions |
| --no-bounds-check | do not do array bounds check |
| --no-div-by-zero-check | do not do division by zero check |
| --no-pointer-check | do not do pointer check |
| --memory-leak-check | enable memory leak check check |
| --overflow-check | enable arithmetic over- and underflow check |
| --deadlock-check | enable global and local deadlock check with mutex |
| --data-races-check | enable data races check |
| --lock-order-check | enable for lock acquisition ordering check |
| --atomicity-check | enable atomicity check at visible assignments |
| --memlimit | configure memory limit, of form "100m" or "2g" |
| --timeout | configure time limit, integer followed by {s,m,h} |
| --force-malloc-success | considers that there is always enough memory available in the device |
| -DGPU_threads=nr | defines the total number of threads by kernel. This flag is used only for ESBMC-GPU v1.0 |