===========
Limitations
===========

Known Sources of Unsoundness in GPUVerify
-----------------------------------------

* By defualt, GPUVerify does not perform any out-of-bounds checking. Hence, a
  verified kernel might still behave unexpectedly when array bounds are
  violated.

* GPUVerify assumes the input arrays to a kernel are all distinct. Not making
  this assumption leads to many false positives. Non-aliasing can be enforced
  by equipping the input arrays with restrict qualifiers. GPUVerify will issue
  a warning when the restrict qualifier is missing and there is more than one
  input array. For example, for the the following CUDA kernel::

    __global__ void foo(int* a, int* b) {
      a[threadIdx.x] = b[threadIdx.x];
    }

  GPUVerify will report it is assuming the the arguments ``a`` and ``b`` of
  ``foo`` to be non-aliased. This warning can be suppressed by changing the
  kernel to::

    __global__ void foo(int* __restrict__ a, int* __restrict__ b) {
      a[threadIdx.x] = b[threadIdx.x];
    }

* GPUVerify's default pointer representation may cause false negatives to occur
  in kernel verification if the kernel explicitly tries to enumerate all
  possible pointer values (effectively: all potential input arrays plus
  ``NULL``). For example, the following CUDA kernel will successfully verify::

    __device__ int *nondet(void);

    __global__ void foo(int* a, int* b) {
      int* p = nondet();
      int* q = nondet();

      __assume(__ptr_offset_bytes(p) == 0);
      __assume(__ptr_offset_bytes(q) == 0);

      if (p != a && p != b && p != NULL &&
          q != a && q != b && q != NULL && p != q) {
        __assert(false);
      }

    }

* GPUVerify assumes that atomic operations do not overflow or underflow the
  values on which they act.

* If an array ``a`` occurs read-only in a kernel, then the ``__read(a)``
  annotation always evaluates to false. As a consequence, the following OpenCL
  kernel successfully verifies::

    __kernel void foo(__global int* a, __global int* b) {
      b[get_global_id(0)] = a[0];
      __assert(!__read(a));
    }

Using Structures as Kernel Parameters
-------------------------------------

By default the clang compiler as used by GPUVerify replace any structure passed
to a kernel by a char pointer plus a memory copy. For example, the following
kernel::

  struct S {
    int *a;
    int *b;
  };

  __global__ void foo(struct S s) {
  }

will internally represented by::

  __global__ void foo(char *s_in) {
    struct S s;
    memcpy(&s, s_in, sizeof(s));
  }

Consequently, although it is possible to write kernel preconditions like
``__requires(s.a == NULL)``, these will be ignored during the verification.
As a workaround ``__assume(s.a == NULL)`` can be used.