NAME: cuda-omp.cu
CITE: \cite{arc:cuda}
TYPE: $\text{C}$
SCALE: {\texttt{1$\leq$NBLK$\leq$4,1$\leq$NTperBLK$\leq$2}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (91.6 files/s, 14284.4 lines/s)"
1,CUDA,36,21,99
civl verify -enablePrintf=false  -inputBLOCK_B=4 -inputTHREADS_B=2 cuda-omp.cu
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 284:
CIVL execution violation in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at cuda-omp.cu:144.2-19 "$assert(($false))":

Input variables:
_gen_argc=X0
_gen_argv=(CHAR[10][])X1
BLOCKS=X2
BLOCK_B=4
THREADS_PER_BLOCK=1
THREADS_B=2
_omp_thread_max=X4

Context: 0==-1*(X2*X3)+4 && 0<=SIZEOF((struct $cuda_kernel_instance)*)+-1 && 0<=SIZEOF(struct $cuda_kernel_instance)+-1 && 0<=SIZEOF(struct $cuda_kernel_instance_node)+-1 && 0<=SIZEOF(struct _CUstream)+-1 && 0<=SIZEOF(struct _CUevent)+-1 && 0<=SIZEOF_INT+-1 && 0<=-1*X0+9 && 0<=X0+-1 && 0<=-1*X2+4 && 0<=X2+-1

Assertion: $assert(false)
-> false

Call stacks:

process p0 (id=0):
  _gen_main at cuda-omp.cu:144.2-9 "$assert" called from
  _CIVL_system at GeneralTransformer:0.-1-20 "_gen_argc, &_gen_a..." inserted by GeneralTransformer.new main function before cuda-omp.cu:41.13-17 "argc"

process p1 (id=1):
  terminated

Logging new entry 0, writing trace to CIVLREP/cuda-omp_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -inputBLOCK_B=4 -inputTHREADS_B=2 cuda-omp.cu 

=== Stats ===
   time (s)            : 7.07
   memory (bytes)      : 1398800384
   max process count   : 14
   states              : 7128
   states saved        : 2995
   state matches       : 898
   transitions         : 8024
   trace steps         : 3865
   valid calls         : 133087
   provers             : z3, cvc4, cvc3
   prover calls        : 74

=== Result ===
The program MAY NOT be correct.  See CIVLREP/cuda-omp_log.txt
NAME: dot.cu
CITE: \cite{sanders-kandrot:2010:cuda-by-example}
TYPE: $\text{C}$
SCALE: {\texttt{1$\leq$N$\leq$6, 1$\leq$NTperBLK$\leq$4}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (87.9 files/s, 13182.2 lines/s)"
1,CUDA,23,28,99
civl verify -enablePrintf=false  -inputN_B=6 -inputthreadsPerBlock_B=4 dot.cu
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -inputN_B=6 -inputthreadsPerBlock_B=4 dot.cu 

=== Stats ===
   time (s)            : 5.78
   memory (bytes)      : 650117120
   max process count   : 14
   states              : 13713
   states saved        : 7656
   state matches       : 223
   transitions         : 13921
   trace steps         : 7671
   valid calls         : 110745
   provers             : z3, cvc4, cvc3
   prover calls        : 75

=== Result ===
The standard properties hold for all executions.
NAME: mm.cu
CITE: \cite{rcac:cuda}
TYPE: $\text{C}$
SCALE: {\texttt{NBLK=4,NTperBLK=1}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (89.9 files/s, 23736.8 lines/s)"
1,CUDA,51,67,146
civl verify -enablePrintf=false  -inputN=2 -inputTILE_WIDTH=1 mm.cu
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 481:
CIVL execution violation in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at mm.cu:210.4-65 "$assert(($forall {int k ... )":

Input variables:
_gen_argc=2
_gen_argv=(CHAR[10][])X1
N=2
TILE_WIDTH=1
A=2
B=2

Context: 0==atoi(&<d0>_gen_argv[1][0]) && 0<=SIZEOF((struct $cuda_kernel_instance)*)+-1 && 0<=SIZEOF(struct $cuda_kernel_instance)+-1 && 0<=SIZEOF(struct $cuda_kernel_instance_node)+-1 && 0<=SIZEOF(struct _CUstream)+-1 && 0<=SIZEOF(struct _CUevent)+-1 && 0<=SIZEOF_REAL+-1

Assertion: $assert(FORALL {int k | ((0<=k)&&(k<(N*N)))} ((C1)[k]==(C2)[k]))
-> FORALL {int k | ((0<=k)&&(k<(N*N)))} ((C1)[k]==(C2)[k])
-> forall k : int . (0 == (real[4])<X_s2v2p0[1]*X_s2v3p0[2]+X_s2v2p0[0]*X_s2v3p0[0],X_s2v2p0[1]*X_s2v3p0[3]+X_s2v2p0[0]*X_s2v3p0[1],X_s2v2p0[2]*X_s2v3p0[0]+X_s2v2p0[3]*X_s2v3p0[2],X_s2v2p0[2]*X_s2v3p0[1]+X_s2v2p0[3]*X_s2v3p0[3]>[k]+-1*(real[4])<X_s2v2p0[0]*X_s2v3p0[2]+X_s2v2p0[0]*X_s2v3p0[0]+X_s2v4p0[0],X_s2v2p0[1]*X_s2v3p0[1]+X_s2v2p0[1]*X_s2v3p0[3]+X_s2v4p0[1],X_s2v2p0[2]*X_s2v3p0[2]+X_s2v2p0[2]*X_s2v3p0[0]+X_s2v4p0[2],X_s2v2p0[3]*X_s2v3p0[1]+X_s2v2p0[3]*X_s2v3p0[3]+X_s2v4p0[3]>[k] || !(0 < -1*k+4) || !(0 <= k))

Call stacks:

process p0 (id=0):
  _gen_main at mm.cu:210.4-11 "$assert" called from
  _CIVL_system at GeneralTransformer:0.-1-20 "_gen_argc, &_gen_a..." inserted by GeneralTransformer.new main function before mm.cu:98.14-18 "argc"

process p1 (id=1):
  terminated

Logging new entry 0, writing trace to CIVLREP/mm_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -inputN=2 -inputTILE_WIDTH=1 mm.cu 

=== Stats ===
   time (s)            : 2.75
   memory (bytes)      : 514850816
   max process count   : 10
   states              : 877
   states saved        : 504
   state matches       : 0
   transitions         : 878
   trace steps         : 480
   valid calls         : 3632
   provers             : z3, cvc4, cvc3
   prover calls        : 15

=== Result ===
The program MAY NOT be correct.  See CIVLREP/mm_log.txt
NAME: sum.cu
CITE: \cite{hathhorn-etal:2012:cuda-semantics}
TYPE: $\text{C}$
SCALE: {\texttt{NBLK=4,NTperBLK=2}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (95.1 files/s, 8464.1 lines/s)"
1,CUDA,13,4,72
civl verify -enablePrintf=false  -inputN=8 -inputNBLOCKS=4 sum.cu
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -inputN=8 -inputNBLOCKS=4 sum.cu 

=== Stats ===
   time (s)            : 2.65
   memory (bytes)      : 514850816
   max process count   : 14
   states              : 1297
   states saved        : 689
   state matches       : 18
   transitions         : 1314
   trace steps         : 689
   valid calls         : 15679
   provers             : z3, cvc4, cvc3
   prover calls        : 6

=== Result ===
The standard properties hold for all executions.
NAME: vectorAdd.cu
CITE: \cite{nvidia:2015:cuda-samples}
TYPE: $\text{C}$
SCALE: {\texttt{1$\leq$N$\leq$6, 1$\leq$NTperBLK$\leq$4}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (91.7 files/s, 21926.6 lines/s)"
1,CUDA,40,51,148
civl verify -enablePrintf=false  -inputN=6 -inputTHREADS_B=3 vectorAdd.cu
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -inputN=6 -inputTHREADS_B=3 vectorAdd.cu 

=== Stats ===
   time (s)            : 4.58
   memory (bytes)      : 650117120
   max process count   : 14
   states              : 4796
   states saved        : 2076
   state matches       : 387
   transitions         : 5179
   trace steps         : 2447
   valid calls         : 69055
   provers             : z3, cvc4, cvc3
   prover calls        : 15

=== Result ===
The standard properties hold for all executions.
