Incrementing in OpenCL

Simple OpenCL kernel that increments a single element of a shared array. This verification example shows that VerCors is capable of verifying actual OpenCL kernel code.

General information

ID102
Articlenone
Back-endSilicon
LanguageOpenCL (kernels)
FeaturesArrays, GPU Kernels
Sources
Path to example fileopencl/opencl_incr.c
Date2017-06-20

Statistical information

Lines of code14 lines (comments not included)
Lines of specification3 lines (21.43% of the total)
Computation time14418 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.