Kernel with host code

Verification example of a GPU kernel, written in PVL, together with host code. Moreover, the kernel has a forward dependency in its execution, and a barrier is used there to redistribute permissions.

General Information

Backend: Silicon
Language: PVL
Features: GPU Kernels, Arrays, Barriers, Loop parallelisations
Path to Example File: carp/forward-host.pvl
Should Verify: Yes
Date: 2017-06-15
Lines of Code: 72 (comments not included)
Lines of Specification: 27 (37.5% of total)
Computation Time: 45.9 seconds

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases ForwardHost
//:: tools silicon
//:: verdict Fail

// vct --silver=silicon_qp  forward-host.pvl

class Ref {

context_everywhere N>0 && a != null && b != null && c != null;

requires (\forall* int i ; 0 <= i && i < N ; Perm(a[i],write));
    requires (\forall* int i ; 0 <= i && i < N ; Perm(b[i],1\2));
    requires (\forall* int i ; 0 <= i && i < N ; Perm(c[i],write));

requires (\forall int i; 0 <= i && i < N ; b [ i ] == i);

ensures  (\forall* int i ; 0 <= i && i < N ; Perm(a[i],write));
    ensures  (\forall* int i ; 0 <= i && i < N ; Perm(b[i],1\2));
    ensures  (\forall* int i ; 0 <= i && i < N ; Perm(c[i],write));
    
    ensures  (\forall int i; 0 <= i && i < N ;  a[i] == i+1);
    ensures  (\forall int i; 0 <= i && i < N ;  b[i] == i  );
    ensures  (\forall int i; 0  < i && i < N ;  c[i] == i+2);

void forward(int N,int[N] a,int[N] b, int[N] c){
    par fwd (int i=0..N)
      requires Perm(a[i],write);
      requires Perm(b[i],1\2);
      requires Perm(c[i],write);

requires b[i]==i;

ensures  Perm(a[i],1\2);
      ensures  Perm(b[i],1\2);      
      ensures  Perm(c[i],write);          
      
      ensures  a[i]==i+1;
      ensures  b[i]==i;
      ensures  i>0 ==> c[i]==i+2;
      ensures  i>0 ==> Perm(a[i-1],1\2);
      ensures  i==N-1 ==> Perm(a[i],1\2);
    {
      a[i]=b[i]+1;
      barrier(fwd){
        requires i < N-1 ==> Perm(a[i],1\2);
        requires i < N-1 ==> a[i]==i+1;
        ensures  i > 0   ==> Perm(a[i-1],1\2);
        ensures  i > 0   ==> a[i-1]==i;
      }
      if (i>0) {
        c[i]=a[i-1]+2;
      }
    }
  }

context_everywhere N>10 && a != null && b != null && c != null;
   requires (\forall* int i ; 0 <= i && i < N ; Perm(a[i],write));
   requires (\forall* int i ; 0 <= i && i < N ; Perm(b[i],write));
   requires (\forall* int i ; 0 <= i && i < N ; Perm(c[i],write));
  void host(int N,int[N] a,int[N] b, int[N] c){
    par(int i=0..N)
      requires Perm(b[i],write);
      ensures  Perm(b[i],write) ** b[i]==i;
    {
      b[i]=i;
    }
  
    forward(N,a,b,c);
    
    assert a[5]==6;
    assert c[5]==6; // <- not true.
  }

}

Language: