Can't reason about old values for which we have write permission in GPU kernels

[sakehl]

The following program does not verify:

#include <cuda.h>

/*@
  context blockDim.x > 0 && blockDim.y == 1 && blockDim.z == 1;
  context gridDim.x > 0 && gridDim.y == 1 && gridDim.z == 1;

  context in != NULL && out != NULL;
  context \pointer_length(in) == 1;
  context \pointer_length(out) == n;
  context n > 0;
  context blockDim.x * gridDim.x >= n;
  context Perm(&in[0], write \ (blockDim.x * gridDim.x));
  context \gtid<n ==> Perm(&out[\gtid], write);

  ensures \gtid<n ==> out[\gtid] == \old(out[\gtid]);
@*/
__global__ void blur_x(int* in, int* out, int n) {
  int tid = blockIdx.x * blockDim.x + threadIdx.x;

  //@ assert tid<n ==> out[tid] == \old(out[blockIdx.x * blockDim.x + threadIdx.x]);
}

I think this is the case because we have write permission, but we make multiple parallel blocks, which each have a contract. We cannot say \old(A)==A as pre-condition, since the pre-condition is also used for the function the kernel turns into.

A quick fix would be to filter out annotations containing old for the function contract and only place them in the contracts of the parallel blocks.

Alternatively we might want to generate things like \old(A) == A for things we have permission over? This is not logical as user that you have to specify this, and that we immediately forget the old value if we have write permission to it.

[pieter-bos]

On dev this reports:

======================================
At /tmp/vercors-interpreted-4864903524201115850.i
--------------------------------------
   64  
   65  
                            [----------
   66    ensures \gtid<n ==> out[\gtid] == \old(out[\gtid]);
                             ----------]
   67  @*/
   68  __cuda_kernel__ void blur_x(int* in, int* out, int n) {
--------------------------------------
At examples/private/lars.cu
--------------------------------------
   14  
   15  
      [-------------------------------------------------------
   16    ensures \gtid<n ==> out[\gtid] == \old(out[\gtid]);
       -------------------------------------------------------]
   17  @*/
   18  __global__ void blur_x(int* in, int* out, int n) {
--------------------------------------
There may be insufficient permission to dereference the pointer. (https://utwente.nl/vercors#ptrPerm)
======================================

Is that what you get in your situation?

Alternatively we might want to generate things like \old(A) == A for things we have permission over? This is not logical as user that you have to specify this, and that we immediately forget the old value if we have write permission to it.

This already is generated, except if you specify --no-infer-heap-context-into-frame (bearing in mind we should fix #1101).

[sakehl]

oww is that is what going on check.

I just always have --no-infer-heap-context-into-frame on by default.

Dev breaks completely, because of trigger not getting rewriten, for which I just made some fixes, but didn't want to push it yet, and first get all my GPU stuff working again.

But closing this for now than.